A Syntactic Approach to Type Soundness

Andrew K. Wright^{∗} Matthias Felleisen^{∗}

Department of Computer Science Rice University Houston, TX 77251-1892

June 18, 1992

Rice Technical Report TR91-160 To appear in: Information and Computation

Abstract

We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the technique with a type soundness theorem for the core of Standard ML, which includes the first type soundness proof for polymorphic exceptions and continuations.

1 Type Soundness

Static type systems for programming languages attempt to prevent the occurrence of type errors during execution. A definition of type error depends on a specific language and type system, but always includes the use of a function on arguments for which it is not defined, and the attempted application of a non-function. A static type system is sound if well-typed programs cannot cause type errors; a programming language with a sound static type system is strongly typed [7].

While it is easy to design a sound type system for an explicitly typed monomorphic language, the formulation of a sound type system for a language based on Hindley/Milnerstyle polymorphism and type inference is delicate [6, 8, 15, 17, 20, 37]. Although the treatment of purely functional languages is relatively well understood in this framework, the incorporation of imperative features such as references and exceptions requires extreme care, and the soundness of such systems is not obvious. A formal proof of soundness is required to lend credibility to the claim that such a system prevents type errors, and may be a crucial tool in the design of the type system.

∗This research was supported in part by the United States Department of Defense under a National Defense Science and Engineering Graduate Fellowship, by NSF grant CCR 89–17022, and by Texas Grant ARP/ATP-91 #003604-014.

We view a static type system for an implicitly typed language as a filter that selects well-typed programs from a larger universe of untyped programs. A partial function eval : Programs ⇀ Answers ∪ {wrong} defines the semantics of untyped programs. The result wrong is returned for programs whose evaluation causes a type error; eval is undefined for programs whose evaluation does not terminate. Let ▷ e : τ mean that the type system assigns program e the type τ, i.e., e is well-typed. The simplest soundness property states that well-typed programs do not yield wrong [20].

Definition (Weak Soundness) If ▷ e : τ then eval(e) ≠ wrong.

While weak soundness establishes that a static type system achieves its primary goal of preventing type errors, it is often possible to demonstrate a stronger property that relates the answer produced to the type of the program. If we view each type τ as denoting different subsets V^{τ} of the set of all answers V, then strong soundness states that an answer v produced by a terminating program of type τ is an element of the subset V^{τ}.

Definition (Strong Soundness) If ▷ e : τ and eval(e) = v then v ∈ V^{τ}.

Strong soundness permits an implementation of the language to associate the representation of a value with its type, and thereby omit the representation tags required by dynamically typed languages. Weak soundness follows from strong soundness since wrong is not a member of V^{τ} for any type τ.

Significant effort has been invested in proving type soundness for Hindley/Milner-style type systems, and their practical realization in the programming language Standard ML [22, 23]. Soundness proofs exist for the functional fragment [20, 36], for extensions including references [6, 17, 35, 37], and for a monomorphic language including first-class continuations [8]. However, there are several drawbacks to the existing proofs. Proofs of type soundness are sensitive to the precise formulation of the semantics of the language— different techniques are required for denotational versus operational formulations of the semantics, and even for different languages within the same semantic framework. The proofs for two different languages are difficult to reconcile to prove soundness for a language including features of both. The existing techniques are complicated, and the resulting proofs are lengthy and error-prone. For an illustration of the difficulties with such proofs, we refer the reader to Tofte’s [37] discussion of Damas’s [6] faulty proof of a type soundness theorem for a polymorphic language with references.

We present a simple approach to the proof of soundness for Hindley/Milner-style polymorphic type systems. Our approach is based on subject reduction, a classical result from combinatory logic [4], and on rewriting as a means to specifying operational semantics [11, 12, 13, 14]. To demonstrate the approach, we develop a proof of soundness for the core^{1} of Standard ML, which extends a functional polymorphic language with references and exceptions. We also show soundness for an extension to Standard ML with first-class continuations. In principle, our approach is uniformly applicable to any language; in practice, the resulting proofs are lengthy but simple, requiring only ordinary inductive techniques.

1Mitchell and Harper refer to the functional polymorphic sublanguage as the essence of ML [24]. However, the difficulties of typing references and exceptions [6, 17, 35, 37] and the fact that they cannot be expressed by facilities of the functional core [10] indicate that they are equally important.

In the next section, we describe a prototypical functional language with a polymorphic type system, and discuss the various approaches that have previously been used to prove type soundness. Section 3 presents the essence of our approach to proving type soundness; the remaining sections develop illustrative proofs of type soundness for a specific functional language and various extensions.

2 Previous Approaches to Proving Type Soundness

Any proof of type soundness is intimately tied to the formulation of the semantics of the language. The earlier proofs relied on denotational semantics; later proofs used structural operational semantics. The following two subsections briefly present these approaches from a historical perspective. The third subsection discusses the problems with them. We begin with a brief introduction to the formulation of Hindley/Milner-style type systems, in order to introduce our notation.

Our prototypical functional language has the following (abstract) syntax:

e ::= c | x | λx.e | e_{1} e_{2} | let x be e_{1} in e_{2}

where x ∈ Var and c ∈ Const. Constants (Const) include both data (integer, real, boolean, etc.) and operations (+, ÷, ∧, ∨, etc.). Variables (Var) are lexically scoped. Juxtaposition denotes application and is left associative; λ-expressions construct call-by-value procedural abstractions. Semantically the let-expression behaves like ((λx.e_{2}) e_{1}), binding the value of e_{1} to x in e_{2}; however, the type system allows x to be polymorphic: different occurrences of x in e_{2} may be assigned different types.

A polymorphic type system for this language has types of the form:

τ ::= ι_{1} | … | ι_{n} | τ_{1} → τ_{2}

where ι_{1}, …, ι_{n} are ground types like int and bool. The type system is formulated as a deductive proof system that assigns types to expressions. The proof system produces conclusions, or type judgments, of the form Γ ▷ e : τ, meaning that expression e has type τ in type environment Γ. Type environments are finite maps from variables to types, and are used to give types to open expressions. The typing rules are:

Γ ▷ x : τ if Γ(x) = τ (var) (const) Γ ▷ c : τ if TypeOf (c) = τ

\frac{Γ[x ↦ τ_{1}] ▷ e : τ_{2}}{Γ ▷ λx.e : τ_{1} → τ_{2}} (abs)

\frac{Γ ▷ e_{1} : τ_{1} → τ_{2} Γ ▷ e_{2} : τ_{1}}{Γ ▷ e_{1} e_{2} : τ_{2}} (app)

\frac{Γ ▷ e_{1} : τ_{1} Γ ▷ e_{2}[x ↦ e_{1}] : τ_{2}}{Γ ▷ let x be e_{1} in e_{2} : τ_{2}} (let)

The function TypeOf assigns types to constants. Γ[x ↦ τ] denotes the functional extension or update of map Γ at x to τ; e[x ↦ e′] means the capture-avoiding substitution of e′ for x in e. Programs are closed expressions. A program e is well-typed if it has a type τ in the empty type environment; we then write ▷ e : τ.

2.1 Proofs based on Denotational Semantics

Milner [20]: Milner formulated and proved a type soundness theorem for a functional language like the above based on a denotational semantics for the language of untyped expressions. The semantic domain is the solution of the following reflexive domain equation [32]:

\begin{aligned} & = & _{0} ⊕ … ⊕ _{n} ⊕ ⊕ \\ & = & → \end{aligned}

0, …, _{n} are basic domains (with bottom), such as integers and booleans; is the function domain; is a domain consisting of the single element wrong; ⊕ is the separated sum; and → builds continuous functions. The meaning function E is constructed so as to assign the denotation wrong to programs that result in type errors. To assign meanings to expressions with free variables, the meaning function takes an environment ρ : Var ∘ ⟶ , a finite map from variables to denotational values.

To establish soundness, Milner introduced a semantic relation ⊧. This relation identifies each type τ with an ideal ^{τ} of the domain [18]. An ideal is simply a subset of the domain that is closed under certain operations (subset and least upper bounds of finite consistent subsets); each of the basic domains forms an ideal. A denotational value v ∈ possesses type τ, written ⊧ v : τ, if v is a member of the ideal corresponding to τ, i.e.,

v ∈ ^{τ} iff ⊧ v : τ.

An environment ρ respects a type environment Γ, written ⊧ ρ : Γ, if the domain of ρ is at least as large as the domain of Γ, and for every variable x in the domain of Γ, ⊧ ρ(x) : Γ(x). A semantic soundness theorem states that if an expression e has type τ in type environment Γ, and if environment ρ respects Γ, then the denotation of e in ρ possesses type τ.

Theorem (Semantic Soundness) If Γ ▷ e : τ and ⊧ ρ : Γ then ⊧ E[[e]]ρ : τ.

This theorem is proved by induction on the structure of e. Strong soundness follows by restricting the theorem to closed expressions.

Theorem (Strong Soundness) If ▷ e : τ then ⊧ E[[e]]∅ : τ.

Weak soundness is a consequence of the fact that wrong does not possess any type.

Theorem (Weak Soundness) If ▷ e : τ then E[[e]]∅ ≠ wrong.

Damas [5, 6]: Damas extended Milner’s results to a language with reference cells and destructive assignment. The proof technique is derived from Milner’s technique; however, the proof is significantly more complicated. The denotational semantics uses the following domain construction:

\begin{aligned} & = & _{0} ⊕ … ⊕ _{n} ⊕ ⊕ ⊕ \\ & = & → → ⊗ \\ & = & ^{∗} \\ & = & _{⊥} \end{aligned}

where the domain of locations is the flat domain of natural numbers, is the domain of stores (sequences of values), and ⊗ is the smash product. Procedures take both an input value and a store, and produce a result and a new store. The meaning function is parameterized over both a store and an environment. Due to the presence of stores, types are no longer ideals in , but are finite maps from store typings to subsets of .^{2} A store typing is a finite map from locations to the types of values stored there. Since the semantic relation (⊧) must involve the types of values in the store, it can no longer be defined by induction on types; its existence must be established by a category theoretical argument that generalizes the technique of inclusive predicates [31]. The complexity of the semantic relation complicates the proof; indeed, Tofte found a mistake in Damas’s proof, although the theorem is not thought to be false [37: page 2].

Abadi, Cardelli, Pierce, and Plotkin [1]: Abadi et al. demonstrate type soundness for a functional language with a dynamic type and related operations. Their proof with respect to a denotational semantics is similar to Milner’s proof, although it is complicated by the presence of dynamic values. A dynamic value is a pair consisting of a value v and a tag, drawn from a set TypeCode, that encodes the type of v. The domain equation includes a domain of dynamic values :

= _{0} ⊕ … ⊕ _{n} ⊕ ⊕ ⊕
= →
= TypeCode ×

As type codes correspond to types, the denotation of a type code is a type. Types, in turn, denote ideals over , but due to the unusual element of the domain equation, establishing that types denote ideals requires extending the ideal model for recursive types [18]. The proof that the required fixed points exist in the new model involves a metric space argument, but is a straightforward extension of the original. Although the type system Abadi et al. use is not polymorphic, it should be possible to extend the type system and the soundness proof to include polymorphism.

Duba, Harper, and MacQueen [8]: Duba et al. present several languages extending a monomorphic functional core with first-class continuations in the spirit of Scheme [28]. They describe several approaches to proving type soundness for the languages. One is with respect to a continuation-passing denotational semantics, based on the following domain equations:

2This is an over-simplification; the reader interested in the precise definition is referred to Damas’s thesis [6].

\begin{aligned} & = & _{0} ⊕ … ⊕ _{n} ⊕ ⊕ \\ & = & → → \\ & = & → \\ & = & ⊕ \end{aligned}

where is the domain of continuations, and is the domain of answers. The meaning function E takes both an environment and a continuation. Two semantic relations state what it means for a value v to possess a type τ, written ⊧ v : τ, and for a continuation κ to accept a value of type τ, written ⊧ κ :: τ. These relations are defined simultaneously by induction on types. The semantic soundness theorem states that if an expression e has type τ in type environment Γ, and if ρ respects Γ, and if continuation κ accepts values of type τ, then the meaning of e in environment ρ and continuation κ is not wrong.

Theorem (Semantic Soundness) If Γ ▷ e : τ and ⊧ ρ : Γ and ⊧ κ :: τ then E[[e]]ρκ ≠ wrong.

Unlike in the purely functional setting, the semantic soundness theorem only states that well-typed programs do not go wrong (weak soundness), not that they produce answers of the expected type. To approach strong soundness, Duba et al. give an argument based on a continuation-passing-style (CPS) translation into the simply typed λ-calculus. For programs of ground type, the denotation of an expression is the same as the denotation of its CPS transform with the identity function as an initial continuation, i.e.,

E[[e]]∅ = E[[CPS(e) (λx.x)]]∅.

Since strong soundness holds for the simply typed λ-calculus, and (CPS(e) (λx.x)) has the same type as e for programs of ground type, strong soundness holds for programs of ground type. However, the argument does not extend to higher types. For further details, we refer the reader to their paper [8: page 169].

2.2 Proofs based on Structural Operational Semantics

Tofte [36, 37]: Tofte reformulated Milner’s functional language with a structural operational semantics [27]. The semantics is specified as a deductive proof system; a conclusion E ⊢ e ⇒ v of a deduction states that expression e evaluates to v in value environment E. A value environment is a finite map from variables to operational values. Values are either basic constants or closures, which result from the evaluation of λ-expressions. The soundness theorem again requires the definition of a semantic relation (⊧) between operational values and types. For basic constants, the relation is explicitly specified by the function TypeOf ; for closures, the relation is defined by induction on types, and by evaluation at correctly typed argument values. The semantic soundness theorem states that if an expression e has type τ in type environment Γ, and if environment E respects Γ, and if e evaluates to a value v in environment E, then v possesses type τ.

Theorem (Semantic Soundness) If Γ ▷ e : τ and ⊧ E : Γ and E ⊢ e ⇒ v then ⊧ v : τ.

The proof is straightforward, and proceeds by induction on the depth of the deduction of E ⊢ e ⇒ v. Strong and weak soundness follow as before.

Tofte turned to structural operational semantics in order to consider references. To this end, he reformulated the semantics with conclusions of the form s, E ⊢ e ⇒ v, s′, meaning that in environment E and store s, expression e evaluates to value v and the new store s′. The semantic relation now involves the contents of the store and the store typing (ST), a map from locations to the types of values stored there. The semantic relation s : ST ⊧ v : τ may be read as “given the ST -typed store s, value v possesses type τ.” Because of the possibility of cycles amongst references in the store, this relation is not definable by induction, but must be defined as the maximal fixed-point of a monotonic operator on the appropriate space. The semantic soundness theorem states that if an expression e has type τ in type environment Γ, and given store s of type ST, environment E respecting Γ, and that e evaluates to v and store s′, then a typing ST′ can be found for s′ such that v possesses type τ.

Theorem (Semantic Soundness) If Γ ▷ e : τ and s : ST ⊧ E : Γ and s, E ⊢ e ⇒ v, s′ then there exists ST′ such that s′ : ST′ ⊧ v : τ.

The theorem is proved by induction on the depth of the deduction of s, E ⊢ e ⇒ v, s′. Lemmas involving the semantic relation are proved using the technique of co-induction that Milner and Tofte developed for this purpose [21]. Leroy and Weis have successfully applied Tofte’s technique to show soundness for a different type system for polymorphic references [17]. Talpin and Jouvelot have also applied the technique to demonstrate soundness for a system that infers types, effects, and regions for references [35].

