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.

• $P \wedge Q \implies Q \wedge P$

• $(P \implies Q \wedge Q \implies R) \implies (P \implies R)$

• $((P \wedge Q) \wedge R) \implies (P \wedge (Q \wedge R))$

• $(P \wedge (Q \vee R)) \implies (P \vee Q) \wedge (P \vee R)$

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)