Skip to content

Instantly share code, notes, and snippets.

@Rufflewind

Rufflewind/PeirceLEM.hs

Forked from ion1/PeirceLEM.hs
Created April 7, 2015 09:00
Show Gist options

  • Select an option

    Learn more about clone URLs
  • Save Rufflewind/2bf0202e016ee9b74b6d to your computer and use it in GitHub Desktop.

Select an option

Learn more about clone URLs
Save Rufflewind/2bf0202e016ee9b74b6d to your computer and use it in GitHub Desktop.
Download ZIP
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 = _
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment