Next | Types Are Theorems; Programs Are Proofs | 14 |

The proof rules match the rules for constructing functions!

Suppose you have a proof of some proposition

The last step is either →I or →E

Say it's →E.

Then we are concluding

*b*from both*a*→*b*and*a*So we have proofs of

*a*→*b*and*a*So we have programs of types

`a -> b`and`a`(Say

`f :: a -> b`and`x :: a`)Then

`f x :: b`

Next | Next |