Skip to content

Instantly share code, notes, and snippets.

@ion1

ion1/PeirceLEM.hs

Last active July 10, 2022 02:24
Show Gist options
  • Star 3 You must be signed in to star a gist
  • Fork 4 You must be signed in to fork a gist
  • Save ion1/058ee03fd82a7b453933 to your computer and use it in GitHub Desktop.
Save ion1/058ee03fd82a7b453933 to your computer and use it in GitHub Desktop.
Download ZIP
Exercise: prove Peirce’s law <=> law of excluded middle in Haskell
Raw
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 = _
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment