An Introduction to Logical Relations

TL;DR

This paper provides an accessible introduction to logical relations, covering fundamental concepts and applications such as normalization, type safety, and reasoning about complex types, aimed at beginners with minimal prerequisites.

Contribution

It offers a beginner-friendly overview of logical relations, explaining core ideas and techniques without assuming prior specialized knowledge.

Findings

Logical relations can be used to prove normalization and type safety.

Relational substitutions help reason about universal and existential types.

Step-indexing and worlds are effective tools for reasoning about recursive types and references.

Abstract

Logical relations (LR) have been around for many years, and today they are used in many formal results. However, it can be difficult to LR beginners to find a good place to start to learn. Papers often use highly specialized LRs that use the latest advances of the technique which makes it impossible to make a proper presentation within the page limit. This note is a good starting point for beginners that want to learn about LRs. Almost no prerequisite knowledge is assumed, and the note starts from the very basics. The note covers the following: LRs for proving normalization and type safety of simply typed lambda calculus, relational substitutions for reasoning about universal and existential types, step-indexing for reasoning about recursive types, and worlds for reasoning about references.

Equations

$$\begin{array}[]{p{1cm} r l }\lx@intercol\textbf{Types:}\hfil\lx@intercol\\ &\tau::={}&\mathit{bool}\mid\tau\rightarrow\tau\\ \lx@intercol\textbf{Terms:}\hfil\lx@intercol\\ &e::={}&x\mid\texttt{true}\mid\texttt{false}\mid\texttt{if}\;e\;\texttt{then}\;e\;\texttt{else}\;e\mid\lambda x:\tau\ldotp\;e\mid e\;e\\ \lx@intercol\textbf{Values:}\hfil\lx@intercol\\ &v::={}&\texttt{true}\mid\texttt{false}\mid\lambda x:\tau\ldotp\;e\\ \lx@intercol\textbf{Evaluation Context:}\hfil\lx@intercol\\ &E::={}&[]\mid\texttt{if}\;E\;\texttt{then}\;e\;\texttt{else}\;e\mid E\;e\mid v\;E\\ \lx@intercol\textbf{Evaluations:}\hfil\lx@intercol\\ \lx@intercol\hfil\mathpar\inferrule{}{\texttt{if}\;\texttt{true}\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}\rightarrow e_{1}}\inferrule{}{\texttt{if}\;\texttt{false}\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}\rightarrow e_{2}}\inferrule{}{(\lambda x:\tau\ldotp\;e)\;v\rightarrow e[^{\textstyle v}/_{\textstyle x}]}\inferrule*[]{e\rightarrow e^{\prime}}{E[e]\rightarrow E[e^{\prime}]}\endmathpar\hfil\lx@intercol\\ \lx@intercol\textbf{Typing contexts:}\hfil\lx@intercol\\ &\Gamma::={}&{\raisebox{1.5pt}{$\scriptstyle\bullet$}}\mid\Gamma,x:\tau\\ \lx@intercol\textbf{Typing rules:}\hfil\lx@intercol\\ \lx@intercol\hfil\mathpar\inferrule*[right=T-False]{}{\Gamma\vdash\texttt{false}:\mathit{bool}}\inferrule*[right=T-True]{}{\Gamma\vdash\texttt{true}:\mathit{bool}}\inferrule*[right=T-Var]{\Gamma(x)=\tau}{\Gamma\vdash x:\tau}\inferrule*[right=T-Abs]{\Gamma,x:\tau_{1}\vdash e:\tau_{2}}{\Gamma\vdash\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}}\inferrule*[right=T-App]{\Gamma\vdash e_{1}:\tau_{2}\rightarrow\tau\Gamma\vdash e_{2}:\tau_{2}}{\Gamma\vdash e_{1}\;e_{2}:\tau}\inferrule*[right=T-If]{\Gamma\vdash e:\mathit{bool}\Gamma\vdash e_{1}:\tau\Gamma\vdash e_{2}:\tau}{\Gamma\vdash\texttt{if}\;e\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}:\tau}\endmathpar\hfil\lx@intercol\end{array}$$

$$f:\forall \alpha .\alpha \to \alpha$$

$$\forall \alpha .int\to \alpha$$

$$\begin{gathered} P(v_L,v_{1H}){\approx }_{L}P(v_L,v_{2H}) \\ \text{for }⊢P:{int}^L\times {int}^H\to {int}^L \end{gathered}$$

$$e\Downarrow v$$

$$e\Downarrow$$

$$e_1{e}_2$$

$${\to }^{\ast }(\lambda x:{\tau }_2.e^{\prime })v_2$$

$$\to e^{\prime }[v_2/x]$$

$${\mathrm{SN}}_{bool}(e)$$

$${\mathrm{SN}}_{{\tau }_1\to {\tau }_2}(e)$$

$$\varnothing (e)=$$

$$\gamma [x\mapsto v](e)=$$

$$\begin{array}{c}\gamma \models \Gamma \\ \text{iff}\\ \mathrm{dom}(\gamma )=\mathrm{dom}(\Gamma )\wedge \forall x\in \mathrm{dom}(\Gamma ).{\mathrm{SN}}_{\Gamma (x)}(\gamma (x))\end{array}$$

$${\mathrm{SN}}_{bool}(\gamma (\text{true}))$$

$${\mathrm{SN}}_{\tau }(\gamma (x))$$

$${\mathrm{SN}}_{\tau }(\gamma (e_1{e}_2))$$

$${\mathrm{SN}}_{{\tau }_2\to \tau }(\gamma (e_1))$$

$${\mathrm{SN}}_{{\tau }_2}(\gamma (e_2))$$

$${\mathrm{SN}}_{{\tau }_1\to {\tau }_2}(\gamma (\lambda x:{\tau }_1.e))$$

$$\Gamma ,x:{\tau }_1⊢e:{\tau }_2\wedge {\gamma }^{\prime }\models \Gamma ,x:{\tau }_1⟹{\mathrm{SN}}_{{\tau }_2}({\gamma }^{\prime }(e))$$

$$(\lambda x:{\tau }_1.\gamma (e))e^{\prime }$$

$$\to \gamma (e)[v^{\prime }/x]\equiv \gamma [x\mapsto v^{\prime }](e)$$

$$(\lambda x:{\tau }_1.\gamma (e))e^{\prime }{\to }^{\ast }\gamma [x\mapsto v^{\prime }](e)$$

$$\mathcal{V}[[-]]:\mathrm{Type}\to \mathcal{P}(\mathrm{ClosedCal})$$

$$\mathcal{V}[[bool]]$$

$$\mathcal{V}[[{\tau }_1\to {\tau }_2]]$$

$$\mathcal{E}[[\tau ]]=\{e\mid \forall e^{\prime }.e{\to }^{\ast }{e}^{\prime }\wedge \mathrm{irred}(e^{\prime })⟹e^{\prime }\in \mathcal{V}[[\tau ]]\}$$

$$\begin{array}{c}\mathrm{irred}(e)\\ \text{iff}\\ \nexists e^{\prime }.e\to e^{\prime }\end{array}$$

$$\begin{array}{c}\mathrm{safe}(e)\\ \text{iff}\\ \forall e^{\prime }.e{\to }^{\ast }{e}^{\prime }⟹\mathrm{Val}(e^{\prime })\vee \exists e^{\prime \prime }.e^{\prime }\to e^{\prime \prime }\end{array}$$

$$\mathcal{G}[[\bullet ]]$$

$$\mathcal{G}[[\Gamma ,x:\tau ]]$$

$$\begin{array}{c}\Gamma \models e:\tau \\ \text{iff}\\ \forall \gamma \in \mathcal{G}[[\Gamma ]].\gamma (e)\in \mathcal{E}[[\tau ]]\end{array}$$

$$\gamma [x\mapsto v](e)=\gamma (e){[}^v{/}_x]$$

$${\gamma }^{\prime }[x\mapsto v]e={\gamma }^{\prime }(e){[}^v{/}_x]$$

Full text

1. 1 Introduction

2. 1.1 Simply Typed Lambda Calculus

3. 1.2 Logical Relations

4. 1.3 Categories of Logical Relations

5. 2 Normalization of the Simply Typed Lambda Calculus

6. 2.1 Strong Normalization of STLC

7. 2.2 Exercises

8. 3 Type Safety for STLC

9. 3.1 Type safety - the classical treatment

10. 3.2 Type safety - using logical predicate

11. 3.3 Exercises

12. 4 Universal Types and Relational Substitutions

13. 4.1 System F (STLC with universal types)

14. 4.2 Properties of System-F: Free Theorems

15. 4.3 Contextual Equivalence

16. 4.4 A Logical Relation for System F

17. 4.5 Compatibility Lemmas

18. 4.6 Exercises

19. 5 Existential types

20. 5.1 STLC with Existential Types

21. 5.2 Example

22. 5.3 Logical Relation

23. 6 Recursive Types and Step Indexing

24. 6.1 Simply Typed Lambda Calculus with Recursive Types

25. 6.2 A Step-Indexed Logical Predicate

26. 6.3 Exercises

27. 7 References and Worlds

28. 7.1 STLC with References

29. 7.2 Properties of STLC with References

30. 7.3 Logical Predicate

31. 7.4 Safety Proof

32. 7.5 Exercises

33. 7.6 Further Reading

34. A Landin’s Knot

1 Introduction

The term logical relations stems from Gordon Plotkin’s memorandum Lambda-definability and logical relations written in 1973. However, the spirit of the proof method can be traced back to Wiliam W. Tait who used it to show strong normalization of System T in 1967.

Names are a curious thing. When I say “chair”, you immediately get a picture of a chair in your head. If I say “table”, then you picture a table. The reason you do this is because we denote a chair by “chair” and a table by “table”, but we might as well have said “giraffe” for chair and “Buddha” for table. If we encounter a new word composed of known words, it is natural to try to find its meaning by composing the meaning of the components of the name. Say we encounter the word “tablecloth” for the first time, then if we know what “table” and “cloth” denotes we can guess that it is a piece of cloth for a table. However, this approach does not always work. For instance, a “skyscraper” is not a scraper you use to scrape the sky. Likewise for logical relations, it may be a fool’s quest to try to find meaning in the name. Logical relations are relations, so that part of the name makes sense. They are also defined in a way that has a small resemblance to a logic, but trying to give meaning to logical relations only from the parts of the name will not help you understand them. A more telling name might be Type Indexed Inductive Relations. However, Logical Relations is a well-established name and easier to say, so we will stick with it (no one would accept “giraffe” to be a chair).

The majority of this note is based on the lectures of Amal Ahmed at the Oregon Programming Languages Summer School, 2015. The videos of the lectures can be found at https://www.cs.uoregon.edu/research/summerschool/summer15/curriculum.html.

1.1 Simply Typed Lambda Calculus

The language we use to present logical predicates and relations is the simply typed lambda calculus (STLC). In the first section, it will be used in its basic form, and later it will be used as the base language when we study new constructs and features. We will later leave it implicit that it is STLC that we extend with new constructs. STLC is defined in Figure 1.

For readers unfamiliar with inference rules: A rule \mathpar \inferrule A B A ∧B \endmathpar is read as if $A$ and $B$ is the case, then we can conclude $A\wedge B$. This means that the typing rule for application \mathpar $\inferrule*[right=T-App]{\Gamma\vdash e_{1}:\tau_{2}\rightarrow\tau\Gamma\vdash e_{2}:\tau_{2}}{\Gamma\vdash e_{1}\;e_{2}:\tau}$\endmathpar says that an application $e_{1}\;e_{2}$ has the type $\tau$ under the typing context $\Gamma$ when $e_{2}$ has type $\tau_{2}$ under $\Gamma$ and $e_{1}$ has type $\tau_{2}\rightarrow\tau$ also under $\Gamma$.

1.2 Logical Relations

A logical relation is a proof method that can be used to prove properties of programs written in a particular programming language. Proofs for properties of programming languages often go by induction on the typing or evaluation judgement. A logical relations add a layer of indirection by constructing a collection of programs that all have the property we are interested in. We will see this in more detail later. As a motivation, here are a number of examples of properties that can be proven with a logical relation:

• •

Termination (Strong normalization)

• •

Type safety

• •

Program equivalences

• –

Correctness of programs

• –

Representation independence

• –

Parametricity and free theorems, e.g.

[TABLE]

The program cannot inspect $\alpha$ as it has no idea which type it will be, therefore $f$ must be the identity function.

[TABLE]

A function with this type cannot exist (the function would need to return something of type $\alpha$, but it only has something of type $\mathit{int}$ to work with, so it cannot possibly return a value of the proper type).

• –

Security-Typed Languages (for Information Flow Control (IFC))

Example: All types in the code snippet below are labelled with their security level. A type can be labelled with either $L$ for low or $H$ for high. We do not want any information flowing from variables with a high label to a variable with a low label. The following is an example of an insecure program because it has an explicit flow of information from low to high:

⬇

x : int@Ly : intH

x = y //This assignment is insecure.

Information may also leak through a side channel. There are many varieties of side channels, and they vary from language to language depending on their features. One of the perhaps simplest side channels is the following: Say we have two variable $x$ and $y$. They are both of integer type, but the former is labelled with low and the latter with high. Now say the value of $x$ depends on the value of $y$, e.g. $x=0$ when $y>0$ and $x=1$ otherwise. In this example, we may not learn the exact value of $y$ from $x$, but we will have learned whether $y$ is positive. The side channel we just sketched looks as follows:

⬇

x : int@Ly : intH

if y > 0 then x = 0 else x = 1

Generally, speaking the property we want is non-interference:

[TABLE]

That is for programs that generate low results, we want “low-equivalent” results. Low-equivalence means: if we execute $P$ twice with the same low value but two different high values, then the low results of the two executions should be equal. In other words, the execution cannot have depended on the high value which means that no information was leaked to the low results.

1.3 Categories of Logical Relations

We can split logical relations into two: logical predicates and logical relations. Logical predicates are unary and are usually used to show properties of programs. Logical relations are binary and are usually used to show equivalences:

[TABLE]

There are some properties that we want logical predicates and relation to have in general. We describe these properties for logical predicates as they easily generalize to logical relations. In general, we want the following things to hold true for a logical predicate that contains expressions $e$111Note: these are rules of thumb. For instance, one exception to the rule is the proof of type safety where the well-typedness condition is weakened to only require $e$ to be closed.:

The expressions is closed and well-types, i.e. {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau. 2. 2.

The expression has the property we are interested in. 3. 3.

The property of interest is preserved by eliminating forms.

2 Normalization of the Simply Typed Lambda Calculus

2.1 Strong Normalization of STLC

In this section, we prove strong normalization for the simply typed lambda calculus which means that every term is strongly normalizing. Normalization of a term is the process of reducing it to its normal form (where it can be reduced no further). If a term is strongly normalizing, then it always reduces to its normal form. In our case, the normal forms of the language are the values of the language.

A first attempt at proving strong normalization for STLC

We will first attempt a syntactic proof of the strong normalization property of STLC to demonstrate how it fails. However, first we need to state what we mean by strong normalization.

Definition 1**.**

For expression $e$ and value $v$:

[TABLE]

Theorem 1** (Strong Normalization).**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau, then $e\Downarrow$

Proof.

¡ This proof gets stuck and is not complete. !

Induction on the structure of the typing derivation.

Case {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\texttt{true}:\mathit{bool}, this term has already terminated.

Case {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\texttt{false}:\mathit{bool}, same as for true.

Case {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\texttt{if}\;e\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}:\tau, simple, but requires the use of canonical forms of bool222See Pierce’s Types and Programming Languages [Pierce, 2002] for more about canonical forms..

Case {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}, it is a value already and it has terminated.

Case $\inferrule*[right=T-App]{\Gamma\vdash e_{1}:\tau_{2}\rightarrow\tau\Gamma\vdash e_{2}:\tau_{2}}{\Gamma\vdash e_{1}\;e_{2}:\tau}$,

by the induction hypothesis, we get $e_{1}\Downarrow v_{1}$ and $e_{2}\Downarrow v_{2}$. By the type of $e_{1}$, we conclude $e_{1}\Downarrow\lambda x:\tau_{2}\ldotp\;e^{\prime}$. What we need to show is $e_{1}\;e_{2}\Downarrow$. By the evaluation rules, we know $e_{1}\;e_{2}$ takes the following steps:

[TABLE]

Here we run into an issue as we know nothing about $e^{\prime}$. As mentioned, we know from the induction hypothesis that $e_{1}$ evaluates to a lambda abstraction which makes $e_{1}$ strongly normalizing. However, this say nothing about how the body of the body of the lambda abstraction evaluates. Our induction hypothesis is simply not strong enough333:(. ∎

The direct style proof did not work in this case, and it is not clear what to do to make it work.

Proof of strong normalization using a logical predicate

Now that the direct proof failed, we try using a logical predicate. First, we define the predicate $\operatorname{SN}_{\tau}(e)$:

[TABLE]

Now recall the three conditions from Section 1.3 that a logical predicate should satisfy. It is easy to verify that $\operatorname{SN}_{\tau}(e)$ only accepts closed well-typed terms. Further, the predicate also requires terms to have the property we are interested in proving, namely $e\Downarrow$. Finally, it should satisfy that “the property of interest is preserved by eliminating forms”. In STLC lambdas are eliminated by application which means that application should preserve strong normalization when the argument is strongly normalizing.

The logical predicate is defined over the structure of $\tau$ which has $\mathit{bool}$ as a base type, so the definition is well-founded444This may seem like a moot point as it is so obvious, but for some of the logical relations we see later it is not so, so we may as well start the habit of checking this now.. We are now ready to prove strong normalization using $\operatorname{SN}_{\tau}(e)$. To this end, we have the following lemmas:

Lemma 1**.**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau, then $\operatorname{SN}_{\tau}(e)$

Lemma 2**.**

If $\operatorname{SN}_{\tau}(e)$, then $e\Downarrow$

These two lemmas are common for proofs using a logical predicate (or relation). We first prove that all well-typed terms are in the predicate, and then we prove that all terms in the predicate have the property we want to show (in this case strong normalization).

The proof of Lemma 2 is by induction on $\tau$. This proof is straightforward because the strong normalization was baked into the predicate. It is generally a straightforward proof as our rules of thumb guide us to bake the property of interest into the predicate.

To prove Lemma 1, we we could try induction over {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau, but the case we will fail to show the case for T-Abs. Instead we prove a generalization of Lemma 1:

Theorem 2** (Lemma 1 generalized).**

If $\Gamma\vdash e:\tau$ and $\gamma\models\Gamma$, then $\operatorname{SN}_{\tau}(\gamma(e))$

This theorem uses a substitution $\gamma$ to close off the expression $e$. In order for $\gamma$ to close off $e$, it must map all the possible variables of $e$ to strongly normalizing terms. When we prove this lemma, we get a stronger induction hypothesis than we have when we try to prove Lemma 1. In Lemma 1, the induction hypothesis can only be used with a closed term; but in this lemma, we can use an open term provided we have a substitution that closes it.

To be more specific, a substitution $\gamma=\{x_{1}\mapsto v_{1},\dots,x_{n}\mapsto v_{n}\}$ works as follows:

Definition 2**.**

[TABLE]

555We do not formally define substitution ($e[^{\textstyle v}/_{\textstyle x}]$). We refer to Pierce [2002] for a formal definition.

and $\gamma\models\Gamma$ is read “the substitution $\gamma$ satisfies the type environment $\Gamma$”, and it is defined as follows:

[TABLE]

To prove Theoremq 2 we need two further lemmas

Lemma 3** (Substitution Lemma).**

If $\Gamma\vdash e:\tau$ and $\gamma\models\Gamma$, then {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\gamma(e):\tau

Proof.

Left as an exercise. ∎

Lemma 4** ($\operatorname{SN}$ preserved by forward/backward reduction).**

Suppose {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau and $e\rightarrow e^{\prime}$

if $\operatorname{SN}_{\tau}(e^{\prime})$, then $\operatorname{SN}_{\tau}(e)$ 2. 2.

if $\operatorname{SN}_{\tau}(e)$, then $\operatorname{SN}_{\tau}(e^{\prime})$

Proof.

Left as an exercise. ∎

Proof. (1 Generalized).

Proof by induction on $\Gamma\vdash e:\tau$.

Case T-True,

Assume:

• •

$\Gamma\vdash\texttt{true}:\mathit{bool}$

• •

$\gamma\models\Gamma$

We need to show:

[TABLE]

There is no variable, so the substitution does nothing, and we just need to show $\operatorname{SN}_{\mathit{bool}}(\texttt{true})$ which is true as $\texttt{true}\Downarrow\texttt{true}$.

Case T-False, similar to the true case.

Case T-Var,

Assume:

• •

$\Gamma\vdash x:\tau$

• •

$\gamma\models\Gamma$

We need to show:

[TABLE]

This case follows from the definition of $\gamma\models\Gamma$. We know that $x$ is well-typed, so it is in the domain of $\Gamma$. From the definition of $\gamma\models\Gamma$, we get $\operatorname{SN}_{\Gamma(x)}(\gamma(x))$. From well-typedness of $x$, we have $\Gamma(x)=\tau$ which then gives us what we needed to show.

Case T-If, left as an exercise.

Case T-App,

Assume:

• •

$\Gamma\vdash e_{1}\;e_{2}:\tau$

• •

$\gamma\models\Gamma$

We need to show:

[TABLE]

which amounts to $\operatorname{SN}_{\tau}(\gamma(e_{1})\;\gamma(e_{2}))$. By the induction hypothesis we have

[TABLE]

By the 3rd property of (1), $\forall e^{\prime}\ldotp\operatorname{SN}_{\tau_{2}}(e^{\prime})\implies\operatorname{SN}_{\tau}(\gamma(e_{1})\;e^{\prime})$, instantiated with (2), we get $\operatorname{SN}_{\tau}(\gamma(e_{1})\;\gamma(e_{2}))$ which is the result we need.

Note this was the case we got stuck in when we tried to do the direct proof. With the logical predicate, it is easily proven because we made sure to bake information about $e_{1}\;e_{2}$ into $\operatorname{SN}_{\tau_{2}\rightarrow\tau}$ when we follow the rule of thumb: “The property of interest is preserved by eliminating forms”.

Case T-Abs,

Assume:

• •

$\Gamma\vdash\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}$

• •

$\gamma\models\Gamma$

We need to show:

[TABLE]

which amounts to $\operatorname{SN}_{\tau_{1}\rightarrow\tau_{2}}(\lambda x:\tau_{1}\ldotp\;\gamma(e))$. Our induction hypothesis in this case reads:

[TABLE]

It suffices to show the following three things:

{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\lambda x:\tau_{1}\ldotp\;\gamma(e):\tau_{1}\rightarrow\tau_{2} 2. 2.

$\lambda x:\tau_{1}\ldotp\;\gamma(e)\Downarrow$ 3. 3.

$\forall e^{\prime}\ldotp\operatorname{SN}_{\tau_{1}}(e^{\prime})\implies\operatorname{SN}_{\tau_{2}}((\lambda x:\tau_{1}\ldotp\;\gamma(e))\;e^{\prime})$

If we use the substitution lemma (Lemma 3) and push the $\gamma$ in under the $\lambda$-abstraction, then we get 1. The lambda-abstraction is a value, so by definition 2 is true.

It only remains to show 3. To do this, we want to somehow apply the induction hypothesis for which we need a $\gamma^{\prime}$ such that $\gamma^{\prime}\models\Gamma,x:\tau_{1}$. We already have $\gamma$ and $\gamma\models\Gamma$, so our $\gamma^{\prime}$ should probably have the form $\gamma^{\prime}=\gamma[x\mapsto v_{?}]$ for some $v_{?}$ of type $\tau_{1}$. Let us move on and see if any good candidates for $v_{?}$ present themselves.

Let $e^{\prime}$ be given and assume $\operatorname{SN}_{\tau_{1}}(e^{\prime})$. We then need to show $\operatorname{SN}_{\tau_{2}}((\lambda x:\tau_{1}\ldotp\;\gamma(e))\;e^{\prime})$. From $\operatorname{SN}_{\tau_{1}}(e^{\prime})$, it follows that $e^{\prime}\Downarrow v^{\prime}$ for some $v^{\prime}$. $v^{\prime}$ is a good candidate for $v_{?}$ so let $v_{?}=v^{\prime}$. From the forward part of the preservation lemma (Lemma 4), we can further conclude $\operatorname{SN}_{\tau_{1}}(v^{\prime})$. We use this to conclude $\gamma[x\mapsto v^{\prime}]\models\Gamma,x:\tau_{1}$ which we use with the assumption $\Gamma,x:\tau_{1}\vdash e:\tau_{2}$ to instantiate the induction hypothesis and get $\operatorname{SN}_{\tau_{2}}(\gamma[x\mapsto v^{\prime}](e))$.

Now consider the following evaluation:

[TABLE]

We already concluded that $e^{\prime}\rightarrow^{*}v^{\prime}$, which corresponds to the first series of steps. We can then do a $\beta$-reduction to take the next step, and finally we get something that is equivalent to $\gamma[x\mapsto v^{\prime}](e)$. That is we have the evaluation

[TABLE]

From $\operatorname{SN}_{\tau_{1}}(e^{\prime})$, we have {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e^{\prime}:\tau_{1} and we already argued that {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\lambda x:\tau_{1}\ldotp\;\gamma(e):\tau_{1}\rightarrow\tau_{2}, so from the application typing rule we get {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash(\lambda x:\tau_{1}\ldotp\;\gamma(e))\;e^{\prime}:\tau_{2}. We can use this with the above evaluation and the forward part of the preservation lemma (Lemma 4) to argue that every intermediate expressions in the steps down to $\gamma[x\mapsto v^{\prime}](e)$ are closed and well typed.

If we use $\operatorname{SN}_{\tau_{2}}(\gamma[x\mapsto v^{\prime}](e))$ with $(\lambda x:\tau_{1}\ldotp\;\gamma(e))\;e^{\prime}\rightarrow^{*}\gamma[x\mapsto v^{\prime}](e)$ and the fact that every intermediate step in the evaluation is closed and well typed, then we can use the backward reduction part of the $\operatorname{SN}$ preservation lemma to get $\operatorname{SN}_{\tau_{2}}((\lambda x:\tau_{1}\ldotp\;\gamma(e))\;e^{\prime})$ which is the result we wanted. ∎

2.2 Exercises

Prove $\operatorname{SN}$ preserved by forward/backward reduction (Lemma 4). 2. 2.

Prove the substitution lemma (Lemma 3). 3. 3.

Go through the cases of the proof for Theorem 2 by yourself. 4. 4.

Prove the T-If case of Theorem 2. 5. 5.

Extend the language with pairs and adjust the proofs.

Specifically, how do you apply the rules of thumb for the case of pairs? Do you need to add anything for the third clause (eliminating forms preservation), or does it work without doing anything for it like it did for case of booleans?

recu

3 Type Safety for STLC

In this section, we prove type safety for simply typed lambda calculus using a logical predicate.

First we need to consider what type safety is. The classical mantra for type safety is: “Well-typed programs do not go wrong.” It depends on the language and type system what go wrong actually means, but in our case a program has gone wrong when it is stuck666In the case of language-based security and information flow control, the notion of go wrong would be that there is an undesired flow of information. (an expression is stuck if it is irreducible but not a value).

3.1 Type safety - the classical treatment

Type safety for simply typed lambda calculus is stated as follows:

Theorem 3** (Type Safety for STLC).**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau and $e\rightarrow^{*}e^{\prime}$, then $\operatorname{Val}(e^{\prime})$ or $\exists e^{\prime\prime}\ldotp e^{\prime}\rightarrow e^{\prime\prime}$.

Traditionally, the type safety proof uses two lemmas: progress and preservation.

Lemma 5** (Progress).**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau, then $\operatorname{Val}(e)$ or $\exists e^{\prime}\ldotp\rightarrow e^{\prime}$.

Progress is normally proved by induction on the typing derivation.

Lemma 6** (Preservation).**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau and $e\rightarrow e^{\prime}$, then {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e^{\prime}:\tau.

Preservation is normally proved by induction on the evaluation. Preservation is also known as subject reduction. Progress and preservation talk about one step, so to prove type safety we have to do induction on the evaluation. Here we do not want to prove type safety the traditional way, but if you are unfamiliar with it and want to learn more, then we refer to Pierce’s Types and Programming Languages [Pierce, 2002].

We will use a logical predicate (as it is a unary property) to prove type safety.

3.2 Type safety - using logical predicate

We define the predicate in a slightly different way compared to Section 2. We define it in two parts: a value interpretation and an expression interpretation. The value interpretation is a function from types to the power set of closed values:

[TABLE]

The value interpretation is defined as:

[TABLE]

We define the expression interpretation as:

[TABLE]

Notice that neither $\mathcal{V}\llbracket\tau\rrbracket$ nor $\mathcal{E}\llbracket\tau\rrbracket$ requires well-typedness. Normally, the logical predicate would require this as our guidelines suggest it. However, as the goal is to prove type safety we do not want it as a part of the predicate. In fact, if we did include a well-typedness requirement, then we would end up proving preservation for some of the proofs to go through. We do, however, require the value interpretation to only contain closed values.

An expression is irreducible if it is unable to take any reduction steps according to the evaluation rules. The predicate $\operatorname{irred}$ captures whether an expression is irreducible:

[TABLE]

The sets are defined on the structure of the types. $\mathcal{V}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$ contains $\mathcal{E}\llbracket\tau_{2}\rrbracket$, but $\mathcal{E}\llbracket\tau_{2}\rrbracket$ uses $\tau_{2}$ directly in $\mathcal{V}\llbracket\tau_{2}\rrbracket$, so the definition is structurally well-founded. To prove type safety, we first define a new predicate, $\operatorname{safe}$:

[TABLE]

An expression $e$ is safe if it can take a number of steps and end up either as a value or as an expression that can take another step.

We are now ready to prove type safety. Just like we did for strong normalization, we use two lemmas:

Lemma 7**.**

If {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\tau, then $e\in\mathcal{E}\llbracket\tau\rrbracket$

Lemma 8**.**

If $e\in\mathcal{E}\llbracket\tau\rrbracket$, then $\operatorname{safe}(e)$

Rather than proving Lemma 7 directly, we prove a more general theorem and get Lemma 7 as a consequence. We are not yet in a position to state the generalization. First, we need to define the interpretation of environments:

[TABLE]

Further, we need to define semantic type safety:

[TABLE]

This definition should look familiar because we use the same trick as we did for strong normalization: Instead of only considering closed terms, we consider all terms but require a substitution that closes it.

We can now define our generalized version of Lemma 7:

Theorem 4** (Fundamental Property).**

If $\Gamma\vdash e:\tau$, then $\Gamma\models e:\tau$

A theorem like this would typically be the first you prove after defining a logical relation. In this case, the theorem says that syntactic type safety implies semantic type safety.

We also alter Lemma 8 to fit with Theorem 4:

Lemma 9**.**

If $\emptyset\models e:\tau$, then $\operatorname{safe}(e)$

Proof.

Suppose $e\rightarrow^{*}e^{\prime}$ for some $e^{\prime}$, then we need to show $\operatorname{Val}(e^{\prime})$ or $\exists e^{\prime\prime}\ldotp e^{\prime}\rightarrow e^{\prime\prime}$. We proceed by case on whether or not $\operatorname{irred}(e^{\prime})$:

Case $\neg\operatorname{irred}(e^{\prime})$, this case follows directly from the definition of $\operatorname{irred}$: $\operatorname{irred}(e^{\prime})$ is defined as $\nexists e^{\prime\prime}\ldotp e^{\prime}\rightarrow e^{\prime\prime}$ and as the assumption is $\neg\operatorname{irred}(e^{\prime})$, we get $\exists e^{\prime\prime}\ldotp e^{\prime}\rightarrow e^{\prime\prime}$.

Case $\operatorname{irred}(e^{\prime})$, by assumption we have {\raisebox{1.5pt}{\scriptstyle\bullet}}\models e:\tau. As the typing context is empty, we choose the empty substitution and get $e\in\mathcal{E}\llbracket\tau\rrbracket$. We now use the definition of $e\in\mathcal{E}\llbracket\tau\rrbracket$ with the two assumptions $e\rightarrow^{*}e^{\prime}$ and $\operatorname{irred}(e^{\prime})$ to conclude $e^{\prime}\in\mathcal{V}\llbracket\tau\rrbracket$. As $e^{\prime}$ is in the value interpretation of $\tau$, we can conclude $\operatorname{Val}(e^{\prime})$. ∎

To prove the Fundamental Property (Theorem 4), we need a substitution lemma:

Lemma 10** (Substitution).**

Let $e$ be syntactically well-formed term, let $v$ be a closed value and let $\gamma$ be a substitution that maps term variables to closed values, and let $x$ be a variable not in the domain of $\gamma$, then

[TABLE]

Proof.

By induction on the size of $\gamma$.

Case $\gamma=\emptyset$, this case is immediate by definition of substitution. That is by definition we have $[x\mapsto v]e=e[^{\textstyle v}/_{\textstyle x}]$.

Case $\gamma=\gamma^{\prime}[y\mapsto v^{\prime}]$, $x\neq y$, in this case our induction hypothesis is:

[TABLE]

We wish to show

[TABLE]

[TABLE]

In the first step (3), we swap the two mappings. It is safe to do so as both $v$ and $v^{\prime}$ are closed values, so we know that no variable capturing will occur. In the second step (4), we just use the definition of substitution (Definition 2). In the third step (5), we use the induction hypothesis777The induction hypothesis actually has a number of premises, as an exercise convince yourself that they are satisfied.. Finally in the last step (6), we use the definition of substitution to get the $y$ binding out as an extension of $\gamma^{\prime}$. ∎

Proof. (Fundamental Property, Theorem 4).

Proof by induction on the typing judgement.

Case T-Abs,

assuming $\Gamma\vdash\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}$, we need to show $\Gamma\models\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}$. Suppose $\gamma\in\mathcal{G}\llbracket\Gamma\rrbracket$ and show

[TABLE]

Now suppose that $\lambda x:\tau_{1}\ldotp\;\gamma(e)\rightarrow^{*}e^{\prime}$ and $\operatorname{irred}(e^{\prime})$. We then need to show $e^{\prime}\in\mathcal{V}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$. $\lambda x:\tau_{1}\ldotp\;\gamma(e)$ is irreducible because it is a value, and we can conclude it takes no steps. In other words $e^{\prime}=\lambda x:\tau_{1}\ldotp\;\gamma(e)$. This means we need to show $\lambda x:\tau_{1}\ldotp\;\gamma(e)\in\mathcal{V}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$. Now suppose $v\in\mathcal{V}\llbracket\tau_{1}\rrbracket$, then we need to show $\gamma(e)[v/x]\in\mathcal{E}\llbracket\tau_{2}\rrbracket$.

Keep the above proof goal in mind and consider the induction hypothesis:

[TABLE]

Instantiate this with $\gamma[x\mapsto v]$. We have $\gamma[x\mapsto v]\in\mathcal{G}\llbracket\Gamma,x:\tau_{1}\rrbracket$ because of assumptions $\gamma\in\mathcal{G}\llbracket\Gamma\rrbracket$ and $v\in\mathcal{V}\llbracket\tau_{2}\rrbracket$. The instantiation gives us $\gamma[x\mapsto v](e)\in\mathcal{E}\llbracket\tau_{2}\rrbracket\equiv\gamma(e)[v/x]\in\mathcal{E}\llbracket\tau_{2}\rrbracket$. The equivalence is justified by the substitution lemma we proved. This is exactly the proof goal we kept in mind.

Case T-App, Show this case as an exercise.

The remaining cases are straightforward. ∎

Now consider what happens if we add pairs to the language (exercise 5 in exercise section 2.2). We need to add a clause to the value interpretation:

[TABLE]

There is nothing surprising in this addition to the value relation, and it should not be a challenge to show the pair case of the proofs.

If we extend our language with sum types.

[TABLE]

Then we need to add the following clause to the value interpretation:

[TABLE]

It turns out this clause is sufficient. One might think that it is necessary to require the body of the match to be in the expression interpretation, which looks something like $\forall e\in\mathcal{E}\llbracket\tau\rrbracket$. This requirement will, however, give well-foundedness problems, as $\tau$ is not a structurally smaller type than $\tau_{1}+\tau_{2}$. It may come as a surprise that we do not need to relate the expressions as the slogan for logical relations is: “Related inputs to related outputs.”

3.3 Exercises

Prove the T-App case of the Fundamental Property (Theorem 4). 2. 2.

Verify the remaining cases of Theorem 4 (T-True,T-False,T-Var, and T-If).

4 Universal Types and Relational Substitutions

In the previous sections, we considered the unary properties and safety and termination, but now we shift our focus to relational properties and specifically program equivalences. Generally speaking, we use logical relations rather than predicates for proving relational properties. A program equivalence is a relational property, so we are going to need a logical relation.

We will consider the language System F which is STLC with universal types. Universal types allow us to write generic functions. For instance, say we have a function that sorts integer lists:

[TABLE]

The function takes a list of integers and returns the sorted list. Say we now want a function sortstring that sorts lists of strings. Instead of implementing a completely new sorting function for this, we could factor out the generic code responsible for sorting from sortint and make a generic function. The type signature for a generic sort function would be:

[TABLE]

The generic sort function takes a type, a list of elements of this type, and a comparison function that compares to elements of the given type. The result of the sorting function is a list sorted according to the comparison function. An example of an application of this function could be

[TABLE]

Whereas sort instantiated with the string type, but given an integer list would not be a well typed instantiation.

[TABLE]

Here the application with the list $(3,7,5)$ is not well typed, but if we instead use a list of strings, then it type checks.

We want to extend the simply typed lambda calculus with functions that abstract over types in the same way lambda abstractions, $\lambda x:\tau\ldotp\;e$, abstract over terms. We do that by introducing a type abstraction:

[TABLE]

This function abstracts over the type $\alpha$ which allows $e$ to depend on $\alpha$.

4.1 System F (STLC with universal types)

We extend STLC as follows to get System F:

[TABLE]

New evaluation: \mathpar \inferrule (Λα .   e)[τ] →e[τ/α] \endmathpar Type environment:

[TABLE]

The type environment consists of type variables, and they are assumed to be distinct type variables. That is, the environment $\Delta,\alpha$ is only well-formed if $\alpha\not\in\operatorname{dom}(\Delta)$888We do not annotate $\alpha$ with a kind as we only have one kind in this language.. With the addition of type environments, we update the form of the typing judgement as follows

[TABLE]

We now need a notion of well-formed types. If $\tau$ is well formed with respect to $\Delta$, then we write:

[TABLE]

We do not include the formal rules here, but they amount to $\operatorname{FTV}(\tau)\subseteq\Delta$, where $\operatorname{FTV}(\tau)$ is the set of free type variables in $\tau$.

We further introduce a notion of well-formed typing contexts. A context is well formed if all the types that appear in the range of $\Gamma$ are well formed.

[TABLE]

For any type judgment $\Delta,\Gamma\vdash e:\tau$, we have as an invariant that $\tau$ is well formed in $\Delta$ and $\Gamma$ is well formed in $\Delta$. The old typing system modified to use the new form of the typing judgment looks like this:

\mathpar

\inferrule*[right=T-False]{}{\Delta;\Gamma\vdash\texttt{false}:\mathit{bool}}$$\inferrule*[right=T-True]{}{\Delta;\Gamma\vdash\texttt{true}:\mathit{bool}}$$\inferrule*[right=T-Var]{\Gamma(x)=\tau}{\Delta;\Gamma\vdash x:\tau}$$\inferrule*[right=T-If]{\Delta;\Gamma\vdash e:\mathit{bool}\Delta;\Gamma\vdash e_{1}:\tau\\ \Delta;\Gamma\vdash e_{2}:\tau}{\Delta;\Gamma\vdash\texttt{if}\;e\;\texttt{then}\;e_{1}\;\texttt{else}\;e_{2}:\tau}$$\inferrule*[right=T-Abs]{\Delta;\Gamma,x:\tau_{1}\vdash e:\tau_{2}}{\Delta;\Gamma\vdash\lambda x:\tau_{1}\ldotp\;e:\tau_{1}\rightarrow\tau_{2}}$$\inferrule*[right=T-App]{\Delta;\Gamma\vdash e_{1}:\tau_{2}\rightarrow\tau\Delta;\Gamma\vdash e_{2}:\tau_{2}}{\Delta;\Gamma\vdash e_{1}\;e_{2}:\tau}\endmathpar Notice that the only thing that has changed is that $\Delta$ has been added to the environment in the judgments. We further extend the typing rules with the following two rules to account for our new language constructs: \mathpar \inferrule*[right=T-TApp]{\Delta;\Gamma\vdash e:\forall\alpha.\tau\Delta\vdash\tau^{\prime}}{\Delta;\Gamma\vdash e[\tau^{\prime}]:\tau[^{\textstyle\tau^{\prime}}/_{\textstyle\alpha}]}$$\inferrule*[right=T-TAbs]{\Delta,\alpha;\Gamma\vdash e:\tau}{\Delta;\Gamma\vdash\Lambda\alpha.\;e:\forall\alpha.\tau}\endmathpar

4.2 Properties of System-F: Free Theorems

In System-F, certain types reveal the behavior of the functions with that type. Let us consider terms with the type $\forall\alpha\ldotp\alpha\rightarrow\alpha$. Recall from Section 1.2 that this has to be the identity function. We can now phrase this as a theorem:

Theorem 5**.**

If all of the following hold

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\forall\alpha\ldotp\alpha\rightarrow\alpha**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\tau**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash v:\tau,

then

[TABLE]

This is a free theorem in this language. Another free theorem from Section 1.2 is for expressions of type $\forall\alpha\ldotp\alpha\rightarrow\mathit{bool}$. All expressions with this type has to be constant functions. We can also phrase this as a theorem:

Theorem 6**.**

If all of the following hold

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\forall\alpha\ldotp\alpha\rightarrow\mathit{bool}**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\tau**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash v_{1}:\tau**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash v_{2}:\tau**

then

[TABLE]

999We have not defined $\approx^{ctx}$ yet. For now, it suffices to know that it equates programs that are behaviorally the same.

We can even allow the type abstraction to be instantiated with different types:

Theorem 7**.**

If all of the following hold

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\forall\alpha\ldotp\alpha\rightarrow\mathit{bool}**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\tau_{1}**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash\tau_{2}**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash v_{1}:\tau_{1}**

• –

{\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash v_{2}:\tau_{2}**

then

[TABLE]

We get these free theorems because the functions do not know the type of the argument which means that they have no way to inspect it. The function can only treat its argument as an unknown “blob”, so it has no choice but to return the same value every time.

The question now is: how do we prove these free theorems? The two last theorems both talk about program equivalence, so the proof technique of choice is a logical relation. The first theorem did not mention a program equivalence, but it can also be proven with a logical relation.

4.3 Contextual Equivalence

To define a contextual equivalence, we first define the notion of a program context. A program context is a complete program with exactly one hole in it:

[TABLE]

For instance,

[TABLE]

is a context where the hole is the body of the lambda abstraction.

We need a notion of context typing. For simplicity, we just introduce it for simply typed lambda calculus. The context typing is written as:

[TABLE]

This means that for any expression $e$ of type $\tau$ under $\Gamma$ if we embed it into $C$, then the type of the embedding is $\tau^{\prime}$ under $\Gamma^{\prime}$. For our example of a context, we would have

[TABLE]

because the hole of the context can be plugged with any expression of type $\mathit{bool}$ with variable $y$ free in it. Such an expression could be $\texttt{if}\;y\;\texttt{then}\;\texttt{false}\;\texttt{else}\;\texttt{true}$ as $y:\mathit{bool}\vdash\texttt{if}\;y\;\texttt{then}\;\texttt{false}\;\texttt{else}\;\texttt{true}:\mathit{bool}$. When the hole in the context is plugged with such an expression, then it is closed and has type $\mathit{bool}\rightarrow\mathit{bool}$. For instance, if we plug the example context with the above expression we have

[TABLE]

Informally we want contextual equivalence to express that two expressions give the same result no matter what program context they are plugged into. In other words, two expressions are contextually equivalent when no program context is able to observe any difference in behavior between the two expressions. For this reason, contextual equivalence is also known as observational equivalence. A hole has to be plugged with a term of the correct type, so we annotate the equivalence with the type of the hole which means that the two contextually equivalent expressions must have that type.

[TABLE]

This definition assumes that $e_{1}$ and $e_{2}$ have type $\tau$ under the specified contexts. Notice from the context typing we have that $C$ plugged with any term must be closed which ensures that it can be evaluated. Further, we require the plugged context to have type $\mathit{bool}$. If we allowed the plugged context to be of function type, then the two functions produced by $C[e_{1}]$ and $C[e_{2}]$ would have to be equivalent. This would of course also need to hold true for the program context that is just a hole because we need to decide whether $e_{1}$ and $e_{2}$ behaves the same which is exactly what we try to define with contextual equivalence. 101010In non-terminating languages, the definition of contextual equivalence only mentions termination and not whether the values produced are equal. For non-terminating languages this makes sense because if a context is able to differentiate two expressions, then it is easy to construct another context that terminates when plugged with one expression but diverges when plugged with the other. .

Contextual equivalence can be used to argue about correctness of a program. For instance, say we have two implementations of a stack, one is implemented using an array and the other using a list. If we can show that the two implementations are contextual equivalent, then we can use either stack implementation in any context with the same result. In particular, if one of the stack implementations is highly optimized, then we would like to use that implementation. However, it is not always clear whether such highly optimized programs do what they are supposed to. In order to argue this, one could implement a stack reference or specification implementation which is slower but where it is easy to see that it behaves like a stack simply by inspecting the implementation. A proof of contextual equivalence between the highly optimized stack implementation and the specification implementation could be seen as a correctness proof with respect to the specification.

In the next part, we will introduce a logical relation such that

[TABLE]

That is we want to show that the logical relation is sound with respect to contextual equivalence.

If we can prove the above soundness, then we can state our free theorems with respect to $\approx^{LR}$ and get the result with respect to $\approx^{ctx}$ as a corollary. In fact, it is very difficult to prove contextual equivalences directly as the proof has to consider every possible program context. Such a proof would be by induction, but the lambda-abstraction case would be very difficult.

4.4 A Logical Relation for System F

In this section, we construct the logical relation for System F, so we can prove the free theorems of Section 4.2. We are defining a relation, so the value interpretation consists of pairs. All pairs in the value relation must be closed and well-typed:

[TABLE]

For succinctness, we leave this implicit when we define the rest of the value relation. As a first try, we naively construct the logical relation in the same way we constructed the logical predicates in the previous sections:

[TABLE]

The value interpretation of the function type is defined based on the slogan for logical relations: “Related inputs to related outputs.” If we had chosen to use equal inputs rather than related, then our definition would be more restrictive than necessary.

We did not define a value interpretation for type variables in the previous sections, so let us try to push on without defining that part.

The next type is $\forall\alpha\ldotp\tau$. When we define the value interpretation, we consider the elimination forms which in this case is type application (cf. the guidelines in Section 1.3). Before we proceed, let us revisit Theorem 7, the last free theorem of Section 4.2. There are some important points to note in this free theorem. First of all, we want to be able to apply $\Lambda$-terms to different types, so we will have to pick two different types in our value interpretation. Further in the lambda-abstraction case, we pick related values, so perhaps we should pick related types here. However, we do not have a notion of related types, and the theorem does not relate the two types, so relating them might not be a good idea after all. With these points in mind, we make a first attempt at constructing the value interpretation of $\forall\alpha\ldotp\tau$:

[TABLE]

Now the question is what type to relate the two expressions under. We need to substitute $?$ for some type, but if we use either $\tau_{1}$ or $\tau_{2}$, then the well-typedness requirement will be broken for one of the two expressions. The solution is for each type variable to keep track of the two types we would have liked to substitute, i.e. $\tau_{1}$ and $\tau_{2}$. This means that we leave $\alpha$ free in $\tau$, but we can close it off with the types we keep track of to fulfil the well-typedness requirement of the logical relation. To this end, we introduce a relational substitution which keeps track of related types for each free type variable:

[TABLE]

We make the relational substitution available by passing it around in the interpretations. For instance, for the type abstraction we have:

[TABLE]

Notice how the definition now is parameterized with $\rho$, but also how $\rho$ is extended with $\alpha$ mapping to $\tau_{1}$ and $\tau_{2}$ before it is passed to the expression interpretation. This means that $\alpha$ is free in $\tau$ which means that we need to interpret type variables in the value interpretation:

[TABLE]

However, the big question is: How should these values be related? To find the answer, we look to Theorem 7 again. In the theorem, the expression $e$ is contextually related to itself when applied to different types and values. That is $e[\tau_{1}]\;v_{1}$ is contextually equivalent to $e[\tau_{2}]\;v_{2}$ which means that $e$ must treat $v_{1}$ and $v_{2}$ the same. This would suggest that, $v_{1}$ and $v_{2}$ should somehow be related under type $\alpha$. To achieve this in the value interpretation, we pick a relation $R$ in the interpretation of type abstractions. Relation $R$ relates values of type $\tau_{1}$ and $\tau_{2}$ which in the example of the free theorem would allow us to relate $v_{1}$ and $v_{2}$. An example of a relation would be $R_{\mathit{ex}}=\{(1,\texttt{true})\}$). We need such a relation when we interpret a type variable $\alpha$, so we make $R$ part of the relational substitution. For instance, if we picked $R_{\mathit{ex}}$ for $\alpha$ and made it part of the relational substitution, then it would be of the form $\rho[\alpha\mapsto(\mathit{int},\mathit{bool},R_{\mathit{ex}})]$ where $\rho$ is the previous relational substitution. In the interpretation of type variables, we simply look-up $R$ in the relational substitution and require the values to be related in the relation. With this in mind, we update the interpretation of type abstractions:

[TABLE]

The relational substitution is now also extended with $R$, and we require $R$ to be in $\operatorname{Rel}[\tau_{1},\tau_{2}]$. That is $\tau_{1}$ and $\tau_{2}$ must be closed values and $R$ only relates well-typed closed values.

[TABLE]

For $R_{\mathit{ex}}$, we have $R_{\mathit{ex}}\in\operatorname{Rel}[\mathit{int},\mathit{bool}]$ as $\mathit{int}$ and $\mathit{bool}$ are closed types and $1$ and true are closed values of type $\mathit{int}$ and true, respectively. In the interpretation of a type variable $\alpha$, we require the pair of values to be related in the relation for that type variable. That is, they must be related under the relation we picked when interpreting $\forall\alpha\ldotp\tau$:

[TABLE]

For convenience, we introduce the following notation: Given

[TABLE]

define the following projections:

[TABLE]

Notice that $\rho_{1}$ and $\rho_{2}$ now are type substitutions, so we write $\rho_{1}(\tau)$ to mean $\tau$ where all the type variables mentioned in the substitution have been substituted with the appropriate types. We can now write the value interpretation for type variables in a more succinct way:

[TABLE]

We need to add $\rho$ to the other parts of the value interpretation as well. Moreover, as we now interpret open types, we require the pairs of values in the relation to be well typed under the type closed off using the relational substitution. So all value interpretations have the form

[TABLE]

We further need to close of the type annotation of the variable in functions, so our value interpretations end up as:

[TABLE]

With the above challenge resolved, the remainder of the definitions are fairly straightforward. The expression interpretation is defined as follows:

[TABLE]

In System F, the environment is extended with a type context $\Gamma$, so we need an interpretation for it.

[TABLE]

The interpretation of the type context is simply a relational substitution for the variables in the context. We also need an interpretation for the typing context $\Gamma$ just like we had one in the previous sections.

[TABLE]

We need the relational substitution in the interpretation of $\Gamma$, because $\tau$ might contain free type variables now. We introduce a convenient notation for the projections of $\gamma$ similar to the one we did for $\rho$:

[TABLE]

Define the projections as follows:

[TABLE]

We are now ready to define when two terms are logically related. We define it in a similar way to the logical predicate we already have defined. First we pick $\rho$ and $\gamma$ to close off the expressions, then we require the closed off expressions to be related under the expression interpretation of the type in question111111From now on we drop the superscript for logically related terms and just write $\approx$.:

[TABLE]

With our logical relation defined, the first thing to prove is the fundamental property:

Theorem 8** (Fundamental Property).**

If $\Delta;\Gamma\vdash e:\tau$ then $\Delta;\Gamma\vdash e\approx e:\tau$

This theorem may seem a bit mundane, but it is actually quite strong. In the definition of the logical relation, $\Delta$ and $\Gamma$ can be seen as maps from place holders that need to be replaced in the expression. When we choose $\rho$ and $\gamma$, we can pick different types and terms to put in the expression which can give us two very different programs.

In some presentations, this is also known as the parametricity lemma. It may even be stated without the short-hand notation for equivalence we use here.

We use a number of compatibility lemmas to prove the theorem. Each of the compatibility lemmas correspond to a typing rule and essentially prove one case of the induction proof for the theorem.

4.5 Compatibility Lemmas

We state a compatibility lemma for each of the typing rules. Each of the lemmas correspond to a case in the induction proof of the Fundamental Property (Theorem 8), so the theorem will follow directly from the compatibility lemmas. We state the compatibility lemmas as rules to illustrate the connection to the typing rules:

$\inferrule*{}{\Gamma;\Delta\vdash\texttt{true}\approx\texttt{true}:bool}$ 2. 2.

$\inferrule*{}{\Gamma;\Delta\vdash\texttt{false}\approx\texttt{false}:bool}$ 3. 3.

$\inferrule*{}{\Gamma;\Delta\vdash x\approx x:\Gamma(x)}$ 4. 4.

$\inferrule*{\Delta;\Gamma\vdash e_{1}\approx e_{2}:\tau^{\prime}\rightarrow\tau\Delta;\Gamma\vdash e_{1}^{\prime}\approx e_{2}^{\prime}:\tau^{\prime}}{\Delta;\Gamma\vdash e_{1}\;e_{1}^{\prime}\approx e_{2}\;e_{2}^{\prime}:\tau}$ 5. 5.

$\inferrule*{\Delta;\Gamma,x:\tau\vdash e_{1}\approx e_{2}:\tau^{\prime}}{\Delta;\Gamma\vdash\lambda x:\tau\ldotp\;e_{1}\approx\lambda x:\tau\ldotp\;e_{2}:\tau\rightarrow\tau^{\prime}}$ 6. 6.

$\inferrule*{\Delta;\Gamma\vdash e_{1}\approx e_{2}:\forall\alpha\ldotp\tau\Delta\vdash\tau^{\prime}}{\Delta;\Gamma\vdash e_{1}[\tau^{\prime}]\approx e_{2}[\tau^{\prime}]:\tau[^{\textstyle\tau^{\prime}}/_{\textstyle\alpha}]}$

The rule for if has been omitted here. Further notice, some of the lemmas are more general than what we actually need. Take for instance the compatibility lemma for expression application. To prove the fundamental property, we really just needed to have the same expressions on both sides of the equivalence. However, the generalized version can also be used to prove that the logical relation is sound with respect to contextual equivalence.

We prove the compatibility lemma for type application here and leave the remaining proofs to the reader. To prove the compatibility lemma for type application, we are going to need the following lemma

Lemma 11** (Compositionality).**

If

• –

$\Delta\vdash\tau^{\prime}$**

• –

$\Delta,\alpha\vdash\tau$**

• –

$\rho\in\mathcal{D}\llbracket\Delta\rrbracket$**

• –

$R=\mathcal{V}\llbracket\tau^{\prime}\rrbracket_{\rho}$**

then

[TABLE]

The lemma says: syntactically substituting some type for $\alpha$ in $\tau$ and then interpreting it is the same as semantically substituting the type for $\alpha$. To prove this lemma, we would need to show $\mathcal{V}\llbracket\tau\rrbracket_{\rho}\in\operatorname{Rel}[\rho_{1}(\tau),\rho_{2}(\tau)]$ which is fairly easy given how we have defined our value interpretation.

Proof. (Compatibility, Lemma 6).

What we want to show is

[TABLE]

So we assume

1. (1)

$\Delta;\Gamma\vdash e_{1}\approx e_{2}:\forall\alpha\ldotp\tau$ 2. (2)

$\Delta\vdash\tau^{\prime}$

According to our definition of the logical relation, we need to show three things:

1. i.

$\Delta;\Gamma\vdash e_{1}[\tau^{\prime}]:\tau[^{\textstyle\tau^{\prime}}/_{\textstyle\alpha}]$ 2. ii.

$\Delta;\Gamma\vdash e_{2}[\tau^{\prime}]:\tau[^{\textstyle\tau^{\prime}}/_{\textstyle\alpha}]$ 3. iii.

$\forall\rho\in\mathcal{D}\llbracket\Delta\rrbracket\ldotp\forall\gamma\in\mathcal{G}\llbracket\Gamma\rrbracket_{\rho}\ldotp(\rho_{1}(\gamma_{1}(e_{1}[\tau^{\prime}])),\rho_{2}(\gamma_{2}(e_{2}[\tau^{\prime}])))\in\mathcal{E}\llbracket\tau[^{\textstyle\tau^{\prime}}/_{\textstyle\alpha}]\rrbracket_{\rho}$

The two first follows from the well-typedness part of (1) together with (2) and the appropriate typing rule. So it only remains to show iii.

Suppose we have $\rho\in\mathcal{D}\llbracket\Delta\rrbracket$ and $\gamma\in\mathcal{G}\llbracket\Gamma\rrbracket_{\rho}$. We then need to show:

[TABLE]

By the definition of the $\mathcal{E}$-relation, we need to show that the two terms step to two related values. We keep this goal in mind and turn our attention to (1). By definition it gives us:

[TABLE]

If we instantiate this with our $\rho$ and $\gamma$, then we get

[TABLE]

which means that $e_{1}$ and $e_{2}$ evaluate to some value $v_{1}$ and $v_{2}$ where $(v_{1},v_{2})\in\mathcal{V}\llbracket\forall\alpha\ldotp\tau\rrbracket_{\rho}$. This means that $v_{1}$ and $v_{2}$ must be of type of type $\forall\alpha\ldotp\tau$. From this, we know that $v_{1}$ and $v_{2}$ are type abstractions, so there must exist $e_{1}^{\prime}$ and $e_{2}^{\prime}$ such that $v_{1}=\Lambda\alpha.\;e_{1}^{\prime}$ and $v_{2}=\Lambda\alpha.\;e_{2}^{\prime}$. We can now instantiate $(v_{1},v_{2})\in\mathcal{V}\llbracket\forall\alpha\ldotp\tau\rrbracket_{\rho}$ with two types and a relation. We choose $\rho_{1}(\tau^{\prime})$ and $\rho_{2}(\tau^{\prime})$ as the two types for the instantiation and $\mathcal{V}\llbracket\tau^{\prime}\rrbracket_{\rho}$ as the relation121212Here we use $\mathcal{V}\llbracket\tau\rrbracket_{\rho}\in\operatorname{Rel}[\rho_{1}(\tau),\rho_{2}(\tau)]$ to justify using the value interpretation as our relation.. This gives us

[TABLE]

For convenience, we write $\rho^{\prime}=\rho[\alpha\mapsto(\rho_{1}(\tau^{\prime}),\rho_{2}(\tau^{\prime}),\mathcal{V}\llbracket\tau^{\prime}\rrbracket_{\rho})]$. By definition of the $\mathcal{E}$-relation, we know that $e_{1}^{\prime}[^{\textstyle\rho_{1}(\tau)}/_{\textstyle\alpha}]$ and $e_{2}^{\prime}[^{\textstyle\rho_{2}(\tau)}/_{\textstyle\alpha}]$ evaluate to some values $v_{1_{f}}$ and $v_{2_{f}}$, respectively, where $(v_{1_{f}},v_{2_{f}})\in\mathcal{V}\llbracket\tau\rrbracket_{\rho^{\prime}}$.

Let us take a step back and see what we have done. We have argued that the following evaluation takes place

[TABLE]

for $i=1,2$. The single step in the middle is justified by the type application reduction. The remaining steps are justified in our proof above. If we further note that $\rho_{i}(\gamma_{i}(e_{i}[\tau^{\prime}]))\equiv\rho_{i}(\gamma_{i}(e_{i}))[\rho_{i}(\tau^{\prime})]$, then we have shown that the two expressions from our goal in fact do evaluate to two values, and they are related. More precisely we have:

[TABLE]

but that is not exactly what we wanted them to be related under. We are, however, in luck and can apply the compositionality lemma (Lemma 11) to obtain

[TABLE]

which means that they are related under the relation we needed. ∎

We call theorems that follows as a consequence of parametricity for free theorems. The theorems from Section 4.2 are examples of free theorems. Next we will prove Theorem 5: All expressions of type $\forall\alpha\ldotp\alpha\rightarrow\alpha$ must be the identity function. The theorem even says that any function of this type will terminate. This is, however, trivial as System-F is a terminating language131313For more on this see Types and Programming Languages by Benjamin Pierce[Pierce, 2002].. In a non-terminating language such as System F with recursive types, we would state a weaker theorem where the expression would only have to be the identity function when it terminates. That is, divergence would also be acceptable behaviour.

Proof of Theorem 5.

From the fundamental property and the well-typedness of $e$, we know {\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e\approx e:\forall\alpha\ldotp\alpha\rightarrow\alpha. By definition this gives us

[TABLE]

We instantiate this with an empty $\rho$ and an empty $\gamma$ to get $(e,e)\in\mathcal{E}\llbracket\forall\alpha\ldotp\alpha\rightarrow\alpha\rrbracket_{\emptyset}$. By the definition of $\mathcal{E}$, we know that $e$ evaluates to some value $F$ and $(F,F)\in\mathcal{V}\llbracket\forall\alpha\ldotp\alpha\rightarrow\alpha\rrbracket_{\emptyset}$. As $F$ is a value of type $\forall\alpha\ldotp\alpha\rightarrow\alpha{}$, we know $F=\Lambda\alpha.\;e_{1}$ for some $e_{1}$. Now instantiate $(F,F)\in\mathcal{V}\llbracket\forall\alpha\ldotp\alpha\rightarrow\alpha\rrbracket_{\emptyset}$ with the type $\tau$ twice and the relation $R=\{(v,v)\}$ (Note: $R\in\operatorname{Rel}[\tau,\tau]$). This gives us $(e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}],e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}])\in\mathcal{E}\llbracket\alpha\rightarrow\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$.

Let us take a quick intermission from the proof. To a large extend, the proof of a free theorem is just unfolding of definitions. However in order for the definitions to line up, it is important that the relation $R$ is picked correctly which makes this an important non-trivial part of the proof. Before we chose the relation in this proof, we picked two types based on the theorem we want to show. In the theorem, we instantiate $e$ with $\tau$, so we picked $\tau$ for the proof. Likewise with $R$: in the theorem $v$ is the argument for the function with the domain $\alpha$, so we picked the singleton relation $\{(v,v)\}$. Picking the correct relation requires some work, but the statement can guide the decision. Finally, if you are not sure what to pick for $R$ try something and see if it works out. If it does not work, then you can simply pick a new relation and you may even have learned something to guide your next pick. Intermission over.

From $(e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}],e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}])\in\mathcal{E}\llbracket\alpha\rightarrow\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$, we know that $e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}]$ evaluates to some value $g$ and $(g,g)\in\mathcal{V}\llbracket\alpha\rightarrow\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$. From the type of $g$, we know that it must be a $\lambda$-abstraction, so $g=\lambda x:\tau\ldotp\;e_{2}$ for some expression $e_{2}$. Now instantiate $(g,g)\in\mathcal{V}\llbracket\alpha\rightarrow\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$ with $(v,v)\in\mathcal{V}\llbracket\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$ to get $(e_{2}[^{\textstyle v}/_{\textstyle x}],e_{2}[^{\textstyle v}/_{\textstyle x}])\in\mathcal{E}\llbracket\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$. From this we know that $e_{2}[^{\textstyle v}/_{\textstyle x}]$ steps to some value $v_{f}$ and $(v_{f},v_{f})\in\mathcal{V}\llbracket\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}$. We have that $\mathcal{V}\llbracket\alpha\rrbracket_{[\alpha\mapsto(\tau,\tau,R)]}\equiv R$ so $(v_{f},v_{f})\in R$ which mean that $v_{f}=v$ as $(v,v)$ is the only pair in $R$.

Now let us take a step back and consider what we have shown above.

[TABLE]

First we argued that $e[\tau]$ steps to some $F$ and that $F$ was a type abstraction, $\Lambda\alpha.\;e_{1}$. Then we performed the type application to get $e_{1}[^{\textstyle\tau}/_{\textstyle\alpha}]$. We then argued that this steps to some $g$ of the form $\lambda x:\tau\ldotp\;e_{2}$ which further allowed us to do a $\beta$-reduction to obtain $e_{2}[^{\textstyle v}/_{\textstyle x}]$. We then argued that this reduced to $v_{f}$ which was the same as $v$. In summation we argued $e[\tau]\;v\rightarrow^{*}v$ which is the result we wanted. ∎

4.6 Exercises

Prove the following free theorem:

Theorem 9**.**

If {\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash e:\forall\alpha\ldotp((\tau\rightarrow\alpha)\rightarrow\alpha) and {\raisebox{1.5pt}{\scriptstyle\bullet}};{\raisebox{1.5pt}{\scriptstyle\bullet}}\vdash k:\tau\rightarrow\tau_{k}, then

[TABLE]

This theorem is a simplified version of one found in Theorems For Free by Philip Wadler[Wadler, 1989].

5 Existential types

In this section, we extend STLC with existential types and show how to make a logical relation for that language.

An existential type is reminiscent of a Java interface. It describes some functionality but leaves out the implementation. An implementation of an existential type must provide the functions and constants specified in the type. This means that there can be many different implementations of the same existential type. When an existential type is used, the user interacts with the exposed constants and functions without knowing the actual implementation.

Take for example a stack. We would expect a stack to have the following functions:

mk

creates a new stack.

push

puts an element on the top of the stack. It takes a stack and an element and returns the resulting stack.

pop

removes the top element of the stack. It takes a stack and returns the new stack along with the element that was popped from it.

An interface would define the above signature which you then would go off and implement141414There is a famous paper called Abstract Data Types Have Existential Type from ’88 by Mitchell and Plotkin [Mitchell and Plotkin, 1988]. The title says it all.. If we wanted to write an interface for a stack, it would look like this (this is meant to be suggestive, so it is in a non-formal notation):

[TABLE]

where $\alpha$ is the type of the stack used in the actual implementation. This means that mk is a function that takes unit and returns a stack. The push function takes a stack and an element and returns a stack. Finally, the pop function takes a stack and returns a stack and an element. The $\mathit{stack}$ type all the $\alpha$’s which means that a client cannot see the actual type of the stack, so they cannot know how it is actually implemented.

We formally write existential types in a similar fashion to how we wrote universal types:

[TABLE]

Here $\tau$ is the same as the record in the stack example. The interface is just a type, so now we need to define how one implements something of an existential type. If we were to implement the stack interface, then we would implement a package of functions that are supposed to be used together. This could look something like (again this is meant to be suggestive):

[TABLE]

Here $\mathit{array}[\mathit{int}]$ is the type we want to use for the concrete implementation and the record of functions is the concrete implementation that uses $\mathit{array}[\mathit{int}]$ to implement a stack.

Existential types hide the implementation from the client, but that does not mean that they are the same. For instance, a $\mathit{stack}$ implementation could use $\mathit{int}$ for $\alpha$. In this case mk could return [math], push would throw away the $\mathit{int}$ argument, and pop would just return a pair of its $\alpha$ argument, which is an $\mathit{int}$ argument here. This implementation clearly doesn’t correspond to what we consider a stack, but it has the correct type. We would expect that all implementations of the interface that correspond to a stack would observationally behave the same. That is, we would expect them to be contextually equivalent. We want to use a logical relation to be able to establish contextual equivalence.

5.1 STLC with Existential Types

The syntactic additions to the language are pack and unpack: We briefly introduce the additions to the syntax and semantics:

[TABLE]

New packages are constructed with pack which makes it the introductory form for the existential type. A package consists of a witness type and an implementation of the existential type. Packages are opened by unpack which allows a client to use the components in the package. This makes unpack the elimination form. The interaction between the two new constructs is expressed in the following evaluation rule: \mathpar \inferrule unpack   $\langle\alpha,x\rangle$ = pack   $\langle\tau^{\prime},v\rangle$   as   ∃α.τ   in   e →e[^τ’/_α][^v/x] \endmathpar The form of the typing judgement remains the same but we add the following two rules: \mathpar \inferrule*Δ; Γ⊢e : τ[^τ’/α] Δ⊢τ’ Δ; Γ⊢pack   $\langle\tau^{\prime},e\rangle$   as   ∃α.τ : ∃α.τ \inferrule*Δ; Γ⊢e_1 : ∃α.τΔ,α;Γ,x:τ⊢e_2 : τ_2 Δ⊢τ_2 Δ; Γ⊢unpack   $\langle\alpha,x\rangle$ = e_1   in   e_2 : τ_2 \endmathpar Intuitively, the typing rule of pack says that provided an implementation of the existential type that implementation has to be well-typed when the witness type is plugged in for $\alpha$. It tells what type we substitute into. In the typing rule for unpack, it is important that $\alpha$ is not free in $\tau_{2}$ which is ensured by $\Delta\vdash\tau_{2}$. This makes sure that the package actually hides the witness type. The witness type can be pulled out of the package within a certain scope using unpack. If $\alpha$ could be returned from that scope, then it would be exposed to the outer world which would defeat the purpose of hiding it. The unpack-expression takes out the components of $e_{1}$ and calls them $\alpha$ and $x$. The two components can then be used in the body, $e_{2}$, of the unpack-expression, but they are used with the aliases given to them by unpack.

5.2 Example

For the remainder of this section, we will use the following example: Take this existential type

[TABLE]

and the following two expressions that we for now claim have type $\tau$

[TABLE]

where $\mathit{int}$ and $\mathit{bool}$ the witness types, respectively. We further claim that these two implementations of $\tau$ are equivalent, and our goal in this note is to show this.

We start by verifying that the two expressions are indeed well-typed and has type $\tau$ by constructing their type derivation trees:

[TABLE]

[TABLE]

To use a package, a client must open it with unpack first. For instance, one could attempt the following unpack:

[TABLE]

This use of unpack does, however, expose the inner workings of $e_{1}$. In particular, it exposes that $e_{1}$ uses integers as an internal representation. The existential type was supposed to hide this information making the implementation opaque, but that is clearly not the case here. The unpack-expression is even syntactically well-formed, but it is not well-typed. The witness type $\mathit{int}$ in $e_{1}$ is not exposed by unpack in the typing rule. This means that the body of an unpack should use the witness type in an abstract way, i.e. it should use $\alpha$. When we type the unpack-expression, $(\texttt{snd}\;p)$ takes an argument of type $\alpha$; but in the above expression, we give it something of type $\mathit{int}$ (if you don’t see the issue, try to construct the type derivation tree). This means that we only can give provide $(\texttt{fst}\;p)$ as an argument, i.e.

[TABLE]

It should come as no surprise that $e_{2}$ only can be used in the exact same way:

[TABLE]

It is also not type check if we return $(\texttt{fst}\;p)$ (or $(\texttt{snd}\;p)$ for that matter) as the body of an unpack cannot have the $\alpha$ free in it.

We can now informally argue why $e_{1}$ and $e_{2}$ are observationally equivalent. In both expressions, there is only one value of type $\alpha$. In $e_{1}$ it is $1$, and in $e_{2}$ it is true. This means that they are going to be the only related values, i.e. we will define $R=\{(1,\texttt{true})\}$ As we have informally argued, they are the only values the two functions can take as arguments. This means that we can easily find the values that they can possibly return: In $e_{1}$ it is $(\lambda x:x=0\ldotp\;)\;1\rightarrow\texttt{false}$, and in $e_{2}$ it is $(\lambda x:\operatorname{not}x\ldotp\;)\;true\rightarrow\texttt{false}$. The only value that is ever exposed from the package is false. If this claim is true, then it is impossible for a client to distinguish the two packages from each other.

5.3 Logical Relation

To formally argue that $e_{1}$ and $e_{2}$ from the previous section are contextually equivalent, we need a logical relation. To this end, we extend our previous logical relation, so it also interprets $\exists\alpha\ldotp\tau$. The values we relate are of the form $(\texttt{pack}\;\langle\tau_{1},v_{1}\rangle\;\texttt{as}\;\exists\alpha\ldotp\tau,\;\texttt{pack}\;\langle\tau_{2},v_{2}\rangle\;\texttt{as}\;\exists\alpha\ldotp\tau)$ and as always our first instinct should be to look at the elimination form, so we want to consider $\texttt{unpack}\;\langle\alpha,x\rangle=\texttt{pack}\;\langle\tau_{i},v_{i}\rangle\;\texttt{as}\;\exists\alpha\ldotp\tau\;\texttt{in}\;e_{i}$ for $i=1,2$. Now it would be tempting to relate the two bodies, but we get a similar issue to what we had for universal types. If we relate the two bodies, then what type should we relate them under? The type we get might be larger than the one we are interpreting which gives us a well-foundedness problem. So by analogy we do not require that the two unpack expressions have related bodies. Instead we relate $v_{1}$ and $v_{2}$ under some relation:

[TABLE]

The relation turns out to be somewhat dual to the one for universal types. Instead of saying $\forall\tau_{1},\tau_{2},R$, we say $\exists\tau_{1},\tau_{2},R$, but as we get $\tau_{1}$ and $\tau_{2}$ directly from the values, we omit them in the definition. We also relate the two values at $\tau$ and extend the relational substitution with the types we have for $\alpha$. Notice that we use $\rho$ to close of the type variables in the two values we related.

With this extension to the value interpretation, we are ready to show that $e_{1}$ and $e_{2}$ are logically related. We reuse the definition of logical equivalence we defined previously. What we wish to show is:

Theorem 10**.**

[TABLE]

Proof.

With an empty environment, this amounts to show $(e_{1},e_{2})\in\mathcal{E}\llbracket\exists\alpha\ldotp\alpha\times(\alpha\rightarrow\mathit{bool})\rrbracket_{\emptyset}$. To show this, we need to establish that $e_{1}$ and $e_{2}$ evaluate to some value and that these two values are related under the same type and relational substitution. The expressions $e_{1}$ and $e_{2}$ are pack-expressions, so they are already values. In other words, it suffices to show $(e_{1},e_{2})\in\mathcal{V}\llbracket\exists\alpha\ldotp\alpha\times(\alpha\rightarrow\mathit{bool})\rrbracket_{\emptyset}$. We now need to pick a relation and show that the implementations are related under $\alpha\times(\alpha\rightarrow\mathit{bool})$ that is

[TABLE]

We pick $R=\{(1,\texttt{true})\}$ as the relation. To two tuples are related if their components are related151515We defined this for logical predicates, but not for logical relations.. In other words, we need to show the following:

$(1,\texttt{true})\in\mathcal{V}\llbracket\alpha\rrbracket_{\emptyset[\mapsto\alpha]{(\mathit{int},\mathit{bool},R)}}$ 2. 2.

$(\lambda x:\mathit{int}\ldotp\;x=0,\lambda x:\mathit{bool}\ldotp\;\operatorname{not}\;x)\in\mathcal{V}\llbracket\alpha\rightarrow\mathit{bool}\rrbracket_{[\alpha\mapsto(\mathit{int},\mathit{bool},R)]}$

Item 1 amounts to showing $(1,\texttt{true})\in R$ which is true. In order to show 2, assume $(v_{1},v_{2})\in\mathcal{V}\llbracket\alpha\rrbracket_{[\alpha\mapsto(\mathit{int},\mathit{bool},R)]}$ which is the same as $(v_{1},v_{2})\in R$. Due to our choice of $R$, we have $v_{1}=1$ and $v_{2}=\texttt{true}$. Now we need to show $(v_{1}=0,\operatorname{not}\;v_{2})\in\mathcal{E}\llbracket\mathit{bool}\rrbracket_{[\alpha\mapsto(\mathit{int},\mathit{bool},R)]}$. Which means that we need to show that the two expressions evaluate to two values related under $\mathit{bool}$. $v_{1}=0$ evaluates to false as $v_{1}$ is 1 and $\operatorname{not}\;v_{2}$ evaluates to false as well as $v_{2}=\texttt{true}$. It remains to show $(\texttt{false},\texttt{false})\in\mathcal{V}\llbracket\mathit{bool}\rrbracket_{[\alpha\mapsto(\mathit{int},\mathit{bool},R)]}$. For base types, the value interpretation relates equal values, so this is indeed true. ∎

6 Recursive Types and Step Indexing

Consider the following program from the untyped lambda calculus:

[TABLE]

The first bit of the evaluation of $\Omega$ is a $\beta$-reduction followed by a substitution at which point we end up with $\Omega$ again. In other words, the evaluation of $\Omega$ diverges. Moreover, it is not possible to assign a type to $\Omega$ (again the interested reader may try to verify this by attempting to assign a type). It can hardly come as a surprise that it cannot be assigned a type, as we previously proved that the simply typed lambda calculus is strongly normalizing, so if we could assign $\Omega$ a type, then it would not diverge.

To type $\Omega$, we need recursive types. If we are able to type $\Omega$, then we do not have strong normalization (as $\Omega$ is not strongly normalizing). With recursive types, we can type structures that are inherently inductive such as lists, trees, and streams. In an ML-like language, a declaration of a tree type would look like this:

⬇

type tree = Leaf

        | Node of int * tree * tree

In Java, we could define a tree class with an int field and two tree fields for the sub trees:

⬇

class Tree {

int value;

Tree left, right;

}

In other words, we can define trees in common programming languages, but we cannot define them in the lambda calculus. Let us try to find a reasonable definition for recursive types by considering what properties are necessary to define trees. We want a type that can either be a node or a leaf. A leaf can be represented by unit (in our trees leafs carry no information), and a node is the product of an int and trees. We put the two constructs together with the sum type:

[TABLE]

This is what we want, but the definition is not well-founded as it is. We are defining the type $\mathit{tree}$, but $\mathit{tree}$ appears on the right hand side of the definition which makes it circular. Instead of writing $\mathit{tree}$, we use a type variable $\alpha$:

[TABLE]

All sides of the above equations are equal, and they are all trees. We could keep going and get an infinite system of equations. If we keep substituting the definition of $\alpha$ for $\alpha$, we keep getting bigger and bigger types. All of the types are trees, and all of them are finite. If we take the limit of this process, then we end up with an infinite tree, and that tree is the tree we conceptually have in our minds. So what we need is the fixed point of the above equation.

Let us define a recursive function for which we want to find a fixed point:

[TABLE]

We want the fixed point which by definition is $t$ such that

[TABLE]

So we want

[TABLE]

The fixed point of this function is written:

[TABLE]

Here $\mu$ is a fixed-point type constructor. As the above is the fixed point by definition, it should be equal to $F$ applied to it:

[TABLE]

Now let us make this look a bit more like types by substituting $F(\alpha)$ for $\tau$.

[TABLE]

The right hand side is really just $\tau$ with $\mu\alpha\ldotp\tau$ substituted with $\tau$:

[TABLE]

We introduce the recursive type $\mu\alpha\ldotp\tau$ to our language. With the recursive type, we can shift our view to an expanded version $\tau[\mu\alpha\ldotp\tau/\alpha]$ and contract back to the original type. Expanding the type is called unfold and contracting is is called fold.

[TABLE]

With recursive types in hand, we can now define our tree type:

[TABLE]

When we work with a recursive type, we need to be able to open the type and use whatever is under the $\mu$. Say we have an expression $e$ of type $\mathit{tree}$. We need to be able to tell whether it is a leaf or a node. To do so, we need to peek under the $\mu$ which is done with an unfold. The unfold gives us an expression where the type has been unfolded by one level. That is, the same expression but where $\alpha$ has been substituted with the definition of $\mathit{tree}$ and the outer $\mu\alpha\ldotp$ has been removed. With the outer $\mu\alpha\ldotp$ gone, we can match on the sum type to find out whether it is a leaf or a node. When we are done working with the type, we can fold it to get the original tree type.

tree=\mu\alpha\ldotp 1+(\mathit{int}\times\alpha\times\alpha)$$1+(\mathit{int}\times(\mu\alpha\ldotp 1+(\mathit{int}\times\alpha\times\alpha))\times(\mu\alpha\ldotp 1+(\mathit{int}\times\alpha\times\alpha)))unfoldfold

This kind of recursive types is called iso-recursive types because there is an isomorphism between a $\mu\alpha\ldotp\tau$ and its unfolding $\tau[\mu\alpha\ldotp\tau/\alpha]$.

6.1 Simply Typed Lambda Calculus with Recursive Types

The syntax of STLC with recursive types is defined as follows:

[TABLE]

Further, the following evaluation rule is added: \mathpar \inferrule unfold  (fold  v) →v \endmathpar Finally, the following typing judgements are added: \mathpar \inferrule*[right=T-Fold]{\Gamma\vdash e:\tau[\mu\alpha.\;\tau/\alpha]}{\Gamma\vdash\texttt{fold}\;e:\mu\alpha.\;\tau}$$\inferrule*[right=T-Unfold]{\Gamma\vdash e:\mu\alpha.\;\tau}{\Gamma\vdash\texttt{unfold}\;e:\tau[\mu\alpha.\;\tau/\alpha]}\endmathpar This extension allows us to define a type for lists of integers:

[TABLE]

In the lambda calculus with recursive types, the $\Omega$ function has type $(\mu\alpha\ldotp\alpha\rightarrow\alpha)\rightarrow(\mu\alpha\ldotp\alpha\rightarrow\alpha)$. We do, however, need to rewrite it slightly as applies a function found under a $\mu$, so it must first unfold it:

[TABLE]

It is indeed possible to type this version of $\Omega$:

[TABLE]

6.2 A Step-Indexed Logical Predicate

In a naive first attempt to construct the value interpretation, we could try:

[TABLE]

We can simplify this slightly; first we use the fact that $\texttt{unfold}\;(\texttt{fold}\;v)$ reduces to $v$. Next we use the fact that $v$ must be a value and the fact that we want $v$ to be in the expression interpretation of $\tau[\mu\alpha\ldotp\tau/\alpha]$. By unfolding the definition of the expression interpretation, we conclude that it suffices to require $v$ to be in the value interpretation of the same type. With these simplifications we get the following definition:

[TABLE]

This is, however, not a well-founded definition. The value interpretation is defined inductively on the type, but $\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]$ is not a structurally smaller type than $\mu\alpha\ldotp\tau$.