Duba, Harper, and MacQueen [8]: Duba et al. also present a proof of type soundness with respect to a structural operational semantics for a monomorphic language with continuations. The proof is an adaptation of Tofte’s technique; however, the semantics is significantly restructured, as the technique of defunctionalization [30] is used to represent the flow of control explicitly. The semantics has two judgment forms. The first kind of conclusion, E; K ⊢ e ⇒ v, indicates that expression e evaluates to answer v in environment E and continuation K. The second kind of conclusion, v ⊢ K ⇒ v′, indicates that continuation K evaluated at value v produces answer v′. As in the denotational case, two semantic relations are defined, indicating what it means for a value to possess a type (⊧ v : τ), and for a continuation to accept a type (⊧ K :: τ). Like the denotational case, the theorem only establishes weak soundness.

Theorem (Semantic Soundness) If Γ ▷ e : τ and ⊧ E : Γ and ⊧ K :: τ and E; K ⊢ e ⇒ v then v ≠ wrong.

It is not clear that the proof goes through in the presence of fixed-point operators [8: page 171], nor how to obtain strong soundness in this framework.

2.3 Discussion

In each case above, the proof of soundness for a language or for a different formulation of a language’s semantics involves the use of a different proof technique. The techniques are often unrelated, so they provide no guidance in proving soundness for new languages or language features. A seemingly minor extension to a language may require a complete restructuring of its denotational or structural operational semantics, and may therefore require a completely new approach to re-establish soundness. For example, in introducing references to Milner’s functional language, Damas changed the domain equations for the denotational semantics to accommodate a store component, necessitating a completely different strategy for induction. In introducing type dynamic, Abadi et al. again changed the domain equations, and extended the ideal model of types to match. To accommodate continuations, Duba et al. changed the domain equations yet again, also foregoing the tools developed by Milner and Damas. They used a separate argument to establish strong soundness. In introducing references to an operational formulation of the functional language, Tofte changed the form of judgments obtained by the semantics, and used the technique of co-induction to establish a proof. For continuations in a structural operational semantics, Duba et al. completely altered the semantics,^{3} again changing the structure of the proof dramatically.

Each of the above proofs considers a language with a single extension to a functional core. It is natural to ask whether two extensions can be merged, such that a natural union of the two type systems is sound. However, since each of the proofs involves a different technique, it is generally impossible to merge the proofs. Tofte’s proof for references and Duba et al.’s proof for continuations give no direct assurance that Standard ML’s type system is sound, even if the other features of Standard ML are ignored.

3 A Syntactic Approach to Proving Type Soundness

Our approach to type soundness is based upon an operational formulation of a language’s semantics by rewriting. Each intermediate state of an evaluation of a program is itself a program, and the evaluation of a program is performed by successive reductions into a new state: e_{1} ⟼ e_{2} ⟼ … Reduction may either continue forever (e ⇑), or may reach a final state where no further evaluation is possible: e_{1} → ⟼ e_{k} and e_{k} −̸→ e_{k+1}. Such a final state represents either an answer or a type error. Thus, proving type soundness reduces to proving that well-typed programs yield only well-typed answers.

Programming language calculi, like the λ-calculus, are the natural choice to specify the semantics of a language such that each intermediate step of evaluation is a program. Plotkin [26] shows how the semantics of a prototypical functional language relates to the λ-calculus. The λ-calculi extensions for state [12, 14] extend this strategy to languages with references and similar constructs. Likewise, the control calculi [13, 14] can be adapted to address non-local control facilities such as exceptions and first-class continuations.

Since the intermediate states of evaluation are programs, we may apply the type system to deduce a type for each state. Our strategy for proving type soundness rests upon two fundamental observations about the types of states. The first observation is that each intermediate state may be assigned the same type as the original program, i.e., reductions preserve type:

3Furthermore, they take this as “evidence that the addition of [continuations] to Standard ML would be a substantial change, rather than an incremental modification, to the language” [8: page 170]. However, we believe that this only indicates a problem with their semantic framework.

if ▷ e_{1} : τ and e_{1} ⟼ e_{2} then ▷ e_{2} : τ.

In combinatory logic, this property is known as subject reduction [4].

The second observation is that sound type systems do not assign a type to irreducible expressions that are the sources of type errors, such as 1 + true. Furthermore, any expression containing such a subexpression is untypable; we call expressions containing such irreducible subexpressions faulty:

if e is faulty, there is no τ such that ▷ e : τ.

Together, these two observations imply that all final states that can be reached from a well-typed program are well-typed answers. With a definition of eval that takes faulty expressions to wrong, the type system is weakly sound.

As all answers produced are well-typed programs, subject reduction also establishes strong soundness. To state that an answer v lies within the correct subset V^{τ} of values, we employ the type system itself:

v ∈ V^{τ} iff ▷ v : τ.

This yields a soundness theorem based on a syntactic connection between answers and types:

if ▷ e : τ then either e ⇑ or e → ⟼ v and ▷ v : τ.

Again, strong soundness follows with a definition of eval that takes faulty expressions to wrong.

In summary, proving a syntactic soundness theorem involves:

• demonstrating subject reduction,

• characterizing answers and faulty expressions, and

• showing that the faulty expressions are untypable.

The structure of the proof always remains the same, whether or not the language includes some combination of references, exceptions, continuations, or other features.

3.1 Related Work

Curry and Feys [4] introduced the notion of subject reduction for combinatory logic. In the language of combinatory logic, the CL-term e of a deduction concluding ▷ e : τ is called the subject, and the type τ is called the predicate. Subject reduction states that reduction of the subject of a deduction preserves the predicate. Subject reduction holds for terms in CL and the λ-calculus [33].

Mitchell and Plotkin [25] present a type preservation theorem, i.e., subject reduction, for a variant of the second order polymorphic λ-calculus. This language has explicitly typed declarations; the proof of type preservation is significantly simpler in the presence of such declarations. They do not develop a type soundness theorem.

Abadi et al. [1] give a proof of soundness for type dynamic with respect to a structural operational semantics, in addition to their denotationally based proof. In their structural operational semantics, substitutions are carried out immediately: λ-expressions evaluate to themselves, rather than closures, and judgments do not contain an environment component. Since answers are syntactic values, the type system can be applied to answers to show that evaluation preserves typing. Although this proof is similar to our proof of subject reduction, its extension to references or continuations apparently involves the same difficulties as Tofte’s and Duba et al.’s proofs.

3.2 Road Map

The next three sections illustrate our approach by proving soundness for several languages. Section 4 considers a functional language, similar to that considered by Milner [20]. Section 5 considers an extension to references, an extension to exceptions, and shows how the results may be merged to consider a language with both. To our knowledge, this is the first proof of soundness for exceptions. Section 6 illustrates soundness for an extension providing firstclass continuations, and is the first proof of strong type soundness for continuations in a polymorphic language. We conclude with a discussion of our technique, and suggestions for its application to other languages.

4 Functional ML

Functional ML is an applicative language with constants, call-by-value higher-order functions, and a Hindley/Milner-style polymorphic type system. A natural basis for a calculus of Functional ML is Plotkin’s untyped λ_{v}-calculus [26].

Let Var be a denumerable set of variables and Const be a set of constants. The expressions and values of Functional ML are:

(Expressions)  e ::= v | e_{1} e_{2} | let x be e_{1} in e_{2}
(Values)  v ::= c | x | Y | λx.e

where x ∈ Var and c ∈ Const. The free variables, F V (e), and bound variables of an expression are defined as usual, with λ- and let-expressions binding their variables. The let-expression binds x in e_{2} but not e_{1}, i.e., let bindings are not recursive. The fixedpoint combinator Y provides recursion. Following Barendregt [2], we adopt the convention that bound variables are always distinct from free variables in distinct expressions, and we identify expressions that differ only by a consistent renaming of the bound variables. ClosedVal is the set of values with no free variables.

4.1 Semantics

The calculus for Functional ML is based upon four relations, called notions of reduction:

(δ)  c v ⟶ δ(c, v) if δ(c, v) is defined
(β_{v})  (λx.e) v ⟶ e[x ↦ v]
(let)  let x be v in e ⟶ e[x ↦ v]
(Y )  Y v ⟶ v (λx.(Y v) x)

To abstract from the precise set of constants, we only assume the existence of a partial function:

δ : Const × ClosedVal ⇀ ClosedVal

that interprets the application of functional constants to closed values and yields closed values. The β_{v} and let reductions use substitution: the notation e[x ↦ v] means the substitution of v for free occurrences of x in e, renaming bound variables of v as necessary to avoid capture. The Y reduction introduces an abstraction around (Y v) as v must be applied to a value (x does not appear free in v by the variable conventions).

We refer to the union of these relations as v, or simply ⟶ when there is no danger of confusion. The notion of reduction v gives rise to a system of reductions, → ⟶. The relation → ⟶ is the reflexive, transitive, and compatible closure of ⟶:

\frac{e_{1} ⟶ e_{2}}{e_{1} → ⟶ e_{2}}  e_{1} → ⟶ e_{1}  \frac{e_{1} → ⟶ e_{2} e_{2} → ⟶ e_{3}}{e_{1} → ⟶ e_{3}}  \frac{e_{1} → ⟶ e_{2}}{C[e_{1}] → ⟶ C[e_{2}]} ( → ⟶)

where

C ::= [] | C e | e C | let x be C in e | let x be e in C | λx.C.

A context C is an expression with one subexpression replaced by a hole, denoted []. The expression C[e] results from placing an expression e in the hole of C; this operation may involve capture of the free variables of e by C. An equational system may be constructed as the congruence closure of v, but plays no rôle for our work.

With an appropriate choice of δ, the calculus satisfies Church-Rosser and Standardization properties; the proofs are variants of Plotkin’s proofs for the λ_{v}-calculus [26]. By Standardization, we know that an expression reduces to a value precisely if a reduction of leftmost-outermost redexes outside of abstractions leads to a value. Based on this idea, we can use the calculus to define an evaluation function [11]. Let ⟼ be the relation:

E[e] ⟼ E[e′] iff e ⟶ e′ (⟼)

where

E ::= [] | E e | v E | let x be E in e.

The special contexts E are evaluation contexts: they ensure that the leftmost-outermost reduction is the only applicable reduction in the entire program. Evaluating from left to right in an application is consistent with Standard ML. Unlike with C contexts, there is no possibility of capture when placing an expression in the hole of an evaluation context, because the hole cannot appear inside a binding construct. Let → ⟼ be the reflexive and transitive closure of ⟼. Then the partial function eval is defined for closed expressions e as:

(eval) eval(e) = v iff e → ⟼ v.

It is easy to see that the decomposition of a program into a v-redex and an evaluation context is unique. It follows that the stepping relation (⟼) is a function, and therefore that eval is a function, too.

4.2 Typing

The type system is a deductive proof system that assigns types to expressions. The types of Functional ML are:

(Types)  τ ::= ι_{1} | … | ι_{n} | α | τ_{1} → τ_{2}

where ι_{1}, …, ι_{n} are ground types for basic constants (int, bool, real, etc.), and α ranges over a denumerable set of type variables. Type variables stand for some fixed but unknown type. Function types, τ_{1} → τ_{2}, are right associative.

The polymorphic type system allows certain variables to be used with a set of different types. For example, if the identity function λx.x is let-bound to the variable f, then f may used as a function of type int → int and applied to values of type int, or f may be used as a function of type bool → bool and applied to values of type bool. Type schemes represent such sets of types (α^{∗} means zero or more distinct type variables):

(TypeSchemes)  σ ::= ∀α^{∗}.τ

The free type variables F T V (σ) of a type or type scheme are defined as usual, where ∀α_{1} … α_{n}.τ binds α_{1} through α_{n} in τ. We identify type schemes that differ only by a consistent renaming of bound type variables, or by a reordering of the binding occurrences. We also identify ∀.τ with τ, so types may be regarded as type schemes with no bound type variables.

A type scheme ∀α_{1} … α_{n}.τ represents the set of types that may be obtained from τ by substituting for α_{1} through α_{n}. This is formalized by the notion of generalization: a type scheme σ generalizes a type τ, written σ ≻ τ, if there is a substitution for the bound variables of σ yielding τ. A substitution S is a (partial) function from type variables to types. A substitution may be applied to a type in the obvious way; we write Sτ. Substitution on type schemes respects bound type variables and is capture-avoiding. Generalization of a type is defined as:

(≻) ∀α_{1} … α_{n}.τ′ ≻ τ iff Sτ′ = τ and Dom(S) = {α_{1}, …, α_{n}} for some S.

Generalization is extended to type schemes:

(≻) σ ≻ σ′ iff whenever σ′ ≻ τ then σ ≻ τ.

Some examples are:

τ ≻ τ
∀α.α → α ≻ int → int
∀α_{1}α_{2}.α_{1} → α_{2} ≻ int → bool
∀α.α → α ≻ α_{2} → α_{2}
∀α_{1}α_{2}.α_{1} → α_{2} ≻ ∀α_{1}.α_{1} → α_{2}

Generalization is a partial order on type schemes.

In order to assign types to open expressions, assumptions about the types of free variables are provided by type environments, denoted Γ. Type environments are finite maps from variables to type schemes. The free type variables F T V (Γ) of a type environment

Γ ▷ x : τ if Γ(x) ≻ τ (var) (const) Γ ▷ c : τ if TypeOf (c) ≻ τ Γ ▷ Y : ((τ_{1} → τ_{2}) → τ_{1} → τ_{2}) → τ_{1} → τ_{2} (Y)

\frac{Γ[x ↦ τ_{1}] ▷ e : τ_{2}}{Γ ▷ λx.e : τ_{1} → τ_{2}} (abs)

\frac{Γ ▷ e_{1} : τ_{1} → τ_{2} Γ ▷ e_{2} : τ_{1}}{Γ ▷ e_{1} e_{2} : τ_{2}} (app)

\frac{Γ ▷ e_{1} : τ_{1} Γ[x ↦ Close(τ_{1}, Γ)] ▷ e_{2} : τ_{2}}{Γ ▷ let x be e_{1} in e_{2} : τ_{2}} (let)

Close(τ, Γ) = ∀α_{1} … α_{n}.τ where {α_{1}, …, α_{n}} = F T V (τ) \ F T V (Γ)

Figure 1: Typing rules for Functional ML

are the free type variables of the type schemes in its range. For stating and proving various lemmas, it is convenient to define substitution on type environments pointwise, i.e., S({⟨x_{1}, σ_{1}⟩, …, ⟨x_{n}, σ_{n}⟩}) = {⟨x_{1}, Sσ_{1}⟩, …, ⟨x_{n}, Sσ_{n}⟩}.

The function TypeOf : Const → TypeSchemes associates a type scheme with every constant. Since we have not precisely specified the set of constants, Functional ML is really a class of languages parameterized by the set Const and the functions δ and TypeOf . Just as the Standardization and Church-Rosser properties restrict the admissible set of δ functions, a particular choice of Const, δ, and TypeOf must satisfy a typability condition for type soundness to hold. For every c, τ, τ′, and v,

if TypeOf (c) ≻ τ′ → τ and ▷ v : τ′,
then δ(c, v) is defined and ▷ δ(c, v) : τ.

(δ-typability)

This condition requires that δ be defined for all constants of functional type and arguments of matching type, and restricts the set of results that δ may produce. This rules out, for the moment, functional constants such as division that are not defined on all values of their input type.

A type judgment Γ ▷ e : τ for e an expression of Functional ML is the conclusion of a deduction constructed according to the inference rules in Figure 1. The judgment Γ ▷ e : τ is read “in type environment Γ, expression e has type τ”. If the type environment in a judgment is empty, we write ▷ e : τ. An expression e is a well-typed program if it is closed and there is a judgment ▷ e : τ.

In this formulation of the typing rules, only one rule is applicable to an expression. Hence if there is a deduction assigning an expression a specific type, that deduction is unique. This permits proofs by induction on the structure of a deduction for a type judgment to proceed by case analysis on the structure of the expression of the type judgment.

