Next: Function Types
Up: Type Theory Preliminaries
Previous: Basic Types
If 
and 
are types, then so is their Cartesian product,
, whose elements are ordered pairs, 
with 
and 
. For example 
consists of the points with integer co-ordinates in the plane. If 
then there are several common ways to denote the first
and second components of the pair. Here are some of the common ways: first
, 1of or 
for the first,
and second, 2of or 
for the second. We have
An n-ary product, say 
is regarded as 
. In general 
is
. Given 
, the 2nd component is 
and the 3rd is 
.
We'll see these selectors in the definition of an automaton (section
4.1).