Next Types Are Theorems; Programs Are Proofs 27

Example

((a ∨ (ab)) → b) → b

1Assume (a ∨ (ab)) → b) Assume we have f :: (Either a (a -> b)) -> b
2Assume a Assume we have x :: a
3From (2), conclude a ∨ (ab)
(∨I)

Left x :: Either a (a -> b)
4From (3) and (1), conclude b
(→E)

f (Left x) :: b
5From (2) and (4), conclude ab (→I)(disch. 2) \x -> f (Left x) :: a -> b
6From (5) conclude a ∨ (ab) (∨I) Right (\x -> f (Left x)) :: Either a (a -> b)
7From (6) and (1), conclude b
(→E)

f (Right (\x -> f (Left x))) :: b
5From (1) and (7), conclude (a ∨ (ab)) → b) → b
(→I) (disch. 1)

\f -> f (Right (\x -> f (Left x))) :: ((Either a (a -> b)) -> b) -> b


Next Next