DeMorganCPS.hs

{-# LANGUAGE RankNTypes    #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UnicodeSyntax #-}

module DeMorganCPS where

-- Products and sums with prettier type notation
data a ∧ b = Pair a b
data a ∨ b = InL a | InR b

-- Equivalent to the De Morgan rule: A ∧ B -> ¬(¬A ∨ ¬B)
productToCPS :: a ∧ b -> (∀ t. (a -> t) ∨ (b -> t) -> t)
productToCPS (Pair a b) x =
   case x of
      InL f -> f a
      InR f -> f b

-- Equivalent to the De Morgan rule: ¬(¬A ∨ ¬B) -> A ∧ B
productFromCPS :: (∀ t. (a -> t) ∨ (b -> t) -> t) -> a ∧ b
productFromCPS f =
   Pair (f (InL id))
        (f (InR id))

-- Equivalent to the De Morgan rule: A ∨ B -> ¬(¬A ∧ ¬B)
sumToCPS :: a ∨ b -> (∀ t. (a -> t) ∧ (b -> t) -> t)
sumToCPS x (Pair l r) =
   case x of
      InL a -> l a
      InR b -> r b

-- Equivalent to the De Morgan rule: ¬(¬A ∧ ¬B) -> A ∨ B
sumFromCPS :: (∀ t. (a -> t) ∧ (b -> t) -> t) -> a ∨ b
sumFromCPS f =
   f (Pair InL InR)