The simple theory of types is arrived at from the lambda calculus by adding a type system, and then some logical constants, and then beefing up the inference rules to reflect the intended meaning of the constants.
First the type system. The type system is based on the premise that there are two collections of elements, the first of which may be thought of as individuals in some domain of discourse (which we will call ind) and the second of which may be thought of either as truth values or as propositions (which we will call bool, anticipating a two valued logic). These two collections are the primitive types.
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 co-domain u, i.e. those functions which are defined for all elements of t and yield 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) |