Next Types Are Theorems; Programs Are Proofs 16

How to construct a function with any type

1Assume ab Assume we have x :: a -> b
2Assume bc Assume we have y :: b -> c
3Assume a Assume we have z :: a
4From (3) and (1), conclude b
(→E)

x z :: b
5From (4) and (2), conclude c
(→E)

y (x z) :: c
6From (3) and (5), conclude ac
(→I) (disch. 3)

\z -> y (x z) :: a -> c
7From (2) and (6), conclude (bc) → (ac)
(→I) (disch. 2)

\y -> (\z -> y (x z)) :: (b -> c) -> (a -> c)
8From (1) and (7), conclude (ab) → (bc) → (ac)
(→I) (disch. 1)

\x -> \y -> (\z -> y (x z)) :: (a -> b) -> (b -> c) -> (a -> c)


Next Next