Type Safety in Five Easy Lemmas

A language is type safe if running a program in the language cannot result in an untrapped error. A trapped error is something like an exception or a message-not-found error, that is, it's an error that is part of the defined behavior of the language. An untrapped error is something like a segmentation fault, that is, the program has run into an undefined state in which the language doesn't define what should happen. A segmentation fault is the underlying operating system catching the error, not the language itself. It is the untrapped errors that hackers take advantage of to break into computer systems. If you want to run untrusted code without getting into trouble, then it's a good idea to only run code that is in a type safe language!

Wright and Felleisen pioneered what has become the most flexible approach to proving that a language is type safe in their 1992 paper A Syntactic Approach to Type Soundness. The general idea is to define a small-step operational semantics for the language and show that if a program is well typed, then it is either done reducing or it can reduce to another well-typed program. The safety of an entire sequence of reductions can then be proved by induction. It is now common practice for language designers to prove type safety for new language designs, or at least for interesting subsets of the languages of interest. Proving type safety does not require advanced mathematics and isn't particularly challenging, except that it is often rather tedious, requiring many technical lemmas in which it is easy to make a mistake.

It turns out that the choice in formulation of the operational semantics can make a significant difference regarding how many lemmas, and how tedious, the proof of type safety becomes. In this blog post, I present an operational semantics that removes the need for many of the standard lemmas. The semantics is based on an abstract machine. The language will be the simply-typed lambda calculus in A-normal form, extended with recursive functions and a few primitive operators. Despite its small size, this language is Turing complete. This language is roughly equivalent to the target language discussed in my previous posts about Structural Induction and the ECD Machine. In the following I present the syntax, operational semantics, and type system of this language. Then I give the proof of type safety. The proof will rely on five lemmas, one lemma for each function or relation used in the operational semantics: the variable $\mathit{lookup}$ partial function, the $\delta$ partial function that defines the behavior of the primitive operators, the $\mathcal{V}$ partial function for evaluating expression, the transition relation $\longmapsto$ for the abstract machine, and the multi-transition relation $\longmapsto^{*}$. The lemma for the transition relation is the main event.

Syntax

$$\begin{array}{lrcl} \text{types} & T & ::= & \mathsf{Int} \mid \mathsf{Bool} \mid T \to T \\ \text{variables} & x,y,z \\ \text{integers} & n \\ \text{operators}&o & ::= & + \mid - \mid \;= \\ \text{constants}&c & ::= & n \mid \mathsf{true} \mid \mathsf{false} \\ \text{expressions} & e & ::= & c \mid x \mid \mathsf{fun}\,f(x{:}T) s\\ \text{definitions} & d & ::= & x = e(e) \mid x = o(\overline{e}) \\ \text{statements} & s & ::= & d; s \mid \mathbf{return}\,e \end{array}$$

Operational Semantics

We use the notation $\epsilon$ for the empty list. Given a list $L$, the notation $a \cdot L$ is a larger list with $a$ as the first element and the rest of the elements are the same as $L$. We use lists of key-value pairs (association lists) to represent mapping from variables to types (type environments) and variables to values (environments). The following lookup (partial) function finds the thing associated with a given key in an association list. $$\begin{align*} \mathit{lookup}(K_1, (K_2,V) \cdot L ) &= \begin{cases} V & \text{if } K_1 = K_2 \\ \mathit{lookup}(K_1,L) & \text{otherwise} \end{cases} \end{align*}$$ Next we define the $\delta$ function, which gives meaning to the primitive operators. $$\begin{align*} \delta(+, n_1, n_2) &= n_1 + n_2 \\ \delta(-, n) &= -n \\ \delta(=, n_1, n_2) &= (n_1 = n_2) \end{align*}$$ The function $\mathcal{V}$ maps expressions to values, using environment $\rho$. The values of this language are constants and closures, as defined below. $$\begin{array}{lrcl} \text{values}& v & ::= & c \mid \langle f(x{:}T) s, \rho \rangle \end{array}$$ The definition of $\mathcal{V}$ uses the $\mathit{lookup}$ function for variables, the $\delta$ function for primitive operations, and turns functions to closures. $$\begin{align*} \mathcal{V}(c, \rho) &= c \\ \mathcal{V}(x,\rho) &= \mathit{lookup}(x,\rho) \\ % \mathcal{V}(o(e)) &= \delta(o, \mathcal{V}(e,\rho)) \\ \mathcal{V}(\mathsf{fun}\,f(x{:}T)s, \rho) &= \langle \mathsf{fun}\,f(x{:}T)s, \rho \rangle \end{align*}$$ A stack $\kappa$ is a list of statement-environment pairs. The state $\sigma$ of the machine is simply a stack. The top of the stack contains the actively-executing statement and its environment. The relation $\longmapsto$ defines transitions between states. There are only three transition rules, for primitive operators, calling functions, and returning from functions. $$\begin{align} & (x=o(\overline{e});s, \rho)\cdot \kappa \tag{Op}\\ \longmapsto \; & (s, (x,v) \cdot \rho) \cdot \kappa \notag \\ & \text{where } v = \delta(o, \overline{\mathcal{V}(e,\rho)}) \notag \\[2ex] & (x=e_1(e_2);s, \rho)\cdot \kappa \tag{Call}\\ \longmapsto \; & (s', (y,v_2) \cdot (f,v_1) \cdot \rho') \cdot (x=e_1(e_2);s, \rho) \cdot \kappa \notag \\ & \text{where } v_1 = \mathcal{V}(e_1,\rho) = \langle \mathsf{fun}\,f(y{:}T)s' , \rho' \rangle \notag \\ & \text{and } v_2 = \mathcal{V}(e_2,\rho) \notag \\ \\[2ex] & (\mathbf{return}\,e,\rho) \cdot (x=e_1(e_2)\;s,\rho') \cdot \kappa \tag{Return}\\ \longmapsto\;& (s, (x,v)\cdot\rho') \cdot \kappa \notag\\ & \text{where } v = \mathcal{V}(e,\rho) \notag \end{align}$$ We define $\longmapsto^{*}$ in the usual way, as follows. $$\begin{gather*} \sigma \longmapsto^{*} \sigma \qquad \frac{\sigma_1 \longmapsto \sigma_2 \quad \sigma_2 \longmapsto^{*} \sigma_3} {\sigma_1 \longmapsto^{*} \sigma_3} \end{gather*}$$ The semantics of this language is given by the following $\mathit{eval}$ function. A state is final if it is of the form $(\mathbf{return}\,e,\rho) \cdot \epsilon$ and $\mathcal{V}(e,\rho) = v$ for some $v$. $$\mathit{eval}(s) = \begin{cases} c & \text{if } (s,\epsilon) \cdot \epsilon \longmapsto^{*} (\mathbf{return}\,e,\rho) \cdot \epsilon \\ & \text{and } \mathcal{V}(e,\rho) = c \\ \mathtt{fun}& \text{if } (s,\epsilon) \cdot \epsilon \longmapsto^{*} (\mathbf{return}\,e,\rho) \cdot \epsilon \\ & \text{and } \mathcal{V}(e,\rho) = \langle \mathsf{fun}\,f(x{:}T)s,\rho'\rangle \\ \mathtt{stuck} & \text{if } (s,\epsilon) \cdot \epsilon \longmapsto^{*} \sigma, \sigma \text{ is not final, and } \not \exists \sigma'. \sigma \longmapsto \sigma'\\ \bot & \text{if } \forall \sigma.\, (s,\epsilon) \cdot \epsilon \longmapsto^{*} \sigma \text{ implies } \exists \sigma'.\, \sigma \longmapsto \sigma' \end{cases}$$

Type System

The types for the constants is given by the $\mathit{typeof}$ function. $$\begin{align*} \mathit{typeof}(n) &= \mathsf{Int} \\ \mathit{typeof}(\mathsf{true}) &= \mathsf{Bool} \\ \mathit{typeof}(\mathsf{false}) &= \mathsf{Bool} \end{align*}$$ The $\Delta$ function maps a primitive operator and argument types to the return type. $$\begin{align*} \Delta(+,\mathsf{Int}\,\mathsf{Int}) &= \mathsf{Int} \\ \Delta(-, \mathsf{Int}) &= \mathsf{Int} \\ \Delta(=,\mathsf{Int}\,\mathsf{Int}) &= \mathsf{Bool} \end{align*}$$ The following presents the type rules for expressions, definitions, and statements. $$\begin{gather*} \frac{\mathit{lookup}(x,\Gamma) = T}{\Gamma \vdash x : T} \qquad \frac{\mathit{typeof}(c) = T}{\Gamma \vdash c : T} \\[2ex] \frac{ (x,T_1) \cdot (f,T_1 \to T_2) \cdot \Gamma \vdash s : T_2 }{ \Gamma \vdash \mathsf{fun}\,f(x{:}T_1)s : T_1 \to T_2 } \\[2ex] \frac{ \Gamma \vdash e_1 : T_1 \to T_2 \quad \Gamma \vdash e_2 : T_1 }{ \Gamma \vdash x=e_1(e_2) : (x,T_2) } \\[2ex] \frac{ \begin{array}{c} \Delta(o,\overline{T}) = T \\ \Gamma \vdash e_i : T_i \text{ for } i \in \{ 1,\ldots,n\} \end{array} }{ \Gamma \vdash x = o(\overline{e}) : (x,T) } \\[2ex] \frac{ \begin{array}{c} \Gamma \vdash d : (x,T_1) \\ (x,T_1) \cdot \Gamma \vdash s : T_2 \end{array} }{ \Gamma \vdash d; s : T_2 } \qquad \frac{\Gamma \vdash e : T}{\Gamma \vdash \mathbf{return}\,e : T} \end{gather*}$$ Our proof of type safety will require that we define notions of well-typed values, well-typed environments, well-typed stacks, and well-typed states. $$\begin{gather*} \frac{\mathit{typeof}(c) = T}{\vdash c : T} \quad \frac{ \Gamma \vdash \rho \quad (x{:}T_1) \cdot (f{:}T_1\to T_2) \cdot \Gamma \vdash s : T_2 }{ \vdash \langle \mathsf{fun}\,f(x{:}T_1)s , \rho \rangle : T_1 \to T_2 } \\[2ex] \frac{}{\epsilon \vdash \epsilon} \qquad \frac{ \vdash v : T \quad \Gamma \vdash \rho }{ (x,T) \cdot \Gamma \vdash (x,v) \cdot \rho } \\[2ex] \frac{}{\vdash \epsilon : T \Rightarrow T} \qquad \frac{ \Gamma \vdash \rho \quad (x,T_1) \cdot \Gamma \vdash s : T_2 \quad \vdash \kappa : T_2 \Rightarrow T_3 }{ \vdash (x=e_1(e_2); s,\rho) \cdot \kappa : T_1 \Rightarrow T_3 } \\[2ex] \frac{ \Gamma \vdash \rho \quad \Gamma \vdash s : T_1 \quad \vdash \kappa : T_1 \Rightarrow T_2 }{ \vdash (s,\rho) \cdot \kappa : T_2 } \end{gather*}$$

Proof of Type Safety

The first lemma proves that when an operator is applied to values of the expected type, the result is a value whose type matches the return type of the operator.

Lemma ($\delta$ is safe)
If $\Delta(o,\overline{T}) = T$ and $\vdash v_i : T_i$ for $i \in \{1,\ldots,n\}$, then $\delta(o,\overline{v}) = v$ and $\vdash v : T$, for some $v$.

Proof. We proceed by cases on the operator $o$.