To solve this issue, we index the interpretation by a natural number, $k$, which we write as follows:

[TABLE]

Hence $v\in\mathcal{V}_{k}\llbracket\tau\rrbracket$ is read as “$v$ belongs to the interpretation of $\tau$ for $k$ steps.” We interpret this in the following way: given a value that is part of an evaluation for $k$ or fewer steps (in the sense that the value is plugged into a program context, and the resulting expression evaluates for fewer than $k$ steps), then the value will have type $\tau$. If we use the same value in a program context evaluates for more than $k$ steps, then we might notice that the value does not have type $\tau$ which means that we might get stuck. This gives us an approximate guarantee.

We use the step as an inductive metric to make our definition well-founded. That is we define the interpretation inductively on the step-index followed by an inner induction on the type structure. Let us start by adding the step-index to our existing value interpretation:

[TABLE]

true and false are in the value interpretation of $\mathit{bool}$ for any $k$, so true and false will for any $k$ look like it has type $\mathit{bool}$. To illustrate how to understand the value interpretation of $\tau_{1}\rightarrow\tau_{2}$, please consider the following time line:

$\lambda$ time-line k$$(\lambda x:\tau_{1}\ldotp\;e)\;e_{2}$$j+1$$(\lambda x:\tau_{1}\ldotp\;e)\;v$$\rightarrow$$j$$e[^{\textstyle v}/_{\textstyle x}][math]"future"

