Now we will try to repeat the above process type-theoretically. That is, we would like to use standard type constructors (such as disjoint union and Cartesian product) to build the smallest type closed under these constructions.
Example. Let
Intuitively, we can express the closure condition for
as:
This means that for
any two elements of
, say
and
and any
,
:
Here we can think of each cross-product as allowing either an and or an
or formula - which one is determined by the standard type - theoretic
identifiers inl and inr.
Note that we have preserved the property of determinism by associating a unique
sequence of inls and inrs with each element of
Now we make the above precise: for any algebraic type expression,
(ie. those involving only the primitive constructors
and
) we can define
through
three axioms:
Exercise. On Problem Set 1 we gave an induction principle for the set of propositional formulae. Rewrite the principle using this new notation. (Hint: see Constable and Howe, ``Implementing Mathematics as an Approach to Automatic Theorem Proving''.)
Nuprl uses the same ``rec'' notation to build recursive types as defined above.
For example if F[X] is as above and we defined
then ``P AND Q'' might be represented by inr(inr((inl(P),inl(Q))))
while ``P OR Q'' would be (inr(inr(inr(inl(P),inl(Q))))).
ML, uses a more legible notation to differentiate type elements.
There, a recursive type rec(T. F[T]) is denoted absrectype T = F[T].
Moreover, we specify our own label for each operand in
a disjoint union. For example, to define we could write
Then ``P AND Q'' would be denoted by AND(VAR(P),VAR(Q)). While
this is more legible, we are
no longer refering to type inhabitants through the original mathematical
notation. We have found that typographical transparency mathematical
transparency!