This type system has the important property that there is an algorithm W to determine whether an expression has a type [20]. Given a type environment and an expression, the algorithm computes a substitution and a type. The algorithm is sound [20] with respect to the type system, meaning that it infers only valid typings.

Theorem (Soundness of W) [Milner] If (S, τ) = W(Γ, e) succeeds then SΓ ▷ e : τ.

The algorithm is also complete [5], meaning that if an expression has a valid typing, then the algorithm will find a typing. Furthermore, the algorithm always terminates.

Theorem (Completeness of W) [Damas, Milner] If S_{1}Γ ▷ e : τ_{1} then (S, τ) = W(Γ, e) succeeds and there exists S′ such that S′(SΓ) = S_{1}Γ and S′Close(τ, SΓ) ≻ τ_{1}. If W(Γ, e) does not succeed, then it stops with fail.

Proving completeness involves demonstrating that if an expression has a type, then it has a principal type, of which all others are substitution instances.

Theorem (Principal Typing) If Γ ▷ e : τ_{1} then there exists τ such that Γ ▷ e : τ and whenever Γ ▷ e : τ_{2} then Close(τ, Γ) ≻ τ_{2}. The type τ is principal for e in Γ.

The existence of a sound and complete algorithm establishes the decidability of the type system. However, this is solely a property of the type system, and says nothing about the relation of the type system to the semantics of the language.

4.3 Type Soundness

Our proof of type soundness rests upon the notion of subject reduction [4]. The subject reduction property states that reductions preserve the type of expressions. Lemma 4.3 below extends subject reduction to Functional ML.

Subject reduction by itself is not sufficient for type soundness. In addition, we must prove that programs containing type errors are not typable. Put differently, if an expression e is irreducible due to some type error, say (/ 1 0), then the type system should not be able to assign a type to the expression. Otherwise, a well-typed program could reduce to such an expression without violating subject reduction, and still cause a type error to occur. We call such expressions with type errors faulty expressions and prove that faulty expressions cannot be typed.

Some obvious facts about deductions that we use with no more ado are:

(i) if Γ ▷ C[e] : τ then there exist Γ′ and τ′ such that Γ′ ▷ e : τ′;

(ii) if there are no Γ′, τ′ such that Γ′ ▷ e : τ′, then there are no Γ, τ such that Γ ▷ C[e] : τ.

These follow from the facts that (1) there is exactly one inference rule for each expression form, and (2) each inference rule requires a proof for each subexpression of the expression in its conclusion. Several facts about generalization follow from the definition of Close:

(i) if σ′ ≻ σ then Close(τ_{1}, Γ[x ↦ σ′]) ≻ Close(τ_{1}, Γ[x ↦ σ]);

(ii) if x ∉ Dom(Γ) then Close(τ_{1}, Γ) ≻ Close(τ_{1}, Γ[x ↦ σ]).

The following lemma states that extra variables in the type environment Γ of a judgment Γ ▷ e : τ that are not free in the expression e may be ignored.

Lemma 4.1 If Γ(x) = Γ′(x) for all x ∈ F V (e), then Γ ▷ e : τ iff Γ′ ▷ e : τ.

A key lemma that we use in the proof of Subject Reduction for Functional ML and its extensions is the Replacement Lemma, adapted from Hindley and Seldin [16: page 181]. This allows the replacement of one of the subexpressions of a typable expression with another subexpression of the same type, without disturbing the type of the overall expression.

Lemma 4.2 (Replacement) If :

(i) D is a deduction concluding Γ ▷ C[e_{1}] : τ,

(ii) D_{1} is a subdeduction of D concluding Γ′ ▷ e_{1} : τ′,

(iii) D_{1} occurs in D in the position corresponding to the hole ([]) in C, and

(iv) Γ′ ▷ e_{2} : τ′,

then Γ ▷ C[e_{2}] : τ.

Proof. We think of deductions as trees with the conclusion at the root. Let D_{2} be the deduction concluding Γ′ ▷ e_{2} : τ′. Cut the subtree D_{1} out of D and replace it with D_{2}. Replace all relevant occurrences of e_{1} in the resulting tree with e_{2}. Then the resulting tree is a valid deduction concluding Γ ▷ C[e_{2}] : τ, as may be shown by induction on the height of the tree [16: page 181].

Subject reduction for Functional ML states that the reductions of v preserve type.

Main Lemma 4.3 (Subject Reduction) If Γ ▷ e_{1} : τ and e_{1} ⟶ e_{2} then Γ ▷ e_{2} : τ.

Proof. The proof proceeds by case analysis according to the reduction e_{1} ⟶ e_{2}.

Case c v ⟶ δ(c, v). Then Γ ▷ c : τ′ → τ and Γ ▷ v : τ′ follow from Γ ▷ c v : τ by app. Hence Γ ▷ δ(c, v) : τ by the δ-typability condition.

Case (λx.e) v ⟶ e[x ↦ v]. From Γ ▷ (λx.e) v : τ we have Γ ▷ v : τ′ and Γ ▷ λx.e : τ′ → τ by app. From the latter, Γ[x ↦ τ′] ▷ e : τ follows by abs. Hence Γ ▷ e[x ↦ v] : τ by Lemma 4.4.

Case let x be v in e ⟶ e[x ↦ v]. From Γ ▷ let x be v in e : τ we have Γ ▷ v : τ′ and Γ[x ↦ Close(τ′, Γ)] ▷ e : τ by let. As Close(τ′, Γ) = ∀α_{1} … α_{n}.τ′ where

{α_{1}, …, α_{n}} = F T V (τ′) \ F T V (Γ), we have Γ ▷ e[x ↦ v] : τ by Lemma 4.4.

Case Y v ⟶ v (λx.(Y v) x). From Γ ▷ Y v : τ, where τ = τ_{1} → τ_{2}, by Y and app

Γ ▷ v : (τ_{1} → τ_{2}) → τ_{1} → τ_{2}. (1)

Then from Γ ▷ Y v : τ,

Γ[x ↦ τ_{1}] ▷ Y v : τ_{1} → τ_{2}  by Lemma 4.1,
Γ[x ↦ τ_{1}] ▷ (Y v) x : τ_{2}  by app,
Γ ▷ λx.(Y v) x : τ_{1} → τ_{2}  by abs,
Γ ▷ v (λx.(Y v) x) : τ_{1} → τ_{2}  by app with (1).

This completes the essence of the proof. It remains to establish several lemmas.

A Substitution Lemma is the key to showing type preservation for reductions involving substitution.

Lemma 4.4 (Substitution) If Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e : τ′ and x ∉ Dom(Γ) and Γ ▷ v : τ and {α_{1}, …, α_{n}} ∩ F T V (Γ) = ∅ then Γ ▷ e[x ↦ v] : τ′.

Proof. We proceed by induction on the length of the proof of Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e : τ′, and case analysis on the last step.

Case e = c. Then TypeOf (c) ≻ τ′ by const, and thus Γ ▷ c : τ′ by const. Then Γ ▷ c[x ↦ v] : τ′ since c[x ↦ v] = c.

Case e = x′. If x′ ≠ x, then Γx′ ≻ τ′ by var, and Γ ▷ x′ : τ′ again by var. Hence Γ ▷ x′[x ↦ v] : τ′ since x′[x ↦ v] = x′.

If x′ = x, then by var

Γ[x ↦ ∀α_{1} … α_{n}.τ](x) ≻ τ′
i.e. ∀α_{1} … α_{n}.τ ≻ τ′,

i.e. we can find a substitution S with domain {α_{1}, …, α_{n}} such that Sτ = τ′. Next, we have SΓ ▷ v : Sτ by Lemma 4.5 since Γ ▷ v : τ, and therefore SΓ ▷ v : τ′. But Dom(S) ∩ F T V (Γ) = ∅, so SΓ = Γ. Also x[x ↦ v] = v, hence Γ ▷ x[x ↦ v] : τ′.

Case e = λx′.e_{1}. By abs, it follows from the assumption Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ λx′.e_{1} : τ′ that τ′ = τ_{1} → τ_{2}, and

Γ[x ↦ ∀α_{1} … α_{n}.τ][x′ ↦ τ_{1}] ▷ e_{1} : τ_{2}
i.e. Γ[x′ ↦ τ_{1}][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : τ_{2}.

Choose a substitution S : {α_{1}, …, α_{n}} → {α′_{1}, …, α′_{n}} such that α′_{1}, …, α′_{n}, α_{1}, …, α_{n}, and F T V (Γ) are all distinct. Then

(2)  Γ[x′ ↦ Sτ_{1}][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : Sτ_{2} by Lemma 4.5,
(3)  Γ[x′ ↦ Sτ_{1}] ▷ v : τ  by Lemma 4.1, and
(4)  F T V (Γ[x′ ↦ Sτ_{1}]) ∩ {α_{1}, …, α_{n}} = ∅  by the choice of S.

Thus, Γ[x′ ↦ Sτ_{1}] ▷ e_{1}[x ↦ v] : Sτ_{2} by the inductive hypothesis with (2), (3), and (4). Since S is a bijection, S^{−1} exists, hence

S^{−1}(Γ[x′ ↦ Sτ_{1}]) ▷ e_{1}[x ↦ v] : S^{−1}(Sτ_{2}) by Lemma 4.5,
i.e. Γ[x′ ↦ τ_{1}] ▷ e_{1}[x ↦ v] : τ_{2}.

But then

Γ ▷ λx′.e_{1}[x ↦ v] : τ_{1} → τ_{2}  by abs,
i.e. Γ ▷ (λx′.e_{1})[x ↦ v] : τ_{1} → τ_{2}.

Syntactic Type Soundness 17 Case e = (e_{1} e_{2}). From Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ (e_{1} e_{2}) : τ′ by the first premise of app

Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : τ_{1} → τ′

(5) Γ ▷ e_{1}[x ↦ v] : τ_{1} → τ′ by ind. hyp.

By the second premise of app

Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{2} : τ_{1}

(6) Γ ▷ e_{2}[x ↦ v] : τ_{1} by ind. hyp.

Then by app with (5) and (6)

Γ ▷ (e_{1}[x ↦ v] e_{2}[x ↦ v]) : τ′

i.e. Γ ▷ (e_{1} e_{2})[x ↦ v] : τ′.

Case e = let x′ be e_{1} in e_{2}. By the first premise of let

Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : τ_{1}

(7) Γ ▷ e_{1}[x ↦ v] : τ_{1} by ind. hyp.

By the second premise of let

Γ[x ↦ ∀α_{1} … α_{n}.τ][x′ ↦ Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ e_{2} : τ′

(8)  i.e. Γ[x′ ↦ Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{2} : τ′.

Since Γ ▷ v : τ

(9) Γ[x′ ↦ Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ v : τ by Lemma 4.1.

Now

{α_{1}, …, α_{n}} ∩ F T V (Γ[x′ ↦ Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])])
⊆ {α_{1}, …, α_{n}} ∩ (F T V (Γ) ∪ F T V (Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])))
= {α_{1}, …, α_{n}} ∩ F T V (Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ]))
= {α_{1}, …, α_{n}} ∩ (F T V (τ_{1}) \ (F T V (τ_{1}) \ F T V (Γ[x ↦ ∀α_{1} … α_{n}.τ])))
= {α_{1}, …, α_{n}} ∩ F T V (τ_{1}) ∩ F T V (Γ[x ↦ ∀α_{1} … α_{n}.τ])
⊆ {α_{1}, …, α_{n}} ∩ (F T V (Γ) ∪ F T V (∀α_{1} … α_{n}.τ))
= {α_{1}, …, α_{n}} ∩ F T V (∀α_{1} … α_{n}.τ)
= {α_{1}, …, α_{n}} ∩ (F T V (τ) \ {α_{1}, …, α_{n}})
= ∅

so by the inductive hypothesis with (8) and (9)

Γ[x′ ↦ Close(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ e_{2}[x ↦ v] : τ′

Γ[x′ ↦ Close(τ_{1}, Γ)] ▷ e_{2}[x ↦ v] : τ′  by Lemma 4.6,
Γ ▷ let x′ be v_{1}[x ↦ v] in e_{2}[x ↦ v] : τ′  by let with (7),
i.e. Γ ▷ (let x′ be v_{1} in e_{2})[x ↦ v] : τ′.

Lemma 4.5 establishes that typing is stable under substitution.

Lemma 4.5 If Γ ▷ e : τ and S is a substitution then SΓ ▷ e : Sτ.

Proof. The proof proceeds by induction on the length of the proof of Γ ▷ e : τ and case analysis on the last step. The proof is an adaptation of Tofte’s proof of a similar lemma [37: lemma 4.2].

Finally, Lemma 4.6 shows that generalizing the type of a variable in the type environment has no impact on the conclusion of a deduction.

Lemma 4.6 If Γ[x ↦ σ] ▷ e : τ and σ′ ≻ σ then Γ[x ↦ σ′] ▷ e : τ.

Proof. The proof proceeds by induction on the length of the proof of Γ[x ↦ σ] ▷ e : τ and case analysis on the last step. The proof is an adaptation of Damas and Milner’s proof of a similar lemma [5: lemma 1]. The only interesting case is the case for let-expressions.

Case e = let x′ be e_{1} in e_{2}. By the first premise of let

Γ[x ↦ σ] ▷ e_{1} : τ_{1}
(10)  Γ[x ↦ σ′] ▷ e_{1} : τ_{1}  by ind. hyp.

By the second premise of let

Γ[x ↦ σ][x′ ↦ Close(τ_{1}, Γ[x ↦ σ])] ▷ e_{2} : τ
Γ[x ↦ σ′][x′ ↦ Close(τ_{1}, Γ[x ↦ σ])] ▷ e_{2} : τ by ind. hyp.
(11)  Γ[x ↦ σ′][x′ ↦ Close(τ_{1}, Γ[x ↦ σ′])] ▷ e_{2} : τ by ind. hyp.

Then Γ[x ↦ σ′] ▷ let x′ be e_{1} in e_{2} : τ by let with (10) and (11).

A corollary of Subject Reduction is that standard reduction steps preserve type.

Corollary 4.7 If Γ ▷ e_{1} : τ and e_{1} → ⟼ e_{2} then Γ ▷ e_{2} : τ.

Proof. First, if e_{1} ⟼ e_{2} then e_{1} = E[e] and e_{2} = E[e′] and e ⟶ e′, so Γ ▷ e_{2} : τ by the Replacement Lemma. Then the result follows by induction on the length of the reduction sequence e_{1} → ⟼ e_{2}.

Subject reduction ensures that if we start with a typable expression, we cannot reach an untypable expression through any sequence of reductions. This by itself, however, does not yield type soundness. Subject reduction simply ensures that any properties implied by typability are preserved by reduction. The critical property we seek is that evaluation of a typable expression cannot get stuck.

Definition 4.8 (Stuck Expressions) The evaluation of an expression e is stuck if e is not a value and there is no e′ such that e ⟼ e′.

Of course, whether an expression eventually reduces to a stuck expression is not a decidable property. We approximate the set of expressions that become stuck with a set of faulty expressions.

Definition 4.9 (Faulty Expressions) The faulty expressions of Functional ML are the expressions containing a subexpression (c v) where δ(c, v) is undefined.

The idea is that any faulty expression may become stuck, i.e., the property “reduces to a faulty expression” is a conservative approximation to “reduces to an expression that is stuck”. Thus the faulty expressions are a superset of the stuck expressions. For example, the expression ((λy.2) (λx.+ 1 true)) is faulty because of the subexpression (+ 1 true), but is not stuck because it reduces to 2.

The behavior of evaluation is summarized by the following lemma. Let e ⇑ mean that e diverges, i.e., e ⟼ e′ for some e′, and for all e′ such that e → ⟼ e′, there exists e′′ such that e′ ⟼ e′′.

Lemma 4.10 (Uniform Evaluation) For closed e, if there is no e′ such that e → ⟼ e′ and e′ is faulty, then either e ⇑ or e → ⟼ v.

Proof. By induction on the length of the reduction sequence, we need only show that either e is faulty, e ⟼ e′ and e′ is closed, or e is a value. From the definition of ⟼, e ⟼ e′ iff e = E[e_{1}], e′ = E[e′_{1}], and e_{1} ⟶ e′_{1}. (Recall that E ::= [] | E e | v E | let x be E in e.) We proceed by induction on the structure of e.

Case e = c, Y, or λx.e. Then e is a value.

Case e = x. Since e is closed, this case cannot occur.

Case e = let x be e_{1} in e_{2}. By the inductive hypothesis with e_{1}, there are three cases to consider. If e_{1} is faulty, then let x be e_{1} in e_{2} is faulty. If e_{1} = E_{1}[e′] and e′ ⟶ e′′ then e = E[e′] where E = let x be E_{1} in e_{2}; thus e ⟼ E[e′′]. Otherwise, if e_{1} is a

value, then let x be e_{1} in e_{2} ⟼ e_{2}[x ↦ e_{1}].

Case e = (e_{1} e_{2}). By the inductive hypothesis with e_{1}, there are three cases to consider. If e_{1} is faulty, then (e_{1} e_{2}) is faulty. If e_{1} = E_{1}[e′] and e′ ⟶ e′′ then e = E[e′] where E = (E_{1} e_{2}); thus e ⟼ E[e′′]. Otherwise, e_{1} is a value. By the inductive hypothesis with e_{2}, there are three subcases to consider. If e_{2} is faulty, then (e_{1} e_{2}) is faulty. If e_{2} = E_{2}[e′] and e′ ⟶ e′′ then e = E[e′] where E = (e_{1} E_{2}); thus e ⟼ E[e′′]. Otherwise, both e_{1} and e_{2} are values, and the possibilities can be summarized as follows:

e e_{2}_{1}  c  λx.e  Y  x
c ⟼ or ; faulty  ⟼ or ; faulty  ⟼ or ; faulty ×
λx.e  ⟼  ⟼  ⟼  ×
Y  ⟼  ⟼  ⟼  ×
x  ×  ×  ×  ×

Cases marked with × cannot occur because the expression is not closed. Cases marked with ⟼ indicate that the combination reduces with E = [].

To relate faulty expressions and typability, we show that no faulty expression is typable.

Main Lemma 4.11 (Faulty Expressions are Untypable) If e is faulty, there are no Γ, τ such that Γ ▷ e : τ.

Proof. It suffices to show that the subexpressions of e that cause e to be faulty are untypable. In general, we proceed by case analysis according to the form of the subexpression, but for Functional ML there is only one case.

Suppose (c v) is faulty and Γ ▷ c v : τ. By app, Γ ▷ c : τ′ → τ and Γ ▷ v : τ′. Then by the δ-typability condition, δ(c, v) is defined, but this contradicts the assumption that (c v) is faulty.

Since the faulty expressions are untypable and we have type preservation, the property “does not reduce to a faulty expression” is implied by typability.^{4}

Theorem 4.12 (Syntactic Soundness) If ▷ e : τ then either e ⇑ or e → ⟼ v and ▷ v : τ.

Proof. By Uniform Evaluation, either e → ⟼ e′ and e′ is faulty, or e ⇑, or e → ⟼ v. Since ▷ e : τ, Subject Reduction implies ▷ v : τ and ▷ e′ : τ. Suppose e → ⟼ e′ and e′ is faulty. Since faulty expressions are untypable, ▷ e′ : τ is a contradiction, therefore this case cannot occur. Hence either e ⇑ or e → ⟼ v and ▷ v : τ.

To state strong and weak soundness theorems, we must have a definition of evaluation that differentiates between programs that diverge and those that cause type errors. Let answers (a) be values or the special result wrong, and define eval′ as:

(eval′) eval′(e) = \{ \begin{matrix}wrong & if e → ⟼ e′ and e′ is faulty; \\ v & if e → ⟼ v. \end{matrix}

Programs that cause a type error return the special answer wrong. Strong and weak soundness are now corollaries of Syntactic Soundness.

Theorem 4.13 (Strong Soundness) If ▷ e : τ and eval′(e) = a then ▷ a : τ.

Theorem 4.14 (Weak soundness) If ▷ e : τ then eval′(e) ≠ wrong.

5 References and Exceptions

Besides functional facilities, first-class references and exceptions are the most important core programming facilities of Standard ML and similar languages. In this section we consider several extensions to Functional ML. The first subsection deals with Reference ML, an extension of Functional ML with references. It uses our previous work on a calculus of state, λ_{v}-S [12, 14], and in particular its cell-oriented variant [3]. The second subsection addresses Exception ML, an extension of Functional ML with exceptions. It uses a modified version of our control calculus, λ_{v}-C [13, 14], especially its fragment with prompts [9]. The final subsection presents Core ML, which includes both references and exceptions.

4Type preservation by itself does not guarantee type soundness. Consider the (trivial) type system where every type is a subtype of every other type. Type preservation holds since every expression can be assigned every type. However, the system does not prevent type errors, because it rejects no expressions.

5.1 Reference ML

Extending the λ_{v}-calculus to a calculus of functions and references requires extending the syntax with a new kind of expression and several new values (underlined):

(Expressions)  e ::= v | e_{1} e_{2} | let x be e_{1} in e_{2} | \underline{ρθ.e}
(Values)  v ::= c | x | Y | λx.e | \underline{ref} | \underline{!} | \underline{:=} | \underline{:= v}
\underline{θ} ::= \underline{\{ ⟨x, v⟩ \}^{∗}}

The expression ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e binds x_{1}, …, x_{n} in v_{1}, …, v_{n} and e. Above, θ represents a finite function from variables to values, i.e., we treat θ as a set of pairs whose first components are distinct. We also identify all ρ-expressions that differ only by a consistent renaming of bound variables.

The values ref, !, and := are the familiar operations of ML.^{5} The application of ref to a value creates a reference cell containing that value. The application of ! to a cell returns the value contained in that cell. The binary assignment operator := evaluates both its operands, the first of which must evaluate to a cell, and assigns the value of the second operand to that cell. Since all operations are curried, the application of the assignment operator to a variable is a value. Specifically, the expression (:= c) may be thought of as a capability to assign to the cell c. The ρ-expression is semantically an abbreviation of a let-expression:

ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e
≡ let x_{1} be ref u_{1} in
…
let x_{n} be ref u_{n} in
(λy_{1} … y_{n}y_{n+1}. y_{n+1}) (:= x_{1} v_{1}) … (:= x_{n} v_{n}) e

where u_{1}, …, u_{n} are arbitrary values (of the right type). In order to simplify the semantics, we do not treat it as such [14]. Intuitively, a ρ-expression plays the rôle of a store fragment during the reduction of a program with imperative assignment statements. A reference cell is represented as a variable; the pair ⟨x, v⟩ in a ρ-expression indicates that reference cell x contains value v.

5.1.1 Semantics

In addition to the reductions for v, the reductions for references are:^{6}

(ref )  ref v ⟶ ρ⟨x, v⟩.x
(deref )  ρθ⟨x, v⟩.R[! x] ⟶ ρθ⟨x, v⟩.R[v]
(assign)  ρθ⟨x, v_{1}⟩.R[:= x v_{2}] ⟶ ρθ⟨x, v_{2}⟩.R[v_{2}]
(ρ_{merge})  ρθ_{1}.ρθ_{2}.e ⟶ ρθ_{1}θ_{2}.e
(ρ_{lift})  R[ρθ.e] ⟶ ρθ.R[e] if R ≠ []

5Introducing ref, !, and := as values rather than special forms like (ref e), (! e), and (:= e_{1} e_{2}) simplifies the proofs of several lemmas that proceed by induction on the structure of expressions. The latter approach requires duplicating much of the work of the case for applications.

6This semantics is due to Crank and Felleisen [3], which was derived from Felleisen and Hieb’s work [14].

A similar definition of evaluation for dealing with state using rewriting techniques also appears in the work of Mason and Talcott [19].

By the variable conventions, x is not free in v in the ref reduction; the domains of θ_{1} and θ_{2} are disjoint in ρ_{merge}; and the free variables of R are disjoint from the domain of θ in ρ_{lift}. We refer to the union of these five reductions as r. The notions of reduction r and v (adapted mutatis mutandis to the full syntax) form the basis for a calculus of functions and references. We refer to the union as vr, and write ⟶^{vr} for a reduction in vr. The extended notion of reduction gives rise to a system of reductions and equations with the extension of contexts to:

C ::= [] | C e | e C | let x be C in e | let x be e in C | λx.C | ρθ.C | ρθ⟨x, C⟩.e.

The calculus satisfies the same basic properties as the λ_{v}-calculus [3].

The definition of r relies on a set of R contexts:

R ::= [] | R e | v R | let x be R in e.

The use of R contexts in the new reductions reflects the additional sequencing restrictions that the introduction of side-effects in a programming language requires for the semantics to be deterministic. In particular, the creation, the dereferencing, and the updating operations on a reference cell must be ordered in a linear fashion, which implies some further ordering among the operations on distinct cells. The R contexts build this minimal order of evaluation into those reductions that refer to reference cells and their operations; following ML, we choose to perform operations from left to right.

For r reductions, a cell is represented by an ordinary variable appearing in the domain of a store fragment θ. When a program creates a new cell via ref, the ref reduction introduces a ρ-expression that records the cell’s current value. The dereference operator ! selects a cell’s value from the closest ρ-expression (relative to R contexts). If the appropriate cell is bound in a ρ-expression that is not the closest one, the intervening ρ-expressions must first be merged with the outer one. This is accomplished with ρ_{lift} and ρ_{merge} reductions, which lift a partial store out of R contexts, and merge it with outer stores (by the variable convention, cells are renamed appropriately to avoid collisions). An assignment replaces a cell’s current value in the closest ρ-expression, after performing all necessary lift and merge steps, and returns the assigned value.

For example, consider the following expression:

((let x be ref (λx.+ !x 2) in := x (λx.+ !x 3)) (let x be ref 2 in (λz.x)(:= x 4)))

In this expression, the two assignments can happen in an arbitrary order, and the system of reductions admits both possibilities. Both assignments, however, must happen before the outermost application is reduced. Figure 2 gives one possible reduction sequence.

The above calculus only constrains the relative ordering of ref , deref , and assign reductions. By defining extended evaluation contexts:

E ::= [] | E e | v E | let x be E in e | ρθ.E

we fix the order in which reductions in v and ref , deref , and assign may be applied. The stepping function ⟼^{vr} is defined as before. To show that ⟼^{vr} is a function requires a simple

((let x be ref (λx.+ !x 2) in := x (λx.+ !x 3)) (let x be ref 2 in (λz.x)(:= x 4)))

→ ⟶ (ρ⟨x, λx.+ !x 2⟩.:= x (λx.+ !x 3)) (ρ⟨x, 2⟩.(λz.x)(:= x 4)) 2 × ref , ρ_{lift}, let
→ ⟶ (ρ⟨x, λx.+ !x 3⟩.λx.+ !x 3) (ρ⟨x, 2⟩.(λz.x)(:= x 4))  assign
→ ⟶ (ρ⟨x, λx.+ !x 3⟩.λx.+ !x 3) (ρ⟨x, 4⟩.x)  assign, β_{v}
→ ⟶ ρ⟨x, λx.+ !x 3⟩⟨y, 4⟩.(λx.+ !x 3) y  2 × ρ_{lift}, ρ_{merge}
→ ⟶ ρ⟨x, λx.+ !x 3⟩⟨y, 4⟩.+ !y 3  β_{v}
→ ⟶ ρ⟨x, λx.+ !x 3⟩⟨y, 4⟩.+ 4 3  deref
→ ⟶ ρ⟨x, λx.+ !x 3⟩⟨y, 4⟩.7  δ

Figure 2: Reducing a program with side-effects

diamond theorem, since the order in which ρ_{lift} and ρ_{merge} reductions happen is not fixed, and the context R in the ρ_{lift} rule is selected in a nondeterministic fashion. The answers returned by evaluation of a program are no longer simply closed values, since an answer may be a reference cell. Answers are values or ρ-expressions enclosing values:

a ::= v | ρθ.v. (answers)

Based on these definitions, evaluation may be defined like before:

(eval_{vr}) eval_{vr}(e) = a iff e → ⟼^{vr} a.

5.1.2 Typing

Typing reference cells in the presence of polymorphism is not straightforward, as the obvious solution is unsound [6, 36, 37]. To assign types to reference cells, we extend the set of types with an additional constructor:

τ ::= ι_{1} | … | ι_{n} | α | τ_{1} → τ_{2} | \underline{τ ref}

The type τ ref is the type of cells containing a value of type τ.

The obvious types for the three operators are indicated by their semantics:

Γ ▷ ref : τ → τ ref
Γ ▷ ! : τ ref → τ
Γ ▷ := : τ ref → τ → τ

For example, the first argument of the assignment operator (:=) must be a reference cell. The second argument must be a value matching the type of the cell. The result is of the same type as the second argument since our assignment operator returns the value assigned. The following expression illustrates why this typing is unsound:

let f be ref (λy.y) in (λz. ! f true) (:= f (λn.+ 1 n))

If the type of the reference bound to x is generalized to ∀α.(α → α) ref , then the reference cell can be treated as having type (int → int) ref for the assignment, and as having type (bool → bool)ref for the dereference, hence this expression is typable as bool. But evaluating this expression leads to a type error:

let f be ref (λy.y) in

(λz. ! f true) (:= f (λn.+ 1 n))

→ ⟶ let f be ρ⟨x, λy.y⟩. x in

(λz. ! f true) (:= f (λn.+ 1 n))

→ ⟶ ρ⟨x, λy.y⟩.

(λz. ! x true) (:= x (λn.+ 1 n))

→ ⟶ ρ⟨x, λn.+ 1 n⟩. ! x true
→ ⟶ ρ⟨x, λn.+ 1 n⟩. + 1 true

As Tofte [36, 37] points out, the problem with the obvious typing is the generalization of type variables that appear free in the type of a value in the store.

The central idea of Tofte’s solution is to ensure that the only storable values are those that will not be used polymorphically at run-time. To this end, type variables are partitioned into imperative and applicative variables: the former set of type variables is named ImpTypeVar; the latter AppTypeVar. Types are classified accordingly: an imperative type cannot contain any applicative type variables. Only values of imperative type can be stored. When the type of a value is generalized in a let-expression, type variables that might appear in the types of values in the store are required to be imperative, and are not generalized.

The notion of generalization requires appropriate adaptation. We still have:

(≻) ∀α_{1} … α_{n}.τ′ ≻ τ if Sτ′ = τ and Dom(S) = {α_{1}, …, α_{n}} for some S,

but the substitution S is required to map imperative type variables to imperative types. Thus, if \underline{α} is an imperative type variable, we have:

∀\underline{α}.\underline{α} → \underline{α} ≻ int → int
and ∀\underline{α}.\underline{α} → \underline{α} ≻ \underline{α} → \underline{α}
but not ∀\underline{α}.\underline{α} → \underline{α} ≻ α → α

since α is potentially applicative (the meta-variable α still represents any type variable— imperative or applicative).

Like all other techniques for typing references, Tofte’s system requires modifying the typing rule for let-expressions. The let rule is split into two rules, according to whether or not the right-hand side of the declaration is a value. Figure 3 gives the new rules. The second rule does not generalize over imperative type variables, and thus will not generalize the type of a value in the store. However, if the expression bound by a let-expression is a value, as in the first rule, then its evaluation cannot create a new cell, so generalization of imperative type variables in its type cannot generalize the type of a value in the store. Tofte uses the terminology expansive and non-expansive to denote this syntactic classification of expressions into those that may create new references, and those that definitely do not create new references. Like Tofte, we classify only values as non-expansive, but a stronger type system is possible by classifying more expressions as non-expansive [36, 37].

\frac{Γ ▷ v : τ_{1} Γ[x ↦ Close(τ_{1}, Γ)] ▷ e : τ_{2}}{Γ ▷ let x be v in e : τ_{2}} (let_{v})

\frac{Γ ▷ e_{1} : τ_{1} Γ[x ↦ AppClose(τ_{1}, Γ)] ▷ e_{2} : τ_{2} e_{1} ∉ Values}{Γ ▷ let x be e_{1} in e_{2} : τ_{2}} (let_{e})

Close(τ, Γ) = ∀α_{1} … α_{n}.τ where {α_{1}, …, α_{n}} = F T V (τ) \ F T V (Γ) AppClose(τ, Γ) = ∀α_{1} … α_{n}.τ where {α_{1}, …, α_{n}} = (F T V (τ) \ F T V (Γ)) ∩ AppTypeVar.

Figure 3: Modified let-expression typing rules

(ref) Γ ▷ ref : τ → τ ref if τ is imperative (deref) Γ ▷ ! : τ ref → τ (assign) Γ ▷ := : (τ ref → τ → τ)

\frac{Γ[x_{1} ↦ τ_{1} ref ] … [x_{n} ↦ τ_{n} ref ] ▷ e : τ Γ[x_{1} ↦ τ_{1} ref ] … [x_{n} ↦ τ_{n} ref ] ▷ v_{i} : τ_{i} τ_{i} is imperative 1 ≤ i ≤ n}{Γ ▷ ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e : τ} (rho)

Figure 4: Additional typing rules for references

Figure 4 gives four additional typing rules for reference cells. The typing rules for ref and ρ-expressions ensure that any value placed in the store has an imperative type. The typing rules for ! and := do not need to be explicitly constrained, since their use is implicitly constrained by the type of a value already in the store.

In addition to the restrictions placed on the typing of constants by Functional ML, we also require that there be no constants of reference type (τ ref ). This ensures that all values of reference type are in fact reference cells, and can be assigned or dereferenced. This restriction is used in the proof of Theorem 5.6.

The new system assigns the same types as the old one to Functional ML expressions. Let ▷^{f} indicate provability in the old, functional system, and let ▷^{r} indicate provability in the system with references.

Proposition 5.1 If e is an expression in Functional ML, and Γ and τ are purely applicative, then Γ ▷^{f} e : τ iff Γ ▷^{r} e : τ.

Since Functional ML expressions do not contain ref or ρ-expressions, no imperative type variables need be chosen to type an expression, and Close and AppClose yield the same type scheme for applicative types.

5.1.3 Type Soundness for References

To prove type preservation for the extended language, we must show that the notion of reduction v extended to the new syntax preserves types, and that the reductions of r preserve types. Showing that the extended v preserves types amounts to re-proving the various lemmas used in section 4.3 for the extended system. In general, we refer to the extension of Lemma 4.n as Lemma 4.n^{+}. Showing that r preserves types involves adding a case for each reduction to the proof of Subject Reduction. The cases involving R contexts use the fact that:

if Γ ▷ R[e] : τ then Γ ▷ e : τ′.

The type environment Γ is the same in both the antecedent and consequent since R contexts do not bind variables.

Main Lemma 5.2 (Subject Reduction for vr) If Γ ▷^{r} e_{1} : τ and e_{1} ⟶^{vr} e_{2} then

Γ ▷^{r} e_{2} : τ.

Proof. The cases for the reductions of v are the same as before, using an appropriately extended Replacement Lemma and a similarly extended Lemma 4.1.

Case ref v ⟶ ρ⟨x, v⟩.x. From Γ ▷ ref v : τ, where τ = τ′ ref and τ′ is imperative, Γ ▷ v : τ′ by ref and app, and Γ[x ↦ τ′ ref ] ▷ v : τ′ by Lemma 4.1^{+}. Since Γ[x ↦ τ′ ref ] ▷ x : τ′ ref by var, Γ ▷ ρ⟨x, v⟩.x : τ′ ref by rho. In order to satisfy the imperative restriction on the typing of ρ-expressions, ref applications must yield values of imperative type, as ensured by ref.

Case ρθ⟨x, v⟩.R[! x] ⟶ ρθ⟨x, v⟩.R[v]. From Γ ▷ ρθ⟨x, v⟩.R[! x] : τ by rho

Γ′ ▷ v : τ′ (12)

where τ′ is imperative and Γ′x = τ′ref . Thus Γ′ ▷ x : τ′ref , hence Γ′ ▷ ! x : τ′ by deref and app. With (12) by the Replacement^{+} Lemma, we have Γ ▷ ρθ⟨x, v⟩.R[v] : τ.

Case ρθ⟨x, v_{1}⟩.R[:= x v_{2}] ⟶ ρθ⟨x, v_{2}⟩.R[v_{2}]. From Γ ▷ ρθ⟨x, v_{1}⟩.R[:= x v_{2}] : τ by rho

Γ′ ▷ v_{1} : τ′ (13)

where τ′ is imperative and Γ′x = τ′ ref . Thus Γ′ ▷ x : τ′ ref , and by assign and app

Γ′ ▷ := x : τ′ → τ′
Γ′ ▷ := x v_{2} : τ′ and Γ′ ▷ v_{2} : τ′  by app.

With (13) and using the Replacement^{+} Lemma twice, we have Γ ▷ ρθ⟨x, v_{2}⟩.R[v_{2}] : τ.

Case ρθ_{1}.ρθ_{2}.e ⟶ ρθ_{1}θ_{2}.e. From Γ ▷ ρθ_{1}.ρθ_{2}.e : τ by rho

Γ′ ▷ ρθ_{2}.e : τ and Γ′ ▷ v_{i} : τ_{i} (14) where θ_{1} = ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩, Γ′ = Γ[x_{1} ↦ τ_{1} ref ] … [x_{n} ↦ τ_{n} ref ], and 1 ≤ i ≤ n. Again by rho

Γ′′ ▷ e : τ and Γ′′ ▷ v′_{j} : τ′_{j} (15)

where θ_{2} = ⟨x′_{1}, v′_{1}⟩ … ⟨x′_{n}, v′_{m}⟩, Γ′′ = Γ′[x′_{1} ↦ τ′_{1}ref ] … [x′_{m} ↦ τ′_{m}ref ], and 1 ≤ j ≤ m. Since Dom(θ_{1}) ∩ Dom(θ_{2}) = ∅ (by the variable conventions),

Γ′′ ▷ v_{i} : τ_{i} for 1 ≤ i ≤ n  by (14),
Γ ▷ ρθ_{1}θ_{2}.e : τ  by rho with (15).

Case R[ρθ.e] ⟶ ρθ.R[e]. We have Γ ▷ R[ρθ.e] : τ, and proceed by induction on the structure of R to show Γ ▷ ρθ.R[e] : τ. Case R = []. Then R[ρθ.e] = ρθ.R[e]. Case R = (R′ e′). Then Γ ▷ (R′[ρθ.e] e′) : τ, and by app

Γ ▷ R′[ρθ.e] : τ′ → τ (16)

(17)  and Γ ▷ e′ : τ′.

Then Γ ▷ ρθ.R′[e] : τ′ → τ by ind. hyp. with (16), and by rho Γ[x_{i} ↦ τ_{i} ref ] ▷ v_{i} : τ_{i} (18)

(19)  and Γ[x_{i} ↦ τ_{i} ref ] ▷ R′[e] : τ′ → τ

where θ = ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩ and 1 ≤ i ≤ n. Since x_{1}, …, x_{n} ∉ F V (e′),

Γ[x_{i} ↦ τ_{i} ref ] ▷ e′ : τ′  by Lemma 4.1^{+} with (17),
Γ[x_{i} ↦ τ_{i} ref ] ▷ R′[e] e′ : τ by app with (19),
Γ ▷ ρθ.R′[e] e′ : τ  by rho with (18).

Case R = (v R′). Similar to the previous case. Case R = let x be R′ in e′. Then Γ ▷ let x be R′[ρθ.e] in e′ : τ, and by let_{e}

Γ ▷ R′[ρθ.e] : τ′ (20)

(21)  and Γ[x ↦ AppClose(τ′, Γ)] ▷ e′ : τ.

Then Γ ▷ ρθ.R′[e] : τ′ by ind. hyp. with (20), and by rho Γ[x_{i} ↦ τ_{i} ref ] ▷ v_{i} : τ_{i} (22)

(23)  and Γ[x_{i} ↦ τ_{i} ref ] ▷ R′[e] : τ′

where θ = ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩ and each τ_{i} is imperative for 1 ≤ i ≤ n. Since x_{1}, …, x_{n} ∉ F V (e′),

Γ[x ↦ AppClose(τ′, Γ)][x_{i} ↦ τ_{i} ref ] ▷ e′ : τ by Lemma 4.1^{+} with (21)
i.e. Γ[x_{i} ↦ τ_{i} ref ][x ↦ AppClose(τ′, Γ)] ▷ e′ : τ.

But each τ_{i} is imperative, due to the restriction on the typing of ρ-expressions, hence

AppClose(τ′, Γ) = AppClose(τ′, Γ[x_{i} ↦ τ_{i} ref ]).

If R′[e] is expansive, then Γ[x_{i} ↦ τ_{i} ref ][x ↦ AppClose(τ′, Γ[x_{i} ↦ τ_{i} ref ])] ▷ e′ : τ

Γ[x_{i} ↦ τ_{i} ref ] ▷ let x be R′[e] in e′ : τ  by let_{e} with (23)
Γ ▷ ρθ.let x be R′[e] in e′ : τ  by rho with (22).

Otherwise, R′[e] is non-expansive, and Γ[x_{i} ↦ τ_{i} ref ][x ↦ Close(τ′, Γ[x_{i} ↦ τ_{i} ref ])] ▷ e′ : τ

Γ[x_{i} ↦ τ_{i} ref ] ▷ let x be R′[e] in e′ : τ  by let_{v} with (23)
Γ ▷ ρθ.let x be R′[e] in e′ : τ  by rho with (22).

Thus Γ ▷ ρθ.R[e] : τ by induction.

It remains to extend the proofs of the various lemmas. The only one that is not straightforward is the Substitution Lemma. As in the definition of generalization, substitutions S in the following proof are required to map imperative type variables to imperative types.

Lemma 5.3 (Substitution) If Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷^{r} e : τ′ and x ∉ Dom(Γ) and

Γ ▷^{r} v : τ and {α_{1}, …, α_{n}} ∩ F T V (Γ) = ∅ then Γ ▷^{r} e[x ↦ v] : τ′.

Proof. The cases from the proof for Functional ML are unchanged, with the exception that the let-expression case applies only when the bound expression is a value. There is one new case for expansive let-expressions, and new cases for the additional syntax.

Case e = ref, !, or :=. In each case, Γ′ ▷ e : τ′ for any Γ′, hence Γ ▷ e : τ′. Also in each case, e[x ↦ v] = e, so Γ ▷ e[x ↦ v] : τ′.

Case e = ρθ.e_{1}. From Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ ρθ.e_{1} : τ′ by rho

Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ τ_{i} ref ] ▷ v_{i} : τ_{i}
and Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ τ_{i} ref ] ▷ e_{1} : τ′

where θ = ⟨x_{1}, v_{1}⟩ … ⟨x_{m}, v_{m}⟩, x_{1}, …, x_{m}, x are distinct, and each τ_{i} is imperative for 1 ≤ i ≤ m. Choose a substitution S : {α_{1}, …, α_{n}} → {α′_{1}, …, α′_{n}} such that α′_{1}, …, α′_{n} are distinct type variables, Sα_{i} = α′_{i}, and {α′_{1}, …, α′_{n}} ∩ ({α_{1}, …, α_{n}} ∪ F T V (Γ) ∪ F T V (τ′) ∪ ⋃_{i} F T V (τ_{i})) = ∅. Then by Lemma 4.5^{+}

S(Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ τ_{i} ref ]) ▷ v_{i} : Sτ_{i}
i.e. Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ Sτ_{i} ref ] ▷ v_{i} : Sτ_{i}
i.e. Γ[x_{i} ↦ Sτ_{i} ref ][x ↦ ∀α_{1} … α_{n}.τ] ▷ v_{i} : Sτ_{i}.

Also by Lemma 4.5^{+},

S(Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ τ_{i} ref ]) ▷ e_{1} : Sτ′
i.e. Γ[x ↦ ∀α_{1} … α_{n}.τ][x_{i} ↦ Sτ_{i} ref ] ▷ e_{1} : Sτ′
i.e. Γ[x_{i} ↦ Sτ_{i} ref ][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : Sτ′.

By applying the inductive hypothesis to each,

Γ[x_{i} ↦ Sτ_{i} ref ] ▷ v_{i}[x ↦ v] : Sτ_{i}
and Γ[x_{i} ↦ Sτ_{i} ref ] ▷ e_{1}[x ↦ v] : Sτ′.

Since S is a bijection, S^{−1} exists; hence

Γ[x_{i} ↦ τ_{i} ref ] ▷ v_{i}[x ↦ v] : τ_{i}
and Γ[x_{i} ↦ τ_{i} ref ] ▷ e_{1}[x ↦ v] : τ′.

Then Γ ▷ ρθ[x ↦ v].e_{1}[x ↦ v] : τ′ by rho, thus Γ ▷ (ρθ.e_{1})[x ↦ v] : τ′.

Case e = let x′ be e_{1} in e_{2} where e_{1} ∉ Values. By the first premise of let_{e}

Γ[x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{1} : τ_{1}
(24)  Γ ▷ e_{1}[x ↦ v] : τ_{1}  by ind. hyp.

By the second premise of let_{e}

Γ[x ↦ ∀α_{1} … α_{n}.τ][x′ ↦ AppClose(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ e_{2} : τ′
i.e. Γ[x′ ↦ AppClose(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{2} : τ′.

Choose a substitution S : {α_{1}, …, α_{n}} ∩ ImpTypeVar → {α′_{1}, …, α′_{m}} such that α′_{1}, …, α′_{m} are distinct imperative type variables, S is a bijection, and {α′_{1}, …, α′_{m}} ∩ (F T V (Γ) ∪ F T V (τ) ∪ {α_{1}, …, α_{n}}) = ∅. Then by Lemma 4.5^{+}

S(Γ[x′ ↦ AppClose(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])][x ↦ ∀α_{1} … α_{n}.τ]) ▷ e_{2} : Sτ′
i.e. Γ[x′ ↦ SAppClose(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{2} : Sτ′
(25) i.e. Γ[x′ ↦ AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])][x ↦ ∀α_{1} … α_{n}.τ] ▷ e_{2} : Sτ′

since the domain of S contains only imperative type variables. From Γ ▷ v : τ since x′ is not free in v

(26) Γ[x′ ↦ AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ v : τ.

Now,

{α_{1}, …, α_{n}} ∩ F T V (Γ[x′ ↦ AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])])
⊆ {α_{1}, …, α_{n}} ∩ (F T V (Γ) ∪ F T V (AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])))
= {α_{1}, …, α_{n}} ∩ F T V (AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ]))
= {α_{1}, …, α_{n}} ∩ F T V (∀α′′_{1} … α′′_{m}.Sτ_{1})
= {α_{1}, …, α_{n}} ∩ (F T V (Sτ_{1}) \ {α′′_{1}, …, α′′_{m}})
= ∅

where {α′′_{1}, …, α′′_{m}} = (F T V (Sτ_{1}) \ F T V (Γ[x ↦ ∀α_{1} … α_{n}.τ])) ∩ AppTypeVar. By the inductive hypothesis with (25) and (26), it follows that

