This post is part of a series on how to reason about code. It describes the Simply Typed Lambda Calculus, a precursor to the formal language understood by Coq, an interactive proof assistant I am learning. More background can be found here, and the post that describes the λ Calculus itself can be found here.

This exposition follows closely that in "Type Theory & Formal Proof" by Nederpelt & Geuvers (abbreviated TTFP throughout).

In the last post, we saw that the λ Calculus is way to make precise the notion of computatation (see here for a capsule history as to why we would want to do this). As such, it should not be surprising that it is a very expressive formalism. It is Turing-complete, and in particular it allows us to write programs that never terminate. We saw the self-application function in the last post, but here's another example, once again from TTFP: let Δ be the term \(\lambda x.xxx\). Then \(\Delta \Delta\twoheadrightarrow_{\beta}\Delta\Delta\Delta\twoheadrightarrow_{\beta}\Delta\Delta\Delta\Delta\twoheadrightarrow_{\beta}\ldots\).

In order to rule out such pathological terms, Church in his 1940 paper "A Formulation of the Simple Theory of Types" added a type system to the λ Calculus. We call the language that results from only permitting "well-typed" λ-terms the Simply Typed Lambda Calculus, or \(\lambda\rightarrow\).

Recall the Untyped λ Calculus: we started with a set of variables \(\mathscr{V}=\{a,b,c,\ldots\}\). \(\mathscr{V}\) is infinite, but start with the lower-case Latin alphabet. We then built terms inductively through:

1. naming :: if \(x\in \mathscr{V}\), then \(x\) is a term (in the λ Calculus)
2. abstraction :: if \(T\) is a term & \(x\in \mathscr{V}\), then \(\lambda x.T\) is a term, where \(x\) may (or may not) occur in \(T\)
3. application :: if \(T_1\) and \(T_2\) are terms, then \(T_1 \enspace T_2\) is a term

giving us an infinite set of λ-terms like \(x\), \(\lambda x.y\), \(\lambda x.y \enspace a\), \(\lambda z.(\lambda x.y \enspace z)\) and so on.

Call the elements of \(\mathscr{V}\) ordinary variables. We now give ourselves a second infinite set of type variables \(\mathbb{V}=\{\alpha,\beta,\gamma,\ldots\}\) & define the set of all simple types \(\mathbb{T}\) inductively:

1. if \(\alpha\in \mathbb{V}\), then \(\alpha\in \mathbb{T}\)
2. if \(\sigma,\tau\in \mathbb{T}\), then \((\sigma\rightarrow\tau)\in \mathbb{T}\)

So \(\mathbb{T}\) contains terms like α, β, \(\alpha\rightarrow\beta\), \((\alpha\rightarrow\beta)\rightarrow\gamma\) and so on. Intuitively, type variables represent what we'd typically think of as a type (the natural numbers \(\mathbb{N}\), or bool, for instance), and the arrow suggests mapping; a term with type \(\sigma\rightarrow\tau\) maps things of type σ to things of type τ.

In \(\lambda\rightarrow\), we assign types (i.e. members of \(\mathbb{T}\)) to terms; we write \(M:\sigma\) for "term \(M\) has type \(\sigma\)." Let's start with the simplest λ terms: ordinary variables. We assume each ordinary variable \(x\) has a unique type, say σ, so that \(x:\sigma\). In general, we assume that we have an infinite number of ordinary variables available for each type σ.

The types of applications & abstractions are built from those of their constituents. In the case of abstraction, if \(x:\sigma\), and \(M:\tau\), then \(\lambda x.M\) takes members of type σ and returns members of type τ, hence its type should be \(\sigma\rightarrow\tau\). We denote this more fully by writing \(\lambda x:\sigma.M:\sigma\rightarrow\tau\).

Analogously, the application \(MN\) is taking something with the type of \(N\), and \(M\) should be an abstraction, and hence have an arrow type; call it \(\sigma\rightarrow\tau\). For \(MN\) to make any sense, \(N\) must have type σ, and hence \(MN:\tau\).

At this point in our development of \(\lambda\rightarrow\), we see that there are many terms we can write down that make no sense from a typing perspective. Suppose, for instance, that \(M:\sigma\rightarrow\tau\) and \(N:\alpha\), then the application \(MN\) has no meaning.

We formalize this by defining the set of pre-typed λ-terms \(\Lambda_{\mathbb{T}}\) as

\begin{equation} \Lambda_{\mathbb{T}} = \mathscr{V}|(\Lambda_{\mathbb{T}}\Lambda_{\mathbb{T}})|(\lambda \mathscr{V}:\mathbb{T}.\Lambda_{\mathbb{T}}) \end{equation}

This is just the set of all terms we can possibly write according to our rules so far. Whether these terms belong in \(\lambda\rightarrow\) is a different question. For any given term in \(\Lambda_{\mathbb{T}}\), the issue of whether or not it makes any sense in terms of typing depends on the types of its constituents. We call a collection of type statements \(x:\sigma, y:\tau, z:\upsilon, \ldots\) where \(x,y,z,\ldots\) are all ordinary variables (i.e. not more complex terms) a context (generally denoted by an upper-case Greek letter). A judgement is a statement \(\Gamma\vdash M:\sigma\) where Γ is a context, \(M\) is some term, and σ is a type; the meaning could be given as "given Γ, it can be shown that \(M\) has type σ."

A pre-typed λ-term \(M\) is called legal if there exist context Γ and type ρ such that \(\Gamma\vdash M:\rho\). \(\lambda\rightarrow\) is the set of legal pre-typed terms.

I've used the phrase "can be shown", above. Let's make that precise.