Here we start at index $k$ and as we run the program, we use up steps until we at some point reach [math] and run out of steps. Say we at step $k$, we have an application of a lambda abstraction. The lambda abstraction is already ready to be applied, but the application may not happen right away. The $\beta$-reduction happens when the argument is an value, but the application may contain a non-value expression as it argument, i.e. $(\lambda x:\tau_{1}\ldotp\;e)\;e_{2}$. It takes a number of steps to reduce $e_{2}$ to a value, and we have no way to tell how many it will take. All we can do is to assume that it has taken some number of steps to evaluate $e_{2}$ to $v$, so we have $j+1$ steps left. At this time, we can perform the $\beta$-reduction which means that we have $e[^{\textstyle v}/_{\textstyle x}]$ with $j$ steps left.

We can now define the value interpretation of $\mu\alpha\ldotp\tau$:

[TABLE]

This definition is almost the same as the one we proposed above but step-indexed. In order to make the definition well-founded, we require $j$ be strictly less than $k$. We do not define a value interpretation for type variables $\alpha$, as we have no polymorphism yet. The only place we have a type variable at the moment is in $\mu\alpha\ldotp\tau$, but in the interpretation we immediately close off the $\tau$ under the $\mu$, so we will never encounter a free type variable.

Finally, we define the expression interpretation:

[TABLE]

To illustrate what is going on here, consider the following time line:

k$$e$$\rightarrow\rightarrow\rightarrow\rightarrow$$k-j$$e^{\prime}[math]$j$

We start with an expression $e$, then we take $j$ steps and get to expression $e^{\prime}$. At this point, if $e^{\prime}$ is irreducible, then it must be in the value interpretation of $\tau$ for $k-j$ steps. As explained above, the step-index approximates where we only can be sure that a value has a given type if we still have steps left. In other words, if we allow the expression interpretation to spend all the steps, then we cannot say anything meaningful about the value.

We also need to lift the interpretation of type environments to step-indexing:

[TABLE]

We are now in a position to lift the definition of semantic type safety to one with step-indexing.

[TABLE]

To actually prove type safety, we do it in two steps. First we state and prove the fundamental theorem:

Theorem 11** (Fundamental property).**

If $\Gamma\vdash e:\tau$, then $\Gamma\models e:\tau$.

When we have proven the fundamental property, we prove that it entails type safety, i.e.

[TABLE]

Thanks to the way we defined the logical predicate, this second step should be trivial to prove.

The difficult part is to prove the fundamental property. This proof requires a lemma that says the value interpretation is monotone, i.e. if a value is in the value interpretation for some step, then it is also in there for any smaller step.

Lemma 12** (Monotonicity).**

If $v\in\mathcal{V}_{k}\llbracket\tau\rrbracket$ and $j\leq k$, then $v\in\mathcal{V}_{j}\llbracket\tau\rrbracket$.

Proof.

The proof is by case on $\tau$.

Case $\tau=\mathit{bool}$, assume $v\in\mathcal{V}_{k}\llbracket\mathit{bool}\rrbracket$ and $j\leq k$, we then need to show $v\in\mathcal{V}_{j}\llbracket\mathit{bool}\rrbracket$. As $v\in\mathcal{V}_{k}\llbracket\mathit{bool}\rrbracket$, we know that either $v=\texttt{true}$ or $v=\texttt{false}$. If we assume $v=\texttt{true}$, then we immediately get what we want to show, as true is in $\mathcal{V}_{j}\llbracket\mathit{bool}\rrbracket$ for any $j$. Likewise for the case $v=\texttt{false}$.

Case $\tau=\tau_{1}\rightarrow\tau_{2}$, assume $v\in\mathcal{V}_{k}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$ and $j\leq k$, we then need to show $v\in\mathcal{V}_{j}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$. As $v$ is a member of $\mathcal{V}_{k}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$, we can conclude that $v=\lambda x:\tau_{1}\ldotp\;e$ for some $e$. By definition of $v\in\mathcal{V}_{j}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$ we need to show

[TABLE]

Suppose $i\leq j$ and $v^{\prime}\in\mathcal{V}_{i}\llbracket\tau_{1}\rrbracket$, we then need to show $e[^{\textstyle v^{\prime}}/_{\textstyle x}]\in\mathcal{E}_{i}\llbracket\tau_{2}\rrbracket$.

By assumption, we have $v\in\mathcal{V}_{k}\llbracket\tau_{1}\rightarrow\tau_{2}\rrbracket$ which gives us

[TABLE]

By transitivity, $j\leq k$, and $i\leq j$, we get $i\leq k$. We use this with $v^{\prime}\in\mathcal{V}_{i}\llbracket\tau_{1}\rrbracket$ to get $e[^{\textstyle v^{\prime}}/_{\textstyle x}]\in\mathcal{E}_{i}\llbracket\tau_{2}\rrbracket$ which is what we needed to show.

Case $\tau=\mu\alpha\ldotp x$, assume $v\in\mathcal{V}_{k}\llbracket\mu\alpha\ldotp\tau\rrbracket$ and $j\leq k$, we then need to show $v\in\mathcal{V}_{j}\llbracket\mu\alpha\ldotp\tau\rrbracket$. From $v\in\mathcal{V}_{k}\llbracket\tau\rrbracket$, we conclude that there must exist a $v^{\prime}$ such that $v=\texttt{fold}\;v^{\prime}$. Now assume $i<j$ and show $v^{\prime}\in\mathcal{V}_{i}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$. From $i<j$ and $j\leq k$, we can conclude $i<k$. We use with

[TABLE]

which we get from $v\in\mathcal{V}_{k}\llbracket\mu\alpha\ldotp\tau\rrbracket$, to get $v^{\prime}\in\mathcal{V}_{i}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$. ∎

Proof (Fundamental Property, Theorem 11).

Proof by induction on the typing derivation.

Case T-Fold,

  Assume

[TABLE]

We need to show

[TABLE]

So suppose we have $k\geq 0$ and $\gamma\in\mathcal{G}_{k}\llbracket\mu\alpha\ldotp\tau\rrbracket$, then we need to show $\gamma(\texttt{fold}\;e)\in\mathcal{E}_{k}\llbracket\mu\alpha\ldotp\tau\rrbracket$ which amounts to showing $\texttt{fold}\;\gamma(e)\in\mathcal{E}_{k}\llbracket\mu\alpha\ldotp\tau\rrbracket$.

So suppose that $j<k$ and that $\texttt{fold}\;\gamma(e)\rightarrow^{j}e^{\prime}$ and $\operatorname{irred}(e^{\prime})$, then we need to show $e^{\prime}\in\mathcal{V}_{k-j}\llbracket\mu\alpha\ldotp\tau\rrbracket$. As we have assumed that $\texttt{fold}\;\gamma(e)$ reduces to something irreducible, and the operational semantics of this language are deterministic, we know that $\gamma(e)$ must have evaluated down to something irreducible. We therefore know that $\gamma(e)\rightarrow^{j_{1}}e_{1}$ where $j_{1}\leq j$ and $\operatorname{irred}(e_{1})$. Now we use our induction hypothesis:

[TABLE]

We instantiate this with $k$ and $\gamma\in\mathcal{G}_{k}\llbracket\Gamma\rrbracket$ to get $\gamma(e)\in\mathcal{E}_{k}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$. Which we then can instantiate with $j_{1}$ and $e_{1}$ to get $e_{1}\in\mathcal{V}_{k-j_{1}}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$.

Now let us take a step back and see what happened:

[TABLE]

We started with a $\texttt{fold}\;\gamma(e)$ which took $j_{1}$ steps to $\texttt{fold}\;e_{1}$. We have just shown that this $e_{1}$ is actually a value because it is in the value interpretation of $\mathcal{V}_{k-j_{1}}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$. To remind us $e_{1}$ is a value let us henceforth refer to it as $v_{1}$. We further know that $\texttt{fold}\;\gamma(e)$ reduces to $e^{\prime}$ in $j$ steps and that $e^{\prime}$ is irreducible. We can further conclude that $e^{\prime}=\texttt{fold}\;v_{1}$ and $j=j_{1}$ as the language is deterministic and $\texttt{fold}\;v_{1}$ is irreducible (because it is a value). Our proof obligation is to show $e^{\prime}=\texttt{fold}\;v_{1}\in\mathcal{V}_{k-j}\llbracket\mu\alpha\ldotp\tau\rrbracket$ to show this suppose we have $l<k-j$ (this also gives us $l<k-j_{1}$ as $j=j_{1}$). We then need to show $v_{1}\in\mathcal{V}_{l}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$, we obtain this result from the monotonicity lemma using the assumption $v_{1}\in\mathcal{V}_{k-j_{1}}\llbracket\tau[^{\textstyle\mu\alpha\ldotp\tau}/_{\textstyle\alpha}]\rrbracket$ and $l<k-j_{1}$. ∎

The $\mathit{list}$ type from Section 6.1 uses the sum type. Sums are a straight forward extension to this language. The extension of the value interpretation would be:

[TABLE]

We can use $k$ directly or $k$ decremented by one depending on whether casing should take up a step or not. Either way the definition is well-founded.

6.3 Exercises

Do the lambda and application case of the proof of the Fundamental Property (Theorem 11). 2. 2.

Try to prove the monotonicity lemma where the definition of the value interpretation has been adjusted with:

[TABLE]

This will fail, but it is instructive to see how it fails.

7 References and Worlds

This section is not based on Amal Ahmed’s lectures at OPLSS ’15, so the reader will have to make do with these notes.

7.1 STLC with References

In order to add references to STLC, we add means to allocate new references, make assignments to existing references, and dereference existing references:

[TABLE]

The expression $\texttt{ref}\;e$ allocates a new cell with an initial value specified by $e$. The expression $e\;\texttt{:=}\;e$ makes an assignment to an existing reference. The expression $\texttt{!}e$ dereferences an existing reference. We also add locations $l$ to the language. Locations are references to the heap.

In order to model references, we need to add a store or a heap to our language. Our heap $h$ is simply a finite partial map from location $\mathrm{Location}$ to the values of the language:

[TABLE]

This is a reasonable model of a real heap: The map contains all the allocated locations. Any real program will only ever allocated a finite amount of memory, and we have infinitely many available heap cells, so we do not have to worry about running out of memory.

We also need to update the operational semantics, so it has the heap available during evaluation. We update the step relation to be a partial relation on configurations where a configuration is a pair of a heap and an expression.

[TABLE]

The pure reductions of the language are all the reductions of STLC. These reductions are pure because they do not make changes to the heap. \mathpar \inferrule e →e’ $\langle h,E[e]\rangle$ →$\langle h,E[e^{\prime}]\rangle$ \endmathpar We introduce an impure reduction, i.e. a reduction that manipulate or interacts with the heap, for each of the three new ways to interact with the heap. \mathpar \inferrule*[right=E-Alloc] l ／∈dom(h) $\langle h,E[\texttt{ref}\;v]\rangle$ →$\langle h[l\mapsto v],E[l]\rangle$ \inferrule*[right=E-Assign] l ∈dom(h) $\langle h,E[l\;\texttt{:=}\;v]\rangle$ →$\langle h[l\mapsto v],E[v]\rangle$ \inferrule*[right=E-Deref] l ∈dom(h) $\langle h,E[\texttt{!}l]\rangle$ →$\langle h,E[h(l)]\rangle$ \endmathpar An allocation $\texttt{ref}\;v$ allocates a new location $l$ on the heap with the initial value $v$. The location must be new in the sense that the heap did not previously use that location. Further, we do not expose the locations in the surface language (this is enforced by the type system), so allocation is the only way to obtain locations. An assignment $l\;\texttt{:=}\;v$ updates the heap at location $l$ to point to $v$. Here the result of an assignment is the assigned value, but often it will just be unit value (we do not opt for this as we have not introduced unit value). Finally, $\texttt{!}l$ dereferences location $l$ which means that it looks up the value denoted by $l$ in the heap.

With the heap introduced, we will also have to change some of the definitions that have been reoccurring in previous sections. One such definition is $\operatorname{irred}$:

[TABLE]

For each of the new expressions, except locations, we introduce a new typing rule to the type system: \mathpar \infer*[right=T-Alloc] Γ⊢e : τ Γ⊢ref   e : ref   τ \infer*[right=T-Assign] Γ⊢e_1 : ref   *τ

Γ⊢e_2 : τ Γ⊢e_1   :=   e_2 : τ \infer[right=T-Deref] Γ⊢e : ref   τ Γ⊢! e : τ \endmathpar

We also introduce the notion of a well-types heap:

[TABLE]

7.2 Properties of STLC with References

With the language defined, we take a step back to consider what properties the language have.

The operational semantics is non-deterministic:

In the reduction rule E-Alloc, we only require $l$ to be a new location that is not in the domain of the heap. It can, however, be any new location which is the cause of the non-determinism. By leaving allocation underspecified, our system can handle different real implementations of allocation. One drawback of non-determinism is that we cannot rely on determinism in our proofs (which we have previously done).

Evaluation can get stuck:

The reduction rules for assignment and dereference require the location to be in the heap. If this is not the case, then the evaluation is stuck. One way to think of this is as a memory fault. No surface language for expressing locations is provided, so to obtain a reference one has allocate it which means that there should (hopefully) be no way to obtain a reference for memory that has not been allocated.

Only mutation on the heap:

The only place we have introduced mutation is on the heap. Variables bound with a $\lambda$-expression can still not be modified.

Values in the same memory cell stay the same type:

The type system enforces the invariant that memory cells always store values of the same type.

Recursion:

It may come as a surprise that the language has recursion as it does not have recursive types or a fixed-point operator. However, recursion can be achieved through the heap with a technique known as Landin’s knot[Landin, 1964].

We demonstrate this technique with the following program

⬇

(let x = ref (\ y : int. y) in

x := (\ n : int. (!x 0));

!x) 0

which recurses through the heap to diverge. We have written the program in an ML-style, but it can be written as a well-typed expression (see Appendix A) in the language we have presented here (assuming the trivial extension with integers). The program first allocates a new reference with a dummy value as the default value. Specifically, the dummy is chosen, so it has the type of the value we actually want to store (in this case, the dummy is the identity function on integers), but otherwise the function does not matter. The reference is stored in variable x. Next, the program assigns the function we are actually interested in to x. This function dereferences x to get a function which it applies to [math]. The function takes an integer as an argument in order to have the correct type. At the point when this function is actually applied, the location denoted by x will contain the function itself, so it will call itself repeatedly. To start the recursion, the program dereferences x, which yields the function we just described, and applies the result to 0.

The example should give an idea about how Landin’s knot can be used to emulate a fixed-point operator which gives general recursion.

7.3 Logical Predicate

In this section, we define a logical relation that we use to prove type safety of STLC with references.

We will have to deal with a couple of new things, but the main thing is how to interpret locations in the value interpretation. The interpretation will of course look something like this

[TABLE]

but what should we require from the location? To answer this question, we should consider the elimination form of things of reference type which is dereference. Dereferencing a location yields the value stored in that location of the heap, so that value should be in the value interpretation, i.e. $h(l)\in\mathcal{V}\llbracket\tau\rrbracket$. However, the value interpretation does not consider a heap in its interpretation, so we cannot write this immediately. We could try to index the value interpretation with a heap, but we are not just interested in safety with respect to one heap. Instead we need a semantic model of the heap.

A semantic model for heaps is called a world. It specifies what values one can expect to find at a given location. We will define worlds in detail later, but for now we will just assume that a world is a function from locations to value predicates. We index our value interpretation with a world, i.e.

[TABLE]

Returning to the elimination form, we still cannot express that the contents of the heap at a specific location has to be in the value interpretation. We can, however, put restrictions on what the world can allow to be at a specific position. Specifically, we want to make sure that if a location $l$ is in the value interpretation, then $l$ can only dereference values that respect safety. This can be achieved by requiring the world to only allow values that respect safety to reside at location $l$. The values that respect safety are exactly what is captured by the value interpretation, so we require the predicate at location $l$ in the world to be equal to the value interpretation.

[TABLE]

This is exactly the definition we would like for our value interpretation of reference types, but unfortunately we cannot use it. The problem is that the domain of the worlds cannot exist. To see why, we need to take a step back and consider what we have been doing when defining value interpretations so far. The value interpretations defined in previous sections have been elements in the space of all predicates over values. We call such a space the space of semantic types. For instance in Section 3, the space of semantic types $T$ was $\mathrm{Pred(\mathrm{Value})}$. The value interpretation we want now is world indexed, so it needs to be from a different space of semantic types, namely

[TABLE]

A world is a function from locations to safe values. A predicate of safe values is in the space of semantic types, so the domain of worlds is

[TABLE]

If we inline $T$ in the definition of $\mathrm{World}$, we get

[TABLE]

which is a recursive domain equation for which no solution exists. This means that we cannot have the proposed definition of the value interpretation as the worlds we need for the definition do not exist. It may not come as a surprise that the proposed definition does not work. After all, this language is similar in its attributes to STLC with recursive types. When we defined the logical relation for that language, we had to introduce step-indexing to approximate the interpretation of values. In our proposed definition, we have nothing like step-indexing, and it would be a bit surprising if we could make do without here.

The solution to circularity in the domain equation seems intuitively similar to the one for recursive types. Rather than using an exact solution to the recursive domain equation, we use an approximate solution. Developing such a solution is beyond the scope of this note, so we only present the definitions necessary to understand the rest. The following is the approximate solution:

[TABLE]

(ignore the $\mathop{\blacktriangleright}$ for now) which allows us to define the domain of worlds

[TABLE]

and finally to define the space of semantic types as

[TABLE]

In order to have an approximation, we approximate over a metric. In this case, the metric is steps. This means that our predicates should be step-indexed with a natural number which is where $\mathrm{UPred}$ comes into the picture. $\mathrm{UPred}$ defines the step-indexed, downwards closed predicates over some domain161616$\mathrm{UPred}(\mathrm{Value})$ was the space of semantic types from which we picked the value interpretation for the logical predicate for STLC with recursive types:

[TABLE]

Because of the approximation, equalities only hold true as long as we have steps left. When we run out of steps, we can no longer distinguish elements from each other and all bets are off. Such an equality is an $k$-equality: $\stackrel{{\scriptstyle\tiny{k}}}{{=}}$. An $k$-equality has properties reminiscent of step-indexed logical relation for STLC with recursive types ($\mu$LR): In $\mu$LR the step-index was the amount of steps we could take without observing that a value was not of a certain type. This meant that when we hit zero steps, everything would be in $\mu$LR. Similarly, for an $k$-equality $\stackrel{{\scriptstyle\tiny{0}}}{{=}}$ is the total relation. For $\mu$LR we had a lemma that stated that the value interpretation was downwards closed. Here we require that the $k$-equalities are downwards closed, i.e. $\stackrel{{\scriptstyle\tiny{k}}}{{=}}\subseteq\stackrel{{\scriptstyle\tiny{k+1}}}{{=}}$.

We could not solve the original domain equation due to cardinality issues related to sets. In some sense, $\mathbb{N}\xrightharpoonup{\textit{\tiny{fin}}}T$ was simply too big. In fact in order to solve the recursive domain equation, we move away from the familiar space of sets into a different space. This space can be thought of as the space of sets with additional structure. The structure is related to the step-indices, and everything in the space must preserve this structure. We mention this because all the definitions that constitute our logical predicate are in this new space which means that they must preserve the added structure of the spaces. In our proofs, we will also have to make sure this structure is preserved which we sometimes do without mention. The proofs also use some of this structure without mention. We will not prove that our definitions have the necessary structure, but we will leave it as an exercise in the end of this section.

There are still a couple of things we have not mentioned in the domain equation. The first is that the space of semantic types are monotone functions with respect to the world. Later in this section, we present the preorder the functions are monotone with respect to along with some intuition for why we want them to be monotone. We will state this as a lemma later, but we will also note that all the predicates mapped to by a world have to be monotone with respect to worlds. The second is the fact that the solution to the recursive domain equation is an isomorphism $\xi$. This means that our definitions will use $\xi$ to move between the two sides. This is also a technicality, but we include it so our definitions are correct. The third and last thing is the black triangle, known as later. The purpose of the later in the recursive domain equation is to make that space of structured sets under it small enough for a solution to exist. In practice, later makes all $k$-equalities under it go one step down. The later is important for the construction of the solution for the recursive domain equation, but that is beyond the scope of this section (we refer the interested reader to Birkedal and Bizjak [2014]).

We can now define the $k$-equality for $\mathrm{UPred}$.

Definition 3**.**

For $B\in\mathrm{UPred}(A)$ and $k\in\mathbb{N}$

[TABLE]

Definition 4**.**

For $B,C\in\mathrm{UPred}(A)$ and $k\in\mathbb{N}$

[TABLE]

That is, two predicates are $k$-equal if they are equal on all elements with smaller steps than $k$.

We can now state the value interpretation for the reference type:

[TABLE]

This is almost the same as the definition we proposed first. The only difference is that the predicate is step indexed (here we use an explicit step, but it is essentially the same as what we had for recursive types), and it uses a $k$-equality rather than a normal equality.

We also need to look at the remainder of the value interpretation. As in all the other logical predicates and relations, the boolean values are always safe, so we just need to add a step index for it to conform with the remaining definitions

[TABLE]

For the function type, we can start with a similar definition to what we had for recursive types:

[TABLE]

Recall that we consider all $j\leq k$ because an application of a lambda-abstraction may not happen immediately. Specifically, the argument may be an expression that needs to evaluate to a value before the application can take place. In this language, evaluating an expression may have side effects. It may assign new values to certain locations, which is fine as long as they are in the value interpretation, or it may also allocate new references which corresponds to adding new locations to the heap. Because of the non-determinism of location allocation, we cannot statically (that is before the execution) say what type of values will be stored where on the heap, so we the world needs to be updated dynamically with this information. To this end, we construct a future world relation that captures allocation of new locations.

Definition 5** (Future worlds).**

For worlds $W$ and $W^{\prime}$:

[TABLE]

For $W^{\prime}\sqsupseteq W$, we say $W^{\prime}$ is a future world of $W$.

The future world relation is extensional in the sense that a future world remains the same as the past world with respect to everything but possible extensions. We use this to finish our value interpretation by saying that the argument should be valid in a future world which means that it may have allocated new locations.

[TABLE]

Generally speaking, if a value is safe with respect to a world, then it should remain that even if the presence of changes to the heap. For instance, if we have a safe location $l$, i.e. a location that is in the value interpretation, then its safety should not be affected by allocation of new locations. We should still only be able to use $l$ to dereference safe values. As the future world relation models changes to the heap, we want our value interpretation to be monotone with respect to future worlds, so safe values are resilient to allocation of new references.

The expression interpretation is also going to look like the one from the logical predicate for STLC with recursive types. That is, if an expression reduces to an irreducible expression, then it must be in the value interpretation. However in this language, it is configurations and not expressions that take evaluation steps, so we need to specify with respect to what heap the expression evaluates in. To this end, we simply take any heap that satisfies the world. For a heap to satisfy a world, it should have the locations specified by the world; and for all the locations in the heap, it should contain a value permitted by the world.

Definition 6** (Heap satisfaction).**

For a heap $h$ and world $W$, we have

[TABLE]

When $h:_{k}W$ we say: $h$ ($k$-)satisfies $W$.

The future world relation is a partial order (exercise). With this definition, we are ready to state the expression interpretation:

[TABLE]

Note that for the result heap $h^{\prime}$ there should exists some future world of $W$ such that $h^{\prime}$ satisfies that world. This means that during the evaluation the expression can only have made allocations consistent with the heap it started evaluation in.

As per usual, we need to have an interpretation of typing contexts. It is defined in a straight forward manner by lifting the simple definition with worlds and step-indexing:

[TABLE]

Finally, we can state semantic type safety:

[TABLE]

7.4 Safety Proof

The safety proof has the same structure as in the previous sections where we proved safety. We do need a number of lemmas for the proof. We leave the proofs of these lemmas as exercises.

First of all, we need our logical predicate to be monotone with respect to worlds.

Lemma 13** (World monotonicity).**

For $W^{\prime}\sqsupseteq W$ we have

• •

If $(k,v)\in\mathcal{V}\llbracket\tau\rrbracket(W)$, then $(k,v)\in\mathcal{V}\llbracket\tau\rrbracket(W^{\prime})$

• •

If $(k,e)\in\mathcal{E}\llbracket\tau\rrbracket(W)$, then $(k,e)\in\mathcal{E}\llbracket\tau\rrbracket(W^{\prime})$

• •

If $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$, then $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W^{\prime})$

Note that it is not all of our definitions that are monotone with respect to future worlds. Specifically, heap satisfaction is not monotone because it would be nonsensical. If heap satisfaction was monotone, then a heap would have to be able to handle that worlds that requires more locations allocated than it has.

We also need to make sure that our definitions are downwards closed. This is reminiscent of Lemma 12 from Section 6 (we do not call it monotonicity here to not confuse it with world monotonicity). For instance, if a value is in the value interpretation at index $k$, then it should also be in there for any smaller step.

Lemma 14** (Downwards closure).**

For $j\leq k$

• •

If $(k,v)\in\mathcal{V}\llbracket\tau\rrbracket(W)$, then $(j,v)\in\mathcal{V}\llbracket\tau\rrbracket(W)$

• •

If $(k,e)\in\mathcal{E}\llbracket\tau\rrbracket(W)$, then $(j,e)\in\mathcal{E}\llbracket\tau\rrbracket(W)$

• •

If $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$, then $(j,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$

• •

If $h:_{k}W$, then $h:_{j}W$

Finally, we need a substitution lemma for the T-Abs case for the Fundamental Property proof.

Lemma 15**.**

Let $e$ be syntactically well-formed, $v$ a closed value, $\gamma$ a substitution of closed values where $x$ is not mapped

[TABLE]

We can now state and prove the fundamental property.

Theorem 12** (Fundamental Property).**

[TABLE]

Proof.

By induction over the typing derivation. In all cases, the case for $k=0$ is vacuously true as no $j<0$ exists.

Case T-True, Let $W$, $k>0$, and $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$ be given and show:

[TABLE]

To this end let $j<k$, $h$, $h^{\prime}$, and $e^{\prime}$ be given such that

• •

$h:_{j}W$,

• •

$\langle h,\texttt{true}\rangle\rightarrow^{j}\langle h^{\prime},e^{\prime}\rangle$, and

• •

$\operatorname{irred}(h^{\prime},e^{\prime})$.

By the evaluation relation, it must be the case that $j=0$, $h^{\prime}=h$ and $e^{\prime}=\texttt{true}$. Now pick $W^{\prime}=W$. By assumption we have $h:_{j}W$ which is one of the two things we need to show. The other thing we must show is $(k,\texttt{true})\in\mathcal{E}\llbracket\mathit{bool}\rrbracket(W)$. This follows immediately from the definition of the value interpretation as boolean values are always in there.

Case T-False, Analogous to the case for T-True.

Case T-Var, Also analogous to the case for T-True but to argue $(k,\gamma(x))\in\mathcal{E}\llbracket\tau\rrbracket(W)$, we use assumptions $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$ and $\Gamma\vdash x:\tau$.

Case T-Deref, Let $W$, $k>0$, and $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$ be given and show:

[TABLE]

To this end let $j<k$, $h$, $h^{\prime}$, and $e^{\prime}$ be given such that

• •

$h:_{j}W$,

• •

$\langle h,\texttt{!}\gamma(e)\rangle\rightarrow^{j}\langle h^{\prime},e^{\prime}\rangle$, and

• •

$\operatorname{irred}(h^{\prime},e^{\prime})$.

By the assumed evaluation, either the dereferenced expression $\gamma{e}$ gets stuck, or it evaluates to some value, i.e.

$\langle h,\gamma(e)\rangle\rightarrow^{j}\langle h^{\prime\prime},e^{\prime\prime}\rangle$ and $\operatorname{irred}(h^{\prime\prime},e^{\prime\prime})$ for some $h^{\prime\prime}$ and non-value $e^{\prime\prime}$. 2. 2.

$\langle h,\gamma(e)\rangle\rightarrow^{i}\langle h^{\prime\prime},v\rangle$ and for some $h^{\prime\prime}$, value $v$, and $i<j$.

In case 1, we use our induction hypothesis: $\Gamma\models e:\mathit{ref}\;\tau$. From this we conclude that $(k-j,e^{\prime\prime})\in\mathcal{V}\llbracket\mathit{ref}\;\tau\rrbracket(W^{\prime})$ for some $W^{\prime}$ which means that $e^{\prime\prime}$ is a value contradicting that it is a non-value.

In case 2, we use the same induction hypothesis to get

• •

$h^{\prime\prime}:_{k-i}W^{\prime\prime}$ and

• •

$(k-i,v)\in\mathcal{V}\llbracket\mathit{ref}\;\tau\rrbracket(W^{\prime\prime})$

for some $W^{\prime\prime}\sqsupseteq W$. By the definition of the value interpretation this means that $v=l$ for some location $l$. Now the dereference can take place, i.e.

[TABLE]

The heap only contains values, so $\langle h^{\prime\prime},h^{\prime\prime}(l)\rangle$ must be irreducible. Since we consider the assumed evaluation it must be the case that $h^{\prime}=h^{\prime\prime}$ and $e^{\prime}=h^{\prime}(l)$. We now want to pick the world necessary for the expression relation. Our pick needs to satisfy $h^{\prime}:_{k-j}W^{\prime}$ and $W^{\prime}\sqsupseteq W$. Since the dereference did not change the heap and we assumed heap satisfaction for $h^{\prime\prime}$ under $W^{\prime\prime}$, we can simply pick $W^{\prime}=W^{\prime\prime}$. However, the assumed heap satisfaction is for step $k-i$, but we need it for the smaller step $k-j$, i.e. $h^{\prime}:_{k-j}W^{\prime}$. Generally when need something for a specific step, it suffices to show it for a greater step because the result will follow from Lemma 14 which it also does in this case.

It remains to show $(k-j,h^{\prime}(l))\in\mathcal{V}\llbracket\tau\rrbracket(W^{\prime})$. That is, the value dereferenced from the heap is safe. To show this we need the following:

• •

From $h^{\prime}:_{k-i}W^{\prime}$, we get that $(k-i,h^{\prime}(l))\in\xi(W^{\prime}(l))$.

• •

From $(k-i,l)\in\mathcal{V}\llbracket\mathit{ref}\;\tau\rrbracket(W^{\prime})$, we get $\xi(W^{\prime}(l))\stackrel{{\scriptstyle\tiny{k-i}}}{{=}}\mathcal{V}\llbracket\tau\rrbracket$.

From this, we conclude $(k-i-1,h^{\prime}(l))\in\mathcal{V}\llbracket\tau\rrbracket(W)$ (remember that the definition of $k$-equality is defined in terms of $k$-cut which takes away a step). We know that $i<j$, so $k-j\leq k-i-1$, so the desired result follows from Lemma 14.

Case T-Alloc, Let $W$, $k>0$, and $(k,\gamma)\in\mathcal{G}\llbracket\Gamma\rrbracket(W)$ be given and show:

[TABLE]

To this end let $j<k$, $h$, $h^{\prime}$, and $e^{\prime}$ be given such that

• •

$h:_{j}W$ and

• •

$\langle h,\texttt{!}\gamma(e)\rangle\rightarrow^{j}\langle h^{\prime},e^{\prime}\rangle$, and

• •

$\operatorname{irred}(h^{\prime},e^{\prime})$.

By the assumed evaluation one of the following must be the case

$\langle h,\gamma(e)\rangle\rightarrow^{j}\langle h^{\prime\prime},e^{\prime\prime}\rangle$ and $\operatorname{irred}(h^{\prime\prime},e^{\prime\prime})$ for some $h^{\prime\prime}$ and non-value $e^{\prime\prime}$. 2. 2.

$\langle h,\gamma(e)\rangle\rightarrow^{i}\langle h^{\prime\prime},v\rangle$ and for some $h^{\prime\prime}$, value $v$, and $i<j$.

In case 1, we use our induction hypothesis: $\Gamma\models e:\tau$. This gives us that $(k-j,e^{\prime\prime})\in\mathcal{V}\llbracket\tau\rrbracket(W^{\prime})$ for some $W^{\prime}$ which means that $e^{\prime\prime}$ is a value contradicting that it is not.

In case 2, we use the same induction hypothesis to get

• •

$h^{\prime\prime}:_{k-i}W^{\prime\prime}$ and

• •

$(k-i,v)\in\mathcal{V}\llbracket\mathit{ref}\;\tau\rrbracket(W^{\prime\prime})$

for some $W^{\prime\prime}\sqsupseteq W$. Now that $e$ has been evaluated to a value, the allocation can happen. Therefore, the next evaluation step is

[TABLE]

As we have just been looking at the assumed evaluation and this expression is irreducible, it must be the case that $e^{\prime}=l$ and $h^{\prime}=h^{\prime\prime}[l\mapsto v]$. Now we need to pick the world for the expression interpretation. In the last step of the evaluation, a new location has been allocated on the heap, so we cannot pick the assumed world $W^{\prime\prime}$ as it does not mention this location. We do, however, use it as a basis for our world and pick $W^{\prime}=W^{\prime\prime}[l\mapsto\xi^{-1}(\mathcal{V}\llbracket\tau\rrbracket)]$, i.e. we allow anything from the value interpretation of $\tau$ to reside at location $l$ (note that we need to apply $\xi^{-1}$ for technical reasons - it can be safely ignored). This means that we need to show the following

• •

$W^{\prime}\sqsupseteq W$

By transitivity of $\sqsupseteq$ it suffices to show $W^{\prime}\sqsupseteq W^{\prime\prime}$ as we already know $W^{\prime\prime}\sqsupseteq W$. Intuitively, this follows from the fact that $W^{\prime}$ extends $W^{\prime\prime}$ with $l$. We know that $l$ is not in the domain of $W^{\prime\prime}$ by assumptions $l\notin\operatorname{dom}(h^{\prime\prime})$ and $h^{\prime\prime}:_{k-i}W^{\prime\prime}$.

• •

$h^{\prime\prime}[l\mapsto v]:_{k-j}W^{\prime}$

By the above argument, we know that $l$ is not in the domain of $h^{\prime\prime}$ and that $\operatorname{dom}(h^{\prime\prime})=\operatorname{dom}(W^{\prime\prime})$, so from the way we defined $W^{\prime}$ it easily follows that $\operatorname{dom}(h^{\prime\prime}[l\mapsto v])=\operatorname{dom}(W^{\prime})$.

Take $l^{\prime}\in\operatorname{dom}(W^{\prime})$. We need to consider two cases:

• –

$l^{\prime}=l$: In this case we must show $(k-j,h^{\prime\prime}[l\mapsto v](l))\in\xi(W^{\prime}(l))(W^{\prime})$, i.e. $(k-j,v)\in\mathcal{V}\llbracket\tau\rrbracket(W^{\prime})$, which follows by assumption and Lemma 14.

• –

$l^{\prime}\neq l$: This follows by $h^{\prime\prime}:_{k-i}W^{\prime\prime}$ and the fact that $\xi(W^{\prime\prime}(l))$ is monotone with respect to the world (to see that this must be the case, take a look at the recursive domain equation).

• •

$(k-i-1,l)\in\mathcal{V}\llbracket\mathit{ref}\;\tau\rrbracket(W^{\prime})$

This amounts to showing $\xi(W(l))=\xi(\xi^{-1}(\mathcal{V}\llbracket\tau\rrbracket))\stackrel{{\scriptstyle\tiny{k-i-1}}}{{=}}\mathcal{V}\llbracket\tau\rrbracket$ which is true as if they are equal, then they are also equal if we limit them to everything of index less than $k-i-1$.

∎

We leave the remaining cases of the above proof as exercises.

The safety predicate we used in previous sections needs to change a bit in this setting, so it takes the heap into account

[TABLE]

We now show the standard “second lemma” that says that the logical predicate is adequate to show safety.

Lemma 16**.**

[TABLE]

Proof.

Assume $\emptyset\models e:\tau$ and let $h$, $h^{\prime}$, $e^{\prime}$ be given such that $\langle h,e\rangle\rightarrow^{*}\langle h^{\prime},e^{\prime}\rangle$. Proceed by case on $\operatorname{irred}(h^{\prime},e^{\prime})$.

Case $\neg\operatorname{irred}(h^{\prime},e^{\prime})$,: In this case, it follows by definition of $\operatorname{irred}$ that there exists $h^{\prime\prime}$ and $e^{\prime\prime}$ such that $\langle h^{\prime},e^{\prime}\rangle\rightarrow\langle h^{\prime\prime},e^{\prime\prime}\rangle$.

Case $\operatorname{irred}(h^{\prime},e^{\prime})$,: Say the evaluation takes $k$ steps to do the assumed evaluation, i.e. $\langle\emptyset,e\rangle\rightarrow^{k}\langle h^{\prime},e^{\prime}\rangle$. Now use assumption $\emptyset\models e:\tau$ to get $(k+1,e)\in\mathcal{E}\llbracket\tau\rrbracket(\emptyset)$. If we use this with the assumed evaluation, $\operatorname{irred}(h^{\prime},e^{\prime})$, and the fact that $\emptyset:_{k}\emptyset$ (trivially true), then we get $W^{\prime}\sqsupseteq\emptyset$ such that $h^{\prime}:_{1}W^{\prime}$ and $(1,e)\in\mathcal{V}\llbracket\tau\rrbracket(W^{\prime})$. This means that $e$ is indeed a value. ∎

It is now a simple matter to prove type safety.

Theorem 13** (STLC with references is type safe).**

If $\emptyset\vdash e:\tau$, then $\operatorname{safe}(e)$

Proof.

Follows from Theorem 12 and Lemma 16. ∎

7.5 Exercises

Verify that the $k$-equality on $\mathrm{UPred}(A)$ satisfy the necessary properties. That is

• •

$\stackrel{{\scriptstyle\tiny{0}}}{{=}}$ is the total relation, i.e. $\forall a,a^{\prime}\in\mathrm{UPred}(A)\ldotp a\stackrel{{\scriptstyle\tiny{0}}}{{=}}a^{\prime}$.

• •

$\stackrel{{\scriptstyle\tiny{k+1}}}{{=}}\subseteq\stackrel{{\scriptstyle\tiny{k}}}{{=}}$, i.e. $\forall a,a^{\prime}\in\mathrm{UPred}(A)\ldotp a\stackrel{{\scriptstyle\tiny{k+1}}}{{=}}a^{\prime}\implies a\stackrel{{\scriptstyle\tiny{k}}}{{=}}a^{\prime}$

A $k$-equality must also satisfy the following property omitted from the above presentation

[TABLE]

That is, if two elements approximates each other for any index, then they should in fact be equal. 2. 2.

Verify that the future world relation is a partial order. That is for worlds $W$, $W^{\prime}$ and $W^{\prime\prime}$ verify that it satisfies the following three properties

• •

Reflexivity: $W\sqsupseteq W$

• •

Antisymmetry: If $W^{\prime}\sqsupseteq W$ and $W\sqsupseteq W^{\prime}$, then $W=W^{\prime}$

• •

Transitivity: If $W^{\prime}\sqsupseteq W$ and $W^{\prime\prime}\sqsupseteq W^{\prime}$, then $W^{\prime\prime}\sqsupseteq W$ 3. 3.

Prove the future world monotonicity lemma, i.e. Lemma 13. 4. 4.

Prove the downwards closure lemma, i.e. Lemma 14. 5. 5.

Prove the substitution lemma, i.e. Lemma 15. 6. 6.

In the space where the recursive domain equation is solved, functions must preserve the added structure, i.e. step indices. Specifically, all functions must be non-expansive. A function is non-expansive if it preserves $k$-equalities, i.e. $f:X\rightarrow Y$ is non-expansive if the following holds true

[TABLE]

Note that the first $k$-equality is defined for elements in $X$ and the second $k$-equality is defined for elements in $Y$. It is these $k$-equalities that must be preserved. The value interpretation is a function of the space in which the recursive domain equation is solved. Prove that this is the case. 7. 7.

Prove the remaining cases of Theorem 12, i.e. T-Assign, T-Abs, T-App, and T-If.

7.6 Further Reading

We refer the interested reader to the note Logical Relations and References [Skorstengaard, 2015] for further reading. It contains: important details that we omitted here for the sake of presentation, a more expressive language which allows for interesting examples but also calls for a different kind of world, and a logical relation rather than a predicate. There is some overlap between this section and the note in question.

Acknowledgements

It is established practice for authors to accept responsibility for any and all mistakes in documents like this. I, however, do not. If you find anything amiss, please let me know so I can figure out who of the following are to blame: Amal Ahmed, Mathias Høier, Morten Krogh-Jespersen, Kent Grigo, and Kristoffer Just Andersen.

Appendix A Landin’s Knot

In this section, we show an implementation of

⬇

(let x = ref (\ y : int. y) in

x := (\ n : int. (!x 0));

!x) 0

in the language with references presented in Section 7. We also demonstrate how this causes a recursion.

First we define the following gadgets:

[TABLE]

The implementation of the program is

[TABLE]

and it does indeed type check which the type derivation tree on the next page demonstrates:

Let $\tau=\mathit{int}\rightarrow\mathit{int}$ \mathpar \inferrule* \inferrule* \inferrule* x : ref   τ ; $\scriptstyle\bullet$⊢x : ref   τ

\inferrule* \inferrule* \inferrule* \inferrule* x : ref   τ, n : int; $\scriptstyle\bullet$⊢x : ref   τ x : ref   τ, n : int; $\scriptstyle\bullet$⊢! x : τ

\inferrule* x : ref   τ, n : int; $\scriptstyle\bullet$⊢0 : int

x : ref   τ, n : int; $\scriptstyle\bullet$⊢! x   0 : int

x : ref   τ ; $\scriptstyle\bullet$⊢λn : int.(! x   0) : τ

x : ref   τ ; $\scriptstyle\bullet$⊢x   :=   (λn : int.(! x   0)) : τ x : ref   τ ; $\scriptstyle\bullet$⊢knot: τ \endmathpar

\mathpar\inferrule

\inferrule* \inferrule* \inferrule* \inferrule* \inferrule* x : ref   τ, y : τ; $\scriptstyle\bullet$⊢x : ref   τ x : ref   τ, y : τ; $\scriptstyle\bullet$⊢! x : τ

x : ref   τ ; $\scriptstyle\bullet$⊢Landin’s: τ →τ

\inferrule* ⋮ x : ref   τ ; $\scriptstyle\bullet$⊢knot: τ

x : ref   τ ; $\scriptstyle\bullet$⊢Landin’s  knot: τ

$\scriptstyle\bullet$; $\scriptstyle\bullet$⊢(λx : ref   τ.Landin’s  knot) : ref   τ →τ

\inferrule* \inferrule* \inferrule* x : int; $\scriptstyle\bullet$⊢x : int $\scriptstyle\bullet$; $\scriptstyle\bullet$⊢dummy: int →int

$\scriptstyle\bullet$; $\scriptstyle\bullet$⊢ref   dummy : ref   τ

$\scriptstyle\bullet$; $\scriptstyle\bullet$⊢(λx : ref   (τ).Landin’s  knot)   (ref   dummy) : τ \endmathpar \mathpar \inferrule* \inferrule* ⋮ $\scriptstyle\bullet$; $\scriptstyle\bullet$⊢(λx : ref   (τ).Landin’s  knot)   (ref   dummy) : τ

\inferrule* $\scriptstyle\bullet$; $\scriptstyle\bullet$⊢0 : int

$\scriptstyle\bullet$; $\scriptstyle\bullet$⊢((λx : ref   (τ).Landin’s  knot)   (ref   dummy))   0 : int \endmathpar

In order to see how the expression diverges, we first consider the left side of the application in which the knot is prepared:

[TABLE]

With the not prepared, [math] is applied to activate it

[TABLE]

the execution keeps alternating between two configurations, so it diverges.