CurryHoward.hs

{-# LANGUAGE ScopedTypeVariables, EmptyCase #-}
{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

module CurryHoward where

type Unit = ()
data Void

type And a b = (a, b)
data Or a b = OrL a | OrR b
type Imp a b = a -> b
type BiImp a b = And (Imp a b) (Imp b a)
type Not a = a -> Void

efq :: Void -> a
efq v = case v of {}

deMorgan0 :: forall a b. And a b -> Not (Or (Not a) (Not b))
deMorgan0 (a, b) = absurd where
  absurd :: Not (Or (Not a) (Not b))
  absurd (OrL notA) = notA a
  absurd (OrR notB) = notB b


deMorgan2 :: forall a b. Or a b -> Not (And (Not a) (Not b))
deMorgan2 orAB = absurd where
  absurd :: Not (And (Not a) (Not b))
  absurd (notA, notB) = case orAB of
    OrL a -> notA a
    OrR b -> notB b