Skip to content

Instantly share code, notes, and snippets.

@Rufflewind
Forked from ion1/PeirceLEM.hs
Created April 7, 2015 09:00
Show Gist options
  • Save Rufflewind/2bf0202e016ee9b74b6d to your computer and use it in GitHub Desktop.
Save Rufflewind/2bf0202e016ee9b74b6d to your computer and use it in GitHub Desktop.
-- 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
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment