| 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 |