Revisiting "well-typed programs cannot go wrong"

Robin Milner proved that well-typed programs cannot go wrong in his 1978 paper A Theory of Type Polymorphism in Programming (Milner 1978). That is, he defined a type system and denotational semantics for the Exp language (a subset of ML) and then proved that the denotation of a well-typed program in Exp is not the “wrong” value. The “wrong” denotation signifies that a runtime type error occurred, so Milner’s theorem proves that the type system is strong enough to prevent all the runtime type errors that could occur in an Exp program. The denotational semantics used by Milner (1978) was based on the standard domain theory for an explicitly typed language with higher-order functions.

I have been exploring, over the last month, whether I can prove a similar theorem but using my new denotational semantics, and mechanize the proof in the Isabelle proof assistant. At first I tried to stay as close to Milner’s proof as possible, but in the process I learned that Milner’s proof is rather syntactic and largely consists of proving lemmas about how substitution interacts with the type system, which does not shed much light on the semantics of polymorphism.

Last week I decided to take a step back and try a more semantic approach and switch to a cleaner but more expressive setting, one with first-class polymorphism. So I wrote down a denotational semantics for System F (Reynolds 1974) extended with support for general recursion. The proof that well-typed programs cannot go wrong came together rather quickly. Today I finished the mechanization in Isabelle and it came in at just 539 lines for all the definitions, lemmas, and main proof. I’m excited to share the details of how it went! Spoiler: the heart of the proof turned out to be a lemma I call Compositionality because it looks a lot like the similarly-named lemma that shows up in proofs of parametricity.

Syntax

The types in the language include natural numbers, function types, universal types, and type variables. Regarding the variables, after some experimentation with names and locally nameless, I settled on good old DeBruijn indices to represent both free and bound type variables. $$\begin{array}{rcl} i,j & \in & \mathbb{N} \\ \sigma,\tau & ::= & \mathtt{nat} \mid \tau \to \tau \mid \forall\,\tau \mid i \end{array}$$ So the type of the polymorphic identity function, normaly written $\forall \alpha.\, \alpha \to \alpha$, is instead written $\forall \left(0 \to 0\right)$.

The syntax of expressions is as follows. I choose to use DeBruijn indices for term variables as well, and left off all type annotations, but I don’t think that matters for our purposes here. $$\begin{array}{rcl} n & \in & \mathbb{N} \\ e & ::= & n \mid i \mid \lambda e \mid e\; e \mid \Lambda e \mid e [\,] \mid \mathtt{fix}\, e \end{array}$$

Denotational Semantics

The values in this language, described by the below grammar, include natural numbers, functions represented by finite lookup tables, type abstractions, and $\mathsf{wrong}$ to represent a runtime type error. $$\begin{array}{rcl} f & ::= & \{ (v_1,v'_1), \ldots, (v_n,v'_n) \} \\ o & ::= & \mathsf{none} \mid \mathsf{some}(v) \\ v & ::= & n \mid \mathsf{fun}(f) \mid \mathsf{abs}(o) \mid \mathsf{wrong} \end{array}$$ A type abstraction $\mathsf{abs}(o)$ consists of an optional value, and not simply a value, because the body of a type abstraction might be a non-terminating computation.

We define the following information ordering on values so that we can reason about one lookup table being more or less-defined than another lookup table. We define $v \sqsubseteq v'$ inductively as follows.

$$\begin{gathered} n \sqsubseteq n \quad \frac{f_1 \subseteq f_2} {\mathsf{fun}(f_1) \sqsubseteq \mathsf{fun}(f_2)} \quad \mathsf{wrong} \sqsubseteq\mathsf{wrong} \\ \mathsf{abs}(\mathsf{none}) \sqsubseteq\mathsf{abs}(\mathsf{none}) \quad \frac{v \sqsubseteq v'} {\mathsf{abs}(\mathsf{some}(v)) \sqsubseteq\mathsf{abs}(\mathsf{some}(v'))}\end{gathered}$$

The denotational semantics maps an expression to a set of values. Why a set and not just a single value? A single finite lookup table is not enough to capture the meaning of a lambda, but an infinite set of finite tables is. However, dealing with sets is somewhat inconvenient, so we mitigate this issue by working in a set monad. Also, to deal with $\mathsf{wrong}$ we need an error monad, so we use a combined set-and-error monad.