Γ[x′ ↦ AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ e_{2}[x ↦ v] : Sτ′.

Since S is a bijection, S^{−1} exists, so by Lemma 4.5^{+}

S^{−1}(Γ[x′ ↦ AppClose(Sτ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])]) ▷ e_{2}[x ↦ v] : S^{−1}(Sτ′)
i.e. Γ[x′ ↦ AppClose(τ_{1}, Γ[x ↦ ∀α_{1} … α_{n}.τ])] ▷ e_{2}[x ↦ v] : τ′.

Then by Lemma 4.6^{+}

Γ[x′ ↦ AppClose(τ_{1}, Γ)] ▷ e_{2}[x ↦ v] : τ′

and by let_{e} with (24)

Γ ▷ let x be e_{1}[x ↦ v] in e_{2}[x ↦ v] : τ′
i.e. Γ ▷ (let x be e_{1} in e_{2})[x ↦ v] : τ′.

The evaluation of an expression in Reference ML can become stuck for several new reasons. The expanded definition of faulty expressions reflects this fact.

Definition 5.4 (Faulty Expressions) The faulty expressions of Reference ML are those expressions containing a subexpression of the form:

(c v) where δ(c, v) is undefined; (! v) where v ∉ Var; (:= v) where v ∉ Var; or ρθ⟨x, v_{2}⟩.C[x v_{1}].

As before, we have a Uniform Evaluation Lemma, stating that programs either yield an answer, diverge, or reduce to a faulty expression.

Lemma 5.5 (Uniform Evaluation) For closed e, if there is no e′ such that e → ⟼^{vr} e′ and e′ is faulty, then either e ⇑ or e → ⟼^{vr} a.

Proof. The proof proceeds by induction on the length of the reduction sequence, and is similar to the proof for Functional ML.

All of the expressions in the expanded definition are untypable.

Main Lemma 5.6 (Faulty Expressions are Untypable) If e is faulty, there are no Γ and τ such that Γ ▷^{r} e : τ.

Proof. Again, it suffices to show that the subexpressions of e that cause e to be faulty are untypable. We proceed by case analysis according to the form of the subexpression, assuming for each case that the expression can be typed, and deriving a contradiction.

Case (c v) where δ(c, v) is undefined. As for Functional ML.

Case (! v) where v ∉ Var. Assume that Γ ▷ ! v : τ. Then Γ ▷ v : τ ref by app and deref, which implies v is a variable (since no other value can have type τ ref ), contrary to the assumption.

Case (:= v) where v ∉ Var. Assume that Γ ▷ := v : τ. Then Γ ▷ v : τ′ ref where τ = τ′ → τ′ by app and assign, which implies v is a variable, contrary to the assumption.

Case ρθ⟨x, v′⟩.C[x v]. Assume that Γ ▷ ρθ⟨x, v′⟩.C[x v] : τ. Then Γ′ ▷ C[x v] : τ by rho, where Γ′(x) = τ′ ref . Since Γ′′ ▷ x v : τ_{2} where Γ′(x) = Γ′′(x), Γ′′ ▷ x : τ_{1} → τ_{2} by app, hence Γ′′(x) ≻ τ_{1} → τ_{2}. This contradicts Γ′′(x) = τ′ ref .

Type soundness now follows as before.

Theorem 5.7 (Syntactic Soundness for Reference ML) If ▷^{r} e : τ then either e ⇑ or

e → ⟼^{vr} a and ▷^{r} a : τ.

Proof. Exactly as for Theorem 4.12, using the appropriately extended lemmas.

5.2 Exception ML

Due to δ-typability, constant functions must be defined for all values of their input type. This precludes constants, such as integer or real division, that are defined on all but a few recognizable input values of correct type. Standard ML solves this problem by introducing exceptions.

Our exception extension provides named exceptions with parameters, a means of raising exceptions, and a means of handling exceptions. Our extension thus includes three new phrases:

exception x_{1} … x_{n} in e,  raise e_{1} e_{2},  e_{3} handle e_{1} e_{2}.

The first phrase declares x_{1}, …, x_{n} to be exception names lexically bound in e. The second phrase requires e_{1} to evaluate to an exception name, and raises that exception with a parameter, the value of e_{2}. The parameter propagates along with the exception, and is used at the site where an exception is handled. The third phrase evaluates its subexpressions e_{1} and e_{2} first, and installs the value of e_{2} as an exception handler for e_{1} exceptions that are raised during the evaluation of e_{3}. The subexpression e_{1} must evaluate to an exception name, and e_{2} must evaluate to a function that accepts parameters of e_{1} exceptions. When an exception is raised, control transfers to the dynamically closest handler for that kind of exception. The handler function is applied to the exception parameter, and the result of the application is returned as the result of the handle-phrase. If there is no active handler for a raised exception, evaluation terminates with an “unhandled exception” answer.

To extend Functional ML with exceptions, we add several new phrases to the syntax:

(Expressions) e ::= v | e_{1} e_{2} | let x be e_{1} in e_{2} | \underline{exception χ in e}
(Values)  v ::= c | x | Y | λx.e | \underline{raise} | \underline{e handle} | \underline{raise v} | \underline{e handle v}
\underline{χ} ::= \underline{x^{∗}}

In the expression exception χ in e, the variables in χ are bound in e. We treat χ as a set of variables, and call these exception names. As raise is a curried binary operator, the application of raise to a value is a value, and is included in the syntactic class of values (like := in Reference ML). Likewise, the expression e handle is a value, and receives an exception name and handler function by ordinary application. Hence the application of e handle to a value is also a value.

5.2.1 Semantics

Raising and handling exceptions requires several new reductions:

(raise)  U[raise x v] ⟶ raise x v if U ≠ []
(handle)  (raise x v_{1}) handle x v_{2} ⟶ v_{2} v_{1}
exception χx_{1}x_{2} in
X[(raise x_{1} v_{1}) handle x_{2} v_{2}]

⟶ exception χx_{1}x_{2} in X[raise x_{1} v_{1}] x_{1} ≠ x_{2}

(reraise)

(unhandle)  v_{1} handle x v_{2} ⟶ v_{1}

These new notions of reduction again rely on (two different kinds of) contexts for the enforcement of a specific order of evaluation for applications in connection with the raising and handling of exceptions:

(raising)  U ::= [] | U e | v U | let x be U in e
(handling)  X ::= [] | X e | v X | let x be X in e | X handle x v.

When an exception is raised, raise reductions propagate the exception outwards, eliminating pending computations. As U contexts do not include the phrase U handle x v, raise reductions propagate the exception only to the closest exception handler. If the closest handler matches the raised exception, a handle reduction applies the handler function to the exception parameter. If the handler does not match the exception, a reraise reduction discards the handler, and the exception may continue to propagate by raise reductions. Should an expression protected by a handler evaluate to a value without raising an exception, the unhandle reduction discards the handler.

The exception-expression requires two additional reductions, similar to those for ρexpressions:^{7}

(exn_{merge}) exception χ_{1} in exception χ_{2} in e ⟶ exception χ_{1}χ_{2} in e
(exn_{lift})  X[exception χ in e] ⟶ exception χ in X[e] if X ≠ []

Indeed, the only difference is that the exception-expression does not bind any values to its variables. The purpose of an exception-expression is to distinguish different exceptions in the reraise reduction, in order that evaluation be deterministic. If x_{1} and x_{2} are different but only λ- or let-bound, subsequent reductions may substitute them to the same exceptionbound variable, making the raise reduction applicable. For example:

exception x in (λy.λz.(raise y v_{1}) handle z v_{2}) x x

→ ⟶ exception x in (raise x v_{1}) handle x v_{2}
→ ⟶ exception x in v_{2} v_{1}.

Insisting that x_{1} and x_{2} be exception-bound in reraise ensures that they refer to distinct exceptions. The reduction handle does not require its variables to be exception-bound, because substitution necessarily replaces both instances of x in the handle redex with the same exception name.

We use x to refer to the six reductions for exceptions introduced above. Taking the union of v (extended to the full syntax) and x yields vx, the notion of reduction for Exception ML. With evaluation contexts extended to:

E ::= [] | E e | v E | let x be E in e | exception χ in E | E handle x v

the stepping function ⟼^{vx} may be defined along the same lines as before. Answers for eval_{vx} are:

(answers) a ::= v | exception χ in v | exception χx in raise x v.

7Due to our use of the variable conventions for exn_{merge}, our exceptions are generative as in Standard ML [22, 23].

Answers of the third form are unhandled exceptions: since handlers are dynamically bound, it is possible for an exception to be raised when no handler for it is installed. Evaluation is defined as:

(eval_{vx}) eval_{vx}(e) = a iff e → ⟼^{vx} a.

We can now extend the domain of δ to admit functions such as division, by allowing δ to return an expression that raises an exception:^{8}

δ : Const × ClosedVal ⇀ ClosedVal ∪ {exception x in raise x v | v is closed}.

Functions such as division can now be defined on every element of their input type, by returning an exception when their application does not make sense.

5.2.2 Typing

We extend the set of types with an additional type constructor:

τ ::= ι_{1} | … | ι_{n} | α | τ_{1} → τ_{2} | \underline{τ exn}

The type τ exn is the type of exceptions with a parameter of type τ.

In typing exceptions in the presence of polymorphism, one encounters similar difficulties as in typing references. The phrase raise e_{1} e_{2} requires e_{1} to be an exception of type τ exn, and e_{2} to be a matching parameter of type τ. If e_{3} has type τ′, the phrase e_{3} handle e_{1} e_{2} requires e_{1} to be an exception of type τ exn, and e_{2} to be a handler for such exceptions. The handler must be a function of type τ → τ′, since it takes the exception parameter as input, and returns a value to be returned in place of the value of e_{3}. The obvious typing for exceptions allows the parameter types of exceptions to be fully polymorphic, permitting the following expression to be typed:^{9}

let rh be exception x in pair (raise x) (λa.λb.(a 3) handle x b) in (snd rh) (λd.(fst rh) true) (λy.+ 1 y)

→ ⟶ exception x in + 1 true

Here, functions to raise and handle the same x-exception are returned as a pair, bound by a let-expression to rh, and then used. In the body of the let-expression, the expression (raise x) has type α_{1} → α_{2}, and (λa.λb.(a 3) handle x b) has type (int → α_{3}) → (α_{1} → α_{3}) → α_{3}. If the exception parameter type α_{1} is generalized, then in the body of the let-expression an x-exception may be raised with an argument of type bool by (fst rh), and caught by (snd rh), which is expecting an argument of type int.

Since the problems of typing exceptions and references are similar, it is not surprising that the same modifications to the typing rules for functional expressions apply: types and type variables are classified as imperative or applicative, and the let rule is split according to whether the bound expression is expansive (see Figure 3). Figure 5 presents the additional typing rules for exceptions. Again, as with Reference ML, we require the additional restriction that there be no constants of exception type (τ exn).

8Usually a set of exceptions that may be raised by constant functions is defined in an initial environment; we take an alternative approach to simplify the presentation.

9The constants pair, fst, and snd provide pairing and projection operations.

(raise) Γ ▷ raise : τ_{1} exn → τ_{1} → τ_{2}

\frac{Γ ▷ e : τ_{2}}{Γ ▷ e handle : τ_{1} exn → (τ_{1} → τ_{2}) → τ_{2}} (handle)

\frac{Γ[x_{1} ↦ τ_{1} exn] … [x_{n} ↦ τ_{n} exn] ▷ e : τ τ_{i} is imperative 1 ≤ i ≤ n}{Γ ▷ exception x_{1} … x_{n} in e : τ} (exn)

Figure 5: Additional typing rules for exceptions

5.2.3 Type Soundness for Exceptions

To establish soundness for the exception typing, we proceed as for references: we establish type preservation for vx, and show that the faulty expressions of Exception ML are untypable.

Main Lemma 5.8 (Subject Reduction for vx) If Γ ▷^{x} e_{1} : τ and e_{1} ⟶^{vx} e_{2} then

Γ ▷^{x} e_{2} : τ.

Proof. The cases for the reductions of v are the same as before.

Case U[raise x v] ⟶ raise x v. From Γ ▷ U[raise x v] : τ

Γ ▷ raise x v : τ′

by app. Hence

Γ ▷ raise x : τ_{1} → τ_{2} (27)

(28)  and Γ ▷ v : τ_{1}

by app. From (27)

Γ ▷ x : τ_{1} exn  by app and raise,
Γ ▷ raise x : τ_{1} → τ  by app and raise,
Γ ▷ raise x v : τ  by app with (28).

Case exception χ_{1} in exception χ_{2} in e ⟶ exception χ_{1}χ_{2} in e. Similar to ρ_{merge} in Lemma 5.2.

Case X[exception χ in e] ⟶ exception χ in X[e]. Similar to ρ_{lift} in Lemma 5.2.

Case v_{1} handle x v_{2} ⟶ v_{1}. Γ ▷ v_{1} : τ from Γ ▷ v_{1} handle x v_{2} : τ by handle and app.

Case (raise x v_{1}) handle x v_{2} ⟶ v_{2} v_{1}. From Γ ▷ (raise x v_{1}) handle x v_{2} : τ by handle, app, and raise

Γ ▷ v_{1} : τ′ and Γ ▷ v_{2} : τ′ → τ

where Γx = τ′ exn. Then Γ ▷ v_{2} v_{1} : τ by app.

Case exception χx_{1}x_{2} in X[(raise x_{1} v_{1}) handle x_{2} v_{2}] ⟶ exception χx_{1}x_{2} in X[raise x_{1} v_{1}] . Then

Γ′ ▷ (raise x_{1} v_{1}) handle x_{2} v_{2} : τ′
Γ′ ▷ (raise x_{1} v_{1}) handle : τ_{2} exn → (τ_{2} → τ′) → τ′ by app,
Γ′ ▷ raise x_{1} v_{1} : τ′  by handle,
Γ ▷ exception χx_{1}x_{2} in X[raise x_{1} v_{1}] : τ  by Replacement^{+}.

With the extension of the various lemmas, the proof of type preservation for Exception ML is complete. The lemmas go through with simple adaptations to the new syntax.

There are several new kinds of faulty expressions for Exception ML.

Definition 5.9 (Faulty expressions) The faulty expressions of Exception ML are those expressions containing a subexpression of the form:

(c v) where δ(c, v) is undefined, (raise v) where v ∉ Var, (e handle v) where v ∉ Var, or exception χx in C[x v],

where

C ::= [] | C e | e C | let x be C in e | let x be e in C | λx.C
| exception χ in C | C handle .

Again, a uniform evaluation lemma can be shown, and the faulty expressions can be proven untypable. Type soundness for Exception ML follows as before.

Theorem 5.10 (Syntactic Soundness for Exception ML) If ▷^{x} e : τ then either e ⇑

or e → ⟼^{vx} a and ▷^{x} a : τ.

5.3 Core ML

We can combine references and exceptions in one language, Core ML, that has all the essential features of Standard ML. In combining the reference and exception extensions, we must ensure that they interact appropriately.

5.3.1 Semantics

To combine the calculi for the two extensions, the R contexts of the reference fragment must be extended to include phrases from the exception fragment; likewise, X contexts must be extended to include phrases from the reference fragment:

R ::= … | R handle v_{1} v_{2}
X ::= … | ρθ.X

The phrase exception χ in R is not included in R in order that exceptions in the store do not escape their bindings, i.e., exception-expressions can move through ρ-expressions by the exn_{lift} reduction, with appropriate variable renaming:

ρθ.exception χx in e ⟶ exception χx in ρθ.e

but not vice versa:

exception χx in ρθ⟨r, x⟩.e −̸→ ρθ⟨r, x⟩.exception χx in e.

If the second were a permissible reduction, the occurrence of x in the store would escape its binding.

