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 .