# Programming Language Theory: From Machine Code to Type Systems and Paradigms > The layers of machine code, assembly and high-level languages, checked against the actual RISC-V encoding; progress and preservation proved over the operational semantics of a tiny language; and a comparison of static with dynamic typing and of functional with object-oriented design. > https://rikai.mugen-giken.com/en/computer-science/cs-basics/programming-language-theory ## 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 of [Computer architecture and the structure of the CPU](/en/computer-science/cs-basics/computer-architecture), 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 . 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. 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: ```text 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 ) 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. ```c int add1(int x) { return x + 1; } ``` Compiled for RISC-V with optimization, this becomes two instructions. ```text 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.

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`} /> ## 3. Compilers and interpreters 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 | 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. 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. 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. ```python 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 ``` (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'$. We prove (1) by induction on the structure of $nv$. When $nv = \mathtt{0}$, none of the rules of 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). For every term $t$ of the language L, if $t \to t'$ and $t \to t''$ then $t' = t''$. 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 (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 (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 (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 , 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 ). ## 5. Types: static and dynamic typing As we saw right after , L has terms that get stuck. A type system is a mechanism for excluding some of those terms **before execution**. 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. (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. (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. 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. 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 (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 (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 (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. If $\vdash t : T$ and $t \to t'$, then $\vdash t' : T$. That is, reduction does not change the type. 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. 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. We induct on $n$. Applying $n$ times yields $\vdash t_n : T$. Applying 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 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. 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$. 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}$. ```text 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.

### 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 | 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. 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$. 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 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. 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). 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. Suppose the first evaluation of $e$ returned the value $v$. By , 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.** In the following Python code, treating `f() + f()` as a "common subexpression" and collapsing it into a single call changes the result. ```python 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 that "evaluation does not alter the state" is violated, so the first step in the proof of (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. ```python 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](/en/computer-science/cs-basics/computer-architecture) works poorly, and this is what the cost of a virtual call really consists of (a misprediction forfeits the gain from pipelining; see ). 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? 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). 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 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. Java makes arrays covariant: if `String` is a subtype of `Object`, then `String[]` is treated as a subtype of `Object[]`. In the terms of , 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. ```java 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 is broken, and Java plugs the hole by adding a dynamic check of the array's element type at run time. Generics (`List` versus `List