Propositions as Types

See Philip Wadler’s clas­sic talk on the sub­ject. If you want more details, see the paper that goes along with it.

In class, we saw some facts about the propo­si­tional cal­cu­lus.

And we proved them in Haskell by com­ing up with a term (proof) of the appro­pri­ate type (propo­si­tion).

conj­Comm :: (b, a) -> (a, b)
conj­Comm (p, q) = (q, p)

impl­Trans :: ((a -> b), (b -> c)) -> (a -> c)
impl­Trans (f, g) x = g (f x)

conj­Assoc :: ((a, b), c) -> (a, (b, c))
conj­Assoc p = (fst (fst p), (snd (fst p), snd p))

distr :: (a, Either b c) -> Either (a, b) (a, c)
distr (a, Left b) = Left (a, b)
distr (a, Right c) = Right (a, c)