$$\begin{aligned} X := E_1 ; E_2 &\equiv \{ v \mid \exists v'. \, v' \in E_1, v' \neq \mathsf{wrong}, v \in E_2[v'/X] \} \\ & \quad \cup \{ v \mid v = \mathsf{wrong}, \mathsf{wrong} \in E_1 \} \\ \mathsf{return}(E) & \equiv \{ v \mid v \sqsubseteq E \} \\ X \leftarrow E_1; E_2 & \equiv \{ v \mid \exists v'.\, v' \in E_1, v \in E_2[v'/X]\}\end{aligned}$$

The use of $\sqsubseteq$ in $\mathsf{return}$ is to help ensure that the meaning of an expression is downward-closed with respect to $\sqsubseteq$. (The need for which is explained in prior blog posts.)

Our semantics will make use of a runtime environment $\rho$ that includes two parts, $\rho_1$ and $\rho_2$. The first part gives meaning to the term variables, for which we use a list of values (indexed by their DeBruijn number). The second part, for the type variables, is a list containing sets of values, as the meaning of a type will be a set of values. We define the following notation for dealing with runtime environments.

$$\begin{aligned} v{::}\rho \equiv (v{::}\rho_1, \rho_2) \\ V{::}\rho \equiv (\rho_1, V{::}\rho_2)\end{aligned}$$

We write $\rho[i]$ to mean either $\rho_1[i]$ or $\rho_2[i]$, which can be disambiguated based on the context of use.

To help define the meaning of $\mathtt{fix}\,e$, we inductively define a predicate named $\mathsf{iterate}$. Its first parameter is the meaning $L$ of the expression $e$, which is a mapping from an environment to a set of values. The second parameter is a runtime environment $\rho$ and the third parameter is a value that is the result of iteration.

$$\begin{gathered} \mathsf{iterate}(L, \rho, \mathsf{fun}(\emptyset)) \quad \frac{\mathsf{iterate}(L, \rho, v) \quad v' \in E(v{::}\rho)} {\mathsf{iterate}(L, \rho, v')}\end{gathered}$$

To help define the meaning of function application, we define the following $\mathsf{apply}$ functiion. $$\mathsf{apply}(V_1,V_2) \equiv \begin{array}{l} x_1 := V_1; \\ x_2 := V_2; \\ \mathsf{case}\,x_1\,\textsf{of}\\ \;\; \mathsf{fun}(f) \Rightarrow (x'_2,x'_3) \leftarrow f; \mathsf{if}\, x'_2 \sqsubseteq x_2 \, \mathsf{then}\, x'_3 \,\mathsf{else}\, \emptyset \\ \mid \_ \Rightarrow \mathsf{return}(\mathsf{wrong}) \end{array}$$

The denotational semantics is given by the following function $E$ that maps an expression and environment to a set of values.

$$\begin{aligned} E[ n ]\rho &= \mathsf{return}(n) \\[1ex] E[ i ]\rho &= \mathsf{return}(\rho[i]) \\[1ex] E[ \lambda e ]\rho &= \{ v \mid \exists f.\, v = \mathsf{fun}(f), \forall v_1 v'_2.\, (v_1,v'_2) \in f \Rightarrow \\ & \qquad\qquad \exists v_2.\, v_2 \in E[ e ] (v_1{::}\rho), v'_2 \sqsubseteq v_2\} \\[1ex] E[ e_1\; e_2 ] \rho &= \mathsf{apply}(E[ e_1 ]\rho, E[ e_2 ]\rho) \\[1ex] E[ \mathtt{fix}\,e ] \rho &= \{ v \mid \mathsf{iterate}(E[ e ], \rho, v) \} \\[1ex] E[ \Lambda e ] \rho &= \{ v \mid \exists v'.\, v = \mathsf{abs}(\mathsf{some}(v')), \forall V. v' \in E[ e ] (V{::}\rho) \} \\ & \quad\; \cup \{ v \mid v = \mathsf{abs}(\mathsf{none}), \forall V. E[ e ](V{::}\rho) = \emptyset \} \\[1ex] E[ e [\,] ] \rho &= \begin{array}{l} x := E [ e ] \rho;\\ \mathsf{case}\,x\,\mathsf{of} \\ \;\; \mathsf{abs}(\mathsf{none}) \Rightarrow \emptyset \\ \mid \mathsf{abs}(\mathsf{some}(v')) \Rightarrow \mathsf{return}(v') \\ \mid \_ \Rightarrow \mathsf{return}(\mathsf{wrong}) \end{array}\end{aligned}$$

We give meaning to types with the function $T$, which maps a type and an environment to a set of values. For this purposes, we only need the second part of the runtime environment which gives meaning to type variables. Instead of writing $\rho_2$ everywhere, we’ll use the letter $\eta$. It is important to ensure that $T$ is downward closed, which requires some care either in the definition of $T[ \forall \tau ]\eta$ or in the definition of $T[ i ]\eta$. We have chosen to do this work in the definition of $T[ i ]\eta$, and let the definition of $T[ \forall \tau ]\eta$ quantify over any set of values $V$ to give meaning to it’s bound type variable.

$$\begin{aligned} T[ \mathtt{nat} ] \eta &= \mathbb{N} \\ T[ i ] \eta &= \begin{cases} \{ v \mid \exists v'.\, v' \in \eta[i], v \sqsubseteq v',v \neq \mathsf{wrong} \} &\text{if } i < |\eta| \\ \emptyset & \text{otherwise} \end{cases} \\ T[ \sigma\to\tau ] \eta &= \{ v\mid \exists f. \,v=\mathsf{fun}(f), \forall v_1 v'_2.\, (v_1,v'_2) \in f, v_1 \in T[\sigma]\eta \\ & \hspace{1.5in} \Rightarrow \exists v_2.\, v_2 \in T[\tau]\eta, v'_2 \sqsubseteq v_2 \} \\ T[ \forall\tau ] \eta &= \{ v \mid \exists v'.\, v = \mathsf{abs}(\mathsf{some}(v')), \forall V.\, v' \in T[\tau ] (V{::}\eta) \} \cup \{ \mathsf{abs}(\mathsf{none}) \} \end{aligned}$$

Type System

Regarding the type system, it is standard except perhaps how we deal with the DeBruijn representation of type variables. We begin with the definition of well-formed types. A type is well formed if all the type variables in it are properly scoped, which is captured by their indices being below a given threshold (the number of enclosing type variable binders, that is, $\Lambda$’s and $\forall$’s). More formally, we write $j \vdash \tau$ to say that type $\tau$ is well-formed under threshold $j$, and give the following inductive definition.

$$\begin{gathered} j \vdash \mathtt{nat} \quad \frac{j \vdash \sigma \quad j \vdash \tau}{j \vdash \sigma \to \tau} \quad \frac{j+1 \vdash \tau }{j \vdash \forall \tau} \quad \frac{i < j}{j \vdash i}\end{gathered}$$

Our representation of the type environment is somewhat unusual. Because term variables are just DeBruijn indices, we can use a list of types (instead of a mapping from names to types). However, to keep track of the type-variable scoping, we also include with each type the threshold from its point of definition. Also, we need to keep track of the current threshold, so when we write $\Gamma$, we mean a pair where $\Gamma_1$ is a list and $\Gamma_2$ is a number. The list consists of pairs of types and numbers, so for example, $\Gamma_1[i]_1$ is a type and $\Gamma_1[i]_2$ is a number whenever $i$ is less than the length of $\Gamma_1$. We use the following notation for extending the type environment:

$$\begin{aligned} \tau :: \Gamma &\equiv ((\tau,\Gamma_2){::}\Gamma_1, \Gamma_2) \\ * :: \Gamma & \equiv (\Gamma_1, \Gamma_2 + 1)\end{aligned}$$

We write $\vdash \rho : \Gamma$ to say that environment $\rho$ is well-typed according to $\Gamma$ and define it inductively as follows.

$$\begin{gathered} \vdash ([],[]) : ([], 0) \quad \frac{\vdash \rho : \Gamma \quad v \in T[ \tau ] \rho_2} {\vdash v{::}\rho : \tau{::}\Gamma} \quad \frac{\vdash \rho : \Gamma} {\vdash V{::}\rho : *{::}\Gamma}\end{gathered}$$

The primary operation that we perform on a type environment is looking up the type associated with a term variable, for which we define the following function $\mathsf{lookup}$ that maps a type environment and DeBruijn index to a type. To make sure that the resulting type is well-formed in the current environment, we must increase all of its free type variables by the difference of the current threshold $\Gamma_2$ and the threshold at its point of definition, $\Gamma_1[i]_2$, which is accomplished by the shift operator $\uparrow^k_c(\tau)$ (Pierce 2002). $$\mathsf{lookup}(\Gamma,i) \equiv \begin{cases} \mathsf{some}(\uparrow^{k}_{0}(\Gamma_1[i]_1) & \text{if } n < |\Gamma_1| \\ & \text{where } k = \Gamma_2 - \Gamma_1[i]_2 \\ \mathsf{none} & \text{otherwise} \end{cases}$$

To review, the shift operator is defined as follows.

$$\begin{aligned} \uparrow^{k}_{c}(\mathtt{nat}) &= \mathtt{nat} \\ \uparrow^{k}_{c}(i) &= \begin{cases} i + k & \text{if } c \leq i \\ i & \text{otherwise} \end{cases} \\ \uparrow^{k}_{c}(\sigma \to \tau) &= \uparrow^{k}_{c}(\sigma) \to \uparrow^{k}_{c}(\tau) \\ \uparrow^{k}_{c}(\forall \tau) &= \forall\, \uparrow^{k}_{c+1}(\tau)\end{aligned}$$

Last but not least, we need to define type substitution so that we can use it in the typing rule for instantiation (type application). We write $[j\mapsto \tau]\sigma$ for the substitution of type $\tau$ for DeBruijn index $j$ within type $\sigma$ (Pierce 2002).

$$\begin{aligned} [j\mapsto \tau]\mathtt{nat} &= \mathtt{nat} \\ [j\mapsto\tau]i &= \begin{cases} \tau & \text{if } j = i \\ i - 1 & \text{if } j < i \\ i & \text{otherwise} \end{cases}\\ [j\mapsto\tau](\sigma\to\sigma') &= [j\mapsto\tau]\sigma \to [j\mapsto \tau]\sigma' \\ [j\mapsto \tau]\forall\sigma &= \forall\, [j+1 \mapsto \uparrow^{1}_{0}(\tau)]\sigma\end{aligned}$$

Here is the type system for System F extended with $\mathtt{fix}$.

$$\begin{gathered} \Gamma \vdash n : \mathtt{nat} \qquad \frac{\mathsf{lookup}(\Gamma,i) = \mathsf{some}(\tau)} {\Gamma \vdash i : \tau} \\[2ex] \frac{\Gamma_2 \vdash \sigma \quad \sigma{::}\Gamma \vdash e : \tau} {\Gamma \vdash \lambda e : \sigma \to \tau} \qquad \frac{\Gamma \vdash e : \sigma \to \tau \quad \Gamma \vdash e' : \sigma} {\Gamma \vdash e \; e' : \tau} \\[2ex] \frac{\Gamma_2 \vdash \sigma \to \tau \quad (\sigma\to \tau){::}\Gamma \vdash e : \sigma \to \tau } {\Gamma \vdash \mathtt{fix}\,e : \sigma \to \tau} \\[2ex] \frac{*::\Gamma \vdash e : \tau} {\Gamma \vdash \Lambda e :: \forall\tau} \qquad \frac{\Gamma \vdash e : \forall \tau} {\Gamma \vdash e[\,] : [0\mapsto\sigma]\tau}\end{gathered}$$

We say that a type environment $\Gamma$ is well-formed if $\Gamma_2$ is greater or equal to every threshold in $\Gamma_1$, that is $\Gamma_1[i]_2 \leq \Gamma_2$ for all $i < |\Gamma_1|$.

Proof of well-typed programs cannot go wrong

The proof required 6 little lemmas and 4 big lemmas. (There were some itsy bitsy lemmas too that I’m not counting.)

Little Lemmas

Lemma [$\sqsubseteq$ is a preorder]  

• $v \sqsubseteq v$

• If $v_1 \sqsubseteq v_2$ and $v_2 \sqsubseteq v_3$, then $v_1 \sqsubseteq v_3$.

[lem:less-refl] [lem:less-trans]

I proved transitivity by induction on $v_2$.

Lemma [$T$ is downward closed] If $v \in T [ \tau ] \eta$ and $v' \sqsubseteq v$, then $v' \in T [ \tau ] \eta$. [lem:T-down-closed]

The above is a straightforward induction on $\tau$

Lemma [$\mathsf{wrong}$ not in $T$] For any $\tau$ and $\eta$, $\mathsf{wrong} \notin T [ \tau ] \eta$. [lem:wrong-not-in-T]

The above is another straightforward induction on $\tau$

Lemma If $\vdash \rho : \Gamma$, then $\Gamma$ is a well-formed type environment. [lem:wfenv-good-ctx]

The above is proved by induction on the derivation of $\vdash \rho : \Gamma$.

Lemma $$T [ \tau ] (\eta_1 \eta_3) = T [ \uparrow^{|\eta_2|}_{ |\eta_1|}(\tau) ] (\eta_1\eta_2\eta_3)$$

The above lemma is proved by induction on $\tau$. It took me a little while to figure out the right strengthening of the statement of this lemma to get the induction to go through. The motivations for this lemma were the following corollaries.

Corollary [Lift/Append Preserves $T$] $$T [ \tau ](\eta_2) = T [ \uparrow^{|\eta_1|}_{0}(\tau) ] (\eta_1\eta_2)$$ [lem:lift-append-preserves-T]

Corollary[Lift/Cons Preserves $T$] $$T [ \tau ] (\eta) = T [ \uparrow^{1}_{0}(\tau) ] (V{::}\eta)$$ [lem:shift-cons-preserves-T]

Of course, two shifts can be composed into a single shift by adding the amounts.

Lemma [Compose Shift] $$\uparrow^{j+k}_{c}(\tau) = \uparrow^{j}_{c}( \uparrow^{k}_{c}(\tau))$$ [lem:compose-shift]

The proof is a straightforward induction on $\tau$.

Big Lemmas

There are one or two big lemmas for each of the “features” in this variant of System F.

The first lemma shows that well-typed occurrences of term variables cannot go wrong.

Lemma [Lookup in Well-typed Environment] 
If $\vdash \rho : \Gamma$ and $\mathsf{lookup}(\Gamma,i) = \mathsf{some}(\tau)$, then $\exists v.\, \rho_1[i] = v$ and $v \in T [ \tau ] \rho_2$. [lem:lookup-wfenv]

The proof is by induction on the derivation of $\vdash \rho : \Gamma$. The first two cases were straightforward but the third case required some work and used lemmas [lem:wfenv-good-ctx], [lem:shift-cons-preserves-T], and [lem:compose-shift].

Lemma [Application cannot go wrong] If $V \subseteq T [ \sigma \to \tau ] \eta$ and $V' \subseteq T [ \sigma ] \eta$, then $\mathsf{apply}(V,V') \subseteq T [ \tau ] \eta$. [lem:fun-app]

The proof of this lemma is direct and does not use induction. However, it does use lemmas [lem:wrong-not-in-T] and [lem:T-down-closed].

Lemma [Compositionality] Let $V = T [ \sigma ] (\eta_1\eta_2)$. $$T [ \tau ] (\eta_1 V \eta_2) = T [ \tau[\sigma/|\eta_1|] ] (\eta_1 \eta_2)$$ [lem:compositionality]

I proved the Compositionality lemma by induction on $\tau$. All of the cases were straightforward except for $\tau=\forall\tau'$. In that case I used the induction hypothesis to show that $$T [ \tau' ] (V \eta_1 S \eta_2) = T [ ([|V\eta_1|\mapsto \uparrow^1_0(\sigma)] \tau' ] (V\eta_1\eta_2) \text{ where } S = T [ \uparrow^1_0(\sigma) ] (V\eta_1\eta_2)$$ and I used Lemma [lem:shift-cons-preserves-T].

Lemma [Iterate cannot go wrong] If

• $\mathsf{iterate}(L,\rho,v)$ and

• for any $v'$, $v' \in T[ \sigma\to\tau ] \rho_2$ implies $L(v'{::}\rho) \subseteq T[ \sigma\to\tau ] \rho_2$,

then $v \in T [ \sigma \to \tau ] \rho_2$. [lem:iterate-sound]

This was straightfroward to prove by induction on the derivation of $\mathsf{iterate}(L,\rho,v)$. The slightly difficult part was coming up with the definition of $\mathsf{iterate}$ to begin with and in formulating the second premise.

The Theorem

Theorem [Well-typed programs cannot go wrong] 
If $\Gamma \vdash e : \tau$ and $\vdash \rho : \Gamma$, then $E [ e ] \rho \subseteq T[ \tau ] \rho_2$. [thm:welltyped-dont-go-wrong]

The proof is by induction on the derivation of $\Gamma \vdash e : \tau$.

• $\Gamma \vdash n : \mathtt{nat}$

  This case is immediate.

• $\frac{\mathsf{lookup}(\Gamma,i) = \mathsf{some}(\tau)} {\Gamma \vdash i : \tau}$

  Lemma [lem:lookup-wfenv] tells us that $\rho_1[i] = v$ and $v \in T [ \tau ] \rho_2$ for some $v$. We conclude by Lemma [lem:T-down-closed].

• $\frac{\Gamma_2 \vdash \sigma \quad \sigma{::}\Gamma \vdash e : \tau} {\Gamma \vdash \lambda e : \sigma \to \tau}$

  After unraveling some definitions, for arbitrary $f,v_1,v_2,v'_2$ we can assume $v_1 \in T [ \sigma ] \rho_2$, $v_2 \in E [ e ](v_1{::}\rho)$, and $v'_2 \sqsubseteq v_2$. We need to prove that $v_2 \in T [ \tau ] (v_1{::}\rho)_2$.

  We can show $\vdash v_1{::}\rho : \sigma{::}\Gamma$ and therefore, by the induction hypothesis, $E [ e ] (v_1{::}\rho) \subseteq T [ \tau ] (v_1{::}\rho)_2$. So we conclude that $v_2 \in T [ \tau ] (v_1{::}\rho)_2$.

• $\frac{\Gamma \vdash e : \sigma \to \tau \quad \Gamma \vdash e' : \sigma} {\Gamma \vdash e \; e' : \tau}$

  By the induction hypothesis, we have $E [ e ] \rho \subseteq T [ \sigma\to\tau ] \rho_2$ and $E [ e' ] \rho \subseteq T [ \sigma ] \rho_2$. We conclude by Lemma [lem:fun-app].

• $\frac{\Gamma_2 \vdash \sigma \to \tau \quad (\sigma\to \tau){::}\Gamma \vdash e : \sigma \to \tau } {\Gamma \vdash \mathtt{fix}\,e : \sigma \to \tau}$

  For an arbitrary $v$, we may assume $\mathsf{iterate}(E[ e ], \rho, v)$ and need to show that $v \in T [ \sigma\to\tau ]\rho_2$.

  In preparation to apply Lemma [lem:iterate-sound], we first prove that for any $v'$, $v' \in T[ \sigma\to\tau ] \rho_2$ implies $E[ e](v'{::}\rho) \subseteq T[ \sigma\to\tau ] \rho_2$. Assume $v'' \in E[ e](v'{::}\rho)$. We need to show that $v'' \in T[ \sigma\to\tau ] \rho_2$. We have $\vdash v'{::}\rho : (\sigma\to\tau){::}\Gamma$, so by the induction hypothesis $E [ e ](v'{::}\rho) \subseteq T[ \sigma\to\tau ](v'{::}\rho)$. From this we conclude that $v'' \in T[ \sigma\to\tau ] \rho_2$.

  We then apply Lemma [lem:iterate-sound] to conclude this case.

• $\frac{*::\Gamma \vdash e : \tau} {\Gamma \vdash \Lambda e :: \forall\tau}$

  After unraveling some definitions, for an arbitrary $v'$ and $V$ we may assume that $\forall V'.\, v' \in E [ e ](V{::}\rho)$. We need to show that $v' \in T [ \tau ] (V{::}\rho_2)$. We have $\vdash V{::}\rho : *{::}\Gamma$, so by the induction hypothesis $E[ e ](V{::}\rho) \subseteq T [ \tau ] (V{::}\rho)_2$. Also, from the assumption we have $v' \in E [ e ](V{::}\rho)$, so we can conclude.

• $\frac{\Gamma \vdash e : \forall \tau} {\Gamma \vdash e[\,] : [0\mapsto\sigma]\tau}$

  Fix a $v' \in E [ e ] \rho$. We have three cases to consider.

  1. $v'=\mathsf{abs}(\mathsf{none})$. This case is immediate.

  2. $v'=\mathsf{abs}(\mathsf{some}(v''))$ for some $v''$. By the induction hypothesis, $v' \in T [ \forall\tau ]\rho_2$. So we have $v'' \in T [ \tau ](V{::}\rho_2)$ where $V=T[\sigma]\rho_2$. Then by Compositionality (Lemma [lem:compositionality]) we conclude that $v'' \in T [ [0\mapsto \sigma]\tau]\rho_2$.

  3. $v'$ is some other kind of value. This can’t happen because, by the induction hypothesis, $v' \in T [ \forall\tau ]\rho_2$.

References

Milner, Robin. 1978. “A Theory of Type Polymorphism in Programming.” Journal of Computer and System Sciences 17 (3): 348–75.

Pierce, Benjamin C. 2002. Types and Programming Languages. MIT Press.

Reynolds, John C. 1974. “Towards a Theory of Type Structure.” In Programming Symposium: Proceedings, Colloque Sur La Programmation, 19:408–25. LNCS. Springer-Verlag.