| Next | Types Are Theorems; Programs Are Proofs | 30 |
Types like Int, Bool, etc. are known to be inhabited
They play the role of axioms in logic
For example, is a -> (a, Int) inhabited?
Of course:
\a -> (a, 3) :: a -> (a, Int)
Similarly, if I is some axiom, then a → a ∧ I is a theorem
| Next | Next |