Simply typed lambda calculus

The simply typed lambda calculus (formula_1), a form
of type theory, is a typed interpretation of the lambda calculus with only one type constructor (formula_2) that builds function types. It is the canonical and simplest example of a typed lambda calculus. The simply typed lambda calculus was originally introduced by Alonzo Church in 1940 as an attempt to avoid paradoxical uses of the untyped lambda calculus, and it exhibits many desirable and interesting properties.
The term "simple type" is also used to refer to extensions of the simply typed lambda calculus such as products, coproducts or natural numbers (System T) or even full recursion (like PCF). In contrast, systems which introduce polymorphic types (like System F) or dependent types (like the Logical Framework) are not considered "simply typed". The former, except full recursion, are still considered "simple" because the Church encodings of such structures can be done using only formula_2 and suitable type variables, while polymorphism and dependency cannot.
Syntax.
In this article, we use formula_4 and formula_5 to range over types. Informally, the "function type" formula_6 refers to the type of functions that, given an input of type formula_4, produce an output of type formula_5.
By convention, formula_2 associates to the right: we read formula_10 as formula_11.
To define the types, we begin by fixing a set of "base types", formula_12. These are sometimes called "atomic types" or "type constants". With this fixed, the syntax of types is:
For example, formula_14, generates an infinite set of types starting with formula_15formula_16formula_17formula_18formula_19formula_20
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: formula_21 for "the type of propositions" and formula_22 for "the type of individuals". The type formula_21 has no term constants, whereas formula_22 has one term constant. Frequently the calculus with only one base type, usually formula_21, is considered.
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. We write formula_26 to denote that the variable formula_27 is of type formula_5. The term syntax, in BNF, is then:
where formula_30 is a term constant.
That is, "variable reference", "abstractions", "application", and "constant". A variable reference formula_27 is "bound" if it is inside of an abstraction binding formula_27. 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.
Typing rules.
To define the set of well-typed lambda terms of a given type, we will define a typing relation between terms and types. First, we introduce "typing contexts" or "typing environments" formula_34, which are sets of typing assumptions. A "typing assumption" has the form formula_35, meaning formula_27 has type formula_4.
The "typing relation" formula_38 indicates that formula_39 is a term of type formula_4 in context formula_41. In this case formula_39 is said to be "well-typed" (having type formula_4). Instances of the typing relation are called "typing judgements". The validity of a typing judgement is shown by providing a "typing derivation", constructed using typing rules (wherein the premises above the line allow us to derive the conclusion below the line). Simply-typed lambda calculus uses these rules:
In words,
Examples of closed terms, "i.e." terms typable in the empty context, are:
These are the typed lambda calculus representations of the basic combinators of combinatory logic.
Each type formula_5 is assigned an order, a number formula_68. For base types, formula_69; for function types, formula_70. That is, the order of a type measures the depth of the most left-nested arrow. Hence:
Semantics.
Intrinsic vs. extrinsic interpretations.
Broadly speaking, there are two different ways of assigning meaning to the simply typed lambda calculus, as to typed languages more generally, sometimes called "intrinsic" vs. "extrinsic", or "Church-style" vs. "Curry-style".
An intrinsic/Church-style semantics only assigns meaning to well-typed terms, or more precisely, assigns meaning directly to typing derivations. This has the effect that terms differing only by type annotations can nonetheless be assigned different meanings. For example, the identity term formula_73 on integers and the identity term formula_74 on booleans may mean different things. (The classic intended interpretations
are the identity function on integers and the identity function on boolean values.)
In contrast, an extrinsic/Curry-style semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view, formula_73 and formula_74 mean the same thing ("i.e.", the same thing as formula_77).
The distinction between intrinsic and extrinsic semantics is sometimes associated with the presence or absence of annotations on lambda abstractions, but strictly speaking this usage is imprecise. It is possible to define a Curry-style semantics on annotated terms simply by ignoring the types ("i.e.", through type erasure), as it is possible to give a Church-style semantics on unannotated terms when the types can be deduced from context ("i.e.", through type inference). The essential difference between intrinsic and extrinsic approaches is just whether the typing rules are viewed as defining the language, or as a formalism for verifying properties of a more primitive underlying language. Most of the different semantic interpretations discussed below can be seen through either a Church or Curry perspective.
Equational theory.
The simply typed lambda calculus has the same equational theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions. The equation for beta reduction
holds in context formula_41 whenever formula_80 and formula_81, while the equation for eta reduction
holds whenever formula_83 and formula_27 does not appear free in formula_85.
Operational semantics.
Likewise, the operational semantics of simply typed lambda calculus can be fixed as for the untyped lambda calculus, using call by name, call by value, or other evaluation strategies. As for any typed language, type safety is a fundamental property of all of these evaluation strategies. Additionally, the strong normalization property described below implies that any evaluation strategy will terminate on all simply typed terms.
Categorical semantics.
The simply typed lambda calculus (with formula_86-equivalence) is the internal language of Cartesian closed categories (CCCs), as was first observed by Lambek. Given any specific CCC, the basic types of the corresponding lambda calculus are just the objects, and the terms are the morphisms. Conversely, every simply typed lambda calculus gives a CCC whose objects are the types, and morphisms are equivalence classes of terms.
To make the correspondence clear, a type constructor for the Cartesian product is typically added to the above. To preserve the categoricity of the Cartesian product, one adds type rules for "pairing", "projection", and a "unit term". Given two terms formula_87 and formula_88, the term formula_89 has type formula_90. Likewise, if one has a term formula_91, then there are terms formula_92 and formula_93 where the formula_94 correspond to the projections of the Cartesian product. The "unit term", of type 1, is written as formula_95 and vocalized as 'nil', is the final object. The equational theory is extended likewise, so that one has
This last is read as "if t has type 1, then it reduces to nil".
The above can then be turned into a category by taking the types as the objects. The morphisms formula_100 are equivalence classes of pairs formula_101 where "x" is a variable (of type formula_4) and "t" is a term (of type formula_5), having no free variables in it, except for (optionally) "x". Closure is obtained from currying and application, as usual.
More precisely, there exist functors between the category of Cartesian closed categories, and the category of simply-typed lambda theories.
It is common to extend this case to closed symmetric monoidal categories by using a linear type system. The reason for this is that the CCC is a special case of the closed symmetric monoidal category, which is typically taken to be the category of sets. This is fine for laying the foundations of set theory, but the more general topos seems to provide a superior foundation.
Proof-theoretic semantics.
The simply typed lambda calculus is closely related to the implicational fragment of propositional intuitionistic logic, i.e., minimal logic, via the Curry–Howard isomorphism: terms correspond precisely to proofs in natural deduction, and inhabited types are exactly the tautologies of minimal logic.
Alternative syntaxes.
The presentation given above is not the only way of defining the syntax of the simply typed lambda calculus. One alternative is to remove type annotations entirely (so that the syntax is identical to the untyped lambda calculus), while ensuring that terms are well-typed via Hindley–Milner type inference. The inference algorithm is terminating, sound, and complete: whenever a term is typable, the algorithm computes its type. More precisely, it computes the term's principal type, since often an unannotated term (such as formula_77) may have more than one type (formula_105, formula_106, etc., which are all instances of the principal type formula_107).
Another alternative presentation of simply typed lambda calculus is based on bidirectional type checking, which requires more type annotations than Hindley–Milner inference but is easier to describe. The type system is divided into two judgments, representing both "checking" and "synthesis", written formula_108 and formula_109 respectively. Operationally, the three components formula_41, formula_39, and formula_5 are all "inputs" to the checking judgment formula_108, whereas the synthesis judgment formula_109 only takes formula_41 and formula_39 as inputs, producing the type formula_5 as output. These judgments are derived via the following rules:
Observe that rules [1]–[4] are nearly identical to rules (1)–(4) above, except for the careful choice of checking or synthesis judgments. These choices can be explained like so:
Observe that the rules for synthesis are read top-to-bottom, whereas the rules for checking are read bottom-to-top. Note in particular that we do not need any annotation on the lambda abstraction in rule [3], because the type of the bound variable can be deduced from the type at which we check the function. Finally, we explain rules [5] and [6] as follows:
Because of these last two rules coercing between synthesis and checking, it is easy to see that any well-typed but unannotated term can be checked in the bidirectional system, so long as we insert "enough" type annotations. And in fact, annotations are needed only at β-redexes.
General observations.
Given the standard semantics, the simply typed lambda calculus is strongly normalizing: that is, well-typed terms always reduce to a value, i.e., a formula_132 abstraction. This is because recursion is not allowed by the typing rules: it is impossible to find types for fixed-point combinators and the looping term formula_133. Recursion can be added to the language by either having a special operator formula_134of type formula_135 or adding general recursive types, though both eliminate strong normalization.
Since it is strongly normalising, it is decidable whether or not a simply typed lambda calculus program halts: in fact, it "always" halts. We can therefore conclude that the language is "not" Turing complete.