Next: Reading Nuprl Proofs Up: Type Theory Preliminaries Previous: Subtypes and Finiteness

## Algebraic Structures and Dependent Types

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].

karla@cs.cornell.edu
Wed Jul 2 08:55:38 EDT 1997