The full collection of types is obtained by constructing function spaces. From any two types, t and u, not necessarily distinct, a space of functions may be constructed, which we write as t u and which contains all the functions with domain t and codomain u, i.e. those functions which are defined for all elements of t and yeild values which are elements of u. The types are therefore the closure of the set {ind, bool} under the function space constructor "".
A grammar for the language of types is as follows:
Type | ::= | bool | | | ind | | | (Type Type) |
The terms of the simple theory of types are the terms of the type-free lambda calculus, decorated with types and subject to formation constraints defined using these annotations. A term is either a constant name decorated with a type, or a variable name decorated with a type, or the application of one term to another (shown by juxtaposition with the function on the left), or a lambda abstraction in which the bound variable name is decorated with a type.
A grammar for the terms is as follows:
Term | ::= | Cname:Type | | | Vname:Type | | | Term Term | | | ( Vname:Type. Term) |