Skip to content

Instantly share code, notes, and snippets.

@plaidfinch
Last active August 29, 2015 14:08
Show Gist options
  • Save plaidfinch/0062a67b01f53ca7bdbf to your computer and use it in GitHub Desktop.
Save plaidfinch/0062a67b01f53ca7bdbf to your computer and use it in GitHub Desktop.
{-# 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)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment