Type Safety in Three Easy Lemmas

Last year I wrote a blog post showing how proofs of type safety can be done with just five easy lemmas if one defines the programming language in a certain way, using a special abstract machine. In this blog post I'll improve on that post in two ways. I'll show that type safety can be proved with just three easy lemmas and I'll use a standard interpreter-based definition of the language instead of a special abstract machine.
For readers interested in mechanized metatheory, here's the mechanized version of this post in Isabelle.

Syntax

This time we do not need to put the language in A-normal form. To review, we study a simple but Turing-complete language with integers, Booleans, and first-class functions that may be recursive. $$\begin{array}{lrcl} \text{types} & T & ::= & \mathtt{Int} \mid \mathtt{Bool} \mid T \to T \\ \text{variables} & x,y,z \\ \text{integers} & n \\ \text{operators}&o & ::= & + \mid - \mid \,=\, \\ \text{Booleans}&b & ::= & \mathtt{true} \mid \mathtt{false}\\ \text{constants}&c & ::= & n \mid b \\ \text{expressions} & e & ::= & c \mid o(e,e) \mid x \mid \mathtt{fun}\,f(x{:}T)\, e \mid e(e) \end{array}$$

Dynamic Semantics

As before, 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, written $\Gamma$) and variables to values (environments, written $\rho$). The following lookup function finds the thing associated with a given key in an association list. The return type of $\mathit{lookup}$ and the use of $\mathit{stuck}$ and $\mathit{return}$ deserves a little explanation, which I give below. $$\begin{align*} \mathit{lookup} & : \alpha \times (\alpha \times \beta) \, \mathit{list}\to \beta \, \mathit{result}\\ \mathit{lookup}(K_1, \epsilon ) &= \mathit{stuck} \\ \mathit{lookup}(K_1, (K_2,V) \cdot L ) &= \begin{cases} \mathit{return}\,V & \text{if } K_1 = K_2 \\ \mathit{lookup}(K_1,L) & \text{otherwise} \end{cases} \end{align*}$$ One might normally consider $\mathit{lookup}$ as a partial function, because it might fail to find a matching key in the association list. However, here we're going to make the partiality explicit by returning a special result called $\mathit{stuck}$. We'll also include $\mathit{timeout}$ in the kinds of results, which we explain shortly. $$\mathit{datatype}\;\;\alpha\,\mathit{result} = \mathit{Result}\,\alpha \mid \mathit{Stuck} \mid \mathit{TimeOut}$$ We define the following auxiliary notation for dealing with the $\mathit{result}$ datatype. The most import definition is the last line, which helps us avoid cluttering our code with lots of $\mathit{case}$'s. $$\begin{align*} \mathit{return}\,a &\equiv \mathit{Result}\;a \\ \mathit{stuck} &\equiv \mathit{Stuck} \\ \mathit{timeout} &\equiv \mathit{TimeOut} \\ X \gets M_1;\; M_2 &\equiv \mathit{case}\,M_1\,\mathit{of} \\ & \qquad \mathit{Stuck} \Rightarrow \mathit{Stuck} \\ & \quad\; \mid \mathit{TimeOut} \Rightarrow \mathit{TimeOut} \\ & \quad\; \mid \mathit{Result}\, R \Rightarrow [X := R]M_2 \end{align*}$$ The values of this language (the results of evaluation) are constants and closures. A closure pairs a function with an environment $\rho$. $$\begin{array}{lrcl} \text{values}& v & ::= & c \mid \langle f(x{:}T)\, e, \rho \rangle \end{array}$$ In many places within the interpreter we're going to extract an integer, Boolean, or closure from a value. The extraction might fail because, for example, even though we may want to extract an integer the value may instead be a Boolean. $$\begin{align*} \mathit{toInt}(n) &= \mathit{return}\,n \\ \mathit{toInt}(b) &= \mathit{stuck} \\ \mathit{toInt}(\langle f(x{:}T)\, e, \rho \rangle ) &= \mathit{stuck} \\ \\ \mathit{toBool}(n) &= \mathit{stuck} \\ \mathit{toBool}(b) &= \mathit{return}\,b \\ \mathit{toBool}(\langle f(x{:}T)\, e, \rho \rangle ) &= \mathit{stuck} \\ \\ \mathit{toClosure}(n) &= \mathit{stuck} \\ \mathit{toClosure}(b) &= \mathit{stuck} \\ \mathit{toClosure}(\langle f(x{:}T)\, e, \rho \rangle ) &= \mathit{return}\,(f,x,e,\rho) \end{align*}$$ Next we define the $\delta$ function, which gives meaning to the primitive operators. $$\begin{align*} \delta(+, v_1, v_2) &= n_1 \gets \mathit{toInt}(v_1);\; n_2 \gets \mathit{toInt}(v_2);\; \mathit{return}\; (n_1 + n_2) \\ \delta(-, v_1, v_2) &= n_1 \gets \mathit{toInt}(v_1);\; n_2 \gets \mathit{toInt}(v_2); \; \mathit{return}\,(n_1 - n_2) \\ \delta(=, n_1, n_2) &= n_1 \gets \mathit{toInt}(v_1);\; n_2 \gets \mathit{toInt}(v_2);\; \mathit{return}\; (n_1 = n_2) \end{align*}$$ The evaluation function $\mathcal{V}$ is a mostly-standard closure-based interpreter. The one thing that is a bit unusual is that we make sure that the interpreter is a total function by ensuring termination. The interpreter includes a third parameter that is a counter. If the counter gets to zero, the result is $\mathit{timeout}$. (This counter technique was described in the earlier blog post.) $$\begin{align*} \mathcal{V}(e,\rho,0) &= \mathit{timeout} \\ \mathcal{V}(x,\rho,1+k) &= \mathit{lookup}(x,\rho) \\ \mathcal{V}(c,\rho,1+k) &= \mathit{return}\,c \\ \mathcal{V}(\mathtt{fun}\,f(x{:}T)\, e, \rho, 1+k) &= \mathit{return}\,\langle f (x{:}T)\,e,\rho\rangle \\ \mathcal{V}(o(e_1,e_2),\rho,1+k) &= v_1 \gets \mathcal{V}(e_1,\rho,k);\; v_2 \gets \mathcal{V}(e_2,\rho,k); \; \delta(o, v_1, v_2) \\ \mathcal{V}(e_1\,e_2,\rho,1+k) &= v_1 \gets \mathcal{V}(e_1,\rho,k); \; v_2 \gets \mathcal{V}(e_2,\rho,k); \\ & \quad\; (f,x,e,\rho') \gets \mathit{toClosure}(v_1); \\ & \quad\; \mathcal{V}(e, (x,v_2) \cdot (f,v_1) \cdot \rho', k) \end{align*}$$ To finish off the dynamic semantics we must define $\mathit{eval}$ which specifies the behavior of whole programs. The behavior of a program is to either return a constant, return $\mathit{diverge}$ which indicates that the program runs forever, or the behavior is undefined. $$\mathit{eval}(e) = \begin{cases} c & \text{if } \mathcal{V}(e,\epsilon,n) = \mathit{Result}\;c \text{ for some } n \\ \mathit{diverge} & \text{if } \forall n.\; \mathcal{V}(e,\epsilon,n) = \mathit{TimeOut} \end{cases}$$

Type System

The types for the constants is given by the $\mathit{typeof}$ partial function. $$\begin{align*} \mathit{typeof}(n) &= \mathsf{Int} \\ \mathit{typeof}(\mathsf{true}) &= \mathsf{Bool} \\ \mathit{typeof}(\mathsf{false}) &= \mathsf{Bool} \end{align*}$$ The $\Delta$ partial 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}) &= \mathsf{Int} \\ \Delta(=,\mathsf{Int},\mathsf{Int}) &= \mathsf{Bool} \end{align*}$$ The following presents the type rules for expressions.
$\Gamma \vdash e : T$
$$\begin{gather*} \frac{\mathit{lookup}(x,\Gamma) = \mathit{Result}\;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 e : T_2 }{ \Gamma \vdash \mathtt{fun}\,f(x{:}T_1)e : 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 e_1(e_2) : T_2 } \qquad \frac{ \begin{array}{c} \Delta(o,T_1,T_2) = T_3 \\ \Gamma \vdash e_1 : T_1 \quad \Gamma \vdash e_2 : T_2 \end{array} }{ \Gamma \vdash o(e_1,e_2) : T_3 } \end{gather*}$$ Our proof of type safety will require that we define notions of well-typed values, results, and environments.
$\vdash v : T$ $$\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 e : T_2 }{ \vdash \langle f(x{:}T_1)e , \rho \rangle : T_1 \to T_2 } \end{gather*}$$ $\vdash r : T$ $$\begin{gather*} \frac{\vdash v : T}{\vdash \mathit{Result}\,v : T} \quad \frac{}{\vdash \mathit{TimeOut} : T} \end{gather*}$$ $\Gamma \vdash \rho$ $$\begin{gather*} \frac{}{\epsilon \vdash \epsilon} \qquad \frac{ \vdash v : T \quad \Gamma \vdash \rho }{ (x,T) \cdot \Gamma \vdash (x,v) \cdot \rho } \end{gather*}$$

Type Safety

The proof of type safety, as promised, includes just three easy lemmas. The first two lemmas are essentially identical to the corresponding lemmas in ``Type Safety in Five''. They establish that the primitive operators and lookup on environments are sound with respect to $\Delta$ and lookup on type environments, respectively. The third lemma is the main event of the proof, showing that $\mathcal{V}$ is sound with respect to the type system. Because we know that $\mathcal{V}$ terminates, we can do the proof by induction on the definition of $\mathcal{V}$, which helps to streamline the proof. We cap off the proof with the Type Safety theorem, which follows almost immediately from the soundness of $\mathcal{V}$.
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}) = \mathit{Result}\;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) = \mathit{Result}\, (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=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) = \mathit{Result}\, (n_1 - n_2)$ and we have $\vdash (n_1 - n_2) : \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) = \mathit{Result}\;(n_1 = n_2)$ and we have $\vdash (n_1 = n_2) : \mathsf{Bool}$.

QED.
Lemma ($\mathit{lookup}$ is safe)
If $\Gamma \vdash \rho$ and $\mathit{lookup}(x,\Gamma) = \mathit{Result}\;T$, then $\mathit{lookup}(x,\rho) = \mathit{Result}\;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) = \mathit{Result}\;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) = \mathit{Result}\;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') = \mathit{Result}\;T$. By the induction hypothesis, we have $\mathit{lookup}(x,\rho') = \mathit{Result}\;v$ and $\vdash v : T$ for some $v$, which completes this case.

QED.
Lemma ($\mathcal{V}$ is safe)
If $\Gamma \vdash e : T$ and $\Gamma \vdash \rho$, then $\vdash \mathcal{V}(e,\rho,k) : T$.
Proof. The proof is by induction on the definition of $\mathcal{V}$.

1. Case $\mathcal{V}(e,\rho,0)$: We have $\mathcal{V}(e,\rho,0) = \mathit{TimeOut}$ and $\vdash \mathit{TimeOut} : T$.
2. Case $\mathcal{V}(x,\rho,1+k)$: We have $\mathcal{V}(x,\rho,1+k) = \mathit{lookup}(x,\rho)$. From $\Gamma \vdash x : T$ we have $\mathit{lookup}(x,\Gamma) = \mathit{Result}\; T$. Then by the $\mathit{lookup}$ is safe lemma, we have $\mathit{lookup}(x,\rho) = \mathit{Result}\;v$ and $\vdash v : T$ for some $v$. Thus we have $\vdash \mathit{lookup}(x,\rho) : T$ and conclude $\vdash \mathcal{V}(x,\rho,1+k) : T$.
3. Case $\mathcal{V}(c,\rho,1+k)$: From $\Gamma \vdash c : T$ we have $\mathit{typeof}(c) = T$ and therefore $\vdash c : T$. We have $\mathcal{V}(c,\rho) = \mathit{Result}\;c$ and therefore $\vdash \mathcal{V}(c,\rho,1+k) : T$.
4. Case $\mathcal{V}(\mathtt{fun}\,f(x{:}T_1) e_1, \rho,1+k)$:
   We have $\mathcal{V}(\mathtt{fun}\,f(x{:}T_1) e_1,\rho,1+k) = \mathit{Result}\;\langle f(x{:}T_1) e_1, \rho \rangle$. From $\Gamma \vdash \mathtt{fun}\,f(x{:}T_1) e_1 : T$ we have $(x,T_1) \cdot (f,T_1 \to T_2) \cdot \Gamma \vdash e_1 : T_2$, with $T = T_1 \to T_2$. Together with $\Gamma \vdash \rho$, we have $\vdash \langle f(x{:}T_1) e_1, \rho \rangle : T$ and therefore $\vdash \mathcal{V}(\mathtt{fun}\,f(x{:}T_1) e_1, \rho,1+k) : T$.
5. Case $\mathcal{V}(o(e_1,e_2), \rho, 1+k))$:
   We have $\Delta(o,T_1,T_2) = T$ and $\Gamma \vdash e_1 : T_1$ and $\Gamma \vdash e_2 : T_2$. By the induction hypothesis, we have $\mathcal{V}(e_1,\rho,k) = \mathit{Result}\;v_1$ and $\vdash v_1 : T_1$ and $\mathcal{V}(e_2,\rho,k) = \mathit{Result}\;v_2$ and $\vdash v_2 : T_2$. Because $\delta$ is safe, we have $\delta(o,v_1,v_2) = \mathit{Result}\;v_3$ and $\vdash v_3 : T$ for some $v_3$. We have $\vdash \delta(o,v_1,v_2) : T$ and therefore $\vdash \mathcal{V}(o(e_1,e_2), \rho, 1+k)) : T$.
6. Case $\mathcal{V}(e_1\,e_2, \rho, 1+k)$: We have $\Gamma \vdash e_1 : T_2 \to T$ and $\Gamma \vdash e_2 : T_2$. By the induction hypothesis, we have $\mathcal{V}(e_1,\rho,k) = \mathit{Result}\;v_1$ and $\vdash v_1 : T_2 \to T$ and $\mathcal{V}(e_2,\rho,k) = \mathit{Result}\;v_2$ and $\vdash v_2 : T_2$. By cases on $\vdash v_1 : T_2 \to T$, we have that $v_1 = \langle f(x{:}T_2)e_3, \rho' \rangle$ and $\Gamma' \vdash \rho'$ and $(x,T_2) \cdot (f,T_2 \to T) \cdot \Gamma' \vdash e_3 : T$ for some $f,x,e_3,\Gamma',\rho'$. So we have $\mathcal{V}(e_1\,e_2, \rho, 1+k) = \mathcal{V}(e_3,(x,v_2) \cdot (f,v_1) \cdot \rho',k)$. Applying the induction hypothesis for a third time, we have $\vdash \mathcal{V}(e_3,(x,v_2) \cdot (f,v_1) \cdot \rho',k) : T$. Therefore $\vdash \mathcal{V}(e_1\,e_2, \rho, 1+k) : T$.

QED.
Theorem (Type Safety)
If $\epsilon \vdash e : T$ and $T \in \{ \mathtt{Int}, \mathtt{Bool}\}$, then either $\mathit{eval}(e) = c$ and $\vdash c : T$ for some $c$ or $\mathit{eval}(e) = \mathit{diverge}$ .
Proof. We consider two cases: whether the program diverges or not.

1. Suppose that $\mathcal{V}(e,\epsilon,k) = \mathit{TimeOut}$ for all $k$. Then $\mathit{eval}(e) = \mathit{diverge}$.
2. Suppose it is not the case that $\mathcal{V}(e,\epsilon,k) = \mathit{TimeOut}$ for all $k$. So $\mathcal{V}(e,\epsilon,k') \neq \mathit{TimeOut}$ for some $k'$. Then because $\mathcal{V}$ is safe, we have $\mathcal{V}(e,\epsilon,k') = \mathit{Result}\,v$ and $\vdash v : T$. Then from $T \in \{ \mathtt{Int}, \mathtt{Bool} \}$ and by cases on $\vdash v : T$, we have $v = c$ for some $c$.

QED.