Interpretations of the GTLC, Part 4: Even Faster

Consider the following statically-typed function. (The type \(\star\) does not occur anywhere in this function.) \[ \lambda f: \mathsf{Int}{\to}\mathsf{Int}. \; x{:}\mathsf{Int} = f(42); \mathbf{return}\,x \] We'd like the execution speed of this function to be the same as if the entire language were statically typed. That is, we don't want statically-typed parts of a gradually-typed program to pay overhead because other parts may be dynamically typed. Unfortunately, in the abstract machines that we've defined so far, there is an overhead. At the point of a function call, such as \(f(42)\) above, the machine needs to check whether \(f\) has evaluated to a closure or to a closure wrapped in a threesome. This act of checking constitutes some run-time overhead.

Taking a step back, there are two approaches that one sees in the literature regarding how a cast is applied to a function. One approach is to build a new function that casts the argument, applies the old function, and then casts the result. The reduction rule looks like this: \[ v : T_1 \to T_2 \Rightarrow T_3 \to T_4 \longrightarrow \lambda x{:}T_3. (v\,(x : T_3 \Rightarrow T_1)) : T_2 \Rightarrow T_4 \] The nice thing about this approach is that there's only one kind of value of function type, functions! So when it comes to function application, we only need one reduction rule, good old beta: \[ (\lambda x{:}T.\,e)\, v \longrightarrow [x{:=}v]e \] The other approach is to leave the cast around the function and then add a second reduction rule for applications. \[ (v_1 : T_1 \to T_2 \Rightarrow T_3 \to T_4) \, v_2 \longrightarrow (v_1\, (v_2 : T_3 \Rightarrow T_1)) : T_2 \Rightarrow T_4 \] The nice thing about this approach is that the cast around the function is easy to access and change, which we took advantage of to compress sequences of such casts. But as we've already pointed out, having two kinds of values at function type induces some run-time overhead, even in parts of the program that are statically typed.

Our solution to this conundrum is to use a hybrid representation and to take advantage of the indirection that is already present in a function call. Instead of having two kinds of values at function type, we have only one: a closure that includes an optional threesome: \[ \langle \lambda x{:}T.\, s, \rho, \tau_\bot \rangle \] When a closure is first created, there is no threesome. Later, when a closure is cast, the threesome is added. \[ V(\lambda x{:}T.\, s,\rho) = \langle \lambda x{:}T.\, s, \rho, \bot \rangle \] The one transition rule for function application passes the optional threesome as a special parameter, here named \(c\), to the function. In the case of an un-casted closure, the function ignores the \(c\) parameter. \begin{align*} (x : T_1 = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v_2,c{:=}\tau_\bot ], (T_1 \overset{T_1}{\Longrightarrow} T_1, (x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_2. s', \rho', \tau_\bot \rangle \\ \text{and } & V(e_2,\rho) = v_2 \end{align*}

When an un-casted closure is cast, we build a wrapper function, similar to the first approach discussed above, but using the special variable \(c\) to refer to the threesome instead of hard-coding the cast into the wrapper function. We add \(\mathit{dom}\) and \(\mathit{cod}\) operations for accessing the parts of a function threesome. \begin{align*} \mathsf{cast}(\langle \lambda x{:}T.\,s, \rho, \bot\rangle ,\tau) &= \begin{cases} \mathbf{blame}\,\ell & \text{if } \tau = (T_1 \overset{I^p;\bot^\ell}{\Longrightarrow} T_2) \\ \langle \lambda x_1.\,s', \rho', \tau \rangle & \text{otherwise} \end{cases} \\ & \text{where } s' = (x_2 = x_1 {:} \mathit{dom}(c); \mathbf{return}\, f(x_2) : \mathit{cod}(c)) \\ & \text{and } \rho' = \{ f{:=}\langle \lambda x{:}T.\,s, \rho, \bot\rangle \} \end{align*} When a closure is cast for the second time, the casts are combined to save space. \begin{align*} \mathsf{cast}(\langle \lambda x{:}T.\,s, \rho, \tau_1\rangle ,\tau_2) &= \begin{cases} \mathbf{blame}\,\ell & \text{if } (\tau_1; \tau_2) = (T_1 \overset{I^p;\bot^\ell}{\Longrightarrow} T_2) \\ \langle \lambda x{:}T.\,s, \rho, (\tau_1; \tau_2)\rangle & \text{otherwise} \end{cases} \end{align*}

That's it. We now have a machine that doesn't perform extra dispatching at function calls. There is still a tiny bit of overhead in the form of passing the \(c\) argument. This overhead can be removed by passing the entire closure to itself (instead of passing the array of free variables and the threesome separately), and from inside the function, access the threesome from the closure.

In the following I give the complete definitions for the new abstraction machine. In addition to \(\mathit{dom}\) and \(\mathit{cod}\), we add a tail call without a cast to avoid overhead when there is no cast. \[ \begin{array}{llcl} \text{expressions} & e & ::= & k \mid x \mid \lambda x{:}T.\, s \mid \mathit{dom}(e) \mid \mathit{cod}(e) \\ \text{statements} & s & ::= & d; s \mid \mathbf{return}\,e \mid \mathbf{return}\,e(e) \mid \mathbf{return}\,e(e) : \tau \\ \text{optional threesomes} & \tau_\bot & ::= & \bot \mid \tau \\ \text{values}& v & ::= & k \mid k : \tau \mid \langle \lambda x{:}T.\, s, \rho, \tau_\bot \rangle \end{array} \] Here's the complete definition of the cast function. \begin{align*} \mathsf{cast}(v, \bot) &= v \\ \mathsf{cast}(k, \tau) &= \begin{cases} k & \text{if } \tau = B \overset{B}{\Longrightarrow} B \\ \mathbf{blame}\,\ell & \text{if } \tau = B \overset{B^p;\bot^\ell}{\Longrightarrow} T\\ k : \tau & \text{otherwise} \end{cases} \\ \mathsf{cast}(k : \tau_1, \tau_2) &= \begin{cases} k & \text{if } (\tau_1;\tau_2) = B \overset{B}{\Longrightarrow} B \\ \mathbf{blame}\,\ell & \text{if } (\tau_1;\tau_2) = B \overset{B^p;\bot^\ell}{\Longrightarrow} T\\ k : (\tau_1;\tau_2) & \text{otherwise} \end{cases} \\ \mathsf{cast}(\langle \lambda x{:}T.\,s, \rho, \bot\rangle ,\tau) &= \begin{cases} \mathbf{blame}\,\ell & \text{if } \tau = (T_1 \overset{I^p;\bot^\ell}{\Longrightarrow} T_2) \\ \langle \lambda x_1.\,s' , \{ f{:=}\langle \lambda x{:}T.\,s, \rho, \bot\rangle \}, \tau \rangle & \text{otherwise} \end{cases} \\ & \text{where } s' = (x_2 = x_1 {:} \mathit{dom}(c); \mathbf{return}\, f(x_2) : \mathit{cod}(c)) \\ \mathsf{cast}(\langle \lambda x{:}T.\,s, \rho, \tau_1\rangle ,\tau_2) &= \begin{cases} \mathbf{blame}\,\ell & \text{if } (\tau_1; \tau_2) = (T_1 \overset{I^p;\bot^\ell}{\Longrightarrow} T_2) \\ \langle \lambda x{:}T.\,s, \rho, (\tau_1; \tau_2)\rangle & \text{otherwise} \end{cases} \end{align*} Here are the updated evaluation rules. \begin{align*} V(k,\rho) &= k \\ V(x,\rho) &= \rho(x) \\ V(\lambda x{:}T.\, s,\rho) &= \langle \lambda x{:}T.\, s, \rho, \bot \rangle \\ V(\mathit{dom}(e),\rho) &= \tau_1 & \text{if } V(e,\rho) = \tau_1 \to \tau_2 \\ V(\mathit{cod}(e),\rho) &= \tau_2 & \text{if } V(e,\rho) = \tau_1 \to \tau_2 \end{align*} Lastly, here are the transition rules for the machine. \begin{align*} (x : T_1 = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v_2,c{:=}\tau_\bot ], (T_1 \overset{T_1}{\Longrightarrow} T_1, (x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_2. s', \rho', \tau_\bot \rangle \\ \text{and } & V(e_2,\rho) = v_2 \\ (x = \mathit{op}(\overline{e}); s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v], \kappa) \\ \text{where }& v = \delta(\mathit{op},V(e,\rho)) \\ (x = e : \tau; s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v'], \kappa) \\ \text{where } & V(e,\rho) = v \text{ and } \mathsf{cast}(v,\tau) = v' \\ (\mathbf{return}\,e, \rho, (\tau, (x,s,\rho')::\kappa)) & \longmapsto (s, \rho'[x{:=}v'], \kappa) \\ \text{where }& V(e,\rho) = v \text{ and } \mathsf{cast}(v,\tau) = v' \\ (\mathbf{return}\,e_1(e_2), \rho,\kappa) & \longmapsto (s, \rho'[y{:=}v_2,c{:=}\tau_\bot],\kappa) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s, \rho',\tau_\bot\rangle\\ \text{and } & V(e_2,\rho) = v_2 \\ (\mathbf{return}\,e_1(e_2) : \tau_1, \rho,(\tau_2,\sigma)) & \longmapsto (s, \rho'[y{:=}v_2,c{:=}\tau_\bot], ((\tau_1; \tau_2), \sigma)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s, \rho',\tau_\bot\rangle\\ \text{and } & V(e_2,\rho) = v_2 \\[2ex] (x = e : \tau; s, \rho, \kappa) & \longmapsto \mathbf{blame}\,\ell\\ \text{where } & V(e,\rho) = v, \mathsf{cast}(v,\tau) = \mathbf{blame}\,\ell \\ (\mathbf{return}\,e, \rho, (\tau,(x,s,\rho')::\kappa)) & \longmapsto \mathbf{blame}\,\ell \\ \text{where }& V(e,\rho) = v, \mathsf{cast}(v,\tau) = \mathbf{blame}\,\ell \end{align*}

I like how there are fewer rules and the rules are somewhat simpler compared to the previous machine. There is one last bit of overhead in statically typed code: in a normal return we have to apply the pending threesome that's on the stack. If one doesn't care about making tail-calls space efficient in the presence of casts, then this wouldn't be necessary. But I care.

Interpretations of the GTLC: Part 3, Going Faster

The intuition for an efficient coercion composition function came from thinking about types, not coercions. We'll start with the UD blame tracking strategy and then later consider D. Also, for now we'll stick with lazy cast checking.

Consider the following sequence of casts: \[ e : T_1 \Rightarrow^{\ell_1} T_2 \Rightarrow^{\ell_2} \cdots \Rightarrow^{\ell_{n-1}} T_n \] We'd like some way to summarize the sequence of types without loosing any important information. That is, we'd like to come up with something that can catch the same cast errors as the entire sequence, blaming the appropriate label, but using less space. Imagine the \(n\) types as a line of differently colored trees on the side of a road. If you're next to the road, staring down the line of trees, you see what looks like one tree with branches of many colors. Some of the branches from further-away trees are hidden from view by closer trees, but some are visible. Now, suppose we wanted to maintain the same view from your standpoint, but save on water. We could replace the line of trees with a single multi-colored tree that includes all the branches visible to you. The figure below depicts three differently-colored trees getting merged into a single multi-color tree. The nodes without color should be considered transparent.

Mapping this idea back to types, the colors are blame labels and transparent nodes are the type \(\star\). Because we need to color individual branches, we need blame labels on every internal node of a type. In particular, we need the notion of a labeled type: \[ \begin{array}{lrcl} \text{optional labels} & p,q & ::= & \epsilon \mid \ell \\ \text{labeled types} & P,Q & ::= & B^p \mid P \to^p Q \mid \star \mid (I^p; \bot^\ell) \end{array} \] (These labeled types are for the UD strategy. We'll discuss the labeled types for D later. Also, the labeled type \(I^p; \bot^\ell\) deserves some explanation, which we'll get to soon.) The \(\mathit{label}\) function returns the top-most label of a labeled type: \begin{align*} \mathit{label}(B^p) &= p \\ \mathit{label}(P \to^p Q) &= p \\ \mathit{label}(\star) &= \epsilon \\ \mathit{label}(I^p; \bot^\ell) &= p \end{align*}