After this extension of the R and X contexts, the resulting notion of reduction for the full syntax is vrx. The E evaluation contexts used in defining ⟼^{vrx} and eval_{vrx} must also be extended:

E ::= [] | E e | v E | let x be E in e | E handle v_{1} v_{2} | ρθ.E | exception χ in E.

Answers are:

(answers)  a ::= {exception χ in} {ρθ.} v
| {exception χx in} {ρθ.} raise x v

(where {phrase} means phrase may be omitted). The complete calculus for Core ML may be found in the appendix.

5.3.2 Typing

To combine the typing rules for the two fragments is easy, since they both rely on the same classification of types as imperative or applicative, and do not interfere. The complete typing rules for Core ML may be found in the appendix.

5.3.3 Type Soundness for Core ML

The type soundness of the resulting calculus requires re-establishing the various lemmas and theorems for the extended syntax and extended evaluation contexts. These proofs are all straightforward. There is a combinatorial increase in the kinds of faulty expressions because of the interaction between the two fragments: references cannot be raised or handled; exceptions cannot be dereferenced nor assigned. The structure of the proof, however, stays the same.

Definition 5.11 (Faulty Expressions) The faulty expressions of Core ML are those expressions containing a subexpression of the form:

(c v) where δ(c, v) is undefined;

(! v) where v ∉ Var, (:= v) where v ∉ Var, ρθ⟨x, v_{2}⟩.C[x v_{1}],

exception χx in C[! x], exception χx in C[:= x], (raise v) where v ∉ Var, (e handle v) where v ∉ Var, exception χx in C[x v],

ρθ⟨x, v⟩.C[raise x], ρθ⟨x, v⟩.C[e handle x], where

C ::= [] | C e | e C | let x be C in e | let x be e in C | λx.C
| ρθ.C | ρθ⟨x, C⟩.e | exception χ in C | C handle .

Type soundness follows from subject reduction, uniform evaluation, and faulty expressions being untypable, as before.

Theorem 5.12 (Syntactic Soundness for Core ML) If ▷^{rx} e : τ then either e ⇑ or

e → ⟼^{vrx} a and ▷^{rx} a : τ.

6 Control ML

In this section we present an extension to Functional ML providing first-class continuations. The typing of our extension is similar to that described by Duba et al. [8], and implemented in Standard ML of New Jersey [34]. It is a simple matter to merge this extension with Core ML.

Control ML extends Functional ML’s syntax with two new constructs:

(Expressions)  e ::= v | e_{1} e_{2} | let x be e_{1} in e_{2} | \underline{abort e}
(Values)  v ::= c | x | Y | λx.e | \underline{callcc}

An abort-expression evaluates its subexpression to a value, and returns this value as the result of the program. When the callcc operator (call-with-current-continuation) is applied to a function f, it captures a representation of the current continuation (or program control stack), encapsulates this continuation in an abstraction, and applies f to this abstraction. If this abstraction is later applied to a value, control transfers to the captured continuation.

6.1 Semantics

While defining calculus reductions for first-class continuations is possible [13, 14], the resulting calculus is inappropriate for our problem. Since we are only interested in evaluation, we take a simpler approach [11]. We give top-level evaluation rules, program reductions, for the control operators by extending the stepping relation (⟼) directly:

(δ, β_{v}, let, Y )  E[e] ⟼ E[e′] iff e ⟶^{v} e′
(callcc)  E[callcc v] ⟼ E[v (λx.abort E[x])]
(abort)  E[abort e] ⟼ e

where

E ::= [] | E e | v E | let x be E in e.

In this style of semantics, the evaluation context E represents the current continuation. An abort reduction simply discards the current continuation, continuing evaluation with its subexpression. The callcc reduction captures the current continuation, encapsulates it in a function, and applies callcc’s argument to this function. The continuations created by callcc are abortive: when invoked, they discard the continuation surrounding their application

let product be λx. callcc

(λk. letrec p be λz. if nil? z then 1 else if = 0 (car z) then k 0 else * (car z) (p (cdr z))

in p x) in product (cons 2 (cons 3 (cons 0 (cons 5 nil))))

Figure 6: A program illustrating a simple use of callcc

(via an abort reduction), installing instead the captured continuation. Answers are simply values, and eval is defined as for Functional ML.

Figure 6 illustrates a simple use of callcc. This program computes the product of a list of numbers, performing no multiplications if the answer is zero. The constants nil, cons, nil?, car, and cdr are the usual constants and operations for lists. The expressions if…then…else… and letrec…be…in… are syntactic sugar for appropriate constant applications. This program computes the product of a list of numbers, performing no multiplications if the answer is zero. The program escapes from pending multiplications by jumping out of the recursion to the continuation of the application of product.

6.2 Typing

The obvious approach to typing callcc leads to the following rule:

(naïve-callcc) Γ ▷ callcc : ((τ_{1} → τ_{2}) → τ_{1}) → τ_{1}

As indicated by the callcc reduction, callcc takes a function whose argument is a procedural abstraction of the evaluation context, the continuation. If the evaluation context expects a value of type τ_{1}, then the continuation has type τ_{1} → τ_{2} for any type τ_{2}. If callcc’s argument ignores this continuation, it must produce a value of type τ_{1}, which implies that callcc’s argument must have type (τ_{1} → τ_{2}) → τ_{1}. The result type of the continuation, τ_{2}, is arbitrary, because the application of k built into the continuation ensures that it never returns.

However, this obvious typing is unsound, as illustrated by the following example:^{10}

let x be callcc (λk. pair (λx.x) (λf. k (pair f (λd.5)))) in (λz. snd x (λx.+ x 1)) (fst x true)

The callcc application returns a pair of type (α → α) × ((α → α) → int), consisting of the identity function and a function that applies a continuation. Since α is not free in the type environment, it is closed over, and x has type scheme ∀α.(α → α) × ((α → α) → int) in the body of the let-expression. In evaluating the body, fst x is the polymorphic identity function, so it may validly be applied to true. Then the second function of the pair is applied to (λx.+ x 1), and the continuation so invoked rebinds x to the pair consisting of (λx.+ x 1) and (λd.5). The second evaluation of fst x true results in an attempt to add 1 to true.

10A variation of this example was discovered by Robert Harper and Mark Lillibridge [sml electronic mailing list, July 8, 1991]. Despite widespread use of a naïvely typed callcc extension in Standard ML of New Jersey, it took two years until this problem was discovered.

As with references and exceptions, a correct typing for continuations builds upon the classification of types as imperative or applicative, and requires the let typing rules of Figure 3. The correct typing rules are:

(callcc) Γ ▷ callcc : ((τ_{1} → τ_{2}) → τ_{1}) → τ_{1} if τ_{1} is imperative.

\frac{Γ ▷ e : τ_{1}}{Γ ▷ abort e : τ_{2}}

(abort)

An abort-expression may have any type, regardless of the type of its subexpression, because when evaluated it never returns.

6.3 Weak Type Soundness

Because abort-expressions can return a value of any type, proving type soundness for the continuation extension is not as simple as for the previous extensions. For example, if e is an expression of type bool, the program:

if e then 1 else (abort true)

is typable according to the above typing rules, but returns either int or bool according to whether e is true or false. Thus subject reduction in the usual sense does not hold; however, a weaker lemma does hold, stating that typability is preserved.

Main Lemma 6.1 (Typability Preservation) If ▷ e_{1} : τ and e_{1} ⟼ e_{2} then ▷ e_{2} : τ′.

Proof. We need only consider the additional cases for the callcc and abort reductions. The others are simply adapted from Lemma 4.3 (Subject Reduction for Functional ML).

Case E[abort e] ⟼ e. Then Γ ▷ e : τ′ for some τ′. But since E[abort e] is closed and E does not bind variables, e is closed, hence ▷ e : τ′.

Case E[callcc v] ⟼ E[v (λx.abort E[x])]. From ▷ E[callcc v] : τ we have ▷ callcc v : τ_{1}, and by callcc and app

▷ v : (τ_{1} → τ_{2}) → τ_{1} (29)

where τ_{1} is imperative.

Since E is closed, x does not appear free in E, and we claim that [x ↦ τ_{1}] ▷ E[x] : τ. The proof of this claim proceeds by induction on the structure of E.

Case E = []. Then τ = τ_{1}, and [x ↦ τ_{1}] ▷ x : τ by var. Case E = (E′ e′). Then ▷ (E′[callcc v] e′) : τ, and by app

▷ E′[callcc v] : τ_{3} → τ (30)
(31)  and ▷ e′ : τ_{3}

for some τ_{3}. Then [x ↦ τ_{1}] ▷ E′[x] : τ_{3} → τ by ind. hyp. with (30). Also

[x ↦ τ_{1}] ▷ e′ : τ_{3} by Lemma 4.1^{+} with (31) since x ∉ F V (E). Hence
[x ↦ τ_{1}] ▷ E′[x] e′ : τ  by app.

Case E = (v E′). Similar to the previous case.

Case E = let x′ be E′ in e′. Then ▷ let x′ be E′[callcc v] in e′ : τ. Since (callcc v) is expansive, E′[callcc v] is expansive. Thus by let_{e}

▷ E′[callcc v] : τ_{3} (32)

(33)  and [x′ ↦ AppClose(τ_{3}, ∅)] ▷ e′ : τ

for some τ_{3}. Then

(34)  [x ↦ τ_{1}] ▷ E′[x] : τ_{3}  by ind. hyp. with (32),

and

[x′ ↦ AppClose(τ_{3}, ∅)][x ↦ τ_{1}] ▷ e′ : τ by Lemma 4.1^{+} with (33)
i.e. [x ↦ τ_{1}][x′ ↦ AppClose(τ_{3}, ∅)] ▷ e′ : τ.

By the critical restriction that τ_{1} is imperative,

AppClose(τ_{3}, ∅) = AppClose(τ_{3}, [x ↦ τ_{1}]),

hence

[x ↦ τ_{1}][x′ ↦ AppClose(τ_{3}, [x ↦ τ_{1}])] ▷ e′ : τ
[x ↦ τ_{1}] ▷ let x′ be E′[x] in e′ : τ  by let_{e} with (34).

This completes the proof of the claim. Hence

[x ↦ τ_{1}] ▷ abort E[x] : τ_{2}  by abort,
▷ (λx.abort E[x]) : τ_{1} → τ_{2}  by abs,
▷ v (λx.abort E[x]) : τ_{1}  by app with (29)
▷ E[v (λx.abort E[x])] : τ  by Replacement^{+}.

The faulty expressions for Control ML are the same as those of Functional ML, extended to the new syntax.

Definition 6.2 (Faulty Expressions) The faulty expressions of Control ML are the expressions containing a subexpression (c v) where δ(c, v) is undefined.

As with Functional ML, the faulty expressions are untypable and Uniform Evaluation holds. However, since we only have typability preservation, we obtain a weaker version of syntactic soundness that does not indicate the type of answers.

Theorem 6.3 (Weak Syntactic Soundness) If ▷ e : τ then either e ⇑ or e → ⟼ v.

Proof. By Uniform Evaluation, either e → ⟼ e′ and e′ is faulty, or e ⇑, or e → ⟼ v. Since ▷ e : τ, Typability Preservation implies ▷ v : τ′ and ▷ e′ : τ′. Suppose e → ⟼ e′ and e′ is faulty. Since faulty expressions are untypable, ▷ e′ : τ′ is a contradiction, therefore this case cannot occur. Hence either e ⇑ or e → ⟼ v.

This weaker theorem establishes weak soundness, but does not imply strong soundness. In fact, if the use of abort is unrestricted, it is not possible to predict the type of an answer, as the example at the beginning of this section illustrates.

6.4 Strong Type Soundness

Examining the proof of Typability Preservation reveals that every reduction with the exception of abort preserves type. In particular, the callcc reduction preserves type, which suggests that callcc by itself is strongly sound. To obtain a proof of strong soundness for callcc, we must eliminate abort from the surface language available to programmers, but retain it in the underlying language of evaluation for callcc reductions. Because the abort expressions introduced by callcc applications have a restricted shape, they never return values of other than the top-level type of the program, and do not compromise strong soundness.

To establish a subject reduction lemma, we define an augmented type system that infers both the ordinary type of an expression and a set of abort types. The abort types of an expression e are the types of the immediate subexpressions of abort-expressions in e. The augmented system does not permit abort types to be generalized, thereby ensuring that each syntactic occurrence of abort can produce only one type of answer. This restriction eliminates expressions such as the following:

let a be λx. abort x in if e then a 1 else a true

Hence if a well-typed program aborts, the answer produced is one of the program’s abort types. Type judgments for this augmented system have the form Γ ▷^{a} e : τ, T, meaning that in type environment Γ, expression e has ordinary type τ and abort types T, where T is a set of types. Figure 7 presents the typing rules of the augmented system.

The augmented type system corresponds closely to our original type system for Control ML. The rule for typing abort-expressions is the only rule that connects the ordinary type and the abort types of an expression. In each axiom (var, const, Y, callcc) the abort set is completely unconstrained; the inference rules simply propagate the abort set. The let-expression rules do not generalize type variables in the set of abort types, hence the augmented system does not permit polymorphic uses of abort, and accepts a subset of the expressions accepted by the ordinary system. A Correspondence Lemma establishes this connection between the ordinary system (▷) and the augmented system (▷^{a}).

Lemma 6.4 (Correspondence)

(i) If Γ ▷ e : τ and e contains no abort-expressions then Γ ▷^{a} e : τ, T for any T;

(ii) If Γ ▷^{a} e : τ, T then Γ ▷ e : τ.

Proof. The proof of each direction shows how to construct a deduction for the consequent from a deduction of the antecedent. Both proofs are straightforward.

Subject Reduction for the augmented system establishes that reduction preserves the set of abort types. As the callcc reduction introduces an abort-expression with the top-level type of the program, the set of abort types preserved by Subject reduction includes the top-level type.

Γ ▷^{a} x : τ, T if Γ(x) ≻ τ (var)

(const) Γ ▷^{a} c : τ, T if TypeOf (c) ≻ τ

Γ ▷^{a} Y : ((τ_{1} → τ_{2}) → τ_{1} → τ_{2}) → τ_{1} → τ_{2}, T (Y)

\frac{Γ[x ↦ τ_{1}] ▷^{a} e : τ_{2}, T}{Γ ▷^{a} λx.e : τ_{1} → τ_{2}, T} (abs)

\frac{Γ ▷^{a} e_{1} : τ_{1} → τ_{2}, T Γ ▷^{a} e_{2} : τ_{1}, T}{Γ ▷^{a} e_{1} e_{2} : τ_{2}, T} (app)

\frac{Γ ▷^{a} v : τ_{1}, T Γ[x ↦ Close(τ_{1}, Γ, T)] ▷^{a} e : τ_{2}, T}{Γ ▷^{a} let x be v in e : τ_{2}, T} (let_{v})

\frac{Γ ▷^{a} e_{1} : τ_{1}, T Γ[x ↦ AppClose(τ_{1}, Γ, T)] ▷^{a} e_{2} : τ_{2}, T e_{1} ∉ Values}{Γ ▷^{a} let x be e_{1} in e_{2} : τ_{2}, T} (let_{e})

(callcc) Γ ▷^{a} callcc : ((τ_{1} → τ_{2}) → τ_{1}) → τ_{1}, T if τ_{1} is imperative

\frac{Γ ▷^{a} e : τ_{1}, T τ_{1} ∈ T}{Γ ▷^{a} abort e : τ_{2}, T} (abort)

Close(τ, Γ, T) = ∀α_{1} … α_{n}.τ
where {α_{1}, …, α_{n}} = F T V (τ) \ (F T V (Γ) ∪ F T V (T))
AppClose(τ, Γ, T) = ∀α_{1} … α_{n}.τ
where {α_{1}, …, α_{n}} = (F T V (τ) \ (F T V (Γ) ∪ F T V (T))) ∩ AppTypeVar

