PeirceLEM.hs

-- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell

{-# LANGUAGE Rank2Types #-}

import Data.Void

type Not a = a -> Void

type Peirce = forall a b. ((a -> b) -> a) -> a
type LEM = forall a. Either (Not a) a

callCC_lem :: Peirce -> LEM
callCC_lem callCC = _

lem_callCC :: LEM -> Peirce
lem_callCC lem = _

-- Bonus exercise: prove Peirce’s law <=> double negation elimination

type DNE = forall a. Not (Not a) -> a

callCC_dne :: Peirce -> DNE
callCC_dne callCC = _

dne_callCC :: DNE -> Peirce
dne_callCC dne = _