The simply typed lambda calculus (), a form

of type theory, is a typed interpretation of the lambda calculus with only one type constructor () 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 use of the untyped lambda calculus. his lambda calculus, as a formal language based on symbolic expressions, consisted of a denumerably infinite series of axioms and variables, but also a finite set of primitive symbols, and also, a finite set of rules I to VI. This finite set of rules included rule V modus ponens as well as IV and VI for substitution and generalization respectively.

{| align="center" cellpadding="9"

| align="center" | <math>{\frac{x\mathbin{:}\sigma \in \Gamma}{\Gamma \vdash x\mathbin{:}\sigma} }</math> (1)

| align="center" | <math>{\frac{c \text{ is a constant of type } T}{\Gamma\vdash c\mathbin{:}T</math> (2)

|-

| align="center" | <math>{\frac{\Gamma,x\mathbin{:}\sigma\vdash e\mathbin{:}\tau}{\Gamma\vdash (\lambda x\mathbin{:}\sigma.~e)\mathbin{:}(\sigma \to \tau)</math> (3)

| align="center" | <math>{\frac{\Gamma\vdash e_1\mathbin{:}\sigma\to\tau\quad\Gamma\vdash e_2\mathbin{:}\sigma}{\Gamma\vdash e_1~e_2\mathbin{:}\tau</math> (4)

|}

In words,

  1. If <math>x</math> has type <math>\sigma</math> in the context, then <math>x</math> has type .
  2. Term constants have the appropriate base types.
  3. If, in a certain context with <math>x</math> having type , <math>e</math> has type , then, in the same context without , has type .
  4. If, in a certain context, <math>e_1</math> has type , and <math>e_2</math> has type , then <math>e_1~e_2</math> has type .

Examples of closed terms, i.e. terms typable in the empty context, are:

  • For every type , a term <math>\lambda x\mathbin{:}\tau.x\mathbin{:}\tau\to\tau</math> (identity function/I-combinator),
  • For types , a term <math>\lambda x\mathbin{:}\sigma.\lambda y\mathbin{:}\tau.x\mathbin{:}\sigma \to \tau \to \sigma</math> (the K-combinator), and
  • For types , a term <math>\lambda x\mathbin{:}\tau\to\tau'\to\tau.\lambda y\mathbin{:}\tau\to\tau'.\lambda z\mathbin{:}\tau.x z (y z) : (\tau\to\tau'\to\tau)\to(\tau\to\tau')\to\tau\to\tau</math> (the S-combinator).

These are the typed lambda calculus representations of the basic combinators of combinatory logic.

Each type <math>\tau</math> is assigned an order, a number . For base types, ; for function types, . That is, the order of a type measures the depth of the most left-nested arrow. Hence:

: <math>o(\iota \to \iota \to \iota) = 1</math>

: <math>o((\iota \to \iota) \to \iota) = 2</math>

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, variously called intrinsic vs. extrinsic, ontological vs. semantical, or Church-style vs. Curry-style.

An intrinsic 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 <math>\lambda x\mathbin{:}\mathtt{int}.~x</math> on integers and the identity term <math>\lambda x\mathbin{:}\mathtt{bool}.~x</math> 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 semantics assigns meaning to terms regardless of typing, as they would be interpreted in an untyped language. In this view, <math>\lambda x\mathbin{:}\mathtt{int}.~x</math> and <math>\lambda x\mathbin{:}\mathtt{bool}.~x</math> mean the same thing (i.e., the same thing as ).

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 an extrinsic semantics on annotated terms simply by ignoring the types (i.e., through type erasure), as it is possible to give an intrinsic 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 an intrinsic or extrinsic perspective.

Equational theory

The simply typed lambda calculus (STLC) has the same equational theory of βη-equivalence as untyped lambda calculus, but subject to type restrictions. The equation for beta reduction

: <math>(\lambda x\mathbin{:}\sigma.~t)\,u =_{\beta} t[x:=u]</math>

holds in context <math>\Gamma</math> whenever <math>\Gamma,x\mathbin{:}\sigma \vdash t\mathbin{:}\tau</math> and , while the equation for eta reduction

: <math>\lambda x\mathbin{:}\sigma.~t\,x =_\eta t</math>

holds whenever <math>\Gamma\vdash t{:}\sigma \to \tau</math> and <math>x</math> does not appear free in .

The advantage of typed lambda calculus is that STLC allows potentially nonterminating computations to be cut short (that is, reduced).

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., 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 <math>\Gamma \vdash e \Leftarrow \tau</math> and <math>\Gamma \vdash e \Rightarrow \tau</math> respectively. Operationally, the three components , , and <math>\tau</math> are all inputs to the checking judgment , whereas the synthesis judgment <math>\Gamma \vdash e \Rightarrow \tau</math> only takes <math>\Gamma</math> and <math>e</math> as inputs, producing the type <math>\tau</math> as output. These judgments are derived via the following rules:

{| align="center" cellpadding="9"

| align="center" | <math>{\frac{x\mathbin{:}\sigma \in \Gamma}{\Gamma \vdash x \Rightarrow \sigma} }</math> [1]

| align="center" | <math>{\frac{c \text{ is a constant of type } T}{\Gamma\vdash c \Rightarrow T</math> [2]

|-

| align="center" | <math>{\frac{\Gamma,x\mathbin{:}\sigma\vdash e\Leftarrow \tau}{\Gamma\vdash \lambda x.~e \Leftarrow \sigma \to \tau</math> [3]

| align="center" | <math>{\frac{\Gamma\vdash e_1\Rightarrow \sigma\to\tau\quad\Gamma\vdash e_2\Leftarrow\sigma}{\Gamma\vdash e_1~e_2 \Rightarrow \tau</math> [4]

|-

| align="center" | <math>{\frac{\Gamma\vdash e \Rightarrow \tau}{\Gamma\vdash e\Leftarrow \tau</math> [5]

| align="center" | <math>{\frac{\Gamma\vdash e \Leftarrow \tau}{\Gamma\vdash (e\mathbin{:}\tau)\Rightarrow \tau</math> [6]

|}

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:

  1. If <math>x\mathbin{:}\sigma</math> is in the context, we can synthesize type <math>\sigma</math> for .
  2. The types of term constants are fixed and can be synthesized.
  3. To check that <math>\lambda x.~e</math> has type <math>\sigma \to \tau</math> in some context, we extend the context with <math>x\mathbin{:}\sigma</math> and check that <math>e</math> has type .
  4. If <math>e_1</math> synthesizes type <math>\sigma \to \tau</math> (in some context), and <math>e_2</math> checks against type <math>\sigma</math> (in the same context), then <math>e_1~e_2</math> synthesizes type .

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:

<ol start="5">

<li>To check that <math>e</math> has type , it suffices to synthesize type .</li>

<li>If <math>e</math> checks against type , then the explicitly annotated term <math>(e\mathbin{:}\tau)</math> synthesizes .

</li>

</ol>

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: every sequence of reductions eventually terminates. and more precisely, it is complete in the complexity class called TOWER. A purely semantic normalisation proof (see normalisation by evaluation) was given by Berger and Schwichtenberg in 1991.

  • We can encode natural numbers by terms of the type <math>(o\to o)\to(o \to o)</math> (Church numerals). Schwichtenberg showed in 1975 that in <math>\lambda^\to</math> exactly the extended polynomials are representable as functions over Church numerals;

</references>