We can validate a judgement \(\Gamma\vdash M:\sigma\) by giving something called a derivation. A derivation is a sequence of applications of derivation rules initialized with the contents of Γ and terminating with the conclusion that \(M:\sigma\). There are three derivation rules for \(\lambda\rightarrow\):

\begin{align} &\textbf{(var) } &\Gamma\vdash x:\sigma\text{ if } x:\sigma\in\Gamma\\ \nonumber\\ &\textbf{(appl) } &\frac{\Gamma\vdash M:\sigma\rightarrow\tau \enspace \Gamma\vdash N:\sigma}{\Gamma\vdash M N:\tau}\\ \nonumber\\ &\textbf{(abst) } &\frac{\Gamma,x:\sigma\vdash M:\tau}{\Gamma\vdash\lambda x:\sigma.M:\sigma\rightarrow\tau}\\ \end{align}

Each rule tells us what we can conclude so long as we know certain things already. In the case of (3) & (4), the premises are written above the line & the conclusions below. In the case of (2), there are no premises: if \(x:\sigma\in\Gamma\), then we are allowed to conclude: \(\Gamma\vdash x:\sigma\). A derivation is collection of applications of these rules, arranged in an inverted tree where the "root", at the bottom, is the statement we are justifying.

Let's work through an example (this is exercise 2.10 (d) in TTFP). Consider the term \(\lambda x:\alpha\rightarrow\beta.(y(xz))z\). What type might it have? Well, we know \(x:\alpha\rightarrow\beta\), therefore, if this term is typable, \(z\) must have type α due to the presence of the application \(xz\) in the middle of the term. That means \(xz:\beta\), so \(y\) must have type \(\beta\rightarrow\mu\) for some \(\mu\). \(y(xz)\) is then applied to \(z\), so μ must have type \(\alpha\rightarrow\gamma\) for some γ.

So we see that if we assume \(y:\beta\rightarrow\alpha\rightarrow\gamma\) and \(z:\alpha\), this term type-checks, and has type \((\alpha\rightarrow\beta)\rightarrow\gamma\). Let's prove this. To simplify our derivation, let's define \(\Gamma = \{x:\alpha\rightarrow\beta, y:\beta\rightarrow\alpha\rightarrow\gamma, z:\alpha\}\). Then:

We see that each leaf of this tree is an application of the (var) rule. Beginning in the upper right-hand corner, we've applied (var) twice to conclude that \(\Gamma\vdash x:\alpha\rightarrow\beta\) and \(\Gamma\vdash z:\alpha\), both of which are valid because of our definition of Γ. Those two statements, in turn, justify concluding that \(\Gamma\vdash xz:\beta\) by the (appl) rule.

To the left, we state that \(\Gamma\vdash y:\beta\rightarrow\beta\rightarrow\gamma\) again by the (var) rule, and combine that with our prior conclusion via the (appl) rule to conclude \(\Gamma\vdash y(xz):\alpha\rightarrow\gamma\). And so forth.

The reader may note a few things from this example. Firstly, derivations can quickly become large & complex. This is a fairly short judgement and it's already spread over the width of the page. Secondly, they entail repetition. In this judgement, we need to introduce \(\Gamma\vdash z:\alpha\) twice, once for each application to \(z\). This is characteristic, and becomes pronounced in more complex judgements that involve repeated sub-terms.

Nederpelt & Geuvers introduce an alternative format for derivations that they call "flag format". They suggest that this is their invention, but don't quite say it, so I'm not sure where it originated. Here, we surround each type declaration with a box (a "flag") and mark the extent of that declaration's context by drawing a line below it (the "flag pole"); all steps to the right of the flag pole assume that declaration in their context. The flag notation for the above derivation is:

We see that this style contains the same information as Figure 1: three invocations of (appl) & one of (abst). We have, however, omitted the applications of the (var) rule in the service of compactness & readability.

Note also that the flag pole corresponding to \(x:\alpha\rightarrow\beta\) extends only through line (6)– in line (7) we abstract over \(x\) changing it from free to bound (the context exists to type free variables). However, the flagpoles for the other two declarations extend to the bottom of the derivation, indicating that the context in the final judgement must be non-empty. Like Nederpelt & Geuvers, I'll be using the flag format going forward.

We are interested in three different problems pertaining to judgements in Type Theory:

Well-typedness/Typability

Consider \(?\vdash term:?\) (or \(context\vdash term:?\)); given a term, is it legal in some context (or, is it legal in the given context)?

Type checking

Consider \(context\vdash^{?} term : type\); given a judgement, is it true?

Term finding

Consider \(context\vdash ?:type\); is there a term of the given type in the given context?

We've refined our formal model for computation with the addition of types in order to rule-out misbehaving terms. We've also laid out the idea of derivation rules & their application in order to validate judgements regarding type. As we'll see, different derivation rules give rise to different type systems. In \(\lambda\rightarrow\) the basic problems of typability, type-checking & term finding are all decidable, but as we move into more powerful type systems, term finding becomes undecidable.

And Church succeeded in his aim: every legal term in \(\lambda\rightarrow\) is strongly normalizing. The problem with \(\lambda\rightarrow\) is that its nice features come at a cost: the set of legal terms therein is not terribly expressive. One can encode the natural numbers (the typed Church numerals) and define addition & multiplication… but not much more. This has led, in the decades since Church's paper, to attempts to extend the type system applied to the λ Calculus in hopes of getting better expressiveness while maintaining the desirable normalization properties. We'll look at some of them in subsequent posts, because they culminate in the Calculus of Inductive Constructions: the formal language recognized by Coq.

Originally published 05/20/24 06:55. Updated 05/21/2024 to build-out the section on term finding to re-use the same context (which is much more interesting).