We'll define a function for composing two labeled types \(P\) and \(Q\) to produce a new labeled type \(P'\), using semicolon as the syntax for this composition function: \[ P ; Q = P' \] We replace each cast with a threesome, that is, a cast annotated with a labeled type. The labeled type is computed by a simple function \(\mathcal{L}\) that we define below. \begin{align*} & e : T_1 \Rightarrow^\ell T_2 \text{ becomes } e : T_1 \overset{P}{\Longrightarrow} T_2 \\ & \text{ where } P = \mathcal{L}(T_1 \Rightarrow^\ell T_2) \end{align*} \begin{align*} \mathcal{L}(B \Rightarrow^\ell B) &= B \\ \mathcal{L}(\star \Rightarrow^\ell \star) &= \star \\ \mathcal{L}(B \Rightarrow^\ell \star) &= B \\ \mathcal{L}(\star \Rightarrow^\ell B) &= B^\ell \\ \mathcal{L}(T_1 \Rightarrow^\ell T_2) &= I ; \bot^\ell \qquad \text{where } I \sim T_1 \\ \mathcal{L}(T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4) &= \mathcal{L}(T_3 \Rightarrow^\ell T_1) \to \mathcal{L}(T_2 \Rightarrow^\ell T_4) \\ \mathcal{L}(T_1 \to T_2 \Rightarrow^\ell \star) &= \mathcal{L}(\star \Rightarrow^\ell T_1) \to \mathcal{L}(T_2 \Rightarrow^\ell \star) \\ \mathcal{L}(\star \Rightarrow^\ell T_3 \to T_4) &= \mathcal{L}(T_3 \Rightarrow^\ell \star) \to^\ell \mathcal{L}(\star \Rightarrow^\ell T_4) \end{align*} A sequence of threesomes is compressed to a single threesome using the composition function: \begin{gather*} e : T_1 \overset{P_1}{\Longrightarrow} T_2 \overset{P_2}{\Longrightarrow} \cdots \overset{P_{n-1}}{\Longrightarrow} T_n \\ \text{becomes} \\ e : T_1 \overset{P}{\Longrightarrow} T_n \\ \text{where } P = P_1; P_2; \cdots; P_{n-1} \end{gather*}

Before we go into the details of the composition function, it helps to see how (well-formed) threesomes correspond to coercions in normal form. With this correspondence in place, we can use the coercion reduction rules to help guide the definition of threesome composition. The function \(\mathit{TC}\) defined below maps threesomes to coercions in normal form. This function is an isomorphism, so it's inverse maps normal coercions back to threesomes. \begin{align*} \mathit{TC}(B \overset{B}{\Longrightarrow} B) &= \iota_B \\ \mathit{TC}(\star \overset{\star}{\Longrightarrow}\star) &=\iota_\star \\ \mathit{TC}(\star \overset{B^\ell}{\Longrightarrow} B) &= B?^\ell \\ \mathit{TC}(B\overset{B}{\Longrightarrow} \star) &= B! \\ \mathit{TC}(\star \overset{B^\ell}{\Longrightarrow} \star) &= B?^\ell; B! \\ \mathit{TC}(T_1 \overset{I; \bot^\ell}{\Longrightarrow} T_2) &= \mathsf{Fail}^\ell \\ \mathit{TC}(T_1 \overset{I^{\ell_1}; \bot^{\ell_2}}{\Longrightarrow} T_2) &= I?^{\ell_1} ; \mathsf{Fail}^{\ell_2} \\ \mathit{TC} (T_1 \to T_2 \overset{P_1 \to P_2}{\Longrightarrow} T_3 \to T_4)&= \mathit{TC}(T_3 \overset{P_1}{\Longrightarrow} T_1) \to \mathit{TC}(T_2 \overset{P_2}{\Longrightarrow} T_4) \\ \mathit{TC} (\star \overset{P_1 \to^\ell P_2}{\Longrightarrow} T_3 \to T_4)&= (\star \to \star)?^\ell ; \mathit{TC}(T_3 \overset{P_1}{\Longrightarrow} \star) \to \mathit{TC}(\star \overset{P_2}{\Longrightarrow} T_4) \\ \mathit{TC} (T_1 \to T_2 \overset{P_1 \to P_2}{\Longrightarrow} \star)&= \mathit{TC}(\star \overset{P_1}{\Longrightarrow} T_1) \to \mathit{TC}(T_2 \overset{P_2}{\Longrightarrow} \star); (\star \to \star)! \\ \mathit{TC} (\star \overset{P_1 \to^\ell P_2}{\Longrightarrow} \star)&= (\star \to \star)?^\ell ; \mathit{TC}(\star \overset{P_1}{\Longrightarrow} \star) \to \mathit{TC}(\star \overset{P_2}{\Longrightarrow} \star); (\star \to \star)! \end{align*}

We're ready to make precise how two labeled types can be composed to form a single labeled type. The two cases in which one of the labeled types is \(\star\) are easy: just return the other type: \begin{align*} \star; Q &= Q \\ P; \star &= P \end{align*} Next, suppose we have \(\mathsf{Int}^{\ell_1}\) followed by \(\mathsf{Int}^{\ell_2}\). These should compose to \(\mathsf{Int}^{\ell_1}\) because if the first cast succeeds, so will the second, making the blame label \(\ell_2\) redundant. In general, for labeled basic types we have the following rule. \begin{equation} \label{eq:1} B^p; B^q = B^p \end{equation} Suppose instead that the basic types don't match. The right-hand side of the following rule is a bit tricky, so let's think about this in terms of coercions. \begin{equation} \label{eq:2} B_1^p ; B_2^q = B_1^p ; \bot^q \qquad \text{if } B_1 \neq B_2 \end{equation} Suppose \(p=\ell_1, q = \ell_2\) and these two labeled types come from the threesomes \[ \star \overset{B_1^{\ell_1}}{\Longrightarrow} \star \overset{B_2^{\ell_2}}{\Longrightarrow} B_2 \] The corresponding coercion sequence is \[ B_1?^{\ell_1} ; B_1! ; B_2?^{\ell_2} \] which reduces to \[ B_1?^{\ell_1} ; \mathsf{Fail}^{\ell_2} \] and that corresponds to the labeled type for errors, \(B_1^{\ell_1}; \bot^{\ell_2}\). We also need to consider a mismatch between basic types and function types: \begin{align} B^p; (P \to^q Q) &= B^q; \bot^q \\ (P \to^p Q); B^q &= (\star \to \star)^p; \bot^q \end{align} The rule for labeled function types takes the label \(p\) for the label in the result and it recursively composes the domain and codomain types. The contra-variance in the parameter type is important for getting the right blame and coincides with the contra-variance in the reduction rule for composing function coercions. \begin{equation} \label{eq:4} (P_1 \to^p P_2) ; (Q_1 \to^q Q_2) = (Q_1; P_1) \to^p (P_2; Q_2) \end{equation} The following figure shows an example similar to the previous figure, but with function types instead of pair types. The analogy with real trees and line-of-sight breaks down because you have to flip to looking at the trees from back-to-front instead of front-to-back for negative positions within the type.

Lastly we need several rules to handle when the error type is on the left or right. \begin{align} (I^p; \bot^\ell); Q &= (I^p; \bot^\ell) \\ P; (I^q; \bot^\ell) &= I^p ; \bot^\ell \qquad \text{if } I \sim P \text{ and } \mathit{label}(P) = p \\ P; (I^q; \bot^\ell) &= I^p ; \bot^q \qquad \text{if } I \not\sim P \text{ and } \mathit{label}(P) = p \end{align}

What's extra cool about labeled types and their composition function is that each rule covers many different rules if you were to formulate them in terms of coercions. For example, the single rule \( B^p; B^q = B^p\) covers four situations when viewed as threesomes or coercions: \begin{align*} (B \overset{B}{\Longrightarrow} B; B \overset{B}{\Longrightarrow} B) &= B \overset{B}{\Longrightarrow} B \\ \iota_B; \iota_B &\longrightarrow \iota_B \\ (\star \overset{B^\ell}{\Longrightarrow} B; B \overset{B}{\Longrightarrow} B) &= \star \overset{B^\ell}{\Longrightarrow} B \\ B?^\ell ; \iota_B &\longrightarrow B?^\ell \\ (B \overset{B}{\Longrightarrow} B; B \overset{B}{\Longrightarrow} \star) &= B \overset{B}{\Longrightarrow} \star \\ \iota_B; B! &\longrightarrow B! \\ (\star \overset{B^\ell}{\Longrightarrow} B; B \overset{B}{\Longrightarrow} \star) &= \star \overset{B^\ell}{\Longrightarrow} \star \\ B?^\ell ; B! & \text{ is already in normal form} \end{align*}

We define a threesomes as a source type, middle labeled typed, and a target type. \[ \begin{array}{llcl} \text{threesomes} & \tau & ::= & T \overset{P}{\Longrightarrow} T \\ \end{array} \] We define the sequencing of threesomes as follows \[ (T_1 \overset{P}{\Longrightarrow} T_2); (T_2 \overset{Q}{\Longrightarrow}T_3) = T_1 \overset{P;Q}{\Longrightarrow} T_3 \] Similarly, we define the notation \(\tau_1 \to \tau_2\) as \[ (T_3 \overset{P}{\Longrightarrow} T_1) \to (T_2 \overset{Q}{\Longrightarrow} T_4) = T_1\to T_2 \overset{P\to Q}{\Longrightarrow} T_3 \to T_4 \]

We can now go back to the ECD machine and replace the coercions with threesomes. Here's the syntax in A-normal form. \[ \begin{array}{llcl} \text{expressions} & e & ::= & k \mid x \mid \lambda x{:}T.\, s \\ \text{definitions} & d & ::= & x=\mathit{op}(e) \mid x : T = e(e) \mid x = e : \tau \\ \text{statements} & s & ::= & d; s \mid \mathbf{return}\,e \mid \mathbf{return}\,e(e) : \tau \\ \text{simple values} & \tilde{v} & ::= & k \mid \langle \lambda x{:}T.\, s, \rho \rangle \\ \text{values}& v & ::= & \tilde{v} \mid \tilde{v} : \tau \end{array} \] The cast function, of course, needs to change. \begin{align*} \mathsf{cast}(k, \tau) &= \begin{cases} k & \text{if } \tau = (B \overset{B}{\Longrightarrow} B) \\ \mathbf{blame}\,\ell & \text{if } \tau = B \overset{B^p;\bot^\ell}{\Longrightarrow} T\\ k : \tau & \text{otherwise} \end{cases} \\ \mathsf{cast}(\langle \lambda x{:}T.s,\rho \rangle, \tau) &= \langle \lambda x{:}T.s,\rho \rangle : \tau \\ \mathsf{cast}(k : \tau_1, \tau_2) &= \begin{cases} k & \text{if } (\tau_1;\tau_2) = B \overset{B}{\Longrightarrow} B \\ \mathbf{blame}\,\ell & \text{if } (\tau_1;\tau_2) = B \overset{B^p;\bot^\ell}{\Longrightarrow} T\\ k : (\tau_1;\tau_2) & \text{otherwise} \end{cases} \\ \mathsf{cast}(\langle \lambda x{:}T.s,\rho \rangle : \tau_1, \tau_2) &= \begin{cases} \langle \lambda x{:}T.s,\rho \rangle : (\tau_1;\tau_2)& \text{if } \mathit{middle}(\tau_1;\tau_2) \neq (I^p;\bot^\ell) \\ \mathbf{blame}\,\ell & \text{if } \mathit{middle}(\tau_1;\tau_2) = (I^p;\bot^\ell) \end{cases} \end{align*} And last but not least, here's the transitions for the ECD machine, but with threesomes instead of coercions. \begin{align*} (x : T_1 = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v_2], (T_1 \overset{T_1}{\Longrightarrow}T_1,(x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_2. s', \rho' \rangle, V(e_2,\rho) = v_2 \\ (x : T_1 = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v'_2], (\tau_2,(x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_2. s', \rho' \rangle : \tau_1 \to \tau_2, \\ & V(e_2,\rho) = v_2, \text{ and } \mathsf{cast}(v_2, \tau_1) = v'_2\\ (x = \mathit{op}(\overline{e}); s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v], \kappa) \\ \text{where }& v = \delta(\mathit{op},V(e,\rho)) \\ (x = e : \tau; s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v'], \kappa) \\ \text{where } & V(e,\rho) = v, \mathsf{cast}(v,\tau) = v' \\ (\mathbf{return}\,e, \rho, (\tau,(x,s,\rho')::\kappa)) & \longmapsto (s, [x{:=}v']\rho', \kappa) \\ \text{where }& V(e,\rho) = v, \mathsf{cast}(v,\tau) = v' \\ (\mathbf{return}\,e_1(e_2) : \tau_1, \rho, (\tau_2,\sigma)) & \longmapsto (s, \rho'[y{:=}v_2], ((\tau_1; \tau_2),\sigma)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s, \rho' \rangle, V(e_2,\rho) = v_2 \\ (\mathbf{return}\,e_1(e_2) : \tau_1, \rho, (\tau_2,\sigma)) & \longmapsto (s, \rho'[y{:=}v'_2], (\tau_5,\sigma)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_1. s, \rho' \rangle : \tau_3 \to \tau_4,\\ & V(e_2,\rho) = v_2, \mathsf{cast}(v_2, \tau_3) = v'_2, \text{ and} \\ & (\tau_4; \tau_1; \tau_2) = \tau_5 \\[2ex] (x = e : \tau; s, \rho, \kappa) & \longmapsto \mathbf{blame}\,\ell\\ \text{where } & V(e,\rho) = v, \mathsf{cast}(v,\tau) = \mathbf{blame}\,\ell \\ (\mathbf{return}\,e, \rho, (\tau,(x,s,\rho')::\kappa)) & \longmapsto \mathbf{blame}\,\ell \\ \text{where }& V(e,\rho) = v, \mathsf{cast}(v,\tau) = \mathbf{blame}\,\ell \end{align*}

We now have an implementation of Lazy UD that is space efficient and relatively efficient in time as well. However, there is one nagging issue regarding the speed of statically-typed code. Notice how there are two transition rules for each kind of function call. The source of the problem is that there are two kinds of values that have function type, closures and closures wrapped in a threesome. In the next post I'll define a unified representation for closures and wrapped closures so that we don't need to dispatch at runtime.

Interpretations of the GTLC, Part 2: Space-Efficient Machines

I briefly mentioned in my previous post that there are implementation challenges regarding gradual typing. One of those challenges regards space efficiency. In their paper Space-Efficient Gradual Typing, Herman, Tomb, and Flanagan observed two circumstances in which function casts can lead to unbounded space consumption. First, some programs repeatedly apply casts to the same function, resulting in a build-up of casts around the function. In the following example, each time the function bound to k is passed between even and odd a cast is added, causing a space leak proportional to n.

let rec even(n : Int, k : Dyn->Bool) : Bool =
   if (n = 0) then k(True : Bool => *)
   else odd(n - 1, k : *->Bool => Bool->Bool)
and odd(n : Int, k : Bool->Bool) : Bool =
   if (n = 0) then k(False)
   else even(n - 1, k : Bool->Bool => *->Bool)

Second, some casts break proper tail recursion. Consider the following example in which the return type of even is \(\star\) and odd is \(\mathsf{Bool}\).

let rec even(n : Int) : Dyn =
  if (n = 0) then True else odd(n - 1) : Bool => *
and odd(n : Int) : Bool =
  if (n = 0) then False else even(n - 1) : * => Bool

Assuming tail call optimization, cast-free versions of the even and odd functions require only constant space, but because the call to even is no longer a tail call, the run-time stack grows with each call and space consumption is proportional to n.

Herman et al.'s solution to this space-efficiency problem relies on Henglein's Coercion Calculus. This calculus defines a set of combinators, called coercions, that can be used to express casts. The key advantage of coercions is that an arbitrarily long sequence of coercions reduces to a sequence of at most three coercions. The following defines the syntax and typing rules for coercions. The two most important coercions are the injection coercion \(I!\) from \(I\) to \(\star\) and the projection coercion \(I?^\ell\) from \(\star\) to \(I\). The definition of the injectable types \(I\) depends on the blame tracking strategy: \begin{align*} I & ::= B \mid \star \to \star & (UD) \\ I & ::= B \mid T \to T & (D) \end{align*} \begin{gather*} \begin{array}{llcl} \text{coercions} & c & ::= & \iota_T \mid I! \mid I?^\ell \mid c\to c \mid c;c \mid \mathsf{Fail}^\ell \end{array} \\[2ex] \frac{}{\vdash \iota_T : T \Rightarrow T} \qquad \frac{}{\vdash T! : T \Rightarrow \star} \qquad \frac{}{\vdash T?^\ell : \star \Rightarrow T} \\[2ex] \frac{\vdash c_1 : T_{21} \Rightarrow T_{11} \quad \vdash c_2 : T_{12} \Rightarrow T_{22}} {\vdash c_1 \to c_2 : T_{11} \to T_{12} \Rightarrow T_{21} \to T_{22}} \\[2ex] \frac{\vdash c_1 : T_1 \Rightarrow T_2 \quad \vdash c_2 : T_2 \Rightarrow T_3} {\vdash c_1 ; c_2 : T_1 \Rightarrow T_3} \qquad \frac{}{\vdash \mathsf{Fail}^\ell : T_1 \Rightarrow T_2} \end{gather*} We sometimes drop the subscript on the \(\iota_T\) when the type \(T\) doesn't matter.

The way in which casts are compiled to coercions depends on whether you're using the D or UD blame tracking strategy. Here's the compilation function for D. \begin{align*} \mathcal{C}_D(\star \Rightarrow^\ell \star) &= \iota \\ \mathcal{C}_D(B \Rightarrow^\ell B) &= \iota \\ \mathcal{C}_D(\star \Rightarrow^\ell I) &= I?^\ell \\ \mathcal{C}_D(I \Rightarrow^\ell \star) &= I! \\ \mathcal{C}_D(T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4) &= c_1 \to c_2 \\ \text{where } & c_1 = \mathcal{C}_D(T_3 \Rightarrow^\ell T_1) \\ \text{and } & c_2 = \mathcal{C}_D(T_2 \Rightarrow^\ell T_4) \\ \mathcal{C}_D(T_1 \Rightarrow^\ell T_2) &= \mathsf{Fail}^\ell \qquad \text{if } \mathit{hd}(T_1) \not\sim \mathit{hd}(T_2) \end{align*} The compilation function for UD is a bit more complicated because the definition of injectable type is more restrictive. \begin{align*} \mathcal{C}_{\mathit{UD}}(\star \Rightarrow^\ell \star) &= \iota \\ \mathcal{C}_{\mathit{UD}}(B \Rightarrow^\ell B) &= \iota \\ \mathcal{C}_{\mathit{UD}}(\star \Rightarrow^\ell B) &= B?^\ell \\ \mathcal{C}_{\mathit{UD}}(\star \Rightarrow^\ell T_3 \to T_4) &= (\star \to \star)?^\ell; (c_1 \to c_2) \\ \text{where } & c_1 = \mathcal{C}_D(T_3 \Rightarrow^\ell \star) \\ \text{and } & c_2 = \mathcal{C}_D(\star \Rightarrow^\ell T_4) \\ \mathcal{C}_{\mathit{UD}}(B \Rightarrow^\ell \star) &= B! \\ \mathcal{C}_{\mathit{UD}}(T_1 \to T_2 \Rightarrow^\ell \star) &= (c_1 \to c_2) ; (\star \to \star)! \\ \text{where } & c_1 = \mathcal{C}_D(\star \Rightarrow^\ell T_1) \\ \text{and } & c_2 = \mathcal{C}_D(T_2 \Rightarrow^\ell \star) \\ \mathcal{C}_{\mathit{UD}}(T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4) &= c_1 \to c_2 \\ \text{where } & c_1 = \mathcal{C}_D(T_3 \Rightarrow^\ell T_1) \\ \text{and } & c_2 = \mathcal{C}_D(T_2 \Rightarrow^\ell T_4) \\ \mathcal{C}_{\mathit{UD}}(T_1 \Rightarrow^\ell T_2) &= \mathsf{Fail}^\ell \qquad \text{if } \mathit{hd}(T_1) \not\sim \mathit{hd}(T_2) \end{align*}

We identify coercion sequencing up to associativity and identity: \begin{align*} c_1 ; (c_2; c_3) &= (c_1 ; c_2); c_3 \\ (c ; \iota) &= (\iota ; c) = c \end{align*} The following are the reduction rules for coercions. The compilation function \(\mathcal{C}\) depends on the choice of blame tracking strategy (D or UD). \begin{align*} I_1!; I_2?^\ell & \longrightarrow \mathcal{C}(I_1 \Rightarrow^\ell I_2) \\ (c_{11} \to c_{12}); (c_{21} \to c_{22}) & \longrightarrow (c_{21};c_{11}) \to (c_{12}; c_{22}) \\ \mathsf{Fail}^\ell; c & \longrightarrow \mathsf{Fail}^\ell \\ \overline{c} ; \mathsf{Fail}^\ell & \longrightarrow \mathsf{Fail}^\ell \\ \end{align*}

The last reduction rule refers to \(\overline{c}\), a subset of the coercions that we refer to as wrapper coercions. We define wrapper coercions and coercions in normal form \(\hat{c}\) as follows. \[ \begin{array}{llcl} \text{optional injections} & \mathit{inj} & ::= & \iota \mid I! \\ \text{optional function coercions} & \mathit{fun} & ::= & \iota \mid \hat{c} \to \hat{c} \\ \text{optional projections} & \mathit{proj} & ::= & \iota \mid I?^\ell \\ \text{wrapper coercions} & \overline{c} & ::= & \mathit{fun}; \mathit{inj} \\ \text{normal coercions} & \hat{c} & ::= & \mathit{proj} ; \mathit{fun}; \mathit{inj} \mid \mathit{proj}; \mathsf{Fail}^\ell \end{array} \] Here we can easily see that coercions in normal form can always be represented by a coercion with a length of at most three.

Theorem (Strong Normalization for Coercions) For any coercion \(c\), there exists a \(\hat{c}\) such that \(c \longrightarrow^{*} \hat{c}\).

With the Coercion Calculus in hand, we can define a space-efficient abstract machine. This machine is a variant of my favorite abstract machine for the lambda calculus, the ECD machine on terms in A-normal form. Herman et al. define an efficient reduction semantics that relies on mutually-recursive evaluation contexts to enable the simplification of coercions in tail position. Our choice of the ECD machine allows us to deal with coercions in tail position in a more straightforward way. Here's the syntax for our coercion-based calculus in A-normal form. The two main additions are the cast definition and the tail-call statement. \[ \begin{array}{llcl} \text{expressions} & e & ::= & k \mid x \mid \lambda x{:}T.\, s \\ \text{definitions} & d & ::= & x=\mathit{op}(e) \mid x:T = e(e) \mid x = e : \hat{c}\\ \text{statements} & s & ::= & d; s \mid \mathbf{return}\,e \mid \mathbf{return}\,e(e) : \hat{c} \\ \text{simple values} & \tilde{v} & ::= & k \mid \langle \lambda x{:}T.\, s, \rho \rangle \\ \text{values}& v & ::= & \tilde{v} \mid \tilde{v} : \overline{c} \end{array} \]

The evaluation function \(V\) maps expressions and environments to values in the usual way. \begin{align*} V(k,\rho) &= k \\ V(x,\rho) &= \rho(x) \\ V(\lambda x{:}T.\, s,\rho) &= \langle \lambda x{:}T.\, s, \rho \rangle \end{align*} The following auxiliary function applies a coercion to a value. \begin{align*} \mathsf{cast}(\tilde{v}, \hat{c}) &= \begin{cases} \tilde{v} & \text{if } \hat{c} = \iota_B \\ \mathbf{blame}\,\ell & \text{if } \hat{c} = \mathsf{Fail}^\ell \\ \tilde{v} : \hat{c} & \text{otherwise} \end{cases} \\ \mathsf{cast}(\tilde{v} : \overline{c_1}, \hat{c_2}) &= \begin{cases} \tilde{v} & \text{if } (\overline{c_1}; \hat{c_2})= \iota_B \\ \mathbf{blame}\,\ell & \text{if } \overline{c_1}; \hat{c_2} \longrightarrow^{*} \mathsf{Fail}^\ell \\ \tilde{v} : \overline{c_3} & \text{if } \overline{c_1}; \hat{c_2} \longrightarrow^{*} \overline{c_3} \text{ and } \overline{c_3} \neq \mathsf{Fail}^\ell \end{cases} \end{align*}

The machine state has the form \((s,\rho,\kappa)\), where the stack \(\kappa\) is essentially a list of frames. The frames are somewhat unusual in that they include a pending coercion. We also need a pending coercion for the empty stack, so we define stacks as follows. \[ \begin{array}{llcl} & \sigma & ::= & [] \mid (x,s,\rho)::\kappa \\ \text{stacks} & \kappa & ::= & (c,\sigma) \end{array} \] The machine has seven transition rules to handle normal execution and two rules to handle cast errors. \begin{align*} (x:T = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v_2], (\iota_T,(x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s', \rho' \rangle, V(e_2,\rho) = v_2 \\ (x : T_1 = e_1(e_2); s, \rho, \kappa) & \longmapsto (s', \rho'[y{:=}v'_2], (c_2,(x,s,\rho)::\kappa)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T_2. s', \rho' \rangle : (c_1 \to c_2), \\ & V(e_2,\rho) = v_2, \text{ and } \mathsf{cast}(v_2,c_1) = v'_2\\ (x = \mathit{op}(\overline{e}); s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v], \kappa) \\ \text{where }& v = \delta(\mathit{op},V(e,\rho)) \\ (x = e : c; s, \rho, \kappa) & \longmapsto (s, \rho[x{:=}v'], \kappa) \\ \text{where } & V(e,\rho) = v, \mathsf{cast}(v,c) = v' \\ (\mathbf{return}\,e, \rho, (c,(x,s,\rho')::\kappa)) & \longmapsto (s, [x{:=}v']\rho', \kappa) \\ \text{where }& V(e,\rho) = v, \mathsf{cast}(v,c) = v' \\ (\mathbf{return}\,(e_1\,e_2) : c_1, \rho, (c_2,\sigma)) & \longmapsto (s, \rho'[y{:=}v_2], (\hat{c_3},\sigma)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s, \rho' \rangle, V(e_2,\rho) = v_2\\ & (c_1; c_2) \longrightarrow^{*} \hat{c_3} \\ (\mathbf{return}\,(e_1\,e_2) : c_1, \rho, (c_2,\sigma)) & \longmapsto (s, \rho'[y{:=}v'_2], (\hat{c_5},\sigma)) \\ \text{where } & V(e_1,\rho) = \langle \lambda y{:}T. s, \rho' \rangle : (c_3 \to c_4),\\ & V(e_2,\rho) = v_2, \mathsf{cast}(v_2, c_3) = v'_2, \text{ and} \\ & (c_4; c_1; c_2) \longrightarrow^{*} \hat{c_5} \\[2ex] (x = e : c; s, \rho, \kappa) & \longmapsto \mathbf{blame}\,\ell\\ \text{where } & V(e,\rho) = v, \mathsf{cast}(v,c) = \mathbf{blame}\,\ell \\ (\mathbf{return}\,e, \rho, (c,\sigma)) & \longmapsto \mathbf{blame}\,\ell \\ \text{where }& V(e,\rho) = v, \mathsf{cast}(v,c) = \mathbf{blame}\,\ell \end{align*}

The space-efficiency of this machine comes from two places. First, the values only ever include a single cast wrapped around a simple value. The cast function maintains this invariant by normalizing whenever a cast is applied to an already-casted value. The second place is the transition rule for tail calls. The coercion in tail position \(c_1\) is sequenced with the pending coercion \(c_2\) and normalized to \(c_3\), which becomes the new pending coercion.

While this machine is space efficient, it is not efficient with respect to time. The reason is that naive coercion reduction is an expensive process: one must search for a redex, reduce it, and plug the contractum back in. Furthermore, the associativity of coercions makes searching for a redex more challenging. In the next post I'll discuss a recursive function that directly maps a sequence of two coercions in normal form to its normal form, using ideas from the paper Threesomes, With and Without Blame I coauthored with Philip Wadler.

Interpretations of the Gradually-Typed Lambda Calculus, Part 1

I just got back from Copenhagen, where I gave a tutorial on gradual typing at the Workshop on Scheme and Functional Programming. I very much enjoyed the workshop and giving the tutorial. Thank you for the invitation Olivier!

For those of you who couldn't be there, this series of blog posts will include the material from my tutorial. For those of you who were there, this series will include some bonus material: an efficient machine for "Eager D" based on recent work by Ronald Garcia and myself.

When I first began working on gradual typing in 2005 and 2006, my focus was on the type system. The main pieces of the type system fell into place that first year, and ever since then I've been thinking about the dynamic semantics. It turns out there are many design choices and implementation challenges regarding the dynamic semantics. In this post I'll restrict my attention to the gradually-typed lambda calculus, as many issues already arise in that setting. I'll quickly review the syntax and type system, then move on to discuss the dynamic semantics.

The following defines the syntax for the gradually-typed lambda calculus. Here I'm writing the dynamic type as $\star$. Also, note that a lambda without a type annotation on its parameter is shorthand for a lambda whose parameter is annotated with $\star$. $$\begin{array}{lrcl} \text{basic types} & B & ::= & \mathsf{Int} \mid \mathsf{Bool} \\ \text{types} & T & ::= & B \mid T \to T \mid \star \\ \text{variables} & x,y,z \\ \text{integers} & n \\ \text{constants}& k & ::= & n \mid \mathsf{true} \mid \mathsf{false} \\ \text{operators}&\mathit{op} & ::= & \mathsf{inc} \mid \mathsf{dec} \mid \mathsf{zero?} \\ \text{expressions} & e & ::= & k \mid \mathit{op}(e) \mid x \mid \lambda x{:}T.\, e \mid e\,e \\ & & & \lambda x.\, e \equiv \lambda x{:}\star.\, e \end{array}$$

The Gradual Type System and Cast Insertion

The type system of the gradually-typed lambda calculus is quite similar to the simply-typed lambda calculus. The only differences are in the rules for application. Instead of requiring the argument's type to be identical to the function's parameter type, we only require that the types be consistent, written $\sim$ and defined below. We also allow the application of expressions of type \(\star\). $$\begin{gather*} \frac{\mathrm{typeof}(k) = B}{\Gamma \vdash k : B} \quad \frac{\mathrm{typeof}(\mathit{op}) = B_1 \to B_2 \quad \Gamma \vdash e : T \quad B_1 \sim T}{ \Gamma \vdash \mathit{op}(e) : B_2} \\[2ex] \frac{x:T \in \Gamma}{\Gamma \vdash x : T} \quad \frac{\Gamma,x:T_1 \vdash e : T_2}{\Gamma \vdash \lambda x:T_1.e : T_1 \to T_2} \\[2ex] \frac{\begin{array}{l}\Gamma \vdash e_1 : T_1 \to T_3 \\ \Gamma \vdash e_2 : T_2 \end{array} \quad T_1 \sim T_2}{\Gamma \vdash e_1\,e_2 : T_3} \quad \frac{\begin{array}{l}\Gamma \vdash e_1 : \star \\ \Gamma \vdash e_2 : T_2 \end{array}}{\Gamma \vdash e_1\,e_2 : \star} \\[4ex] B \sim B \qquad \star \sim T \qquad T \sim \star \qquad \frac{T_1 \sim T_3 \quad T_2 \sim T_4}{T_1 \to T_2 \sim T_3 \to T_4} \end{gather*}$$ The lack of contra-variance in how function parameters are handled in the consistency relation not a mistake. Unlike subtyping, the consistency relation is symmetric, so it wouldn't matter if we wrote $T_3 \sim T_1$ instead of $T_1 \sim T_3$. Also, consistency is not transitive, which is why we don't use a separate subsumption rule, but instead use consistency in the rules for application.

The dynamic semantics of the gradually-typed lambda calculus is not defined in terms of the surface syntax, but instead it is defined on an intermediate language that extends the simply-typed lambda calculus with explicit casts. $$\begin{array}{lrcl} \text{blame labels} & \ell \\ \text{expressions} & e &::=& \ldots \mid e : T \Rightarrow^\ell T \end{array}$$ We use a non-standard notation for casts so that they are easier to read, so that they go left to right. The casts are annotated with blame labels, which we treat here as symbols, but in a real implementation would include the static location (line and character position) of the cast. We use a single blame label without any notion of polarity because these casts are really just casts, not contracts between two parties.

Cast insertion is a type-directed translation, so it is the same as the type system with the addition of an output term. $$\begin{gather*} \frac{\mathrm{typeof}(k) = B}{\Gamma \vdash k \leadsto k : B} \quad \frac{\begin{array}{l}\mathrm{typeof}(\mathit{op}) = B_1 \to B_2 \\ \Gamma \vdash e \leadsto e' : T \end{array} \quad B_1 \sim T}{ \Gamma \vdash \mathit{op}(e) \leadsto \mathit{op}(e' : T \Rightarrow^\ell B_1): B_2} \\[2ex] \frac{x:T \in \Gamma}{\Gamma \vdash x \leadsto x : T} \quad \frac{\Gamma,x:T_1 \vdash e \leadsto e' : T_2} {\Gamma \vdash (\lambda x:T_1.e) \leadsto (\lambda x:T_1.e') : T_1 \to T_2} \\[2ex] \frac{\begin{array}{l}\Gamma \vdash e_1 \leadsto e'_1 : T_1 \to T_3 \\ \Gamma \vdash e_2 \leadsto e'_2 : T_2 \end{array} \quad T_1 \sim T_2}{\Gamma \vdash e_1\,e_2 \leadsto e'_1 \, (e'_2 : T_2 \Rightarrow^\ell T_1): T_3} \\[2ex] \frac{\begin{array}{l}\Gamma \vdash e_1 \leadsto e'_1 : \star \\ \Gamma \vdash e_2 \leadsto e'_2 : T_2 \end{array}} {\Gamma \vdash e_1 \, e_2 \leadsto (e'_1: \star \Rightarrow^\ell T_2 \to \star )\,e'_2 : \star} \end{gather*}$$

We often abbreviate a pair of casts $$(e : T_1 \Rightarrow^{\ell_1} T_2) : T_2 \Rightarrow^{\ell_2} T_3$$ to remove the duplication of the middle type as follows $$e : T_1 \Rightarrow^{\ell_1} T_2 \Rightarrow^{\ell_2} T_3$$

Design Choices Regarding the Dynamics

Consider the following example in which a function is cast to the dynamic type and then cast to a type that is inconsistent with the type of the function. \begin{align*} & \mathsf{let}\, f = (\lambda x:\mathsf{Int}. \,\mathsf{inc}\,x) : \mathsf{Int}\to\mathsf{Int} \Rightarrow^{\ell_0} \star \Rightarrow^{\ell_1} \mathsf{Bool}\to \mathsf{Bool}\\ & \mathsf{in} \, f\, \mathsf{true} \end{align*} A few questions immediately arise:

• Should a runtime cast error occur during the evaluation of the right-hand side of the let? Or should the runtime error occur later, when f is applied to \textsf{true}?
• When the runtime cast error occurs, which cast should be blamed, $\ell_0$ or $\ell_1$? More generally, we want to define a subtyping relation to characterize safe casts (casts that never fail), and the specifics of subtyping relation depend on the blame tracking strategy.

Ron, Walid, and I wrote a paper, Exploring the Design Space of Higher-Order Casts (ESOP 2009), that characterized the different answers to the above questions in terms of Henglein's Coercion Calculus. One can choose to check higher-order casts in either a lazy or eager fashion and one can assign blame to only downcasts (D) or the one can share blame between upcasts and downcasts (UD). The semantics of casts with lazy checking is straightforward whereas eager checking is not, so we'll first discuss lazy checking. Also, the semantics of the D approach is slightly simpler than UD, so we'll start with lazy D. We'll delay discussing the Coercion Calculus until we really need it.

The Lazy D Semantics

We'll define an evaluation (partial) function $\mathcal{E}$ that maps a term and environment to a result. That is, we'll give Lazy D a denotational semantics. The values and results are defined as follows: \[ \begin{array}{lrcl} & F & \in & V \to_c R \\ \text{values} & v \in V & ::= & k \mid F \mid v : T \Rightarrow^\ell \star \mid v : T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4 \\ \text{results}& r \in R & ::= &v \mid \mathbf{blame}\,\ell \end{array} \]

To handle the short-circuiting of evaluation in the case of a cast error (signaled by $\mathbf{blame}\,\ell$), we use the following monadic operators: \begin{align*} \mathbf{return}\,v &= v \\ \mathbf{letB}\,X = M\,\mathbf{in}\, N &= \mathbf{case}\,M\,\mathbf{of}\,\\ & \quad\;\; \mathbf{blame}\,\ell \Rightarrow \mathbf{blame}\,\ell \\ & \quad \mid v \Rightarrow [X{:=}v]N \end{align*}

The primitive operators are given their semantics by the $\delta$ function. \begin{align*} \delta(\mathsf{inc},n) &= n + 1 \\ \delta(\mathsf{dec},n) &= n - 1 \\ \delta(\mathsf{zero?},n) &= (n = 0) \end{align*}

In lazy cast checking, when determining whether to signal a cast error, we only compare the heads of the types: \begin{align*} \mathit{hd}(B) &= B \\ \mathit{hd}(T_1 \to T_2) &= \star \to \star \end{align*}

The following auxiliary function, named cast, is the main event. It is defined by cases on the source and target types $T_1$ and $T_2$. The line for projecting from $\star$ to $T_2$ picks the $\ell$ blame label from the projection (the down-cast), which is what gives this semantics its "D". \begin{align*} \mathsf{cast}(v,T_1,\ell,T_2) &= \mathbf{blame}\,\ell \qquad \text{if } \mathit{hd}(T_1) \not\sim \mathit{hd}(T_2) \\ \mathsf{cast}(v,B,\ell,B) &= v \\ \mathsf{cast}(v,\star,\ell,\star) &= v \\ \mathsf{cast}(v,\star,\ell,T_2) &= \mathbf{case}\,v\,\mathbf{of}\, (v' : T_3 \Rightarrow^{\ell'} \star) \Rightarrow \\ & \qquad \mathsf{cast}(v',T_3,\ell,T_2) \\ \mathsf{cast}(v,T_1,\ell,\star) &= v : T_1 \Rightarrow^\ell \star \\ \mathsf{cast}(v,T_{11}\to T_{12},\ell,T_{21}\to T_{22}) &= v : T_{11}\to T_{12} \Rightarrow^\ell T_{21}\to T_{22} \end{align*}

The apply auxiliary function performs function application, and is defined by induction on the first parameter. \begin{align*} \mathsf{apply}(F,v_2) &=F(v_2) \\ \mathsf{apply}(v : T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4,v_2) &= \mathbf{letB}\,X_3 = \mathsf{cast}(v_2,T_3,\ell,T_1)\,\mathbf{in} \\ & \quad \mathbf{letB}\,X_4 = \mathsf{apply}(v,X_3)\,\mathbf{in} \\ & \quad \mathsf{cast}(X_4, T_2, \ell, T_4) \end{align*}

With these auxiliary functions and monadic operators in hand, the definition of the evaluation function $\mathcal{E}$ is straightforward. \begin{align*} \mathcal{E}(k,\rho) &= \mathbf{return}\, k \\ \mathcal{E}(x,\rho) &= \mathbf{return}\, \rho(x) \\ \mathcal{E}(\lambda x{:}T.\,e, \rho) &= \mathbf{return}\, (\lambda v.\, \mathcal{E}(e, \rho[x\mapsto v])) \\ \mathcal{E}(\mathit{op}(e)) &= \mathbf{letB}\, X = \mathcal{E}(e,\rho) \,\mathbf{in}\, \delta(\mathit{op},X) \\ \mathcal{E}(e : T_1 \Rightarrow^\ell T_2) &= \mathbf{letB}\, X = \mathcal{E}(e,\rho) \,\mathbf{in}\, \mathsf{cast}(X,T_1 ,\ell, T_2) \\ \mathcal{E}(e_1\,e_2) &= \mathbf{letB}\,X_1 = \mathcal{E}(e_1,\rho)\,\mathbf{in}\\ & \quad \mathbf{letB}\,X_2 = \mathcal{E}(e_2,\rho)\,\mathbf{in}\\ & \quad \mathsf{apply}(X_1,X_2) \end{align*} The semantics for the Lazy D Gradually-Typed Lambda Calculus is defined by the following $\mathit{eval}$ partial function. \[ \mathit{eval}(e) = \begin{cases} \mathit{observe(r)} & \text{if }\emptyset \vdash e \leadsto e' : T \text{ and } \mathcal{E}(e',\emptyset) = r \\ \bot & \text{otherwise} \end{cases} \] where \begin{align*} \mathit{observe}(k) &= k \\ \mathit{observe}(F) &= \mathit{function} \\ \mathit{observe}(v : T_1\to T_2\Rightarrow^\ell T_3\to T_4) &= \mathit{function} \\ \mathit{observe}(v : T \Rightarrow \star) &= \mathit{dynamic} \\ \mathit{observe}(\mathbf{blame}\,\ell) &= \mathbf{blame}\,\ell \end{align*}

Exercise: Calculate the output of eval for the example program at the beginning of this post.

Similar to object-oriented languages, we can define a subtyping relation that characterizes when a cast is safe, that is, when a cast will never fail. The following is the subtyping relation for the D semantics. \begin{gather*} \frac{}{T <: \star} \qquad \frac{}{B <: B} \qquad \frac{T_3 <: T_1 \quad T_2 <: T_4}{T_1 \to T_2 <: T_3 \to T_4} \end{gather*} This subtyping relation is what I expected to see. The dynamic type plays the role of the top element of this ordering and the rule for function types has the usual contra-variance in the parameter type. The Subtyping Theorem connects the dynamic semantics with the subtyping relation.

Theorem (Subtyping) If the cast labeled with \(\ell\) in program \(e\) respects subtyping, then \(\mathit{eval}(e) \neq \mathbf{blame}\,\ell\).

The Lazy UD Semantics

One interpretation of the dynamic type $\star$ is to view it as the following recursive type: \[ \star \equiv \mu \, d.\, \mathsf{Int} + \mathsf{Bool} + (d \to d) \] (See, for example, the chapter on Dynamic Typing in Robert Harper's textbook Practical Foundations for Programming Languages.) In such an interpretation, one can directly convert from $\star \to \star$ to $\star$, but not, for example, from $\mathsf{Int}\to\mathsf{Int}$ to $\star$. Instead, one must first convert from $\mathsf{Int}\to\mathsf{Int}$ to $\star \to \star$ and then to $\star$.

Let I be the subset of types that can be directly injected into $\star$: \[ I ::= B \mid \star \to \star \] The definition of values for Lazy UD changes to use I instead of T for the values of type $\star$. \[ \begin{array}{lrcl} \text{values} & v \in V & ::= & k \mid F \mid v : I \Rightarrow^\ell \star \mid v : T_1 \to T_2 \Rightarrow^\ell T_3 \to T_4 \end{array} \] This change in the definition of value necessitates some changes in the cast function. The second and third-to-last lines below contain most of the changes. \begin{align*} \mathsf{cast}(v,T_1,\ell,T_2) &= \mathbf{blame}\,\ell \qquad \text{if } \mathit{hd}(T_1) \not\sim \mathit{hd}(T_2) \\ \mathsf{cast}(v,B,\ell,B) &= v \\ \mathsf{cast}(v,\star,\ell,\star) &= v \\ \mathsf{cast}(v,\star,\ell,T_2) &= \mathbf{case}\,v\,\mathbf{of}\, (v' : I \Rightarrow^{\ell'} \star) \Rightarrow \\ & \qquad \mathsf{cast}(v',I,\ell,T_2) \\ \mathsf{cast}(v,I,\ell,\star) &= v : I \Rightarrow^\ell \star \\ \mathsf{cast}(v,T_{11}\to T_{12},\ell,\star) &= v : T_{11}\to T_{12} \Rightarrow^\ell \star \to \star \Rightarrow^\ell \star \\ & \text{if } T_{11} \neq \star, T_{12} \neq \star \\ \mathsf{cast}(v,T_{11}\to T_{12},\ell,T_{21}\to T_{22}) &= v : T_{11}\to T_{12} \Rightarrow^\ell T_{21}\to T_{22} \end{align*}

The rest of the definitions for Lazy UD are the same as those for Lazy D. The following is the subtyping relation for Lazy UD. With this subtyping relation, the type \(\star\) does not play the role of the top element. Instead, a type $T$ is a subtype of \(\star\) if it is a subtype of some injectable type \(I\). \begin{gather*} \frac{}{\star <: \star} \qquad \frac{T <: I}{T <: \star} \qquad \frac{}{B <: B} \qquad \frac{T_3 <: T_1 \quad T_2 <: T_4}{T_1 \to T_2 <: T_3 \to T_4} \end{gather*}

Theorem (Subtyping) If the cast labeled with \(\ell\) in program \(e\) respects subtyping, then \(\mathit{eval}(e) \neq \mathbf{blame}\,\ell\).

Exercise: Calculate the output of the Lazy UD eval for the example program at the beginning of this post.

In the next post I'll turn to the efficient implementation of Lazy D and UD.

Rationale for "Type Safety in Five"

In my last post Type Safety in Five Easy Lemmas, I made a claim that the formulation of the operational semantics of a language makes a big difference regarding how many lemmas, and how tedious, the proof of type safety becomes. While I showed that the particular semantics that I used led to a simple proof, with just five easy lemmas, I didn't compare it to the alternatives. Perhaps there's an even better alternative! In this post I discuss the alternatives that I know about and why they lead to more lemmas and more tedium. This post is organized by design decision.

Why A-normal form?

The syntax of the little language is in A-normal form, that is, it's flattened out so that expressions don't have sub-expressions, but instead, more complex computations have to be built up from several variable assignments. It's much more common to see type-safety proofs on languages that are not in A-normal form, that is, languages with arbitrary nesting of expressions. This nesting of expressions can be handled in one of two ways in the operational semantics: either with extra so-called congruence reduction rules or by using evaluation contexts. The congruence rule approach adds many more cases to the "$\longmapsto$ is safe" lemma (or equivalently, the progress and preservation lemmas). The evaluation contexts approach requires an extra lemma often called the unique decomposition lemma.

You might be thinking, real languages aren't in A-normal form, so one would really need to compile to A-normal form and prove that the compilation is type preserving (as we did in the Work Horse post). This is true, but I'd argue that it's nice to have a separation of concerns and take care of intra-expression control flow in one function and lemma instead of dealing with it throughout the operational semantics and proof of type safety.

Why environments instead of substitution?

The operational semantics passed around environments that associated values with variables and used the $\mathit{lookup}$ function to find the value for a variable. The more common alternative is to perform substitution, that is, during a function call, to go through the body of the function replacing occurrences of the parameters with their arguments. I'll probably get flamed for saying this, but substitution has a lot of disadvantages compared to environments. First, the substitution function is difficult to define properly. Second, it requires that you prove that substitution is type preserving, which is rather tedious because it touches every kind of expression (or statement) in the language. In comparison, the lemma that we proved about the $\mathit{lookup}$ function didn't mention any expressions. Third, substitution is really slow. Technically, that doesn't effect the complexity of the proof, but it does affect your ability to test your theorems. As I mentioned in the Work Horse post, it's a good idea to implement an interpreter and test whether your theorems hold on lots of example programs before trying to prove your theorems. If your interpreter uses substitution, it will be very very slow. You might instead use environments, but keep substitution in your formal semantics, but then your interpreter and your formal semantics differ so that properties of one may not imply properties of the other.

Why functions with names (for recursion) instead of fix?

The only way that I know of to implement fix, the fixpoint combinator, is with substitution, and we don't want substitution.

Also, I should highlight how we handle recursion in the operational semantics. First, the $\mathcal{V}$ function doesn't do much, it just captures the current environment. An alternative used by Milner and Tofte is to extend the environment with a binding for the function itself. This alternative makes the proof of type safety more challenging because, instead of using induction, you have to use coinduction. (See their paper Co-induction in relational semantics.) While coinduction is a beautiful concept, it's nice to be able to stick to good old induction. Now, because $\mathcal{V}$ doesn't do much, we need to make up for it in the transition relation. Notice that the transition for function call extends the environment with the function itself. I forget where I learned this trick. If you know of any references for this, please let me know!

Conclusion

I think that's it for the important design decisions, but I may be forgetting something. If you have any questions regarding the rationale for anything else, please post a comment! So to sum up, if you want your type safety proof to be less tedious, I recommend using A-normal form and formulating your semantics as an environment-passing abstract machine. Oh, and if you want recursive functions, than extend your lambdas with a name and be lazy about extending the environment: wait until the function call to add the function itself to the environment.

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.

The Work Horse of PL Theory: Structural Induction

The main idea in the Crash Course post was that we can define infinite sets and relations by giving a list of rules (some of which are recursive), that is, by giving an inductive definition. Such inductive definitions are used everywhere. In the crash course we used them to define the syntax of the language, the operational semantics, and the type system.

Once you define a programming language, the next step is to implement an interpreter or compiler and write lots of programs. The point of this, from the design point of view, is to make sure that your definition actually matches your intuitions about how your language should behave. Once you're reasonably happy with the definition of the language, you might want to gain further confidence in the design by proving that the language has the properties that you think it should. For example, you might want reduction to be deterministic, so you would try prove that for each program there is one unique reduction sequence. Another property that you might want is type safety, which means that values aren't misused but also includes things like memory safety (no segmentation faults, buffer overruns, etc.).

It may seem rather daunting to consider proving something about all possible programs. After all, there's an infinite number of them! Fortunately, if we use inductive definitions to specify our languages, then there's a proof technique called structural induction that we can use to prove things about them.

A Simple Example

Let's begin with an example of using structural induction on the relation $R$ that we defined in the Crash Course. Recall that this relation was defined by the following two rules.

• $(0,1) \in R$.
• For any natural numbers $n$ and $m$, if $(n,m) \in R$, then $(n+1,m+1) \in R$.

Also recall that we had informally described this relation as mapping each natural number to its successor. The following is the formal version of that statement. $$\forall x\, y.\, (x,y) \in R \to y = x + 1$$ Now how would we go about proving this statement mathematically?

A proof by structural induction creates a recipe for proving the property of interest for any element of the set. The recipe includes a case for each rule in the inductive definition of the set. Because every element in the set is the root of a tree of rule applications (a derivation), the recipe can be applied to each node in the tree, starting at the leaves, to eventually build a proof for the element at the root.

But it's easy to get lost in generalities, so let's get back to our example and build a recipe for generating a proof that $y = x + 1$ for any pair $(x,y) \in R$.

1. We need to give a proof that $y = x + 1$ for the case where $x=0,y=1$, so by simple arithmetic we have $1 = 0 + 1$.
2. The second rule in the definition of $R$ is more interesting. We're going to give a recipe for creating a proof of $y = x + 1$ for the element in the conclusion of this rule, $(n+1,m+1) \in R$, out of the proof of $y = x + 1$ for the premise of this rule, $(n,m) \in R$. That is, we need to take a proof of $m=n+1$ and create a proof of $m+1=(n+1)+1$. Of course, that's really easy: we just add one to both sides!

So we've created a recipe that includes cases for all of the rules that defined the relation $R$. Furthermore, in the second case, we didn't assume anything about $n$ or $m$, so we can apply the second case in lots of different situations. Now let's see how this recipe can be used to create proofs for elements of $R$. In the Crash Course, we built a derivation that showed $(2,3) \in R$. The derivation started with $(0,1) \in R$ (by rule 1), then had $(1,2) \in R$ (by rule 2), and finally $(2,3) \in R$ (by rule 2). Now let's apply our proof recipe to each of these steps. We have $1 = 0 + 1$ by case 1 above, then $2 = 1 + 1$ by case 2, and finally $3 = 2 + 1$ again by case 2. Thus, we've seen that our property holds for one element of the relation, namely for $(2,3)$. However, this process would have worked for any element of $R$. Thus, the above two recipes can be taken as enough to prove that $y = x + 1$ for every pair $(x,y) \in R$.

A More Interesting Example

Let's now move on to an example of a proof about programming languages. In the post My new favorite abstraction machine, I wrote down a translation that puts the simply-typed lambda calculus (STLC) into A-normal form (ANF) and then defined an abstract machine that operates on the ANF. The proof of type safety for this definition of the STLC includes two parts: the first shows that the translation of a well-typed program always produces a well-typed program in ANF and the second part proves that the ANF is type safe, that is, the abstract machine doesn't get stuck. Let's prove the first part by structural induction. Formally, what we'd like to prove is $$\forall e\,T. (\emptyset \vdash e : T) \to (\emptyset; T \models \mathit{ToANF}(e))$$ where $\emptyset \vdash e : T$ refers to the type system for STLC (see the definition here) and $\emptyset; T \models \mathit{ToANF}(e)$ is the type system for ANF statements. We have not yet given a definition of the type system for ANF statements, definitions, or expressions, so we must pause here to do so. We make one small change to the syntax of ANF statements to make the proof go through easier, allowing a sequence of declarations in a statement: replacing the statement $d; s$ with $\overline{d}; s$. $$\begin{gather*} \Gamma \models c : \mathit{typeof}(c) \quad \frac{ (x,T) \in \Gamma }{ \Gamma \models x : T } \quad \frac{ \Gamma,x{:}T_1 ; T_2 \models s }{ \Gamma \models (\lambda x{:}T_1.\, s) : T_1 \to T_2 } \\[3ex] \frac{ \Gamma \models e_1 : T_1 \to T_2 \quad \Gamma \models e_2 : T_1 }{ \Gamma \models x = e_1(e_2) \Rightarrow \{ (x,T_2) \} } \\[2ex] \frac{ \Gamma \models \overline{e} : \overline{T} \quad \Delta(\mathit{op},\overline{T}) = T }{ \Gamma \models x = \mathit{op}(\overline{e}) \Rightarrow \{ (x,T) \} } \\[3ex] \Gamma \models \epsilon \Rightarrow \emptyset \quad \frac{ \Gamma \models d \Rightarrow \Gamma' \quad \Gamma \cup \Gamma' \models \overline{d} \Rightarrow \Gamma'' }{ \Gamma \models d \, \overline{d} \Rightarrow \Gamma' \cup \Gamma'' } \\[3ex] \frac{ \Gamma \models \overline{d} \Rightarrow \Gamma' \quad \Gamma \cup \Gamma'; T \models s }{ \Gamma; T \models \overline{d}; s } \quad \frac{ \Gamma \models e : T }{ \Gamma; T \models \mathbf{return}\,e } \end{gather*}$$

The ToANF function is defined in terms of a recursive function ANF. It typically helps to prove something separately for each function, so let's try to come up with a lemma about ANF that will help prove that ToANF preserves types. Looking at the definition of ToANF, what we'd like to be true is the following property. $$\forall e\,T. (\emptyset \vdash e : T) \to \exists e' \overline{d}.\, \mathit{ANF}(e) = (e',\overline{d}) \land (\emptyset; T \models \overline{d}; \mathbf{return}\,e')$$ Let's see if we can prove this by structural induction. (We won't be able to but the failure will point out what minor modifications need to be made.)

A First Attempt

Our first choice is what to do structural induction on. There's several things in the above statement defined using inductive definitions. The expression $e$ and the typing derivation $\emptyset \vdash e : T$ are both good candidates because they appear to the left of the implication. Let's do induction on the typing derivation because that tends to give us more ammunition than induction on the structure of expressions.

There are five rules that define the typing relation for the STLC, so we'll need five cases.

1. Case $$\frac{ (x,T) \in \emptyset }{ \emptyset \vdash x : T }$$ The premise $(x,T) \in \emptyset$ is false, so this case is vacuously true. However, this should make us start to worry, something fishy is going on.
2. Case $$\frac{ \emptyset,x{:}T_1 \vdash e' : T_2 }{ \emptyset \vdash \lambda x{:}T_1.\, e' : T_1 \to T_2 }$$ The proof recipe for this case needs to take a proof for the premise and create a proof for the conclusion. However, our property doesn't apply to the premise because the type environment $\emptyset,x{:}T_1$ isn't empty. At this point we're stuck and we must have the good sense to give up this proof attempt.

A Successful Structural Induction

But what have we learned? What we're trying to prove must not fix the type environment as being empty, but needs to work with any type environment. Let's reformulate the property with an arbitrary $\Gamma$ replacing the $\emptyset$. $$\forall \Gamma\,e\,T. (\Gamma \vdash e : T) \to \exists e' \overline{d}.\, \mathit{ANF}(e) = (e',\overline{d}) \land (\Gamma; T \models \overline{d}; \mathbf{return}\,e')$$ Let's try the proof by induction on $\Gamma \vdash e : T$ again.

1. Case $$\frac{ (x,T) \in \Gamma }{ \Gamma \vdash x : T }$$ We have $\mathit{ANF}(x) = (x,\epsilon)$, so we need to show that $\mathbf{return}\,x$ is well typed. From $(x,T) \in \Gamma$ we have $\Gamma \models x : T$ and therefore $\Gamma; T \models \mathbf{return}\,x$.
2. Case $$\frac{ \Gamma,x{:}T_1 \vdash e' : T_2 }{ \Gamma \vdash \lambda x{:}T_1.\, e' : T_1 \to T_2 }$$ We have $\mathit{ANF}(\lambda x{:}T_1.\,e') = (F, \epsilon)$ where $F = \lambda x{:}T_1.\, (\overline{d}; \mathbf{return}\,e'')$ and $(e'',\overline{d}) = \mathit{ANF}(e')$. So we need to prove that $\Gamma; T_1 \to T_2 \models \mathbf{return}\,F$ and so it suffices to prove that $\Gamma \models F : T_1 \to T_2$. Our recipe for this case takes as input a proof for the premise, so we know that $$\begin{align*} &(\Gamma,x{:}T_1 \vdash e' : T_2) \to \\ & \exists e'' \overline{d}.\, \mathit{ANF}(e') = (e'',\overline{d}) \land (\Gamma,x{:}T_1; T_2 \models \overline{d}; \mathbf{return}\,e'') \end{align*}$$ (The statement is called an induction hypothesis. It's always a good idea to write out an induction hypothesis carefully because it's easy to get it wrong. To get an induction hypothesis right, just instantiate the forall in the property you are trying to prove with the appropriate variables from the premise. Do this mechanically; thinking about it too much can lead to errors! Also, always tell your reader when you're using the induction hypothesis; think of it as the climax of the case!)

   Because $\mathit{ANF}$ is a function (in the mathematical sense), we know that the $e''$ and $\overline{d}$ in the existential must be the same as the variables of the same name in our current proof. So our induction hypothesis tells us that $\Gamma,x{:}T_1; T_2 \models (\overline{d}; \mathbf{return}\, e'')$. We then just apply the typing rule for lambda's to prove our goal, that $\Gamma \models F : T_1 \to T_2$.

3. Case $$\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 }$$ We have $\mathit{ANF}(e_1\,e_2) = (x,\overline{d}_1 \overline{d}_2; x=e'_1(e'_2))$, where $(e'_1,\overline{d}_1) = \mathit{ANF}(e_1)$, $(e'_2,\overline{d}_1) = \mathit{ANF}(e_2)$, and $x$ is a fresh variable. We need to prove that $$\Gamma; T_2 \models \overline{d}_1 \overline{d}_2; x=e'_1(e'_2); \mathbf{return}\,x$$ We have two induction hypotheses, one for each premise: $$\begin{align*} & (\Gamma \vdash e_1 : T_1\to T_2) \to \\ & \exists e'_1 \overline{d}_1.\, \mathit{ANF}(e_1) = (e'_1,\overline{d}_1) \land (\Gamma; T_1\to T_2 \models \overline{d}_1; \mathbf{return}\,e'_1) \end{align*}$$ and $$\begin{align*} & (\Gamma \vdash e_2 : T_1) \to \\ & \exists e'_2 \overline{d}_2.\, \mathit{ANF}(e_2) = (e'_2,\overline{d}_2) \land (\Gamma; T_1 \models \overline{d}_2; \mathbf{return}\,e'_2) \end{align*}$$ So we have $\Gamma \models \overline{d}_1 \Rightarrow \Gamma_1$ and $\Gamma \cup \Gamma_1 \models e'_1 : T_1 \to T_2$ from the first induction hypothesis (IH for short). We have $\Gamma \models \overline{d}_2 \Rightarrow \Gamma_2$ and $\Gamma \cup \Gamma_2 \models e'_2 : T_1$ from the second IH. Looking back at what we need to prove, there's a bit of a jump that needs to happen to get us from $\overline{d}_1$ and $\overline{d}_2$ being well-typed separately to their concatenation being well typed. Let's posit the following lemma: $$\Gamma \models \overline{d}_1 \Rightarrow \Gamma_1 \land \Gamma \models \overline{d}_2 \Rightarrow \Gamma_2 \to \Gamma \models \overline{d}_1 \overline{d}_2 \Rightarrow \Gamma_1 \cup \Gamma_2$$ under the assumption that the variables on the left-hand sides are all distinct. Also, we need to show that $$\Gamma \cup \Gamma_1 \cup \Gamma_2 \models x = e'_1(e'_2) \Rightarrow \{(x,T_2)\}$$ Again there's a bit of a jump that needs to happen. This time, the problem is that we know $e'_1$ and $e'_2$ are well typed in smaller environments (missing $\Gamma_2$ in the former case and missing $\Gamma_1$ in the later). So we need a lemma that tells us it is ok to add more variables to the environment so long as those variables to don't interfere with variables that are already there. This lemma comes up so frequently it has a special name. It is know as the Weakening Lemma. $$(\Gamma \models e : T) \land (\Gamma \subseteq \Gamma') \to (\Gamma' \models e :T)$$ Applying this lemma twice, we have $$\Gamma \cup \Gamma_1 \cup \Gamma_2 \models e'_1 : T_1 \to T_2$$ and $$\Gamma \cup \Gamma_1 \cup \Gamma_2 \models e'_2 : T_1$$ which gives us $$\Gamma \cup \Gamma_1 \cup \Gamma_2 \models x = e'_1(e'_2) \Rightarrow \{(x,T_2)\}$$ and then applying the concatenation lemma again, we have $$\Gamma \models \overline{d}_1 \overline{d}_2; x=e'_1(e'_2) \Rightarrow \Gamma_1 \cup \Gamma_2 \cup \{(x,T_2)\}$$ All that remains is to deal with the final $\mathbf{return}\,x$. But it's easy to see that $$\Gamma \cup \Gamma_1 \cup \Gamma_2 \cup \{ (x,T_2) \} \models x : T_2$$ so we can conclude this case, having shown that $$\Gamma; T_2 \models \overline{d}_1 \overline{d}_2; x=e'_1(e'_2); \mathbf{return}\,x$$

So far we've handled three of the five cases, so the proof is not yet complete. I'd encourage the reader to try and fill in the two remaining cases (for constants and primitive operators) and the two lemmas that we used. (Hint: use structural induction to prove the lemmas.)

Conclusion

If you define a set using an inductive definition, then you can prove stuff about every element of the set (even if the set is infinite!) by structural induction. To do this, create a recipe that includes a case for each rule in the inductive definition. Your recipe for each case takes as input the proof for the premises and it should output a proof for the conclusion of the rule. That's all it takes! Just make sure not to skip any cases and be extra careful with the induction hypotheses!