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

{-# LANGUAGE Rank2Types #-}
module PeirceLEM where

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 = callCC $ \ nlem -> Left $ nlem . Right
-- suppose LEM false and A true; since A true, LEM true; but this is contradiction;
-- hence we know if LEM false, then A false.
-- since A false => LEM true, we know further that LEM false => LEM true
-- apply Peirce: (X false => X true) implies X true
-- thus we get LEM true

lem_callCC :: LEM -> Peirce
lem_callCC (Left nx) = ($ absurd . nx)
lem_callCC (Right x) = const x

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

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

callCC_dne :: Peirce -> DNE
callCC_dne callCC = callCC $ \ nlem -> absurd . ($ nlem . const)

dne_callCC :: DNE -> Peirce
dne_callCC dne f = dne $ \ nlem -> nlem . f $ absurd . nlem

lem_dne :: LEM -> DNE
lem_dne (Left nx) = absurd . ($ nx)
lem_dne (Right x) = const x

dne_lem :: DNE -> LEM
dne_lem dne = dne $ \ nlem -> nlem . Left $ nlem . Right