Simply Typed Lambda Calculus - Syntax

Syntax

In this article, we use and to range over types. Informally, the function type refers to the set of functions that, given an input of type, produce an output of type . By convention, associates to the right: we read as .

To define the types, we begin by fixing a set of base types, . These are sometimes called atomic types or type constants. With this fixed, the syntax of types is:

.

For example, if, then, and are all valid types (among others).

We also fix a set of term constants for the base types. For example, we might assume a base type nat, and the term constants could be the natural numbers. In the original presentation, Church used only two base types: for "the type of propositions" and for "the type of individuals". The type has no term constants, whereas has one term constant. Frequently the calculus with only one base type, usually, is considered.

The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. We write to denote that the variable is of type . The term syntax is then:

where is a term constant.

That is, variable reference, abstractions, application, and constant. A variable reference is bound if it is inside of an abstraction binding . A term is closed if there are no unbound variables.

Compare this to the syntax of untyped lambda calculus:

We see that in typed lambda calculus every function (abstraction) must specify the type of its argument.