Next: Some Final Comments
Up: Class note 28
Previous: Termination
We now wish to look at the type constructor Cartesian Product and attempt to
understand its syntax and typing rules. Recall that in ML, we
deconstruct a pair using fst and snd where fst
and
. We will modify these slightly in order to generalize and have
one typing rule for both combined. Before we do this, we should be aware that
we will need to extend our definition of Type to include:
The rule for typing a pair is:
For notational purposes let 
. We will also
introduce another operator at this point called spread which is
an LT as follows:
We of course need some sort of reduction rule, so we'll call the following
a spread reduction:
We can use this new operator to get fst
and 
in the
following manner:
- fst
-
What remains to be shown is a typing rule for this operator. The following
will give us everything we need to completely characterize the
Cartesian Product:
