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

Revisions

  1. Rufflewind revised this gist Apr 7, 2015. 1 changed file with 18 additions and 4 deletions.
    22 changes: 18 additions & 4 deletions PeirceLEM.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,6 +1,7 @@
    -- Exercise: prove Peirce’s law <=> law of excluded middle in Haskell

    {-# LANGUAGE Rank2Types #-}
    module PeirceLEM where

    import Data.Void

    @@ -10,17 +11,30 @@ 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_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 lem = _
    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_dne callCC = callCC $ \ nlem -> absurd . ($ nlem . const)

    dne_callCC :: DNE -> Peirce
    dne_callCC dne = _
    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
  2. @ion1 ion1 revised this gist Apr 7, 2015. 1 changed file with 10 additions and 0 deletions.
    10 changes: 10 additions & 0 deletions PeirceLEM.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -14,3 +14,13 @@ 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 = _
  3. @ion1 ion1 revised this gist Apr 7, 2015. 2 changed files with 16 additions and 16 deletions.
    16 changes: 16 additions & 0 deletions PeirceLEM.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,16 @@
    -- 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 = _
    16 changes: 0 additions & 16 deletions PierceLEM.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -1,16 +0,0 @@
    -- Exercise: prove Pierce’s law <=> law of excluded middle in Haskell

    {-# LANGUAGE Rank2Types #-}

    import Data.Void

    type Not a = a -> Void

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

    callCC_lem :: Pierce -> LEM
    callCC_lem callCC = _

    lem_callCC :: LEM -> Pierce
    lem_callCC lem = _
  4. @ion1 ion1 created this gist Apr 7, 2015.
    16 changes: 16 additions & 0 deletions PierceLEM.hs
    View file
    Original file line number Diff line number Diff line change
    @@ -0,0 +1,16 @@
    -- Exercise: prove Pierce’s law <=> law of excluded middle in Haskell

    {-# LANGUAGE Rank2Types #-}

    import Data.Void

    type Not a = a -> Void

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

    callCC_lem :: Pierce -> LEM
    callCC_lem callCC = _

    lem_callCC :: LEM -> Pierce
    lem_callCC lem = _