Next: Reading Nuprl Proofs
Up: Type Theory Preliminaries
Previous: Subtypes and Finiteness
In algebra and automata theory definitions are given using so-called
(algebraic) structures. For example, a monoid is a type
together with a binary operation 
and an element, 
. The operation is associative and 
is an
identity. The monoid is the triple 
. The
``signature'' or type of this structure is 
.
This type is called a dependent product in Nuprl. The basic
underlying form is 
where 
is a
function from types to types, e.g. 
.
We can explain the bound variables 
in two ways. In
Jackson's thesis these arise by iterating the binary dependent product
construction as follows. Let 
be a type with exactly one
element, say 
. Then take 
as a type with 
as a parameter. Call it
. Next build 
. Call this 
, finally build 
. We see that are just the binding
variables used in creating the product.
Another approach is to consider the type of names 
(a
subtype of Atom in Nuprl) and define a function 
where 
and 
. Then the monoid signature is
This is the approach taken by Jason
Hickey [15].