The simply typed lambda calculus (
Contents
- Syntax
- Typing rules
- Intrinsic vs extrinsic interpretations
- Equational theory
- Operational semantics
- Categorical semantics
- Proof theoretic semantics
- Alternative syntaxes
- General observations
- Important results
- References
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 are still considered simple because the Church encodings of such structures can be done using only
Syntax
In this article, we use
To define the types, we begin by fixing a set of base types,
For example,
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:
The syntax of the simply typed lambda calculus is essentially that of the lambda calculus itself. We write
where
That is, variable reference, abstractions, application, and constant. A variable reference
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
The typing relation
In words,
- If
x has typeσ in the context, we know thatx has typeσ . - Term constants have the appropriate base types.
- If, in a certain context with
x having typeσ ,e has typeτ , then, in the same context withoutx ,λ x : σ . e has typeσ → τ . - If, in a certain context,
e 1 σ → τ , ande 2 σ , thene 1 e 2 τ .
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
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
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
holds whenever
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
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
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
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
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
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:
- If
x : σ is in the context, we can synthesize typeσ forx . - The types of term constants are fixed and can be synthesized.
- To check that
λ x . e has typeσ → τ in some context, we extend the context withx : σ and check thate has typeτ . - If
e 1 σ → τ (in some context), ande 2 σ (in the same context), thene 1 e 2 τ .
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:
- To check that
e has typeτ , it suffices to synthesize typeτ . - If
e checks against typeτ , then the explicitly annotated term( e : τ ) synthesizesτ .
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
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.