1. If the operator $o$ is $+$, then we have $T_1=T_2=\mathsf{Int}$ and $T=\mathsf{Int}$. Then because $\vdash v_i : \mathsf{Int}$, we know that $v_i = n_i$ for $i \in \{1,2\}$. Then $\delta(+,n_1,n_2) = n_1 + n_2$ and we have $\vdash (n_1 + n_2) : \mathsf{Int}$.
2. If the operator $o$ is $-$, then we have $T_1=\mathsf{Int}$ and $T=\mathsf{Int}$. Then because $\vdash v_1 : \mathsf{Int}$, we know that $v_1 = n$ for some $n$. Then $\delta(-,n) = -n$ and we have $\vdash -n : \mathsf{Int}$.
3. If the operator $o$ is $=$, then we have $T_1=T_2=\mathsf{Int}$ and $T=\mathsf{Bool}$. Then because $\vdash v_i : \mathsf{Int}$, we know that $v_i = n_i$ for $i \in \{1,2\}$. Then $\delta(=,n_1,n_2) = n_1 = n_2$ and we have $\vdash (n_1 = n_2) : \mathsf{Bool}$.

QED.

The second lemma says that if you have an environment that is well-typed with respect to the type environment, and if a variable x is associated with type T in the type environment, then looking up x in the environment produces a value that has type T.

Lemma ($\mathit{lookup}$ is safe)
If $\Gamma \vdash \rho$ and $\mathit{lookup}(x,\Gamma) = T$, then $\mathit{lookup}(x,\rho) = v$ and $\vdash v : T$ for some $v$.
Proof. We proceed by induction on $\Gamma \vdash \rho$.

1. Case $\epsilon \vdash \epsilon: \qquad (\Gamma=\epsilon, \rho = \epsilon)$
   But then we have a contradition with the premise $\mathit{lookup}(x,\Gamma) = T$, so this case is vacuously true.
2. Case $\begin{array}{c}\vdash v : T' \quad \Gamma' \vdash \rho' \\ \hline (x',T') \cdot \Gamma' \vdash (x',v) \cdot \rho' \end{array}$:
   Next we consider two cases, whether $x = x'$ or not.
   1. Case $x = x'$: Then $\mathit{lookup}(x, \rho) = v$ and $T = T'$, so we conclude that $\vdash v : T$.
   2. Case $x \neq x'$: Then $\mathit{lookup}(x,\rho) = \mathit{lookup}(x,\rho')$ and $\mathit{lookup}(x,\Gamma) = \mathit{lookup}(x,\Gamma') = T$. By the induction hypothesis, we have $\mathit{lookup}(x,\rho') = v$ and $\vdash v : T$ for some $v$, which completes this case.

QED.

The next lemma proves that a well-typed expression evaluates to a value of the expected type.

Lemma ($\mathcal{V}$ is safe)
If $\Gamma \vdash e : T$ and $\Gamma \vdash \rho$, then $\mathcal{V}(e,\rho) = v$ and $\vdash v : T$ for some $v$.
Proof. We proceed by cases on the expression $e$.

1. Case $e = c$:
   From $\Gamma \vdash c : T$ we have $\mathit{typeof}(c) = T$ and therefore $\vdash c : T$. Also, we have $\mathcal{V}(c,\rho) = c$, which completes this case.
2. Case $e = x$:
   From $\Gamma \vdash x : T$ we have $\mathit{lookup}(x,\Gamma) = T$. We then apply the lookup is safe lemma to obtain $\mathit{lookup}(x,\rho) = v$ and $\vdash v : T$ for some $v$. Thus, we have $\mathcal{V}(x,\rho) = v$ and this case is complete.
3. Case $e = \mathsf{fun}\,f(x{:}T_1) s$:
   We have $\mathcal{V}(\mathsf{fun}\,f(x{:}T_1) s,\rho) = \langle\mathsf{fun}\,f(x{:}T_1) s, \rho \rangle$. From $\Gamma \vdash \mathsf{fun}\,f(x{:}T_1) s : T$ we have $(x,T_1) \cdot (f,T_1 \to T_2) \cdot \Gamma \vdash s : T_2$, with $T = T_1 \to T_2$. Together with $\Gamma \vdash \rho$, we conclude that $\vdash \langle\mathsf{fun}\,f(x{:}T_1) s, \rho \rangle : T$.

