Programming Language Theory: From Machine Code to Type Systems and Paradigms

0. Key points

• All a CPU can execute is a fixed-length string of bits (machine code). Assembly language merely attaches human-readable names to those bit strings; between assembly and a high-level language there is a qualitative break, namely a meaning-preserving translation.
• The difference between a compiler and an interpreter is a difference of implementation strategy, not of language. The same language can have both. Where the distinction really bites is whether errors are found before execution or during it.
• The value of a type system comes down to two theorems: progress and preservation. Together they guarantee that a well-typed program never gets stuck in mid-execution (type soundness).
• Static type checking, so long as it is sound, is necessarily incomplete. This is not immaturity of implementation but a limit of principle, derived from the undecidability of the halting problem.
• The central notion of functional programming is referential transparency, which makes the theorem “the same expression evaluates to the same value however often it is evaluated” true. The central notions of object-oriented programming are dynamic dispatch and subtyping, and the subtyping rule for function types is contravariant in the argument.

1. Motivation: why do we need a “language”?

As we saw in Definition 6.1［Computer Architecture and the Structure of a CPU］ of Computer architecture and the structure of the CPU, what a CPU understands is nothing but strings of 32 or 64 bits. On the machines of the 1940s people really did write out those bit strings on paper and enter them with switches or punched cards.

The work was unbearable in two distinct ways. First, one makes mistakes. A single wrong bit yields a different instruction, and since that instruction is usually “valid” too, the machine cheerfully goes on computing the wrong thing. Second, nothing can be revised. Insert one instruction into the middle of a program and every branch target after it shifts.

The idea that emerged was: write in symbols and let the machine do the translating. There is a leap hidden here — the self-reference that the translator is itself a program. When Grace Hopper completed the A-0 system in 1952 and John Backus’s team at IBM completed the FORTRAN compiler in 1957, many engineers held that machine-generated code could never beat hand-written code. Today that scepticism has been thoroughly overturned.

But the moment translation is handed to a machine, a new question appears: what does it mean for a translation to be correct? To answer it we must first define “the meaning of a program” mathematically. This article starts from that definition and works up to the design principles of type systems and paradigms.

2. The staircase of abstraction: machine code and assembly

2.1. Machine code is an encoding of instructions

Take the 32-bit RISC-V instruction addi (add immediate) as our example. The convention fixing which instruction name corresponds to which arrangement of bits is the instruction set architecture of Definition 8.1［Computer Architecture and the Structure of a CPU］. This instruction has the layout called the I-format: from the top, a 12-bit immediate, a 5-bit source register number rs1, a 3-bit funct3, a 5-bit destination register number rd, and a 7-bit opcode.

Example 2.1（Encoding the addi instruction by hand）

Let us encode the instruction “add 1 to the value in register a0 and put it back in a0”. In RISC-V, a0 is register number 10, that is 01010 in binary. The opcode of addi is 0010011 and its funct3 is 000. The immediate 1 is 000000000001 in 12 bits.

Concatenating these from the top:

000000000001  01010  000  01010  0010011
  imm = 1     rs1=10 funct3 rd=10  opcode

Removing the separators and regrouping into blocks of four bits gives 0000 0000 0001 0101 0000 0101 0001 0011, that is 0x00150513 in hexadecimal. By the same procedure add a0, a0, a1 (R-format; the encoding of the R-format is also computed in Example 8.2［Computer Architecture and the Structure of a CPU］) comes out as 0x00B50533, and the return instruction ret (really jalr x0, 0(x1)) as 0x00008067.

So the single line of assembly addi a0, a0, 1 is nothing more than an alternative notation standing in one-to-one correspondence with the 32-bit integer 0x00150513.

That this correspondence is one-to-one is decisive. The assembler’s whole job is to look up instruction names in a table of opcodes, turn register names into numbers, resolve labels into addresses, and pack the bits. It introduces no new concepts.

2.2. What did high-level languages add?

A single line of C, by contrast, often expands into several instructions.

int add1(int x) { return x + 1; }

Compiled for RISC-V with optimization, this becomes two instructions.

add1:
    addi a0, a0, 1     # 0x00150513
    ret                # 0x00008067

What happens here is not a mere substitution of symbols. It uses knowledge of the calling convention (“the argument x is in the first argument register a0”; “the return value also goes in a0”), of the correspondence between types and representations (“int is 32-bit two’s complement”), and of an optimization decision (“a local variable may be allocated to a register”). What high-level languages added is the abstraction that takes such decisions out of human hands.

flowchart TD
A["high-level source (C, Python, OCaml)"] --> B["intermediate representation (syntax tree, IR)"]
B --> C["assembly language (addi a0, a0, 1)"]
C --> D["machine code (0x00150513)"]
D --> E["the CPU executes"]
B -.meaning-preserving translation.-> C

The staircase from source code to execution. Above the dashed arrow is notation written by humans, below it are representations handled by machines

3. Compilers and interpreters

Definition 3.1（Translator and interpreter）

Consider a language $S$ (the source language), a language $T$ (the target language) and a language $I$ (the implementation language).

A compiler is a program $C$ written in $I$ which, given a program $p$ of $S$ as input, outputs a program $C(p)$ of $T$ such that for every input $d$ the result of applying $p$ to $d$ agrees with the result of applying $C(p)$ to $d$.

An interpreter is a program $J$ written in $I$ which takes a pair consisting of a program $p$ of $S$ and an input $d$, and directly outputs the result of applying $p$ to $d$.

What this definition is meant to bring out is that being compiled or interpreted is not an attribute of a language. Both achieve the same goal, “realize the meaning of $p$”, and differ only in the shape of their output. Indeed C has interpreters (Cling, for one), and Python has implementations that generate machine code (the JIT of PyPy). To say “Python is an interpreted language” means, accurately, “the principal implementation of Python, CPython, is a bytecode interpreter”.

Aspect	Compiled	Interpreted
When errors are found	Syntax and type errors are detected at translation time (before execution)	Detected when the line in question is reached
Execution speed	Fast, since optimization can be done at translation time	Carries the overhead of interpreting each instruction
Startup	The translation time must be paid first	Runs immediately
Portability	Must be retranslated for each target machine	The same code runs wherever there is an interpreter
Use of run-time information	Limited to what is statically known	Can optimize on the basis of the path actually taken

Remark 3.2

The last row is the reason JIT (just-in-time compilation) exists. The fact that “the last ten thousand times, this call site received objects of the same type” cannot be known statically; it can only be observed at run time. A JIT bets on such observations to generate specialized code and falls back to interpretation when the bet fails. Compilation and interpretation are not opposites; the accurate view is that they differ in the moment at which information becomes available.

4. Stating the meaning of a program precisely

To say “the translation preserves meaning” we need a definition of meaning. Here we demonstrate, on a minimal language, the most widely used approach: operational semantics, which gives meaning by specifying how a term is rewritten one step at a time.

Definition 4.1（Syntax and reduction relation of the language L）

Terms $t$ are given by the following grammar.

$$t ::= \mathtt{true} \mid \mathtt{false} \mid \mathtt{if}\ t\ \mathtt{then}\ t\ \mathtt{else}\ t \mid \mathtt{0} \mid \mathtt{succ}\ t \mid \mathtt{pred}\ t \mid \mathtt{iszero}\ t$$

Numeric values $nv$ and values $v$ are defined by

$$nv ::= \mathtt{0} \mid \mathtt{succ}\ nv, \qquad v ::= \mathtt{true} \mid \mathtt{false} \mid nv$$

The one-step reduction relation $t \to t'$ is the least relation generated by the following rules.

$$\begin{aligned} &\text{(E-IfTrue)} && \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_2 \\ &\text{(E-IfFalse)} && \mathtt{if}\ \mathtt{false}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_3 \\ &\text{(E-If)} && \frac{t_1 \to t_1'}{\mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to \mathtt{if}\ t_1'\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3} \\ &\text{(E-Succ)} && \frac{t \to t'}{\mathtt{succ}\ t \to \mathtt{succ}\ t'} \\ &\text{(E-PredZero)} && \mathtt{pred}\ \mathtt{0} \to \mathtt{0} \\ &\text{(E-PredSucc)} && \mathtt{pred}\ (\mathtt{succ}\ nv) \to nv \\ &\text{(E-Pred)} && \frac{t \to t'}{\mathtt{pred}\ t \to \mathtt{pred}\ t'} \\ &\text{(E-IszeroZero)} && \mathtt{iszero}\ \mathtt{0} \to \mathtt{true} \\ &\text{(E-IszeroSucc)} && \mathtt{iszero}\ (\mathtt{succ}\ nv) \to \mathtt{false} \\ &\text{(E-Iszero)} && \frac{t \to t'}{\mathtt{iszero}\ t \to \mathtt{iszero}\ t'} \end{aligned}$$

A term to which no rule applies is called a normal form. A normal form that is not a value is called a stuck term.

Being stuck is what “run-time error” means in this formalization. For instance $\mathtt{pred}\ \mathtt{false}$ matches the shape of neither E-PredZero nor E-PredSucc, and E-Pred cannot be used either because $\mathtt{false}$ cannot be reduced; so no rule applies. Nor is it a value. On a real machine this is the situation in which an exception “pred cannot be applied to a Boolean” is raised.

Example 4.2（Following an evaluation sequence to the end）

Let us reduce the term $\mathtt{if}\ (\mathtt{iszero}\ (\mathtt{pred}\ (\mathtt{succ}\ \mathtt{0})))\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0}$, noting on each line the rules used.

$$\begin{aligned} &\ \mathtt{if}\ (\mathtt{iszero}\ (\mathtt{pred}\ (\mathtt{succ}\ \mathtt{0})))\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} \\ \to&\ \mathtt{if}\ (\mathtt{iszero}\ \mathtt{0})\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} && \text{premise of E-If derived by E-Iszero, whose premise is E-PredSucc (} nv = \mathtt{0} \text{)} \\ \to&\ \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{succ}\ \mathtt{0} && \text{premise of E-If derived by E-IszeroZero} \\ \to&\ \mathtt{0} && \text{E-IfTrue} \end{aligned}$$

Since $\mathtt{0}$ is a value, we stop here. Note that on the second line it is the single rule E-If, and nothing else, that decides “evaluate the condition to the end first”. Without that rule one could equally well write a semantics in which the branch is taken with the condition still unevaluated. Giving a semantics is exactly the work of fixing such choices explicitly.

This set of rules transcribes directly into an executable program. What follows is a complete interpreter for the language L.

def is_numeric(t):
    if t == ("zero",):
        return True
    if t[0] == "succ":
        return is_numeric(t[1])
    return False

class Stuck(Exception):
    pass

def step(t):
    """Reduce the term t by one step; raise Stuck if no rule applies."""
    k = t[0]
    if k == "if":
        _, t1, t2, t3 = t
        if t1 == ("true",):
            return t2                       # E-IfTrue
        if t1 == ("false",):
            return t3                       # E-IfFalse
        return ("if", step(t1), t2, t3)     # E-If
    if k == "succ":
        return ("succ", step(t[1]))         # E-Succ
    if k == "pred":
        u = t[1]
        if u == ("zero",):
            return ("zero",)                # E-PredZero
        if u[0] == "succ" and is_numeric(u):
            return u[1]                     # E-PredSucc
        return ("pred", step(u))            # E-Pred
    if k == "iszero":
        u = t[1]
        if u == ("zero",):
            return ("true",)                # E-IszeroZero
        if u[0] == "succ" and is_numeric(u):
            return ("false",)               # E-IszeroSucc
        return ("iszero", step(u))          # E-Iszero
    raise Stuck(t)

def evaluate(t):
    while True:
        try:
            t = step(t)
        except Stuck:
            return t                        # a normal form has been reached

term = ("if", ("iszero", ("pred", ("succ", ("zero",)))), ("zero",), ("succ", ("zero",)))
print(evaluate(term))                       # ('zero',)
print(evaluate(("pred", ("false",))))       # ('pred', ('false',))  <- stuck

Lemma 4.3（Basic properties of values）

(1) If $nv$ is a numeric value, then there is no term $t'$ with $nv \to t'$. (2) If $v$ is a value, then there is no term $t'$ with $v \to t'$.

Proof（Lemma 4.3）

We prove (1) by induction on the structure of $nv$. When $nv = \mathtt{0}$, none of the rules of Definition 4.1 has a left-hand side of the form $\mathtt{0}$ (the left-hand side of E-PredZero is $\mathtt{pred}\ \mathtt{0}$, not $\mathtt{0}$). Hence no reduction is possible.

When $nv = \mathtt{succ}\ nv_1$, the only rule whose left-hand side begins with $\mathtt{succ}$ is E-Succ. To use E-Succ we need the premise $nv_1 \to t_1'$, but by the induction hypothesis $nv_1$ cannot be reduced, so the premise cannot be met. Hence $\mathtt{succ}\ nv_1$ cannot be reduced either.

(2) A value is $\mathtt{true}$, $\mathtt{false}$ or a numeric value. No rule has $\mathtt{true}$ or $\mathtt{false}$ on its left-hand side (the left-hand side of E-IfTrue is a term beginning with $\mathtt{if}$), and for numeric values the claim is (1).

∎

Theorem 4.4（Determinism of reduction）

For every term $t$ of the language L, if $t \to t'$ and $t \to t''$ then $t' = t''$.

Proof（Theorem 4.4）

We argue by induction on the derivation of $t \to t'$, splitting into cases on the shape of $t$.

Case $t = \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$. If $t_1 = \mathtt{true}$, the only applicable rule is E-IfTrue: using E-If would require the premise $t_1 \to t_1'$, and by Lemma 4.3 (2) $\mathtt{true}$ cannot be reduced, so E-If is unavailable. Hence $t' = t'' = t_2$. The case $t_1 = \mathtt{false}$ is the same. If $t_1$ is neither $\mathtt{true}$ nor $\mathtt{false}$, then neither E-IfTrue nor E-IfFalse matches, so both reductions come from E-If, with premises $t_1 \to s_1$ and $t_1 \to s_1'$ respectively. By the induction hypothesis $s_1 = s_1'$, whence $t' = t''$.

Case $t = \mathtt{pred}\ t_1$. If $t_1 = \mathtt{0}$, only E-PredZero applies (the premise $\mathtt{0} \to \cdot$ of E-Pred fails by Lemma 4.3 (1)), and $t' = t'' = \mathtt{0}$. If $t_1 = \mathtt{succ}\ nv$ with $nv$ a numeric value, E-PredSucc applies, while E-Pred would demand the premise $\mathtt{succ}\ nv \to \cdot$, which fails by Lemma 4.3 (1). Hence $t' = t'' = nv$. This is where part (1) of the lemma does essential work. If $t_1$ has the form $\mathtt{succ}\ u$ with $u$ not a numeric value, then E-PredSucc does not match, so both reductions are by E-Pred and the induction hypothesis settles the matter. For all other shapes of $t_1$, only E-Pred is available.

The case $t = \mathtt{iszero}\ t_1$ is argued exactly as for $\mathtt{pred}$. When $t = \mathtt{succ}\ t_1$, only E-Succ applies and the claim follows from the induction hypothesis. When $t$ is a value it cannot be reduced by Lemma 4.3, contradicting the hypothesis, so that case does not arise.

∎

Determinism is the formal content of “the same program yields the same result however often it is run”. Introduce concurrency or randomness and the theorem fails, and at that moment the difficulty of debugging leaps upward (on the machinery for controlling order and fixing results under concurrent execution, see Definition 6.1［What an Operating System Does］).

5. Types: static and dynamic typing

As we saw right after Definition 4.1, L has terms that get stuck. A type system is a mechanism for excluding some of those terms before execution.

Definition 5.1（The typing relation of the language L）

Let the types be $T ::= \mathtt{Bool} \mid \mathtt{Nat}$. The relation $\vdash t : T$ (“the term $t$ has type $T$”) is the least relation generated by the following rules.

$$\begin{aligned} &\text{(T-True)} && \vdash \mathtt{true} : \mathtt{Bool} \qquad &&\text{(T-False)} && \vdash \mathtt{false} : \mathtt{Bool} \qquad &&\text{(T-Zero)} && \vdash \mathtt{0} : \mathtt{Nat} \\[4pt] &\text{(T-If)} && \frac{\vdash t_1 : \mathtt{Bool} \quad \vdash t_2 : T \quad \vdash t_3 : T}{\vdash \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 : T} &&\text{(T-Succ)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{succ}\ t : \mathtt{Nat}} \\[4pt] &\text{(T-Pred)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{pred}\ t : \mathtt{Nat}} &&\text{(T-Iszero)} && \frac{\vdash t : \mathtt{Nat}}{\vdash \mathtt{iszero}\ t : \mathtt{Bool}} \end{aligned}$$

Note that T-If demands the same $T$ for $t_2$ and $t_3$. This one spot is the principal source of the incompleteness of type systems that we come to below.

Lemma 5.2（Canonical forms）

(1) If $v$ is a value and $\vdash v : \mathtt{Bool}$, then $v = \mathtt{true}$ or $v = \mathtt{false}$. (2) If $v$ is a value and $\vdash v : \mathtt{Nat}$, then $v$ is a numeric value.

Proof（Lemma 5.2）

(1) A value is $\mathtt{true}$, $\mathtt{false}$ or a numeric value. Suppose $v$ were a numeric value. If $v = \mathtt{0}$, the only rule assigning it a type is T-Zero, so only $\vdash v : \mathtt{Nat}$ is derivable, contradicting $\vdash v : \mathtt{Bool}$. If $v = \mathtt{succ}\ nv$, the only rule assigning it a type is T-Succ, and again the conclusion is $\mathtt{Nat}$. Hence $v$ is not a numeric value, and is therefore $\mathtt{true}$ or $\mathtt{false}$.

(2) Similarly, if $v = \mathtt{true}$ then T-True yields only $\mathtt{Bool}$, and if $v = \mathtt{false}$ then T-False yields only $\mathtt{Bool}$. Both contradict the hypothesis $\vdash v : \mathtt{Nat}$, so $v$ is a numeric value.

∎

Theorem 5.3（Progress）

A term $t$ with $\vdash t : T$ is either a value or there exists a term $t'$ with $t \to t'$. That is, a well-typed term is not a stuck term.

Proof（Theorem 5.3）

We argue by induction on the derivation of $\vdash t : T$.

If T-True, T-False or T-Zero was used last, then $t$ is $\mathtt{true}$, $\mathtt{false}$ or $\mathtt{0}$ respectively, all of which are values.

In the case of T-If we have $t = \mathtt{if}\ t_1\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$ with $\vdash t_1 : \mathtt{Bool}$. By the induction hypothesis $t_1$ is either a value or reducible. If it is reducible, then E-If lets the whole of $t$ reduce. If $t_1$ is a value, then $\vdash t_1 : \mathtt{Bool}$ and Lemma 5.2 (1) make $t_1$ equal to $\mathtt{true}$ or $\mathtt{false}$, so E-IfTrue or E-IfFalse applies.

In the case of T-Succ we have $t = \mathtt{succ}\ t_1$ with $\vdash t_1 : \mathtt{Nat}$. By the induction hypothesis $t_1$ is a value or reducible. If reducible, E-Succ reduces $t$. If a value, then by Lemma 5.2 (2) $t_1$ is a numeric value, so $\mathtt{succ}\ t_1$ is itself a numeric value and hence a value.

In the case of T-Pred we have $t = \mathtt{pred}\ t_1$ with $\vdash t_1 : \mathtt{Nat}$. If $t_1$ is reducible we use E-Pred. If $t_1$ is a value then by Lemma 5.2 (2) it is a numeric value, and a numeric value has the form $\mathtt{0}$ or $\mathtt{succ}\ nv$. E-PredZero applies in the first case, E-PredSucc in the second. The point is that these two cases exhaust the numeric values; a case such as $\mathtt{pred}\ \mathtt{false}$ never arises here, because $\vdash \mathtt{false} : \mathtt{Nat}$ is not derivable.

The case of T-Iszero has the same structure, with E-IszeroZero and E-IszeroSucc covering all shapes of numeric value.

∎

Theorem 5.4（Preservation）

If $\vdash t : T$ and $t \to t'$, then $\vdash t' : T$. That is, reduction does not change the type.

Proof（Theorem 5.4）

We argue by induction on the derivation of $t \to t'$, checking each rule. Throughout, the typing rules are determined uniquely by shape, so from the shape of $t$ we can read off the typing rule used last (the inversion lemma).

E-IfTrue: $t = \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3 \to t_2$. The derivation of $\vdash t : T$ ends with T-If, so $\vdash t_2 : T$ is among its premises. Hence $\vdash t' : T$. For E-IfFalse the premise $\vdash t_3 : T$ is available in the same way.

E-If: $t \to \mathtt{if}\ t_1'\ \mathtt{then}\ t_2\ \mathtt{else}\ t_3$ with premise $t_1 \to t_1'$. From the premises of T-If we have $\vdash t_1 : \mathtt{Bool}$, $\vdash t_2 : T$ and $\vdash t_3 : T$. By the induction hypothesis $\vdash t_1' : \mathtt{Bool}$. Applying T-If to these three gives $\vdash t' : T$.

E-Succ: by T-Succ, $T = \mathtt{Nat}$ and $\vdash t_1 : \mathtt{Nat}$. By the induction hypothesis $\vdash t_1' : \mathtt{Nat}$, and T-Succ gives $\vdash \mathtt{succ}\ t_1' : \mathtt{Nat}$.

E-PredZero: $\mathtt{pred}\ \mathtt{0} \to \mathtt{0}$. By T-Pred, $T = \mathtt{Nat}$, and by T-Zero, $\vdash \mathtt{0} : \mathtt{Nat}$.

E-PredSucc: $\mathtt{pred}\ (\mathtt{succ}\ nv) \to nv$. By T-Pred, $T = \mathtt{Nat}$ and $\vdash \mathtt{succ}\ nv : \mathtt{Nat}$. The only rule that can derive this is T-Succ, so $\vdash nv : \mathtt{Nat}$ is among its premises.

E-Pred: apply the induction hypothesis to the premise $\vdash t_1 : \mathtt{Nat}$ of T-Pred and reapply T-Pred.

E-IszeroZero: $\mathtt{iszero}\ \mathtt{0} \to \mathtt{true}$. By T-Iszero, $T = \mathtt{Bool}$, and by T-True, $\vdash \mathtt{true} : \mathtt{Bool}$. E-IszeroSucc is the same with T-False.

E-Iszero: apply the induction hypothesis to the premise of T-Iszero and reapply T-Iszero. This exhausts all the reduction rules.

∎

Corollary 5.5（Type soundness）

If $\vdash t : T$, then for every reduction sequence $t \to t_1 \to \cdots \to t_n$ starting from $t$, the term $t_n$ is not a stuck term. That is, a well-typed program never gets stuck in mid-execution.

Proof（Corollary 5.5）

We induct on $n$. Applying Theorem 5.4 $n$ times yields $\vdash t_n : T$. Applying Theorem 5.3 to this $t_n$ shows that $t_n$ is either a value or further reducible. Since a stuck term is by definition a normal form that is not a value, $t_n$ cannot satisfy both conditions at once, and so is not stuck.

∎

This two-step scheme, “progress + preservation = soundness”, has been the standard proof obligation in designing a type system ever since Wright and Felleisen formulated it in 1994. Add a new language feature and you reprove these two theorems. That, in substance, is what “designing a type system” means.

5.1. Static checking is necessarily incomplete

Corollary 5.5 guarantees only one direction. Well-typed implies safe, but not conversely. The term $\mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$ reduces by E-IfTrue to $\mathtt{0}$ and finishes without trouble, yet it has no type, because T-If demands that the branches agree. Is this a defect of the toy language L? It is not.

Theorem 5.6（Incompleteness of sound static checking）

Let $\mathcal{L}$ be a Turing-complete programming language and let $P$ be the set of all programs that do not halt with a type error when executed. If $C \subseteq \mathcal{L}$ is decidable (whether a given program belongs to $C$ can always be determined in finite time) and sound ($C \subseteq P$), then $C \subsetneq P$. That is, there is necessarily a program that is safe but is not accepted by $C$.

Proof（Theorem 5.6）

First we show that $P$ is undecidable, by reduction from the halting problem. Given a pair consisting of a Turing machine $M$ and an input $w$, we construct mechanically the following program $p_{M,w}$.

body of p(M, w):
  simulate M on w              # may never halt
  evaluate 1 + true            # reaching here is always a type error

Since $\mathcal{L}$ is Turing complete, a simulator for $M$ can be written in $\mathcal{L}$. Then $p_{M,w}$ raises a type error precisely when the simulation halts and the second line is reached. Hence

$$p_{M,w} \in P \iff M \text{ does not halt on } w$$

holds. If $P$ were decidable, this correspondence would make the halting problem decidable as well, contradicting Turing’s result. So $P$ is undecidable.

Now $C$ is decidable and $P$ is undecidable, so $C \ne P$. Since $C \subseteq P$ by hypothesis, $C \subsetneq P$ follows. The elements of $P \setminus C$ are exactly the programs that are safe yet not accepted.

∎

The reach of sound static type checking. Only the inside of the heavy curve consists of well-typed programs, and safe programs always remain outside it

Note

The theorem does not say that making the type checker cleverer is pointless. The larger $C$ is, the fewer safe programs are rejected. Generics, sum types and flow-sensitive narrowing are precisely the tools for pushing $C$ closer to $P$. All the theorem forbids is the completed state $C = P$.

5.2. Comparing static and dynamic

Aspect	Static typing (Java, OCaml, Rust, TypeScript)	Dynamic typing (Python, Ruby, JavaScript)
Error detection	Before execution; errors on unreached paths are found too	At run time; a test that exercises the code is needed
Programs rejected	Rejects programs that are safe but ill-typed	Rejects nothing; you find out by running
Performance	Types are fixed, so value representations can be optimized	Carries the cost of checking type tags at run time
Maintainability	Types act as a machine-checked specification	The specification depends on documents and tests
Flexibility of expression	Extra code is sometimes needed to satisfy the checker	Prototypes and exploratory code can be written briefly
Refactoring	The type checker points out call sites you forgot to update	Omissions surface only when the code is run

Example 5.7（Carrying out type inference to the end）

The labour of writing types in a statically typed language can be cut down considerably by type inference. Let us determine the type of the function twice (which applies its argument f twice) by collecting and solving constraints.

$$\mathtt{twice} = \lambda f.\ \lambda x.\ f\ (f\ x)$$

Let the type of $f$ be a type variable $\alpha$ and the type of $x$ be $\beta$.

1. For the inner application $f\ x$ to be typable, $f$ must be a function taking $\beta$. Writing $\gamma$ for the result type gives the constraint $\alpha = \beta \to \gamma$.
2. In the outer application $f\ (f\ x)$, $f$ receives $\gamma$. Writing $\delta$ for the result gives the constraint $\alpha = \gamma \to \delta$.
3. From the two constraints, $\beta \to \gamma = \gamma \to \delta$. An equation between function types decomposes into equations between arguments and between results, so $\beta = \gamma$ and $\gamma = \delta$.
4. Hence $\gamma = \delta = \beta$ and $\alpha = \beta \to \beta$.

The type of the whole is $(\beta \to \beta) \to \beta \to \beta$, and since no constraint remains on $\beta$ we quantify universally to obtain $\forall \beta.\ (\beta \to \beta) \to \beta \to \beta$. Without a single type annotation, the most general type was determined uniquely. This procedure is Hindley–Milner type inference, and it underlies OCaml, Haskell, and the local type inference of Rust.

6. Paradigms: functional and object-oriented

6.1. Functional: referential transparency generates theorems

The theoretical matrix of functional programming is the $\lambda$-calculus of the 1930s. Its terms are just three: variables $x$, abstractions $\lambda x.\ t$, and applications $t_1\ t_2$; and its rule of computation is just one, $\beta$-reduction $(\lambda x.\ t)\ u \to t[x := u]$. This minimal system has the same computational power as the Turing machine.

Theorem 6.1（Church–Rosser theorem (confluence)）

For a term $t$ of the $\lambda$-calculus, if $t \twoheadrightarrow t_1$ and $t \twoheadrightarrow t_2$ (where $\twoheadrightarrow$ is the reflexive transitive closure of $\beta$-reduction), then there exists a term $s$ with $t_1 \twoheadrightarrow s$ and $t_2 \twoheadrightarrow s$.

Remark 6.2

The standard proof is the one by Tait and Martin-Löf using parallel reduction, and a complete version appears in Chapter 3 of Barendregt’s textbook. Here it is enough to grasp what the statement means. Where Theorem 4.4 said that there is only one order of reduction, Church–Rosser says that there may be several orders but that the results converge. Hence a normal form is unique if it exists, and whichever part of an expression one evaluates first, the final result is the same. This is the ground on which parallel execution and lazy evaluation do not destroy meaning.

Definition 6.3（Referential transparency）

A language is called referentially transparent when its evaluation relation is deterministic, the result of evaluating an expression depends only on the bindings of its free variables, and evaluation does not alter the state of the machine (mutation of variables, input/output, the current time, and so on).

Proposition 6.4（Soundness of common subexpression elimination）

In a referentially transparent language, suppose an expression $e$ evaluates to the value $v$ under an environment $\rho$. Then replacing both of two occurrences of $e$ inside a larger expression by $v$ does not change the result of evaluating the whole.

Proof（Proposition 6.4）

Suppose the first evaluation of $e$ returned the value $v$. By Definition 6.3, evaluation does not alter the state, so the environment $\rho$ is the same before and after that first evaluation. The second evaluation therefore takes place under the same environment $\rho$. Evaluation of the same expression in the same environment returns the same value, by the assumption of determinism. Hence the second result is $v$ as well. Since both occurrences evaluate to the same value $v$, replacing them by $v$ leaves the value of the whole unchanged.

∎

This proposition justifies the optimization of computing $e$ once and reusing the result (common subexpression elimination). Conversely, without referential transparency the optimization is unsound.

Example 6.5（Side effects break optimization）

In the following Python code, treating f() + f() as a “common subexpression” and collapsing it into a single call changes the result.

counter = 0

def f():
    global counter
    counter += 1
    return counter

print(f() + f())        # 1 + 2 = 3

counter = 0
a = f()
print(a + a)            # 1 + 1 = 2

The outputs are 3 and 2, which disagree. The assumption of Definition 6.3 that “evaluation does not alter the state” is violated, so the first step in the proof of Proposition 6.4 (that the environment is the same) fails. Functional languages isolate side effects with types, or forbid them, not out of asceticism but in order to use this kind of equational reasoning safely.

6.2. Object-oriented: dynamic dispatch and subtyping

At the centre of object orientation is not inheritance but dynamic dispatch: the receiver decides at run time which code is to be called. What it really amounts to is a record bundling data together with function pointers.

def make_circle(r):
    return {"area": lambda: 3.14159 * r * r, "name": lambda: "circle"}

def make_square(s):
    return {"area": lambda: s * s, "name": lambda: "square"}

shapes = [make_circle(1.0), make_square(2.0)]
for sh in shapes:
    print(sh["name"](), sh["area"]())   # circle 3.14159 / square 4.0

Which function sh["area"] denotes is not settled until we look inside sh. At the level of machine code this comes down to two instructions: read a function pointer from memory and jump indirectly to that address (the virtual function tables of C++ and Java have exactly this structure). Because the branch target is not statically determined, the branch prediction discussed in Computer architecture and the structure of the CPU works poorly, and this is what the cost of a virtual call really consists of (a misprediction forfeits the gain from pipelining; see Proposition 7.2［Computer Architecture and the Structure of a CPU］).

Definition 6.6（Subtyping and the subsumption rule）

We require the relation $S \le T$ between types (”$S$ is a subtype of $T$”) to be a relation for which the following subsumption rule is sound.

$$\frac{\Gamma \vdash t : S \qquad S \le T}{\Gamma \vdash t : T}$$

That is, wherever a $T$ is expected, a value of type $S$ may be placed instead.

This is the type-theoretic version of Liskov’s substitution principle. What, then, is the subtyping relation between function types?

Proposition 6.7（Variance of function types）

Subtyping of function types is given by

$$S_1 \to S_2 \le T_1 \to T_2 \quad\Longleftarrow\quad T_1 \le S_1 \ \text{and}\ S_2 \le T_2$$

That is, the argument position is contravariant (the direction is reversed) and the result position is covariant (the direction is preserved).

Proof（Proposition 6.7）

Let $f$ be a function of type $S_1 \to S_2$ and suppose we use it where a $T_1 \to T_2$ is expected. What Definition 6.6 demands is that no type error arise from that use.

For the argument: the caller believes it holds a $T_1 \to T_2$ and so passes arbitrary values of type $T_1$. Since $f$ can accept only values of type $S_1$, every value of type $T_1$ must pass as a value of type $S_1$. That is precisely $T_1 \le S_1$.

For the result: $f$ returns a value of type $S_2$, and the caller treats it as a $T_2$, so every value of type $S_2$ must pass as a value of type $T_2$. That is $S_2 \le T_2$.

Hence, under these two conditions, the use of $f$ causes no type error.

∎

Example 6.8（Covariance breaks things: Java arrays）

Java makes arrays covariant: if String is a subtype of Object, then String[] is treated as a subtype of Object[]. In the terms of Proposition 6.7, writing into an array occupies an argument position (an operation that receives an Object), so soundness requires contravariance. As a result of choosing covariance, the following code compiles.

String[] names = new String[1];
Object[] objs = names;          // permitted, since arrays are covariant
objs[0] = Integer.valueOf(42);  // at compile time this is an Object[], so it passes

At run time, however, the third line throws ArrayStoreException. This is a state in which type soundness in the sense of Corollary 5.5 is broken, and Java plugs the hole by adding a dynamic check of the array’s element type at run time. Generics (List<String> versus List<Object>) are designed to be invariant precisely so as not to repeat the same mistake.

6.3. Which one is “right”?

The two optimize different faces of the same problem. Consider a two-dimensional table whose axes are “kinds of shape” and “operations on shapes”: the directions of extension are orthogonal.

	New data (add a triangle)	New operation (add perimeter)
Functional (algebraic data types + pattern matching)	A branch must be added to every existing function	It suffices to add one new function
Object-oriented (classes + dynamic dispatch)	It suffices to add one new class	A method must be added to every existing class

This is what Wadler calls the expression problem. The direction that is easy for one is the painful direction for the other. Recent languages (Scala, Rust, Swift, Kotlin) provide both algebraic data types and traits or protocols so that one can choose whichever side is easier to extend, according to the nature of the subject. It is best to regard a paradigm not as a creed but as a design decision about which axis of extension to favour.

7. Exercises

Exercise 7.1Easy

Reduce the term $\mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0}))$ of the language L to a normal form, naming the rules of Definition 4.1 used at each step. Verify also that this term is typable by Definition 5.1.

Solution

The outermost term has the form $\mathtt{pred}\ u$ with $u = \mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})$. Since $u$ is $\mathtt{succ}\ nv$ with $nv = \mathtt{succ}\ \mathtt{0}$ a numeric value, E-PredSucc applies.

$$\mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})) \to \mathtt{succ}\ \mathtt{0} \qquad (\text{E-PredSucc},\ nv = \mathtt{succ}\ \mathtt{0})$$

Since $\mathtt{succ}\ \mathtt{0}$ is a numeric value it is a value, and by Lemma 4.3 (1) it cannot be reduced further. A normal form is reached in one step. Trying E-Pred first is impossible, because its premise $u \to u'$ fails by the same lemma.

As for typing: T-Zero gives $\vdash \mathtt{0} : \mathtt{Nat}$, two applications of T-Succ give $\vdash \mathtt{succ}\ (\mathtt{succ}\ \mathtt{0}) : \mathtt{Nat}$, and finally T-Pred gives $\vdash \mathtt{pred}\ (\mathtt{succ}\ (\mathtt{succ}\ \mathtt{0})) : \mathtt{Nat}$. Just as Theorem 5.4 asserts, the reduct $\mathtt{succ}\ \mathtt{0}$ also has type $\mathtt{Nat}$, by T-Zero and T-Succ.

Exercise 7.2Standard

Exhibit a term of the language L that is not typable and yet reduces to a value (does not get stuck), and verify both facts. Explain also why this phenomenon does not contradict Corollary 5.5.

Solution

Take $t = \mathtt{if}\ (\mathtt{iszero}\ \mathtt{0})\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$.

It is not typable. The only rule that could give $t$ a type is T-If, and its premises demand $\vdash \mathtt{0} : T$ and $\vdash \mathtt{false} : T$ for the same $T$. The only rule typing $\mathtt{0}$ is T-Zero, so $T = \mathtt{Nat}$; the only rule typing $\mathtt{false}$ is T-False, so $T = \mathtt{Bool}$. Since $\mathtt{Nat} \ne \mathtt{Bool}$ these are incompatible, and $t$ has no type.

It reaches a value. Deriving the premise of E-If by E-IszeroZero gives $t \to \mathtt{if}\ \mathtt{true}\ \mathtt{then}\ \mathtt{0}\ \mathtt{else}\ \mathtt{false}$, and then E-IfTrue gives $\to \mathtt{0}$. And $\mathtt{0}$ is a value.

