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

→ corresponds to

`->`The rules for proving things with → are the same as for computing with function types

If that was all there was to it, it would be a mildly interesting trivium

But *everything* in logic corresponds to something in the type system

What about more interesting types and propositions?

For example ∧ means “and”:

((a→b) ∧a) →b

(a∧b) → (b∧a)

(a∧b) → (b→ (a→c)) →c

In the programming type world, ∧ is a

**pair type**

Next | Next |