QED.

Now for the fourth and most important lemma. This lemma states that if a state is well typed, then either the state is a final state or the state can transition to a new state of the same type. In the literature, this lemma is often split into two lemmas called progress and preservation. In the setting of an abstract machine, it's convenient to merge these two lemmas into one lemma. Note that the conclusion of this lemmas includes two alternatives: the state is final or it can take a step. The power of this lemma is that it rules out the third alternative, that the state is not final and can't take a step. Such a situation is referred to as "stuck" and corresponds to untrapped errors.

Lemma ($\longmapsto$ is safe)
If $\vdash \sigma : T$, then either $\sigma$ is a final state or $\sigma \longmapsto \sigma'$ and $\vdash \sigma' : T$.
Proof. Because $\vdash \sigma : T$ we know that $\sigma = (s,\rho) \cdot \kappa$, $\Gamma \vdash \rho$, $\Gamma \vdash s : T_1$, and $\vdash \kappa : T_1 \Rightarrow T$. We proceed by cases on $s$ because the transition rule that will apply depends primarily on $s$.

1. Case $s = (x = o(\overline{e}); s')$:
   We have $\Gamma \vdash x = o(\overline{e}) : (x,T_1)$ and $(x,T_1) \cdot \Gamma \vdash s' : T_1$. So $\Delta(o,\overline{T}') = T_1$ and $\Gamma \vdash e_i : T'_i$ for $i \in \{ 1,\ldots,n\}$. Because $\mathcal{V}$ is safe, we have $\mathcal{V}(e_i,\rho) = v_i$ and $\vdash v_i : T'_i$ for $i \in \{ 1,\ldots,n\}$. Because $\delta$ is safe, we have $\delta(o,\overline{v}) = v$ and $\vdash v : T_1$ for some $v$. Thus, the current state takes the following transition. $$(x = o(\overline{e}); s', \rho) \cdot \kappa \longmapsto (s', (x,v) \cdot \rho) \cdot \kappa$$ We have $(x,T_1) \cdot \Gamma \vdash (x,v) \cdot \rho$
   and therefore $\vdash (s', (x,v) \cdot \rho) \cdot \kappa : T$
2. Case $s = (x = e_1(e_2); s')$:
   From $\Gamma \vdash x = e_1(e_2); s': T_1$ we have $\Gamma \vdash x = e_1(e_2) : (x,T_2)$ and $(x,T_2) \cdot \Gamma \vdash s' : T_1$. Thus, we also have $\Gamma \vdash e_1 : T_3 \to T_2$ and $\Gamma \vdash e_2 : T_3$. Because $\mathcal{V}$ is safe, there exist $v_1$ and $v_2$ such that $\mathcal{V}(e_1,\rho) = v_1$, $\mathcal{V}(e_2,\rho) = v_2$, $\vdash v_1 : T_3 \to T_2$, and $\vdash v_2 : T_3$. The only way for $\vdash v_1 : T_3 \to T_2$ to be true is for $v_1$ to be a closure. That is, $v_1 = \langle \mathsf{fun}\,f(y{:}T_3) s'',\rho' \rangle$. This closure is well typed, so we have $\Gamma' \vdash \rho'$ and $(y:T_3) \cdot (f,T_3 \to T_2) \cdot \Gamma' \vdash s'' : T_2$. We have what we need to know that the current state $\sigma = (x = e_1(e_2); s', \rho) \cdot \kappa$ transitions as follows. $$\sigma \longmapsto (s'', (y,v_2) \cdot (f,v_1) \cdot \rho') \cdot \sigma$$ We can deduce $\vdash \sigma : T_2 \Rightarrow T$
   and $(y,T_3) \cdot (f,T_3\to T_2) \cdot \Gamma' \vdash (y,v_2)\cdot (f,v_1) \cdot \rho'$
   so we have everything necessary to conclude $$\vdash (s'', (y,v_2) \cdot (f,v_1) \cdot \rho') \cdot \sigma : T$$
3. Case $s = (\mathbf{return}\,e)$:
   If the stack $\kappa$ is empty, then $\sigma$ is a final state and this case is complete. If the stack is not empty, we have $\kappa = (s',\rho') \cdot \kappa'$. Then, because $\vdash \kappa : T_1 \Rightarrow T$, we have $s' = (x = e_1(e_2); s'')$, $\Gamma' \vdash \rho'$, $(x,T_1) \cdot \Gamma' \vdash s'' : T_2$, and $\vdash \kappa' : T_2 \Rightarrow T$. Because $\Gamma \vdash \mathbf{return}\,e : T_1$, we have $\Gamma \vdash e : T_1$ and therefore $\mathcal{V}(e,\rho) = v$ and $\vdash v : T_1$ for some $v$ (because $\mathcal{V}$ is safe). So the current state $\sigma$ takes the following transition: $$(\mathbf{return}\,e,\rho) \cdot (x = e_1(e_2); s'', \rho') \cdot \kappa' \longmapsto (s'', (x,v) \cdot \rho') \cdot \kappa'$$ We have $(x,T_1) \cdot \Gamma' \vdash (x,v) \cdot \rho'$, which is the last thing we needed to conclude that $\vdash (s'', (x,v) \cdot \rho') \cdot \kappa' : T$.

QED.

Lemma ($\longmapsto^{*}$ is safe)
If $\vdash \sigma : T$ and $\sigma \longmapsto^{*} \sigma'$, then $\vdash \sigma' : T$.
Proof. The proof is by induction on $\sigma \longmapsto^{*} \sigma'$.

1. Case $\sigma \longmapsto^{*} \sigma$: We already have $\vdash \sigma : T$.
2. Case $\begin{array}{c} \sigma \longmapsto \sigma_1 \quad \sigma_1 \longmapsto^{*} \sigma' \\\hline \sigma \longmapsto^{*} \sigma'\end{array}$: Because $\longmapsto$ is safe and deterministic (the three transition rules obviously do not overlap), we have $\vdash \sigma_1 : T$. Then by the induction hypothesis, we conclude that $\vdash \sigma' : T$.

QED.

Theorem (Type Safety)
If $\epsilon \vdash s : T$, then either

1. $\mathit{eval}(s) = c$ and $\vdash c : T$, or
2. $\mathit{eval}(s) = \mathtt{fun}$ and $T = T_1 \to T_2$ for some $T_1,T_2$, or
3. $\mathit{eval}(s) = \bot$ (the program does not terminate).

Proof. Suppose that the program terminates. We have $(s,\epsilon) \cdot \epsilon \longmapsto^{*} \sigma$ for some $\sigma$ and $\neg \exists \sigma'.\, \sigma \longmapsto \sigma'$. Because $\longmapsto^{*}$ is safe, we have $\vdash \sigma : T$. Then because $\longmapsto$ is safe, we know that either $\sigma$ is final or it can take a step. But we know it can't take a step, so it must be final. So $\sigma = (\mathbf{return}\,e, \rho) \cdot \epsilon$ and $\Gamma \vdash e : T$. Then because $\mathcal{V}$ is safe, we have $\mathcal{V}(e,\rho) = v$ and $\vdash v : T$. If $v = c$, then we have $\mathit{eval}(s) = c$ and $\vdash c : T$. If $v = \langle \mathsf{fun}\,f(x{:}T) s',\rho'\rangle$, then $T = T_1 \to T_2$, $\mathit{eval}(s) = \mathtt{fun}$, and $\vdash \mathtt{fun}: T_1 \to T_2$.
QED.

That's it! Type safety in just five easy lemmas.