We have a collection of
atomic
/elementary types: ,
,
,
,
,
. The last of these represents the empty type
and is not present in ML, although it will be important in encoding
logic as types.
We also have the following type constructors:
Remarks: Up to this point, we have considered primitive recursive type theory. Why? Because we can believe it. That is, contradiction is impossible.
Trying to axiomatize the integers (as opposed to the naturals) is tricky. It is easy to get systems with circular models. Try this as an exercise.
The Boyer-Moore theorem prover (Nqthm) is based on this collection of types; it is described in their book, ``A Computational Logic''.
This is also called concrete mathematics because the elements of the types can be written down explicitly; the notation is a ``picture'' of the data.