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

Types like

`Int`,`Bool`, etc. are known to be inhabitedThey play the role of

**axioms**in logicFor 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 |