Why there is no contradiction. Corollary 5.5 is the one-way implication “typable $\Rightarrow$ not stuck”; it does not assert the converse “not stuck $\Rightarrow$ typable”. And as Theorem 5.6 shows, no decidable type system for which the converse holds exists at all (for a Turing-complete language). The $\mathtt{false}$ branch is never executed, but the type checker judges on the conservative assumption that either branch may be executed.

Exercise 7.3Standard

Write out in full the case $t = \mathtt{iszero}\ t_1$ in the proof of Theorem 4.4, making explicit where Lemma 4.3 is used.

Solution

We split into cases on the shape of $t_1$.

(a) $t_1 = \mathtt{0}$. The candidate rules are E-IszeroZero and E-Iszero. Using E-Iszero would require the premise $\mathtt{0} \to t_1'$, but $\mathtt{0}$ is a numeric value, so by Lemma 4.3 (1) the premise fails. Hence only E-IszeroZero applies and $t' = t'' = \mathtt{true}$.

(b) $t_1 = \mathtt{succ}\ nv$ with $nv$ a numeric value. Here $t_1$ is itself a numeric value, so again by Lemma 4.3 (1) the premise of E-Iszero fails. Only E-IszeroSucc applies and $t' = t'' = \mathtt{false}$.

(c) $t_1 = \mathtt{succ}\ u$ with $u$ not a numeric value. E-IszeroSucc requires the $nv$ on its right-hand side to be a numeric value, so it does not match; E-IszeroZero does not match either. Hence both reductions are by E-Iszero, with premises $t_1 \to s$ and $t_1 \to s'$ respectively. By the induction hypothesis $s = s'$, and therefore $t' = \mathtt{iszero}\ s = \mathtt{iszero}\ s' = t''$.

(d) $t_1$ of none of the above shapes ($\mathtt{true}$, $\mathtt{false}$, or a term beginning with $\mathtt{if}$ or $\mathtt{pred}$). Neither E-IszeroZero nor E-IszeroSucc matches, so both reductions are by E-Iszero and the argument of (c) gives $t' = t''$. Note that when $t_1$ is $\mathtt{true}$ or $\mathtt{false}$ the premise of E-Iszero also fails, by Lemma 4.3 (2), so $t$ cannot be reduced at all and the case does not arise under the hypothesis $t \to t'$.

Exercise 7.4Hard

Suppose the subtyping rule for function types were declared covariant in the argument as well: $S_1 \to S_2 \le T_1 \to T_2$ whenever $S_1 \le T_1$ and $S_2 \le T_2$. Assuming that the types Cat and Dog are both subtypes of Animal, construct a program that passes the type checker under this rule but breaks at run time.

Solution

Let $g$ be the function “take a cat and make it do something a cat does”: $g : \mathtt{Cat} \to \mathtt{Unit}$, whose body invokes an operation available only on Cat (say “sharpen its claws”).

Under the hypothetical covariant rule, $\mathtt{Cat} \le \mathtt{Animal}$ and $\mathtt{Unit} \le \mathtt{Unit}$ yield

$$\mathtt{Cat} \to \mathtt{Unit} \ \le\ \mathtt{Animal} \to \mathtt{Unit}$$

So by the subsumption rule of Definition 6.6, $g$ may be used as a value of type $\mathtt{Animal} \to \mathtt{Unit}$.

Now pass $g$ to a higher-order function $h$ that takes an $\mathtt{Animal} \to \mathtt{Unit}$ as its argument, and inside $h$ apply it to a value of type $\mathtt{Dog}$. Since $\mathtt{Dog} \le \mathtt{Animal}$, this application passes the type checker. At run time, however, the body of $g$ demands “sharpen its claws” of the value it was given, and Dog has no such operation, so it breaks. A term was well typed and yet got stuck, so type soundness in the sense of Corollary 5.5 is lost.

Under the correct rule Proposition 6.7, deriving $\mathtt{Cat} \to \mathtt{Unit} \le \mathtt{Animal} \to \mathtt{Unit}$ would require $\mathtt{Animal} \le \mathtt{Cat}$, which does not hold, so the very first step is blocked. The Java arrays of Example 6.8 are a real instance of exactly this violation of contravariance.

References

• Benjamin C. Pierce, Types and Programming Languages, MIT Press, 2002 — Chapter 3 (semantics of arithmetic expressions), Chapter 8 (typed arithmetic expressions, progress and preservation), Chapter 15 (subtyping). The language L and the skeleton of the theorems in this article follow this book’s development.
• Robert Harper, Practical Foundations for Programming Languages, 2nd ed., Cambridge University Press, 2016 — a general treatment of structural operational semantics and type safety.
• A. Wright and M. Felleisen, “A Syntactic Approach to Type Soundness”, Information and Computation 115 (1994), 38–94 — the formulation of type soundness proofs via progress and preservation.
• H. P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed., North-Holland, 1984 — Chapter 3 contains a complete proof of the Church–Rosser theorem.
• A. V. Aho, M. S. Lam, R. Sethi, J. D. Ullman, Compilers: Principles, Techniques, and Tools, 2nd ed., Addison-Wesley, 2006 — the standard textbook from lexical analysis through optimization and code generation.
• B. H. Liskov and J. M. Wing, “A Behavioral Notion of Subtyping”, ACM Transactions on Programming Languages and Systems 16(6) (1994), 1811–1841 — a rigorous formulation of the substitution principle.
• RISC-V International, The RISC-V Instruction Set Manual, Volume I: Unprivileged ISA — https://riscv.org/technical/specifications/ the primary source for instruction formats and encodings.