---
tags: programming languages, 2020, 2021
---
$\newcommand{\sem}[1]{[\![#1]\!]}$
# Typed Lambda Calculus

"Well-typed programs cannot “go wrong”."

Robin Milner, [A Theory of Type Polymorphism in Programming](https://www.sciencedirect.com/science/article/pii/0022000078900144) (1978)

(The quote is also a pun. Technically, in the paper, "wrong" is an expression that has no type and the paper proves a theorem that well-typed expressions cannot reduce to "wrong".)

---

For the lecture, I selected from the below the following.

- Introduce the Y-combinator and show that $\mathsf Yg$ is a fixed point of every $g$.
- Discuss that the Y-combinator depends on self-application.
- Excursion on why the Y-combinator is called paradoxical, going back to Russell's barber paradox and the origins of the $\lambda$-calculus as a foundation of mathematics.
- Excursion on type checking arithmetic expressions in C.
- Typing rules for (Abs) and (App)
$$
\frac{x:X\quad e:T}{\lambda x.e : X\to T}({\sf Abs})
\quad\quad
\frac{a:X\to Y\quad\quad b:X}{a\ b:Y}({\sf App})
$$
- Under the assumption $x:X$ we computed the type of $\lambda f. \lambda x. f(fx)$ to be $(X\to X)\to (X\to X)$.
- On the other hand, trying to type the $Y$-combinator generates the constraint $X=X\to X$, an equation that cannot be solved for $X$.

---

# Introduction

The main difficulty in understanding lambda calculus stems from the fact that every lambda expression can be applied to any other lambda expression. In particular, this allows self-application: Whenever $e$ is lambda expression, then also
$$ e\ e $$

is a lambda expression.

But what could it mean to apply a function to itself?

**Activity:** Think about
- which lambda terms we have seen so far make use of self application;
- do programming languages you know allow self-application.

The outcome of the activity above suggests that even if we prohibit self-application, there are still a lot of interesting expressions that do remain.

In this lecture, we will introduce simply typed lambda calculus. Simply typed lambda calculus has many interesting properties:

- No self-application.
- There are type-checking and type-inference algorithms.
- Types are tautologies of a propositional logic.
- Typable terms are proofs.
- All computations terminate.

## Simply typed lambda calculus

One thing that is puzzling about the lambda calculus is that it does not make a distinction between functions and arguments, or, in other words, between programs and data.

This leads to the fact that we can write meaningless programs such as
$$(\lambda x. xx)(\lambda x. xx)$$

**Exercise:** Can you reduce $(\lambda x. xx)(\lambda x. xx)$ to normal form?

We are now going to add types to the lambda calculus. Meaningless programs such as $(\lambda x. xx)(\lambda x. xx)$ become untypable. But we will also loose some useful programs such as the $\mathsf Y$-combinator

$$\mathsf Y \stackrel{\rm def}{\ =\ }\lambda f.(\lambda x. f(x x)) (\lambda x. f(x x))$$

This tension between types and expressiveness is due to an important theorem of computability theory: Any calculus (=programming language) that allows us to implement all computable functions $\mathbb N\to\mathbb N$, must allow us to implement non-terminating (usually formalized as partial) functions. [^recursivefunctions]

[^recursivefunctions]: This theorem is not difficult to prove, but does currently not fit into this course.

This tension also appears in programming languages. On the one hand, as a programmer, we like to be supported by a compiler that discovers errors, on the other hand we don't like to be restricted in the kind of code we are allowed to write.

Untyped lambda calculus is one extreme: Every lambda term is a program. The only thing one can do with it, is running it. No compiler would discover any meaningful errors. Everything is allowed. The simply typed lambda calculus is the other extreme in that all well-typed programs are guaranteed to terminate (all computations are meaningful). This comes at the cost of not having general recursion (or while loops). Real programming languages are somewhere in between.

## Function Types (Curry Style)

Types are built inductively. We can have any number of base types, often denoted by letters such as $o$ and $\iota$ ("iota"). Then we can also form function types according to the BNF

$$\tau ::= \iota \mid \tau\to\tau$$

**Example:** If $A,B,C$ are types, then following are types as well.
\begin{gather}
A\to A\\
A\to (B\to A)\\
(A\to (B \to C))\to((A\to B)\to(A\to C))
\end{gather}

**Exercise/Activity:** Write down lambda terms that have these types.

Next we use types to restrict the ways lambda terms can be formed. In particular, self-application as in $\lambda x\,. xx$ will not be permitted.

To treat free and bound variables properly we need to give the typing rules relative to a so-called context that keeps track of the free variables appearing in a term. Thus, a context is a set (or, sometimes, a list) of variable declarations of the form $$x:\tau$$ where $\tau$ is a type. [^abuse] If $\Gamma$ is a set of such variable declarations, then we denote a context that contains $x:\tau$ by $$\Gamma, x:\tau.$$ Here, the comma can be read as a union in the sense that $\;\Gamma, x:\tau\;$ is a shorthand for $\;\Gamma\cup\{x:\tau\}$.

Before we come to the typing rules recall that the BNF

exp ::= x | \x.exp | exp exp x in Var

defining the untyped lambda calculus can also be written as a set of rules
$$
\frac{x \in Var}{x \in exp}
\quad\quad
\frac{x\in Var \quad M\in exp}{\lambda x\,.M\in exp}
\quad\quad
\frac{M\in\exp\quad\quad N\in exp}{M\, N \in \exp}
$$

The typing rules that we introduce now replace the type "$exp$" by a more refined collection of types that allow us, informally speaking, to distinguish functions from arguments. Instead of writing $M\in exp$, we will have $M:\tau$ for a type $\tau$. Importantly, a term $M$ can be applied to an argument $N$ only if $M$ has type $\sigma\to\tau$ for some types $\sigma,\tau$ and $N$ has type $\sigma$.

The well-typed terms in context $\Gamma$ of the ***simply typed lambda calculus*** are defined by recursion on abstract syntax via the rules

$$
\frac{x:\tau \in \Gamma}{\Gamma \vdash x:\tau}
\quad\quad
\frac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma\vdash\lambda x\,.M:\sigma\to\tau}
\quad\quad
\frac{\Gamma \vdash M:\sigma\to\tau\quad\quad\Gamma\vdash N:\sigma}{\Gamma\vdash M\, N:\tau}
$$

This is called Curry-style simply typed lambda calculus and plays an important role in programming languages and type theory. It is the simplest typed programming language but already illustrates a number of important ideas, some of which we will be looking at in the next section.

## Type Checking, Type Inference

Type checking is one of the most important techniques used by compilers to discover bugs at compile-time as opposed to leaving the users discover bugs at run-time. Moreover, a powerful type system enables the compiler to return meaningful error messages to the programmer.

How do we design a type system and a type checking algorithm for a compiler?

In a nutshell, for the simply typed lambda calculus, the answer is already contained in the rules $$
\frac{x:\tau \in \Gamma}{\Gamma \vdash x:\tau}
\quad\quad
\frac{\Gamma,x:\sigma \vdash M:\tau}{\Gamma\vdash\lambda x\,.M:\sigma\to\tau}
\quad\quad
\frac{\Gamma \vdash M:\sigma\to\tau\quad\quad\Gamma\vdash N:\sigma}{\Gamma\vdash M\, N:\tau}
$$
The first is boring and the second and third can be summarised by pictures.

The "term only" version of the pictures shows how to parse a $\lambda$-term into a tree in a top down fashion (first pass of compilation). The "types only" version shows how to compute and check the types by going through the syntax tree bottom up (second pass of compilation).

**Activity:** Review these two phases of compilation at the hand of an arithmetic expression. Show how code generation can easily be done in a second pass going bottom up through the parse tree. Explain that the computation of types follows the same pattern as the computation of values. Hint at how great that is for co ecking and code generation, follow the same structure and can be implemented in the same way.

**Discussion (types as abstract values):** Students might ask about the significance of this analogy of types and values. One can discuss and explain that types are abstracts values. In fact, types are engineered to be abstractions of values that can be computed at compile time. One could go here into a bit of computability theory, explaining why most interesting properties cannot be decided at compile time. But the quest for ever more powerful typesystems (and other methods of program analysis) has been an important impetus is programming language research.

**Activity:** Type inference for $$\lambda x.x$$ yields *most general type* $$\tau\to\tau$$ where $\tau$ is a type variable. Actually, it could be more accurate to write this type as [^2ndorder]
$$\forall\tau.\tau\to\tau$$What is the significance of using a type variable? This leads to the next topic.

**Type checking and type inference:**
- ***Type checking*** is the problem to decide whether the types assigned to different fragments of their programs are compatible. For example, if I have a function $\lambda x.x:int\to int$ and a $5:int$ and $true:bool$ then $(\lambda x.x)5$ type checks but $(\lambda x.x)true$ does not.
- ***Type inference*** is the problem of finding the most general type of a given program fragment. For example, the function $\lambda x.x$ can safely be applied at run-time to any type $\tau$. This idea appears in programming languages as, for example,
- [Hindley-Milner type inference](https://en.wikipedia.org/wiki/Hindley-Milner_type_system), eg in ML and Haskell
- [late binding](https://en.wikipedia.org/wiki/Late_binding), eg in Lisp, Smalltalk, Java and
- [duck typing](https://en.wikipedia.org/wiki/Duck_typing).
- ***Static typing*** will do type checking/type inference before the execution of the program.
- This allows the compiler to statically find programming mistakes at compile time and prevents run-time errors (which are much more costly as they may only appear after code has been shipped).
- Type inference allows some of the flexibility of dynamic typing in a static type discipline. For example, we statically infer that the type of $\lambda x.x$ is $\tau\to\tau$ but can dynamically, and safely, decide which particular type will instantiate $\tau$ at run-time.
- ***Dynamic typing*** does type checking only at run-time. I think of this as similar to raising an exception at run-time, but automatically provided by the compiler instead of explicitely implemented in the source code.

Type checking can be reduced to type inference. But there are type systems for which type inference is not decidable but type checking is.

There is an easy algorithm to decide these problems for the simply typed $\lambda$-calculus.

**Algorithm to compute the most general type in the simply typed lambda calculus:**

1. Take a lambda term $M$ and parse it into an abstract syntax tree. Let $C$ be the empty set.

2. Assign distinct type-variables to all the leaves of the tree.

3. Compute the types bottom up in the abstract syntax tree:
- in case of an abstraction, if the left child has type $\sigma$ and the right child has type $\tau$, the parent has type $\sigma\to\tau$
- in case of an application, if the left child has type $\sigma$ and the right child has type $\tau$, the parent has type $\tau'$ for a fresh type variable $\tau'$; add to the set $C$ of constraints the equation $\sigma=\tau\to\tau'$.

4. Solve the equations in $C$. If there is an equation $\tau=T$ where $T$ is a type that contains $\tau$,
- then the equations have no solution and the $\lambda$-term is not typable; STOP [^nosolution]
- else go to 5.

5. Let $\tau$ be the type at the root of the tree after simplifying the constraints in $C$. Let $\Gamma=\{x_1:\tau_1,\ldots x_n:\tau_n\}$ by the list of types assigned to the free variables of $M$. Then the result of the type inference is $$\Gamma \vdash M:\tau$$

Note that the most general type is only determined up to a choice of type variables. For example, I can write $\,\lambda x.x:\tau\to\tau\,$ or $\,\lambda x.x:\sigma\to\sigma\,$ or $\,\lambda x.x:A\to A\,$, etc. We often rename the type variables at the end to make the result look nicer.

**Examples/Exercises:** The most general type
- of $\lambda x.x$ is $\tau\to\tau$, which we also write as $\ \lambda x.x:\tau\to\tau$
- of $\lambda x.xx$ does not exist [^lambdax.xx]
- of $\lambda f.\lambda x. f\,x$ is $(\sigma\to\tau)\to\sigma\to\tau$ or, briefly, $\ \lambda f.\lambda x. f\,x : (\sigma\to\tau)\to\sigma\to\tau$
- of $\lambda f.\lambda x. f\,(f\,x)$ is $(\tau\to\tau)\to\tau\to\tau$ or $\ \lambda f.\lambda x. f\,x : (\tau\to\tau)\to\tau\to\tau$
- of $(\lambda\, x\,y. x\,y\,z)(\lambda\, a\,b.a)$ is $\tau\to\tau$ but there is also a free variable $z$ which can be of any type; we can include this in our notation by writing $$z:\sigma \vdash (\lambda\, x\,y. x\,y\,z)(\lambda\, a\,b.a):\tau\to\tau$$

You can have a look at the pictures of the trees I used to arrive at the results above: [1](https://github.com/alexhkurz/programming-languages/blob/master/Exercise-typinference-1.jpg), [2](https://github.com/alexhkurz/programming-languages/blob/master/Exercise-typinference-2.jpg), [3](https://github.com/alexhkurz/programming-languages/blob/master/Exercise-typinference-3.jpg), [4](https://github.com/alexhkurz/programming-languages/blob/master/Exercise-typinference-4.jpg).

## Semantics

(This is only a very short note on semantics since we didn't have time to do this in class)

### Introduction

Recall that there are meaningless terms such as $\lambda x.xx$. These terms are not functions in the sense that they produce a result on all possible inputs.

So this raises the question how a $\lambda$-calculus would look like in which all terms are functions.

Is it possible to filter out all meaningless terms so that we are only left with $\lambda$-terms that are legitimate functions?

The answer is yes and no.

Yes, we can use type systems to make sure that all typable terms are legitimate functions.

No, there is no type system in a term is a total function if and only if it is typable. [^clarification]

In this section we are going to explain that $\lambda$-terms are indeed functions. For this purpose, the so-called Church-style lambda calculus is notationally more convenient. In Church-style lambda calculus variable declarations are not needed since each variable already comes with its type. For example, in Fortran, a variable `i` is always an integer. We write
$$x^\tau$$

to denote a variable of type $\tau$. Here the type $\tau$ is not a type annotation but part of the name of the variable. [^churchcurry]

The rules for the calculus then become
$$
\frac{}{x^\tau:\tau}
\quad\quad
\frac{M:\tau}{\lambda x^\sigma\,.M:\sigma\to\tau}
\quad\quad
\frac{M:\sigma\to\tau\quad\quad N:\sigma}{\Gamma\vdash M\, N:\tau}
$$

First, we need to define the meaning of the types.

For each basic type $\iota$, we fix a set $A_\iota$. By induction on the definition of types we define the semantics $A_{\sigma\to\tau}$ of a function type $\sigma\to\tau$ to be the set of mathematical functions $\{f:A_\sigma\to A_\tau\}$. We can summarise this as

\begin{align}
\sem{\iota} &= A_\iota\\
\sem{\sigma\to\tau} &= \sem{\tau}^{\sem{\sigma}}
\end{align}

The meaning of terms must depend, due to the presence of variables, as in universal algebra, on an environment $\rho$ assigning a value in $A_\iota$ to each variable of type $\iota$.

\begin{align}
\sem{x^\tau} &= \rho(x)\\
\sem{\lambda x^\sigma\,.M}_\rho &= a\mapsto \sem{M}_{\rho[x\mapsto a]}\\
\sem{MN}_\rho & = \sem{M}_\rho(\sem{N}_\rho)
\end{align}

**Notation:** The environment $$\rho[x\mapsto a]$$ agrees with $\rho$ on all variables different from $x$ and evaluates $x$ to $a$. The notation $$a\mapsto \sem{M}_{\rho[x\mapsto a]}$$ denotes the mathematical function that maps $a$ to $\sem{M}_{\rho[x\mapsto a]}$.

**Remark:** Compare this to the use we made of [environments in universal algebra](https://hackmd.io/8sIMhAURSvm5ez9RDM4bXg#Environments). The crucial difference is that we now have a clause that changes the environment. In words, the meaning of $\lambda x^\sigma\,.M$ is a function that maps a $\lambda$-term $a$ to the meaning of $M$ where the free variable $x$ in $M$ has [R-value](https://hackmd.io/YjupXqLvQ7SFVewFI9TEXA#L--and-R-values-of-a-variable) $a$. Note that this does not change the R-value of the mathematical variable $x$, it rather changes the environment recording the R-value of $x$.

We dont have time now to continue this story, but at least we have seen that the definition

\begin{align}
\sem{\lambda x^\sigma\,.M}_\rho &= a\mapsto \sem{M}_{\rho[x\mapsto a]}\\
\end{align}

indeed allows us to say that the meaning of $\lambda x^\sigma\,.M$ is a proper mathematical function in the usual sense. This is reassuring and forms the basis for all of functionsal programming, from Lisp over ML to Haskell.

To be continued next semester if there is time ...

## Further References

- Pierce: [Types and Programming Languages](https://www.cis.upenn.edu/~bcpierce/tapl/) is an excellent introduction to programming languages that puts types center stage. Highly recommended.
- Reynolds: Theories of Programming Languages. 1998. Chapter 15.
- The article [Typability and type checking in System F are equivalent and undecidable](https://www.sciencedirect.com/science/article/pii/S0168007298000475/pdf?md5=658d9f66b1f04d036b20ed31f416609d&pid=1-s2.0-S0168007298000475-main.pdf) concerns a more advanced typed lambda calculus, but contains a useful general discussion in Section 1.3 about the importance of type inference and type checking for programming language design.
- The article [Teaching Denotational Semantics](http://www.cs.bham.ac.uk/~axj/pub/papers/Jung-2014-Teaching-denotational-semantics.pdf) by Jung contains an interesting discussion of Church vs Curry style and the outlines of a course on denotational semantics which I would have loved to present the main ideas of.

There are obvioiusly many more references worth reading, I may add some more later ...

[^abuse]: Note that in $\tau ::= o \mid \tau\to\tau$ the symbol $\tau$ is a variable in the sense of context-free grammars or a constant in the sense of term-rewriting. In particular, in $\tau\to\tau$, the $\tau$ can stand in for two different types. On the other hand, in the typing rules, the symbol $\tau$ is a meta-variable, or place-holder, and inside the same expression, the same symbol $\tau$ needs to be replaced with the same type.

[^2ndorder]: So far we only have 'function types' as in $\sigma\to\tau$. Adding quantification to this as in $\forall \tau. T$ where $T$ is a type depending on $\tau$ leads to the [Girard-Reynolds 2nd order $\lambda$-calculus/System F](https://en.wikipedia.org/wiki/System_F). For example, one can then *define* the natural numbers as the set of all polymorphic functions of type $$\forall\tau: (\tau\to\tau)\to\tau\to\tau$$

[^nosolution]: It is this clause that prevents typing of lambda terms that contain an expression such as $xx$, since this expression would force $x:\tau$ to satisfy $\tau=\tau\to\tau'$.

[^lambdax.xx]: According to the algorithm we label the leafs with $\tau$. The application $xx$ is of type $\tau'$ and the equation is $\tau=\tau\to\tau'$. This equation has no solution, therefore $\lambda x.xx$ is not typable.

[^churchcurry]: Consequently, if we are fully precise, the terms of the Church-style lambda calculus are different from the terms of the lambda calculus (which are the same as the terms of the Curry-style lambda calculus).

[^clarification]: Clarification: When I say "legitimate" function or "total" function I mean a function $\mathbb N\to\mathbb N$ in the sense of [mathematics](https://hackmd.io/s/B1gOX4lO7). When I say "type system" and "typable", I am assuming that typability is decidable. An undecidable type system is much less useful.