Figure 7: The augmented type system for Control ML

Main Lemma 6.5 (Subject Reduction) If ▷^{a} e_{1} : τ, T and τ ∈ T and e_{1} ⟼ e_{2} then

▷^{a} e_{2} : τ′, T and τ′ ∈ T.

Proof. The proof proceeds by case analysis according to the reduction e_{1} ⟼ e_{2}. Each case is easily adapted from the corresponding case in the proof of Typability Preservation with straightforward adaptations of the necessary lemmas.

With Uniform Evaluation and the fact that faulty expressions are untypable (in the ordinary system), we obtain a syntactic soundness theorem for abort-free expressions.

Theorem 6.6 (Syntactic Soundness) If ▷ e : τ and e contains no abort-expressions then either e ⇑ or e → ⟼ v and ▷ v : τ.

Proof. By Uniform Evaluation, either e → ⟼ e′ and e′ is faulty, or e ⇑, or e → ⟼ v. Since ▷ e : τ and e contains no abort-expressions, by Correspondence ▷^{a} e : τ, {τ}. Subject Reduction then implies ▷^{a} e′ : τ, {τ}. Similarly ▷^{a} v : τ, {τ}, and by Correspondence ▷ e′ : τ and ▷ v : τ. Suppose e → ⟼ e′ and e′ is faulty. Since faulty expressions are untypable, ▷ e′ : τ is a contradiction, therefore this case cannot occur. Hence either e ⇑ or e → ⟼ v and ▷ v : τ.

7 Discussion

Subject reduction is the key lemma in our approach to proving type soundness. In order to demonstrate subject reduction, it must be possible to assign a type to each intermediate evaluation state of a program. This is most easily accomplished by specifying evaluation as rewriting. Rewriting may be specified as local reductions, as our calculus for Core ML, or as program (or top-level) rewriting, as in Control ML.

Through most of this paper, we present the semantics of the various languages with calculi that permit local reductions. It is also possible to use our proof technique with a semantics that specifies only program reductions (⟼), as in Control ML. Such a semantics for Reference ML is slightly simpler, as the ref, ρ_{merge}, and ρ_{lift} reductions coalesce into one program reduction, but the structure of the proof is essentially the same. Our work on an alternative type system for references uses this approach [38]. We chose to use calculi in this paper as the resulting proofs are more regular in structure.

In specifying the semantics of references as a calculus, we use an additional expression form, the ρ-expression, that is not present in ML. As noted earlier, ρ-expressions may be regarded as abbreviations, both from a semantic perspective and a typing perspective (the typing rule for ρ-expressions can be derived from the abbreviation). In principle, it is possible to eliminate ρ-expressions from the syntax, however the specification of redexes in the reduction rules becomes complicated. Alternatively, ρ-expressions may be considered as belonging to the state space of evaluation, and not to the language of programs that may be written by a programmer. In a presentation of the typing rules for consumption by programmers, the typing rule for ρ-expressions may be deleted. However, unlike ρ-expressions, the abort-expressions of the continuation fragment cannot be considered as abbreviations [10]. To obtain a strong soundness theorem, abort-expressions must be considered as belonging only to the evaluation space, and not to the syntax of programs. The exception fragment has no such additional expressions.

Other operational or denotational techniques for specifying semantics introduce additional semantic objects, such as closures and stores, rather than additional expression forms. Since the type system does not apply to such objects, stating and proving strong type soundness requires introducing a semantic relation (⊧) between semantic objects and types (see Section 2). We believe that introducing additional expression forms and typing rules is the simpler choice, and offer the simpler proofs produced by our method as evidence.

While in this paper we have concentrated on the essential aspects of ML, there are other features of static type systems that we believe our technique can address. Standard ML contains a datatype specification mechanism that allows the definition of new types and associated data constructors. This mechanism is indispensable when writing non-trivial ML programs. Subtyping, inheritance, and type inference for records are a strong focus of recent research efforts to explain object-oriented languages, as many popular objectoriented languages have unsound static type systems. Reppy [29] has successfully addressed concurrency with our technique; it should also be possible to treat nondeterminism and distributed computing. We have used our technique to prove an alternative type system for references sound [38]. Finally, it may be possible to adapt our technique to demonstrate the consistency of module systems like that of Standard ML.

Acknowledgements

We would like to thank Bob Harper for pointing out that type preservation is known as subject reduction in combinatory logic, and Hans Boehm and the anonymous referees for comments on earlier drafts of this paper.

Syntactic Type Soundness 45

Appendix: The Core of Standard ML

Syntax

e ::= v | e_{1} e_{2} | let x be e_{1} in e_{2} | ρθ.e | exception χ in e
v ::= c | x | Y | λx.e | ref | ! | := | raise | e handle | := v | raise v | e handle v
θ ::= { ⟨x, v⟩ }^{∗}
χ ::= x^{∗}
a ::= {exception χ in} {ρθ.} v | {exception χx in} {ρθ.} raise x v

Semantics eval(e) = a iff e → ⟼ a E[e] ⟼ E[e′] iff e ⟶ e′ E ::= [] | E e | v E | let x be E in e | E handle v_{1} v_{2} | ρθ.E | exception χ in E

Functional ML

(δ)  c v ⟶ δ(c, v) if δ(c, v) is defined
(β_{v})  (λx.e) v ⟶ e[x ↦ v]
(let)  let x be v in e ⟶ e[x ↦ v]
(Y )  Y v ⟶ v (λx.(Y v) x)

References

(ref )  ref v ⟶ ρ⟨x, v⟩.x
(deref )  ρθ⟨x, v⟩.R[! x] ⟶ ρθ⟨x, v⟩.R[v]
(assign)  ρθ⟨x, v_{1}⟩.R[:= x v_{2}] ⟶ ρθ⟨x, v_{2}⟩.R[v_{2}]
(ρ_{merge})  ρθ_{1}.ρθ_{2}.e ⟶ ρθ_{1}θ_{2}.e
(ρ_{lift})  R[ρθ.e] ⟶ ρθ.R[e] if R ≠ []
R ::= [] | R e | v R | let x be R in e | R handle v_{1} v_{2}

Exceptions

(raise)  U[raise x v] ⟶ raise x v if U ≠ []
(handle)  (raise x v_{1}) handle x v_{2} ⟶ v_{2} v_{1}
exception χx_{1}x_{2} in
X[(raise x_{1} v_{1}) handle x_{2} v_{2}]

⟶ exception χx_{1}x_{2} in X[raise x_{1} v_{1}] x_{1} ≠ x_{2}

(reraise)

(unhandle)  v_{1} handle x v_{2} ⟶ v_{1}
(exn_{merge}) exception χ_{1} in exception χ_{2} in e ⟶ exception χ_{1}χ_{2} in e
(exn_{lift})  X[exception χ in e] ⟶ exception χ in X[e] if X ≠ []
U ::= [] | U e | v U | let x be U in e
X ::= [] | X e | v X | let x be X in e | X handle v_{1} v_{2} | ρθ.X

Typing Functional ML

Γ ▷ x : τ if Γ(x) ≻ τ (var) (const) Γ ▷ c : τ if TypeOf (c) ≻ τ Γ ▷ Y : ((τ_{1} → τ_{2}) → τ_{1} → τ_{2}) → τ_{1} → τ_{2} (Y)

\frac{Γ[x ↦ τ_{1}] ▷ e : τ_{2}}{Γ ▷ λx.e : τ_{1} → τ_{2}} (abs)

\frac{Γ ▷ e_{1} : τ_{1} → τ_{2} Γ ▷ e_{2} : τ_{1}}{Γ ▷ e_{1} e_{2} : τ_{2}} (app)

\frac{Γ ▷ v : τ_{1} Γ[x ↦ Close(τ_{1}, Γ)] ▷ e : τ_{2}}{Γ ▷ let x be v in e : τ_{2}} (let_{v})

\frac{Γ ▷ e_{1} : τ_{1} Γ[x ↦ AppClose(τ_{1}, Γ)] ▷ e_{2} : τ_{2} e_{1} ∉ Values}{Γ ▷ let x be e_{1} in e_{2} : τ_{2}} (let_{e})

Close(τ, Γ) = ∀α_{1} … α_{n}.τ where {α_{1}, …, α_{n}} = F T V (τ) \ F T V (Γ)

AppClose(τ, Γ) = ∀α_{1} … α_{n}.τ where {α_{1}, …, α_{n}} = (F T V (τ) \ F T V (Γ)) ∩ AppTypeVar

References

(ref) Γ ▷ ref : τ → τ ref if τ is imperative (deref) Γ ▷ ! : τ ref → τ (assign) Γ ▷ := : (τ ref → τ → τ)

\frac{Γ[x_{1} ↦ τ_{1} ref ] … [x_{n} ↦ τ_{n} ref ] ▷ e : τ Γ[x_{1} ↦ τ_{1} ref ] … [x_{n} ↦ τ_{n} ref ] ▷ v_{i} : τ_{i} τ_{i} is imperative 1 ≤ i ≤ n}{Γ ▷ ρ⟨x_{1}, v_{1}⟩ … ⟨x_{n}, v_{n}⟩.e : τ} (rho)

Exceptions

(raise) Γ ▷ raise : τ_{1} exn → τ_{1} → τ_{2}

\frac{Γ ▷ e : τ_{2}}{Γ ▷ e handle : τ_{1} exn → (τ_{1} → τ_{2}) → τ_{2}} (handle)

\frac{Γ[x_{1} ↦ τ_{1} exn] … [x_{n} ↦ τ_{n} exn] ▷ e : τ τ_{i} is imperative 1 ≤ i ≤ n}{Γ ▷ exception x_{1} … x_{n} in e : τ} (exn)

References

[1] Abadi, M., Cardelli, L., Pierce, B., and Plotkin, G. Dynamic typing in a statically-typed language. ACM Transactions on Programming Languages and Systems 13, 2 (April 1991), 237–268. Previously appeared in: Proceedings of the 16th Annual Symposium on Principles of Programming Languages (January 1989), 213–227.

[2] Barendregt, H. P. The Lambda Calculus: Its Syntax and Semantics, revised ed., vol. 103 of Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1984.

[3] Crank, E., and Felleisen, M. Parameter-passing and the lambda calculus. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 233–244.

[4] Curry, H. B., and Feys, R. Combinatory Logic, Volume I. North-Holland, Amsterdam, 1958.

[5] Damas, L., and Milner, R. Principal type schemes for functional programs. Proceedings of the 9th Annual Symposium on Principles of Programming Languages (January 1982), 207–212.

[6] Damas, L. M. M. Type Assignment in Programming Languages. PhD thesis, University of Edinburgh, 1985.

[7] Donahue, J., and Demers, A. Data types are values. ACM Transactions on Programming Languages and Systems 7, 3 (July 1985), 426–445.

[8] Duba, B. F., Harper, R., and MacQueen, D. Typing first-class continuations in ML. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 163–173.

[9] Felleisen, M. The theory and practice of first-class prompts. Proceedings of the 15th Annual Symposium on Principles of Programming Languages (1988), 180–190.

[10] Felleisen, M. On the expressive power of programming languages. Science of Computer Programming 17 (1991), 35–75. Preliminary version in: Proceedings of the European Symposium on Programming, LNCS 432 (1990), 134–151.

[11] Felleisen, M., and Friedman, D. P. Control operators, the SECD-machine, and the λ-calculus. In Formal Description of Programming Concepts III, M. Wirsing, Ed. Elsevier Science Publishers B.V. (North-Holland), Amsterdam, 1986, pp. 193–217.

[12] Felleisen, M., and Friedman, D. P. A syntactic theory of sequential state. Theoretical Computer Science 69, 3 (1989), 243–287. Preliminary version in: Proceedings of the 14th Annual Symposium on Principles of Programming Languages, 1987, 314-325.

[13] Felleisen, M., Friedman, D. P., Kohlbecker, E. E., and Duba, B. A syntactic theory of sequential control. Theoretical Computer Science 52, 3 (1987), 205–237. Preliminary version in: Proceedings of the Symposium on Logic in Computer Science, 1986, 131–141.

[14] Felleisen, M., and Hieb, R. The revised report on the syntactic theories of sequential control and state. Tech. Rep. TR-100, Rice University, June 1989. To appear in: Theoretical Computer Science, 1992.

[15] Hindley, R. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society 146 (December 1969), 29–60.

[16] Hindley, R. J., and Seldin, J. P. Introduction to Combinators and λ-Calculus. Cambridge University Press, 1986.

[17] Leroy, X., and Weis, P. Polymorphic type inference and assignment. Proceedings of the 18th Annual Symposium on Principles of Programming Languages (January 1991), 291–302.

[18] MacQueen, D. B., Plotkin, G., and Sethi, R. An ideal model for recursive polymorphic types. Proceedings of the 11th Annual Symposium on Principles of Programming Languages (January 1984), 165–174.

[19] Mason, I., and Talcott, C. Programming, transforming, and proving with function abstractions and memories. In Proceedings of the International Conference on Automata, Languages, and Programming, LNCS 372 (1989), Springer-Verlag, pp. 574– 588.

[20] Milner, R. A theory of type polymorphism in programming. Journal of Computer and System Sciences 17 (1978), 348–375.

[21] Milner, R., and Tofte, M. Co-induction in relational semantics. Theoretical Computer Science 87 (1991), 209–220.

[22] Milner, R., and Tofte, M. Commentary on Standard ML. MIT Press, Cambridge, Massachusetts, 1991.

[23] Milner, R., Tofte, M., and Harper, R. The Definition of Standard ML. MIT Press, Cambridge, Massachusetts, 1990.

[24] Mitchell, J. C., and Harper, R. The essence of ML. Proceedings of the 15th Annual Symposium on Principles of Programming Languages (January 1988), 28–46.

[25] Mitchell, J. C., and Plotkin, G. D. Abstract types have existential type. ACM Transactions on Programming Languages and Systems 10, 3 (July 1988), 470–502. Also appeared in: Proceedings of the 11th Annual Symposium on Principles of Programming Languages, 1984, 37-51.

[26] Plotkin, G. D. Call-by-name, call-by-value and the lambda-calculus. Theoretical Computer Science 1 (1975), 125–159.

[27] Plotkin, G. D. A structural approach to operational semantics. Tech. Rep. DAIMI FN-19, Århus University, September 1981.

[28] Rees, J., and Clinger, W. Revised^{3} report on the algorithmic language Scheme. SIGPLAN Notices 21, 12 (December 1986), 37–79.

[29] Reppy, J. H. Higher-order Concurrency. PhD thesis, Cornell University, 1991.

[30] Reynolds, J. Definitional interpreters for higher order programming languages. ACM Conference Proceedings (1972), 717–740.

[31] Reynolds, J. C. On the relation between direct and continuation semantics. Proceedings of the International Conference on Automata, Languages, and Programming (1974), 141–156.

[32] Scott, D. Data types as lattices. SIAM Journal of Computing 3, 5 (1976), 522–586.

[33] Seldin, J. P. A sequent calculus for type assignment. Journal of Symbolic Logic 42 (1977), 11–28.

[34] Standard ML of New Jersey release notes (version 0.75). AT&T Bell Laboratories, November 1991.

[35] Talpin, J.-P., and Jouvelot, P. The type and effect discipline. Tech. Rep. EMP-CRI A/206, Ecole des Mines de Paris, July 1991.

[36] Tofte, M. Operational Semantics and Polymorphic Type Inference. PhD thesis, University of Edinburgh, 1987.

[37] Tofte, M. Type inference for polymorphic references. Information and Computation 89, 1 (November 1990), 1–34.

[38] Wright, A. K. Typing references by effect inference. In Proceedings of the European Symposium on Programming, LNCS 582 (1992), Springer-Verlag, pp. 473–491.