Standard ML-NJ weak polymorphism and imperative constructs

John Mitchell^{∗} Ramesh Viswanathan^{∗}

Department of Computer Science Stanford University, Stanford, CA 94305

                           {mitchell, vramesh}@cs.stanford.edu

July 15, 1994

Abstract

Standard ML of New Jersey (SML-NJ) uses “weak type variables” to restrict the polymorphic use of functions that may allocate reference cells, manipulate continuations, or use exceptions. However, the type system used in the SML-NJ compiler has not previously been presented in a form other than source code nor proved correct. We present a set of typing rules, based on a careful analysis of the concepts underlying “weak polymorphism”, that appears to subsume the implemented algorithm and uses type variables of only a slightly more general nature than the compiler. One insight in the analysis is that allowing a variable to occur both “ordinarily” and “weakly” in a type permits a simpler and more flexible formulation of the typing rules. In particular, we are able to treat applications of polymorphic functions to imperative arguments with greater flexibility than SML-NJ. The soundness of the type system is proved for imperative code using operational semantics, by showing that evaluation preserves typability. By incorporating assumptions about memory addresses in the type system, we avoid proofs by co-induction.

1 Introduction

In the absence of side effects and so-called control effects (continuations and exceptions), the type inference methods developed by Curry, Hindley and Milner [CF58, Hin69, Mil78] provide an effective and useful method for detecting type errors at compile time. For any typable untyped expression, the type inference algorithm computes a single most general type, from which all other types of the expression may be derived easily. Although the worst-case complexity is high [KMM91, KTU90], the algorithm has been found efficient in practice. More importantly, experience suggests that it is possible for a programmer to predict, with relative ease, the type that the algorithm will produce. In addition, type inference allows a form of error detection that is unfamiliar to explicitlytyped programming. Even when a declaration is typable, the programmer may detect an error by noticing that the type inferred by the compiler differs from the type expected by the programmer (c.f. [Koe92]).

Unfortunately, the straightforward, predictable polymorphic typing algorithm fails for programs with side-effects or control effects. To illustrate the problems involved, we use a lambda calculus extended with let-expressions (for polymorphism) and imperative operators ref , ! and : = . Briefly, ref x allocates a new cell, initialized to x, r : = x updates the contents of reference r to the value of x, and !r returns the current contents of reference r. The incorrectness of the naive polymorphic typing of side-effects is illustrated by the program

∗Supported in part by an NSF PYI Award, with matching funds from AT&T, Digital Equipment Corporation, the Powell Foundation and Xerox Corporation; and by the Wallace F. and Lucille M. Davis Faculty Scholarship.

let r = ref (λx. x) in r : = λx. x + 1 ; !r true

where ; is the usual sequencing operator (definable by lambda abstraction under call-by-value). If we apply the Milner typing algorithm, we give r type ∀α.[(α → α) ref ] , where τ ref is the type of references to values of type τ . Intuitively, this means that for any type σ, α can be instantiated to σ to give r the type (σ → σ) ref . Both expressions in the body of the declaration are well-typed, under this assumption, since we can take the instances (int → int) ref and (bool → bool) ref for the two occurrences of r, respectively. However, since the assignment changes the value of r from a polymorphic function to an integer function, the application of !r to true results in a run-time type error. Thus, a naive polymorphic treatment of side-effects does not prevent run-time type errors in the presence of assignment.

We can view solutions to this problematic interaction of polymorphism and side-effects from a general perspective, by understanding the way polymorphic type inference works. In typing an expression of the form let x = e_{1} in e_{2} , the most general type τ of e_{1} is calculated. Certain type variables in τ are determined to be “generic” or “polymorphic”. If α_{1}, …, α_{n} is a list of all the generic variables in τ , we write the type of e_{1} as ∀α_{1} … ∀α_{n}.τ . In typing e_{2} , all the generic/polymorphic type variables may then be replaced by types, independently chosen for each occurrence of x. For example, if e_{1} has type ∀α.α → int , and e_{2} is the expression x x, then e_{2} may be typed by replacing α by int → int in the first occurrence of x and int in the second occurrence. If a type variable is determined to be non-polymorphic, it can only be replaced by the same type in all occurrences of the let-bound variable x. Thus a critical aspect of polymorphic type inference is the method for identifying the type variables that may be safely be treated as polymorphic. In the absence of side-effects or control effects, there is a simple condition depending on the types of free variables of e_{1} . The main topic of this paper, and previous studies of polymorphism and imperative constructs, is the safe and flexible extension of the condition for pure terms to terms with side-effects. Over the past decade, a number of restrictions on the polymorphic uses of references have been proposed. Some of these have been implemented and others have been analyzed and proved correct, as described below. Our main contribution is a precise definition of a type system that appears to subsume the algorithm used in SML-NJ and a correctness proof for it. Although similar problems occur with continuations and exceptions, as illustrated in [HL91, WF92], we restrict our attention to side effects, in this paper.

In Standard ML of New Jersey [AM87, AM91], so-called “weak type variables” are used to characterize functions that may create reference cells after some number of applications. Since the type of a polymorphic function may become more specialized with each application (as, for example, when a polymorphic function is applied to a monomorphic argument), many functions that create references could create polymorphic references for some actual parameters, and monomorphic references for others. For example, the function

λf. λx. ref(fx)

creates a reference to the result of applying the first actual parameter to the second. This function is unproblematic for creating references to integers or booleans, but we cannot allow the result of application to two arguments to be used polymorphically because of the phenomenon described above. The most restrictive solution to the problem of typing references would be to require some fixed, non-polymorphic type for this function. A more flexible approach might be to force every argument to this function to be non-polymorphic. However, this too is overly restrictive since the reference cell is not created until the second actual parameter is supplied. For example, we may safely obtain a polymorphic function by applying to the polymorphic identity, provided any eventual second argument is non-polymorphic. The main innovation of SML-NJ weak typing, over previous approaches, is to use numeric indices on each type variable to count the number of function applications required to produce a reference cell of that type. Although this system has seen widespread and largely successful use in recent years, the SML-NJ algorithm has never been presented in a form other than relatively complicated source code, and consequently has never been analyzed or proved sound.

We present our type system as a set of typing rules, using a mild extension of the weak type variables of SML-NJ. These rules were derived from experiments with the algorithm implemented in Standard ML of New Jersey, Version 75 (November 11, 1991) and perusal of the source code. Although our original intention was to formalize the implemented algorithm exactly, we found it easier and more informative to define a more general type system with simpler typing rules and fewer apparent special cases. One insight came as a result of examining the way that the type of an expression depends on the types of its non-polymorphic free variables. In SML-NJ, every weak type variable appears throughout the type of an expression with the same strength. For example, the expression ref has the type α^{1} → α^{1} ref . Such a restriction forces the numeric superscripts in the type of a free variable to characterize two sources of storage allocation. They must simultaneously give a lower bound on the number of applications of the variable itself that may produce a reference, and a lower bound on the number of applications of the expression containing the variable. Thus, in typing an expression, the type assumption of a free variable needs to be modified according to the sub-expression that one is typing. We avoide this is by allowing both “ordinary” and “weak” occurrences of a type variable in a type. This leads to the formulation of a stronger typing rule for application than the compiler output indicates. Consequently, our typing rules appear to subsume the implemented algorithm, particularly for applications of purely functional expressions to potentially imperative arguments. We show that our typing rules are sound, using an operational semantics of ML with references, implying the semantic soundness of any algorithm that decides a conservative approximation to these rules.

More expressive type systems have been developed by Leroy and Weis [LW91], and, independently, by Talpin, Jouvelot and others [TJ92, Wri92], partly based on the framework of Gifford’s FX system [JG91]. In contrast to the SML-NJ algorithm and preceding ML compilers, which keep track of the types of all values in the store, these approaches approximately identify the values in the store that are accessible in a particular context. This additional accesibility information leads to type systems that are capable of giving functions which use references only locally the same types as their corresponding applicative versions. However, to be able to maintain this information, more complicated type expressions are required. While the more complex systems are promising, it is more difficult to predict the types of certain functions. Since we believe that the success of ML typing lies not only in its correctness, but the ease with which it may be understood in programming, any added complication to the type system deserves careful scrutiny. Consequently, it seems worthwhile to explore systems using only weak type variables and determine the limits of this approach.

2 Weak Polymorphism

In the approach we refer to as weak polymorphism, each type variable has an associated degree of strength, or degree for short. In the SML-NJ implementation, a degree may be a nonnegative integer, or ∞. Variables of infinite degree are printed without any degree designation. Intuitively, the degree of a type variable α, occurring in the typing of some expression e, indicates how many applications of e are required to produce a reference to a value whose type contains α. Functions that do not produce references at all are typed using variables of infinite degree. For example, the type of ref itself is

ref : α^{1} → α^{1} ref

where the superscript indicates that α^{1} is a weak type variable of degree 1. This type implies that when the function ref is applied, α may appear in the type of a stored value, and should not be treated polymorphically. However, the α in the type of ref is polymorphic, as is any type variable of non-zero degree. This means that ref may be applied to an argument of any type, but the result cannot be used polymorphically. Another example is the list-producing function λx. ref[x] , which has type α^{1} → α^{1} list ref since it takes one application of this function to produce a reference to a value whose type contains α, or some type substituted for α. Since each application weakens the type of a function, each surrounding lambda abstraction strengthens every type variable in the type. The reader may enjoy giving the example used in the introduction, λf. λx. ref(fx) , to the SML-NJ compiler and seeing where the strength 2 appears.

We may put the SML-NJ type system in perspective by reviewing the history of polymorphic type systems for imperative constructs. Early implementations of ML only allowed references to values of monomorphic, statically-known types. This approach guarantees soundness, but makes it impossible to write polymorphic functions that create or use references. In his thesis, Damas introduced the first type system to allow polymorphic use of functions that create references [Dam85]. Unfortunately, although his system has not been shown unsound, his claimed soundness proof is incorrect. Tofte was the first to give a type discipline for polymorphic references together with a correct soundness proof [Tof88, Tof90]. The central idea of Tofte’s solution is to partition the types into “imperative” and “applicative” types, requiring all type variables that occur in an imperative type to be imperative. Values of imperative type can be stored, but only applicative type variables are treated polymorphically, successfully avoiding the creation of references to polymorphic values. MacQueen’s system, implemented in the Standard ML of New Jersey ML compiler, is largely derived from Tofte’s, using the numeric “degree” of a weak type variable to count how many function applications it takes for a type variable to become “imperative.”

The power of weak polymorphism may be understood by comparison with Tofte’s system. In Tofte’s system, any type variable that appears in the type of a value that could potentially be stored has to be imperative and hence cannot be used polymorphically, even if the value does not actually appear in the store yet. Technically, imperative type variables are treated non-polymorphically only in the types of so-called “expansive” expressions, which include let expressions. Therefore, we illustrate the limitations of Tofte’s system using the following expression, rid , which is a version of the identity function using side-effects.

rid ≡ let z = dummy in λx.!(ref x)

Since x is stored, its type must be imperative. Consequently, in Tofte’s system, the expression e is given a type u → u, where u is an imperative type variable that cannot be generalized. With weak polymorphism, however, we can take into account the fact that rid must be applied once before the reference to x is created. This allows us to give rid the type α^{1} → α^{1} , where the type variable α^{1} can now be generalized. Since rid may be used polymorphically using weak polymorphism, but not in Tofte’s system, the expression

                             let f = rid in f 1 ; f true

is typable in SML-NJ but not in Tofte’s system.

In our typing rules, we generalize the SML-NJ type expressions slightly to associate numeric indices with ordinary type variables. In addition, a type variable can have both “ordinary” and “weak” occurrences, as well as occur with different strengths in a type. Aside from these relatively minor changes, which allow us to express the relationship between degrees of various type variables more clearly, our type expressions are identical to the those used in Standard ML of New Jersey. It seems that significantly more complicated typing rules are needed if only the SML-NJ type expressions are used. In fact, we were not able to devise a sound system with SML-NJ type expressions using ordinary proof rules without excessively complicated side conditions.

3 Language

3.1 Syntax

In describing our typing rules and proving them correct, we use an untyped call-by-value language with ML-style imperative features. In writing the expressions of our language we allow arbitrary term constructors of specified arity. More formally, the language is parameterized by a set C of pairs, ⟨f, n⟩, where n ≥ 0 gives the arity of the term constructor f . Having term constructors, as opposed to term constants, allows one to represent non-strict operators in the call-by-value language. The expressions are given by the grammar

e : : = x | f(e_{1}, …, e_{n}) | e_{1} e_{2} | λx. e | let x = e_{1} in e_{2} |
l | ref | !e | e_{1} : = e_{2}

where ⟨f, n⟩ ∈ C , x ∈ V ar, l ∈ Loc, Var is a denumerable set of variables, and Loc is a denumerable set of location constants. The location constants do not appear in user programs (this would be tantamount to allowing the user to pick addresses), but help in defining the operational semantics. We thus define programs to be closed expressions not containing any location constants.

In defining the operational semantics, it is useful to distinguish a subset of closed expressions that cannot be further evaluated. These are called values. Besides some expressions that depend on the particular choice of term constructors, the set of values always includes λ -abstractions, location constants, and the constant ref.

v : : = ⋯ | λx. e | l | ref

The additional values that depend on the term constructors are specified in a set V . Each element of V is of the form f(d_{1}, …, d_{n}) where ⟨f, n⟩ ∈ C and each d_{i} is an expression or a value.

3.2 Operational Semantics

We use a rewriting semantics to specify operational behaviour. In defining the operational semantics, we use a syntactic form wrong to represent run-time errors.

We begin by defining a relation, ⇝, with e ⇝ r indicating that e is a purely functional redex reducing directly to r, i.e., without any side-effects. The result, r, of the reduction is either another expression or wrong . The behaviour of the functional term constructors is given by a set F of pairs of the form ⟨e, r⟩, indicating that e reduces to r, where e is an expression of the form f(e_{1}, …, e_{n}) and r is another expression or wrong . The purely functional reduction relation, ⇝,

(E[e], s) ⟼ (E[e′], s)  if e ⇝ e′, e′ ≠ wrong
(E[ref v], s) ⟼ (E[l], s[l ↦ v]) where l ∉ dom(s)
(E[!l], s) ⟼ (E[s(l)], s)
(E[l : = v], s) ⟼ (E[v], s[l ↦ v])
(E[e], s) ⟼ (wrong, s)  if e ⇝ wrong
(E[!v], s) ⟼ (wrong, s)  if v ∉ Loc
(E[v_{1} : = v_{2}], s) ⟼ (wrong, s)  if v_{1} ∉ Loc

Table 1: One-step evaluation relation.

is defined by

(λx. e) v ⇝ [v/x]e
let x = v in e ⇝ [v/x]e
v_{1} v_{2} ⇝ wrong if v_{1} not a λ-abstraction, ref
e ⇝ r  if ⟨e, r⟩ ∈ F

To impose an order on the evaluation of subexpressions, we use the notion of an evaluation context [WF92]. The evaluation contexts E[ ] are defined by the following grammar

E[ ] : : = [ ] | E e | v E | let x = E in e | ⋯ | ref E | !E | E : = e | v : = E

where the unspecified productions are used to reflect the order of evaluation of the arguments of term constructors and are of the form f(d_{1}, …, d_{n}) , where exactly one of the d_{i}’s is an evaluation context E and the others are values v or expressions e. Intuitively, the hole in an evaluation context specifies the next subexpression to be evaluated.

To handle imperative features, our operational rules will manipulate “stores” in addition to terms, where a store is a finite partial map from location constants to values. The basic one-step evaluation relation ⟼ is defined in Table 1, with (e, s) ⟼ (r, s′) indicating that the expression e in store s evaluates in one step to the result r resulting in new store s′. The result r is either another expression or the run-time error wrong .

The result of execution of any program, obtained by evaluating it in the initial empty store, is captured by a partial function Eval. Writing ⟼ for the reflexive and transitive closure of ⟼, Eval(e) = a iff (e, init) ⟼ (a, s′) for some store s′, where the answer a is either a value or wrong and init is the empty store that is undefined on all locations. A program e may diverge, in which case Eval(e) is undefined. We say that a program e does not lead to a run-time error if Eval(e) ≠ wrong .

4 Type System

4.1 Type Expressions and Instances

Our type expressions are built from type variables using the constructor → for function types, and ref for reference cells, in addition to type constructors for other datatypes. To incorporate weak polymorphism, every “weak” type variable will have an index which is its degree of strength. However, unlike ML, an ordinary type variable will also have an associated index in our type system.

We start with a set B of type constructors for datatypes such as integers, lists etc. Each element of B is a pair of the form ⟨b, n⟩, where n ≥ 0 gives the arity of the type constructor b.

Let TVars be an infinite set of type variables whose elements will be indicated by metavariables α, α_{1}, …, β, β_{1}, . . .. A “weak” occurrence of a type variable will be signified by underlining it. As mentioned before, every “weak” and “ordinary” occurrence of a type variable has an associated index, which will be a natural number. We thus arrive at the following grammar for generating pre-types, some of which will be deemed to be well-formed types:

ρ : : = α^{j} | \underline{α}^{j} | ρ_{1} → ρ_{2} | ρ_{1} ref | b(ρ_{1}, …, ρ_{n})

In this grammar we assume that ⟨b, n⟩ ∈ B and j ∈ N . Intuitively, a pre-type of the form ρ_{1} → ρ_{2} can be used as the type of some expression only if any type variable occurring “imperatively” in ρ_{1} does not occur “applicatively” in ρ_{2} and vice-versa. We now elaborate the precise condition distinguishing types from pre-types.

For any pre-type ρ, we define its free type variables, FTV(ρ) , to be the set of variable names appearing in it, without regard to their index or whether they are underlined. More precisely,

FTV(α^{j}) = {α}
FTV(\underline{α}^{j}) = \{α\}
FTV(ρ_{1} → ρ_{2}) = FTV(ρ_{1}) ∪ FTV(ρ_{2})
FTV(ρ_{1} ref ) = FTV(ρ_{1})
FTV(b(ρ_{1}, …, ρ_{n})) = FTV(ρ_{1}) ∪ ⋯ ∪ FTV(ρ_{n})

Intuitively, a weak occurrence of a type variable α indicates that α appears in the type of a value to which a reference may potentially be created. The index j in a weak occurrence \underline{α}^{j} indicates that at least j applications of the relevant expression are needed before the reference to the type containing α is actually created. Thus, only \underline{α}^{0} is deemed to be an imperative occurrence and indicates that α is imperative, i.e., appears in the type of a stored value. On the other hand ordinary type variables never appear in the type of a stored value. Thus the applicative variables, ATV(ρ) , i.e., those variables that do not appear in the store typing can be defined by

ATV(α^{j}) = {α}
ATV(\underline{α}^{j}) = \{α\} if j > 0
ATV(\underline{α}^{0}) = ϕ
ATV(ρ_{1} → ρ_{2}) = ATV(ρ_{1}) ∪ ATV(ρ_{2})
ATV(ρ_{1} ref ) = ATV(ρ_{1})
ATV(b(ρ_{1}, …, ρ_{n})) = ATV(ρ_{1}) ∪ ⋯ ∪ ATV(ρ_{n})

The imperative type variables are the free type variables that do not occur applicatively:

ITV(ρ) = FTV(ρ) \ ATV(ρ)

We say that a pre-type ρ is imperative if all its free variables occur imperatively, i.e., ITV(ρ) = FTV(ρ) .

Since the index in a weak occurrence indicates the number of applications needed before it becomes imperative, we would intuitively expect every application to decrement the strength in every occurrence by 1 . We will also decrement the index in ordinary occurrences after an application. All this is formally captured by the weakening map W defined on indexed variables as

W (α^{j}) = \{ \begin{matrix}α^{j−1} & if j > 0 \\ undefined & otherwise \end{matrix}
W (\underline{α}^{j}) = \{ \begin{matrix}\underline{α}^{j−1} & if j > 0 \\ \underline{α}^{0} & otherwise \end{matrix}

and extended to all pre-types in the obvious way using the type constructors, →, ref , b. If ordinary occurrences of type variables were allowed to have negative indices then we can avoid having W (α^{0}) undefined. However, we prefer the present framework as it allows us to define substitutions more elegantly.

We can now give some intuition for the indices in ordinary occurrences of a type variable. These are used to keep track of any applications and abstractions occurring in the body of an expression. The weakening map W is used in typing an application to decrease the index in every ordinary occurrence by 1 . Analogously, in typing an abstraction, we will increase the indices in ordinary occurrences by 1 . Thus if an there is an ordinary occurrence of a type variable α in the type ρ of an expression e, its index relative to the indices of other occurrences of α in ρ gives us information about any applications and abstractions within the body of e. This allows a more uniform treatment when a type containing weak occurrences of type variables is substituted for an ordinary occurrence of a type variable. This arises, for example, when a purely functional expression is applied to an expression using imperative features, as is further discussed in Section 5.

The main property guaranteed by the type system is that when a type variable α appears in the type of a stored value after evaluation of an expression e, all occurrences of α in the type of e must be imperative. This requires some restrictions on the pre-types that can be used as types of expressions. The well-formed monotypes, indicated by meta variables τ, τ′, τ′′, …, τ_{1}, τ_{2}, … are defined as follows:

• For any α ∈ TVars, j ∈ N , α^{j}, \underline{α}^{j} are monotypes.

• If τ_{1}, τ_{2} are well-formed monotypes then τ_{1} → τ_{2} is a well-formed monotype, provided

(i) For all α ∈ FTV(τ_{1}) ∩ FTV(τ_{2}) , α ∈ ITV(τ_{1}) iff α ∈ ITV(τ_{2}) .

(ii) W (τ_{2}) is defined and is a well-formed monotype.

• τ_{1} ref is a well-formed monotype, if τ_{1} is a well-formed monotype.

• b(τ_{1}, …, τ_{n}) is a well-formed monotype, if τ_{1}, …, τ_{n} are well-formed monotypes.

Condition (i) on a type τ_{1} → τ_{2} forces any imperative type variable of τ_{1} to also occur only imperatively in τ_{2} and vice-versa. When an expression of type τ_{1} → τ_{2} is applied to an expression of type τ_{1} , the type of the resulting expression is W (τ_{2}) , which is why we require Condition (ii) .

The polymorphic types, indicated by σ, σ_{1}, …, are given by the grammar

σ : : = τ | ∀α.σ

where τ is a monotype and α ∈ TVars . The variables α_{1}, …, α_{n} are bound in the polymorphic type ∀α_{1} … α_{n}. τ . We consider polymorphic types which differ only by a consistent renaming of bound variables equivalent. We define the set of free type variables, FTV(σ) , of a polytype as FTV(∀α_{1} … α_{n}. τ) = FTV(τ) \ {α_{1}, …, α_{n}} and similarly ITV(σ) as the set of free variables in σ that occur imperatively.

The instances of a polytype are defined using substitutions. A substitution S with domain T ⊆ TVars is a map from T to the well-formed monotypes. Intuitively, the substitution S specifies the type to replace ordinary occurrences with index 0 , with the types for other occurrences determined systematically from this. To state the types to use for other occurrences of a type variable, we will define maps Set_{i}, i ≥ 0 and Inc on monotypes. We will specify the behaviour of these maps on indexed variables, with the obvious extension to monotypes. The map Set_{i} sets all occurrences of a type variable, except those that are imperative, to a weak occurrence with strength i.

Set_{i}(α^{j}) = \underline{α}^{i}
Set_{i}(\underline{α}^{j}) = \{ \begin{matrix}\underline{α}^{i} & if j > 0 \\ \underline{α}^{0} & otherwise \end{matrix}

The following map, Inc , increments the indices in all occurrences of type variables, except the imperative ones.

Inc(α^{j}) = α^{j+1}
Inc(\underline{α}^{j}) = \{ \begin{matrix}\underline{α}^{j+1} & if j > 0 \\ \underline{α}^{0} & otherwise \end{matrix}

The effect of a substitution S with domain T on an indexed type variable is given by S(α^{j}) = Inc^{j}(S(α)) and S(\underline{α}^{j}) = Set_{i}(S(α)) , for α ∈ T , where Inc^{j} denotes the n -fold composition of Inc . If S has domain T , then S leaves any variable not in T unchanged. The type S(τ) and S(σ) for monotype τ and polytype σ can then be defined in the usual way, with possible renaming of bound variables. We often use [S(α_{1})/α_{1}, …, S(α_{n})/α_{n}] to denote the substitution S with domain {α_{1}, …, α_{n}}. Note that for a monotype τ , S(τ) may not necessarily be a wellformed monotype.

We say that a well-formed monotype τ′ is an instance of a polymorphic type σ = ∀α_{1} … α_{n}. τ , written ∀α_{1} … α_{n}. τ ≻ τ′, if there exists a finite substitution S with domain {α_{1}, …, α_{n}} such that S τ = τ′.

4.2 Typing Rules

The type system is given by a set of axioms and inference rules. The formulas that are derivable in this proof system are judgements of the form Γ, R ▷ e: τ , where Γ is a variable context, R is a location context, e and expression, and τ a monotype. The variable context Γ states assumptions about the free variables of e and is a set of pairs x: σ, where σ is a polytype, and no variable x appears twice in Γ . The location context R gives the types of values stored in the location constants that may appear in e. It is a set of pairs l: τ , where τ is an imperative monotype, with no location constant l appearing twice. A provable judgement Γ, R ▷ e: τ can thus be read as “the expression e has type τ in context Γ, R ”. Since expressions that appear in ML prorams never contain location constants, we never need assumptions about location constants in typing them. However, since expressions containing location constants could be the result of an evaluation step, and our proof of soundness proceeds by showing that evaluation preserves typability, we include location contexts, R, in our judgements. A type system for ML program expressions can be obtained by letting R be empty in all the axioms and inference rules.

Just as for pre-types, we will place some restrictions on valid typing judgements for expressions. Define the imperative type variables of a context to be the set of type variables that are imperative in any type appearing in the context, i.e.,

ITV(Γ, R) = ⋃_{x:σ∈Γ} ITV(σ) ∪ ⋃_{l:τ∈R} ITV(τ)

To motivate the restrictions that we will place on typing judgements, consider a store s with domain {l_{1}, …, l_{m}} such that the value, s(l_{i}) , stored in location l_{i} has type τ_{i}. Let e_{1}, …, e_{n} be closed expressions with e_{i} having type σ_{i}. Informally, a judgement, {x_{1}: σ_{1}, …, x_{n}: σ_{n}}, {l_{1}: τ_{1}, …, l_{m}: τ_{m}}▷ e: τ , asserts that if, starting in store s, we evaluate expressions e_{1}, …, e_{n} and substitute the resulting values for x_{1}, …, x_{n} in e, the resulting expression evaluates to a value of type τ . In this case, we want any type variable free in the type of a value in the final store to be imperative in τ . Any variable that is imperative in one of the σ_{i} ’s or τ_{i} ’s may be free in the type of a stored value after evaluation of the e_{i} ’s or in the initial store, and will therefore be free in the type of a stored value in the final store obtained after evaluation of e. We therefore say that a judgement Γ, R ▷ e: τ is a well-formed typing judgment iff

• τ is well-formed monotype, and

• For all α ∈ ITV(Γ, R) ∩ FTV(τ) , α ∈ ITV(τ) .

The type system depends on a set of typings for term constructors. These are given by a function TypeOf defined on all term constructors f , where if ⟨f, n⟩ ∈ C , then TypeOf (f ) is an expression of the form (τ_{1}, …, τ_{n} ⇒ τ) . We use the following notational conventions in the presentation of the type system. We write Γ(x) (and similarly R(l) ) for the unique σ with x: σ in Γ , if it exists, and Γ, x: σ for Γ ∪ {x: σ}, assuming x ∉ Γ . For any set of type variables, T , we define the substitution Imp_{T} with domain T by Imp_{T} (α) = \underline{α}^{0} . The closure of τ with respect to Γ , written Clos_{Γ}τ is the polytype ∀α_{1}, …, α_{n}.τ , where {α_{1}, …, α_{n}} = ATV(τ) \ FTV(Γ) and FTV(Γ) is the set of all free type variables in the types appearing in Γ . The restriction on only binding applicative type variables keeps variables that might appear in the types of stored values from being used polymorphically.

(var)  Γ, R ▷ x: Imp_{T} (τ)  if Γ(x) ≻ τ

(loc) Γ, R ▷ l: R(l) ref

(const)  \frac{Γ, R ▷ e_{1}: Sτ_{1} ⋯ Γ, R ▷ e_{n}: Sτ_{n}}{Γ, R ▷ f(e_{1}, …, e_{n}): Sτ} if TypeOf (f) = (τ_{1}, …, τ_{n} ⇒ τ), ITV(Sτ_{i}) ∩ ATV(Sτ) = ϕ

(abs)  \frac{Γ, x: τ_{1}, R ▷ e: W (τ_{2})}{Γ, R ▷ λx. e: τ_{1} → τ_{2}}

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

(let)  \frac{Γ, R ▷ e_{1}: τ_{1}  Γ, x: Clos_{Γ}τ_{1}, R ▷ e_{2}: τ}{Γ, R ▷ let x = e_{1} in e_{2}: τ}

(ref ) Γ, R ▷ ref: τ → Set_{1}(τ) ref

(deref )  \frac{Γ, R ▷ e: τ ref}{Γ, R▷!e: τ}

(assign)  \frac{Γ, R ▷ e_{1}: τ ref  Γ, R ▷ e_{2}: τ}{Γ, R ▷ e_{1} : = e_{2}: τ}

An implicit side-condition on all the axioms and typing rules is that the type judgement in the consequent is a well-formed typing judgment. This condition is non-trivial only for (var) , (const) , (ref ) , and (abs) . In other words, for all the remaining rules, if the premises are well-formed typing judgments, so is the consequent.

The typing rule for ref enforces the restriction that any value placed in the store must have a type in which all type variables are imperative. Thus, while ref can be applied to an expression of unrestricted type τ , the resulting reference cell would have an imperative type, since W (Set_{1}(τ)) is an imperative type for any type τ . Since applicative variables do not appear in the type of a stored value, the (let) rule generalizes all applicative type variables that are not free in the variable-context. Further, by our restriction on well-formed typing judgements, these applicative variables also cannot occur free in R, since all the free variables of R are imperative.

To understand the (abs) rule, we can give an alternative but equivalent formulation. For any set T of type variables, we define the map Up_{\T} on monotypes, increasing the strength of all variables except imperative occurrences of variables from T , by

Up_{\T} (\underline{α}^{0}) = \underline{α}^{0} if α ∈ T
Up_{\T} (\underline{β}^{i}) = \underline{β}^{i+1} if β ∉ T or i > 0
Up_{\T} (α^{i}) = α^{i+1}

Then the (abs) rule, together with the side-condition that the resulting judgement is well-formed, is equivalent to the rule

\frac{Γ, x: τ_{1}, R ▷ e: τ_{2}}{Γ, R ▷ λx. e: τ_{1} → Up_{\T} (τ_{2})}

with T ⊇ ITV(Γ, x: τ_{1}, R) , T ⊆ ATV(τ_{1}) and for any α ∈ ITV(Γ, R) ∩ FTV(τ_{1}), α ∈ ITV(τ_{1}) . Focussing only on the condition that T ⊇ ITV(Γ, x: τ_{1}) , this rule has the effect of permitting any of the imperative variables of τ_{2} , except those occurring imperatively in Γ, x: τ_{1}, R, to be made applicative. The variables that are imperative in τ_{2} but not in Γ, x: τ_{1}, R are those that appear in a stored value as a result of the evaluation of e. Since the evaluation of λx. e does not evaluate e, the references that e creates would not result from the evaluation of λx. e and hence can be safely made applicative.

Since stores are defined using values, which are syntactic expressions, we can use the type system to define store typings for stores. We say that a store s has store typing R, written s: R, if Dom(s) = Dom(R) and for all l ∈ Dom(s) we can derive the judgement ϕ, R ▷ s(l): R(l) .

5 Relation to SML-NJ

In the absence of a simple presentation of the algorithm used by the New Jersey implementation of ML, it is difficult to prove that all the expressions typable in ML are typable in our type system. Such a result coupled with our soundness proof would establish the soundness of SML-NJ. However, by allowing mixed “ordinary” and “weak” occurrences of a type variable and associating indices with “ordinary” occurrences as well, and a more careful accounting of the strengths during application and abstraction we are able to type-check many expressions which SML-NJ rejects. In this section, we give examples of such expressions. Along with demonstrating the expressive power of our type system, these examples help understand how the type system works.

In [LW91], Leroy and Weis give examples of various benchmark expressions to type-check. Their expressions fall into two categories. One class of expressions is those which use references only locally and which are given the same types in their type system as the corresponding applicative expressions. The other class of expressions are those which exercise the compatibility between functions that create mutable data and higher-order functions, all of which are rejected by SML-NJ. Leroy and Weis take this to be strong evidence that SML-NJ does not handle full functionality correctly. However, our type system gives all such expressions in [LW91, TJ92] the correct types. We illustrate this by considering just one example. Consider the expression (λx. x) ref . With our abstraction and application rules it can be seen that ϕ ▷ λx. x: (α^{0} → \underline{α}^{1} ref ) →(α^{1} → \underline{α}^{2} ref ) and hence ϕ ▷ (λx. x) ref: α^{0} → \underline{α}^{1} ref which is the same type as ref . However, SML-NJ rejects this expression. Thus our type system demonstrates that weak polymorphism, if formulated carefully, can indeed work well when applicative and imperative functions are mingled.

The other concept in our system that is different from SML-NJ is the association of indices with ordinary type variables, which allows us to infer any applications in the body of an expression. Thus λx. x has the type α^{0} → α^{1} , while λx. x nil has the type (α^{0} list → β^{1}) → β^{1} . The increase in the index of α in the result type of λx. x relative to its index in the argument type indicates the lack of any applications , while the index of β remaining the same in both argument and result types of λx. x nil indicates the application inside its body. (Since the occurrences of β are all ordinary, we also have λx. x nil : (α^{0} list → β^{6}) → β^{6} , for example.) On the other hand SML-NJ gives these expressions the types α → α and (α list → β) → β, with α and β implicitly considered to be of strength ∞. However, since such a type gives no information about applications inside the body, SML-NJ is forced to be conservative when such expressions are applied to say, ref . Hence, SML-NJ rejects (λx. x nil) ref correctly, but is also forced to reject (λx. x) ref . Using indices on ordinary type variables, we correctly deal with both these expressions as shown below:

(λx. x nil) : ∀αβ.(α^{0} list → β^{1}) → β^{1} ≻ (α^{0} list → \underline{α}^{1} list ref ) → \underline{α}^{1} list ref

Hence, (λx. x nil) ref : \underline{α}^{0} list ref . On the other hand,

(λx. x) : ∀α.α^{0} → α^{1} ≻ (α^{0} → \underline{α}^{1} ref ) →(α^{1} → \underline{α}^{2} ref )

and thus, (λx. x) ref : α^{0} → \underline{α}^{1} ref .

6 Soundness

In this section, we prove the soundness of the type system. The main lemma is a weaker form of the subject reduction property which shows the preservation of typability, for closed expressions, under evaluation. Since wrong , the run-time error, is not typable and only closed expressions are compiled, this is sufficient to prove the correctness of our type system. Since store typings were defined in Section 4.2 using derivability in the type system, rather than as maximal fixed points, we do not have to use co-induction in our proofs. This makes our soundness proof simpler than the one given in [Tof90].

We begin by proving some syntactic properties of the type system. In the following we use ⊢ Γ, R ▷ e: τ to indicate that the judgement Γ, R ▷ e: τ is derivable. Our first lemma is a generalization of the standard property of closure of typing derivations under substitution. It shows that by substituting for variables in a provable typing judgement, adding assumptions to the context, and making any number of variables in the type of the expression imperative, we still obtain provable typing judgements. To make the lemma easier to state, we first define the notion of an “instance” of a typing judgement.

Definition 6.1 Let Γ, R ▷ e: τ and Γ′, R′ ▷ e: τ′ be well-formed typing judgements. We say that Γ′, R′ ▷ e: τ′ is an instance of Γ, R ▷ e: τ if there is a substitution S such that ∀x ∈ Dom(Γ), Γ′(x) = Imp_{T_{x}}(S Γ(x)) for some set T_{x}, ∀l ∈ Dom(R), R′(l) = S R(l) , and τ′ = Imp_{T} (S τ) for some set T .

Lemma 6.2 If Γ′, R′ ▷ e: τ′ is an instance of Γ, R ▷ e: τ and ⊢ Γ, R ▷ e: τ , then ⊢ Γ′, R′ ▷ e: τ′.

Proof The proof proceeds by induction on the proof of Γ, R ▷ e: τ and case analysis on the last axiom or proof rule used. We describe the representative cases of (var) and (abs) . The latter case is particularly illustrative since it uses the restrictions on well-formed types and well-formed typing judgements. In each case, assume that Γ′, R′ ▷ e: τ′ is an instance of Γ, R ▷ e: τ via substitution S and sets T_{x}, for each x ∈ Dom(Γ) , and set T .

(var) The axiom has the form

Γ, R ▷ x: Imp_{T_{1}}(τ_{1})

with τ = Imp_{T_{1}}(τ_{1}) . Let Γ(x) = ∀α_{1} … α_{n}. ρ and let S_{1} be the substitution with domain {α_{1}, …, α_{n}} such that τ_{1} = S_{1} ρ. We need to find substitution S′ and variable-set T′, so that τ′ is the result of making the variables of T′ imperative in an instance of Γ′(x) via substitution S′. Let Γ′(x) = ∀β_{1} … β_{n}. ρ′. Consider the substitution S′ with domain {β_{1}, …, β_{n}} given by S′(β_{i}) = S(S_{1}(α_{i})) . Then, τ′ = Imp_{ITV(τ′)}(S′ Γ′(x)) and hence Γ′, R ▷ x: τ′ is a valid application of the (var) axiom.

(abs) The last step is of the form

\frac{Γ, x: τ_{1}, R ▷ e′: W (τ_{2})}{Γ, R ▷ λx. e′: τ_{1} → τ_{2}}

with τ = τ_{1} → τ_{2} . Consider Γ′′ = Γ′, x: Imp_{T} (S τ_{1}), τ′′ = W (Imp_{T} (S τ_{2})) . We prove that ⊢ Γ′′, R′ ▷ e′: τ′′, from which it follows using the (abs) rule that ⊢ Γ′, R′ ▷ λx. e′: τ′. We first see that Γ′′, R′ ▷ e′: τ′′ is a well-formed judgement. Since, τ′ = Imp_{T} (S τ_{1}) → Imp_{T} (S τ_{2}) is a well-formed type expression, we must have that τ′′ is a well-formed type expression. Now, suppose that α ∈ ITV(Γ′′, R′) ∩ FTV(τ′′) . If α ∈ ITV(Γ′, R′) then since Γ′, R′ ▷ e′: τ′ is a well-formed typing judgment we have that α ∈ ITV(Imp_{T} (S τ_{2})) and hence α ∈ ITV(τ′′) . And, if α ∈ ITV(Imp_{T} (S τ_{1})) then since τ′ is a well-formed type expression we get that α ∈ ITV(Imp_{T} (S τ_{2})) and hence α ∈ ITV(τ′′) . We next observe that τ′′ = Imp_{T} (S(W (τ_{2}))) , since for any substitution S, S(W (τ)) = W (S(τ)) if W (τ) is defined. Hence using substitution S, T_{x} = T , we can obtain Γ′′, R′ ▷ e′: τ′′ as an instance of Γ, x: τ_{1}, R ▷ e′: W (τ_{1}) which is therefore derivable by the induction hypothesis.

As corollaries of Lemma 6.2, we obtain statements describing the behaviour of derivable typejudgements under substitutions, and adding variables and locations to the context. In our type system adding assumptions to the context may have the effect of forcing some additional variables in the type of the expression to be imperative.

Corollary 6.3 (Type Substitution) Suppose ⊢ Γ, R ▷ e: τ . Let S be any substitution and T any set of type variables such that SΓ, SR▷e: Imp_{T} (S τ) is a well-formed typing judgement. Then, ⊢ SΓ, SR ▷ e: Imp_{T} (S τ) .

Corollary 6.4 (Adding Variables and Locations) Suppose ⊢ Γ, R▷e: τ . Let Γ′ ⊇ Γ, R′ ⊇ R. Then ⊢ Γ′, R′ ▷ e: Imp_{ITV(Γ′,R′)} τ .

Proof For any well-formed monotype τ and any set of type variables T , Imp_{T} (τ) is still a well-formed monotype.

We now establish a term-substitution property which is crucial to proving the subject reduction property for β -reduction and the reduction of let -expressions. The property we are interested in is Corollary 6.6 which is not provable directly by induction. We therefore prove a stronger statement in the following lemma. The statement of the lemma also provides formal justification for allowing type variables to be made imperative in the (var) rule.

Lemma 6.5 Assume that ⊢ Γ, x: ∀α_{1} … α_{n}.τ, R ▷ e: τ′ and {α_{1}, …, α_{n}} ∩ FTV(Γ, R) = ∅. If ⊢ Γ, R ▷ v: Imp_{ITV(Γ,R)} τ then ⊢ Γ, R ▷ [v/x]e: τ′.

Proof By induction on the proof of Γ, x: ∀α_{1} … α_{n}.τ, R ▷ e: τ′.

(var) e = x′. If x′ ≠ x then the lemma is trivially true. Otherwise, there is a substitution S with domain {α_{1}, …, α_{n}} such that τ′ = Imp_{T} (Sτ) . By the definition of well-formed typing judgements, we can assume that T ⊇ ITV(Γ, R) . Since {α_{1}, …, α_{n}} ∩ FTV(Γ, R) = ∅ we have that SΓ, SR = Γ, R. Thus, applying Lemma 6.2 to Γ, R ▷ v: Imp_{ITV(Γ,R)} τ , we can derive the judgment

Γ, R ▷ v: Imp_{T} (S(Imp_{ITV(Γ,R)} τ))

And, since T ⊇ ITV(Γ, R) , Imp_{T} (S(Imp_{ITV(Γ,R)} τ)) = τ′. Hence ⊢ Γ, R ▷ [v/x]x: τ′.

(abs) e = λx′. e_{1} . Then,

\frac{Γ, x: ∀α_{1} … α_{n}.τ, x′: τ_{1}, R ▷ e_{1}: W (τ_{2})}{Γ, x: ∀α_{1} … α_{n}.τ, R ▷ λx′. e_{1}: τ_{1} → τ_{2}}

Let {β_{1}, …, β_{n}} be distinct variables such that β_{i} ∉ FTV(Γ, R) ∪ {α_{1} …, α_{n}}. Let S be the substitution defined by S(α_{i}) = β_{i}^{0} , Γ′ = Γ, x′: Sτ_{1} . By the definition of well-formed typing judgements and the nature of S, all imperative variables of Γ′, x: ∀α_{1} …, α_{n}.τ, R can only appear imperatively in S(W (τ_{2})) . Hence, using Lemma 6.2, and substitution S on the premise of the (abs) rule, we can derive

Γ′, x: ∀α_{1} … α_{n}.τ, R ▷ e_{1}: S(W (τ_{2}))

since SΓ, SR = Γ, R. By the choice of S, {α_{1}, …, α_{n}} ∩ FTV(Γ′, R) = ∅. We have that ⊢ Γ, R ▷ v: τ′′, where τ′′ = Imp_{ITV(Γ,R)} τ . Using Corollary 6.4, ⊢ Γ′, R ▷ v: Imp_{ITV(Γ′,R)} τ′′. Since ITV(Γ′, R) ⊇ ITV(Γ, R) , we thus have that ⊢ Γ′, R ▷ v: Imp_{ITV(Γ′,R)} τ . Hence, by induction hypothesis, we can derive

Γ′, R ▷ [v/x]e_{1}: S(W (τ_{2}))

Let S′(β_{i}) = α_{i}^{0} . Using S′ with Corollary 6.4, we can derive

Γ′, x′: τ_{1}, R ▷ [v/x]e_{1}: W (τ_{2})

Now, using the (abs) rule, we can get the desired judgement.

The (loc), (const), (app) cases are trivially true, and the (let) case is similar to the (abs) case.

Corollary 6.6 (Term Substitution) If ⊢ Γ, x: ∀α_{1} … α_{n}.τ ▷ e: τ′ and ⊢ Γ ▷ v: τ with {α_{1}, …, α_{n}}∩ FTV (Γ) = ϕ then ⊢ Γ ▷ [v/x]e: τ′.

Proof We have that Γ, R ▷ v: τ is derivable. By the restriction on well-formed typing judgements, Imp_{ITV(Γ,R)} τ = τ . Hence, by Lemma 6.5, we have the desired result.

Using the above lemmas, we are now ready to connect the type system with the operational semantics. To establish the correspondence with the semantics, we need to assume some properties of the typings for the term constructors, since our proof system depends on them. The following definition states what we require of the typings for the term constructors.

Definition 6.7 The typing for term-constructors given by Typeof is admissible if the resulting proof system for deriving typing judgments has the following properties:

(i) For all values v ∈ V (i.e., other than λ -abstractions, ref, and location constants), if ⊢ ϕ, R ▷ v: τ for any store typing R, type τ , then τ is of the form b(τ_{1}, …, τ_{n}) for some type constructor b.

(ii) Let ⟨e_{1}, e_{2}⟩ ∈ F . For any R, τ , if ⊢ ϕ, R ▷ e_{1}: τ then ⊢ ϕ, R ▷ e_{2}: τ .

It is a consequence of (i) that the only functional values are λ -abstractions and ref , and the only values that are reference cells are location constants. (Indeed, we could have eliminated ref from being a value as well, by having the redex ref ⇝ λx. ref x). Condition (ii) requires the typings for term constructors to be consistent with their operational properties as given by their functional reductions. We assume in the following lemmas that the given typings for termconstructors is admissible.

Our operational semantics was described by defining the notions of redexes, evaluation contexts, and evaluation steps, in that order. The presentation of the lemmas for establishing the soundness of our type system follows the same order. First, we prove subject reduction for the purely functional reductions.

Lemma 6.8 (Subject Reduction for Functional Reductions) If ⊢ ϕ, R ▷ e_{1}: τ and e_{1} ⇝ e_{2} then ⊢ ϕ, R ▷ e_{2}: τ .

Proof By case analysis on e_{1} ⇝ e_{2} .

Case (λx. e) v ⇝ [v/x]e. Assume ⊢ ϕ, R ▷ (λx. e) v: τ . Then ⊢ ϕ, R ▷ λx. e: τ_{1} → τ_{2}, ⊢ ϕ, R ▷ v: τ_{1} and τ = W (τ_{2}) . From ⊢ ϕ, R ▷ λx. e: τ_{1} → τ_{2} , we have ⊢ x: τ_{1}, R ▷ e: W (τ_{2}) . Using Corollary

6.6 we get ⊢ ϕ, R ▷ [v/x]e: τ .

Case (let x = v in e) ⇝ [v/x]e. Assume ⊢ ϕ, R ▷ let x = v in e: τ . Then

⊢ ϕ, R ▷ v: τ_{1}, ⊢ x: Clos_{ϕ}τ_{1}, R ▷ e: τ

Since ϕ, R ▷ v: τ_{1} is a well-formed typing judgement, if α ∈ ATV(τ_{1}) then α ∉ FTV(R) . Hence, using Corollary 6.6 we get ⊢ ϕ, R ▷ [v/x]e: τ .

Case v_{1} v_{2} ⇝ wrong . Since v_{1} is not a λ -abstraction or ref, it must be a location constant or a value in V . The former can only have a type of the form τ′ ref and the latter can only have a type of the form b(τ_{1}, …, τ_{n}) by condition (i) of admissibility. Hence, ⊬ ϕ, Rv_{1}τ_{1} → τ_{2} for any R, τ_{1}, τ_{2} . Hence ⊬ ϕ, R ▷ v_{1} v_{2}: τ for any R, τ and the statement is true vacuously.

Otherwise e_{1} ⇝ e_{2} is a redex involving term-constructors and the statement is true by condition (ii) of admissibility.

We might expect a proof of soundness to proceed by extending Lemma 6.8 to establish subject reduction for evaluation. In more detail, suppose that (e, s) ⟼ (e′, s′) . We would like to establish that if e has type τ , then so does e′. Note that because of the possiblity of creation of reference cells, e′ may mention location constants that do not appear in e′. For this reason, the typing of e′ must involve assumptions about additional location constants. By our restriction on typing judgements, e′ can then have type τ only if the type variables in the types of the new location constants appearing in e′ all appear imperatively in τ . Unfortunately this condition on type variables may not be true, since there is nothing in our type system to force “new” type variables to be used whenever possible. As a result, an applicative type variable in τ could “accidentally” be the same as one in the type of a new reference cell created. However, as (iii) of the following lemma shows, such applicative variables in τ can be suitably renamed so that e′ can be given the renamed type. The form of the renaming is the crucial formal justification for allowing all applicative variables to be treated polymorphically in the (let) rule. It is also in the proof of (iii) that we see the formal origin of our restrictions on the syntactic form of types and typing judgements. Parts (i) and (ii) express obvious properties, but have been stated explicitly merely for ease of reference in the proof of Lemma 6.10.

Lemma 6.9 Let E[ ] be any evaluation context and suppose that ⊢ ϕ, R ▷ E[e]: τ . Then,

(i) ⊢ ϕ, R ▷ e: τ_{1} for some type τ_{1} .

(ii) If ⊢ ϕ, R ▷ e′: τ_{1} , then ⊢ ϕ, R ▷ E[e′]: τ .

(iii) Suppose that for some R′ ⊇ R and some expression e′, we have that ⊢ ϕ, R′ ▷ e′: τ_{1} . Let {α_{1}, …, α_{n}} = ATV(τ) . Then for some distinct variables β_{1}, …, β_{n} such that β_{i} ∉ FTV(R′) we have that ⊢ ϕ, R′ ▷ E[e′]: S_{E}τ where S_{E} = [β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}] .

Proof By induction on the structure of E[ ] . Statements (i) and (ii) can be proved trivially, so we only show details for (iii) . Note that for any distinct β_{1}, …, β_{n} such that β_{i} ∉ FTV(R′) we have that ϕ, R▷E[e′]: [β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}]τ is a well-formed judgement since ATV([β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}]τ) = {β_{1}, …, β_{n}}.

• E[ ] ≡ [ ] . Let {α_{1}, …, α_{n}} = ATV(τ_{1}) . Choose any β_{1}, …, β_{n} such that β_{i} ∉ FTV(R′) . Since ϕ, R′ ▷ e′: τ_{1} is a well-formed judgement and FTV(R′) = ITV(R′) we have that α_{i} ∉ FTV(R′) . Hence for S_{[ ]} = [β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}] , S_{[ ]}R′ = R′. Hence using Lemma 6.2, ⊢ ϕ, R′ ▷ e′: S_{[ ]}τ_{1} .

• E[ ] ≡ E_{1} e_{2} . Then we can derive

ϕ, R ▷ E_{1}[e]: τ′ → τ_{2}  (1)
ϕ, R ▷ e_{2}: τ′  (2)

and τ = W (τ_{2}) . Let {α_{1}, …, α_{n}} = ATV(τ) . Clearly ITV(τ_{2}) ⊆ ITV(τ) . Hence ATV(τ) ⊆ ATV(τ_{2}) ⊆ ATV(τ′ → τ_{2}) . Thus, ATV(τ′ → τ_{2}) = {α_{1}, …, α_{n}, α_{n+1}, …, α_{p}} for some variables α_{n+1}, …, α_{p}. By inductive hypothesis about E_{1}[ ] ,

⊢ ϕ, R′ ▷ E_{1}[e′]: S_{E_{1}}(τ′) → S_{E_{1}}(τ_{2})

where S_{E_{1}}(α_{i}) = β_{i}^{0}, 1 ≤ i ≤ p for some variables β_{1}, …, β_{n} such that β_{i} ∉ FTV(R′) . Since (1) is a well-formed judgement, Dom(S_{E_{1}}) ∩ FTV(R′) = ϕ. Hence S_{E_{1}}R = R. Note that ϕ, R′ ▷ e_{2}: S_{E_{1}}τ′ is a well-formed judgement since ATV(S_{E_{1}}τ′) ⊆ {β_{1}, …, β_{p}} and {β_{1}, …, β_{p}} ∩ FTV(R′) = ϕ. Hence using Lemma 6.2 on (2) with substitution S_{E_{1}} , we get that ⊢ ϕ, R′ ▷ e_{2}: S_{E_{1}}τ′. Thus using (app) , ⊢ ϕ, R′ ▷ E[e′]: S_{E_{1}}(W (τ_{2})) , i.e.,

⊢ ϕ, R′ ▷ E[e′]: S_{E_{1}}(W (τ_{2}))  (3)

since W (S_{E_{1}}τ_{2}) = S_{E_{1}}(W (τ_{2})) , as W τ_{2} is defined. Let S′ = [α_{n+1}^{0}/β_{n+1}, …, α_{p}^{0}/β_{p}] . Take S_{E} = S′ ∘ S_{E_{1}} . Since Dom(S′) ∩ R′ = ϕ, using substitution S′ and Corollary 6.3 on (3) we get ⊢ ϕ, R′ ▷ E[e′]: S_{E}(τ) .

• E[ ] ≡ v E_{1} . Then we can derive

\begin{matrix}ϕ, R ▷ v: τ′ → τ_{2} \\ ϕ, R ▷ E_{1}[e]: τ′ \end{matrix}

and τ = W (τ_{2}) . Let ATV(τ′) = {α_{1}, …, α_{n}}. By inductive hypothesis about E_{1} , we have variables β_{1}, …, β_{n} ∉ FTV(R′) such that

ϕ, R′ ▷ E_{1}[e′]: S_{E_{1}}(τ′)

with S_{E_{1}} = [β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}] . Since ATV(τ′) ⊆ ATV(τ′ → τ_{2}) , we have ATV(τ′ → τ_{2}) = {α_{1}, …, α_{n}, α_{n+1}, …, α_{p}} for some variables α_{n+1}, …, α_{p}. Choose any distinct variables β_{n+1}, …, β_{p} such that β_{j} ∉ FTV(R′), n + 1 ≤ j ≤ p. Consider S′ = [β_{1}^{0}/α_{1}, …, β_{p}^{0}/α_{p}] . We claim that S′τ′ = S_{E_{1}}τ′. For consider any α ∈ FTV(τ′) . If α ∈ ATV(τ′) then clearly S′(α) = S_{E_{1}}(α) . Otherwise α ∈ ITV(τ′) whence α ∈ ATV(τ_{2}) by out restriction on the well-formed type τ′ → τ_{2} . This is the formal origin of our restriction on well-formed types. Hence α ∈ Dom(S′) and S′(α) = S_{E_{1}}(α) . Then we use similar reasoning as in the previous case.

• E[ ] ≡ let x = E_{1} in e_{2} . Then we can derive

ϕ, R ▷ E_{1}[e]: τ′  (4)
x: Clos_{ϕ}τ′, R ▷ e_{2}: τ  (5)

By induction hypothesis,

⊢ ϕ, R′ ▷ E_{1}[e′]: S_{E_{1}}τ′  (6)

for some suitable S_{E_{1}} . By the form of substitution S_{E_{1}} , Clos_{ϕ}τ_{1} = Clos_{ϕ}S_{E_{1}}(τ_{1}) , which was precisely the purpose of the inductive statement in (iii). Let {α_{1}, …, α_{n}} = ATV(τ) . Choose any distinct β_{1}, …, β_{n} such that β_{i} ∉ FTV(R′) ∪ ITV(τ′) . Let S_{E} = [β_{1}^{0}/α_{1}, …, β_{n}^{0}/α_{n}] . Then clearly

x: Clos_{ϕ}τ_{1}, R′ ▷ e_{2}: S_{E}τ

is a well-formed judgement. Also since FTV(Clos_{ϕ}τ_{1}) = ITV(Clos_{ϕ}τ_{1}) and since (5) is a wellformed judgement, α_{i} ∉ FTV(Clos_{ϕ}τ_{1}) . Thus using Lemma 6.2 on (5) with substitution S_{E} we have

⊢ x: Clos_{ϕ}(S_{E_{1}}τ′), R′ ▷ e_{2}: S_{E}τ

Combining with (6),

⊢ ϕ, R′ ▷ E[e′]: S_{E}τ

Other cases of evaluation contexts are similar.

Under suitable assumptions about the store in which an expression is evaluated, we can now establish that evaluation of typable expressions leads to typable expressions.

Lemma 6.10 (Preservation of Typability) Suppose (e, s) ⟼ (e′, s′) and R is a store typing such that s: R and ⊢ ϕ, R ▷ e: τ . Then there is a store typing R′ such that s′: R′ and for some type τ′, ⊢ ϕ, R′ ▷ e′: τ′.

Proof By case analysis on ⟼.

• (E[e], s) ⟼ (E[e′], s) with e ⇝ e′. Assume that ⊢ ϕ, R ▷ E[e]: τ . From Lemma 6.9(i), we have that ⊢ ϕ, R ▷ e: τ_{1} for some type τ_{1} . By Lemma 6.8, ⊢ ϕ, R ▷ e′: τ_{1} . Now, using Lemma 6.9(ii), ⊢ ϕ, R ▷ E[e′]: τ . And, by assumption s: R.

• (E[ref v], s) ⟼ (E[l], s[l ↦ v]) .

By Lemma 6.9(i), ⊢ ϕ, R ▷ ref v: τ_{1} for some type τ_{1} . Hence ⊢ ϕ, R ▷ v: τ′_{1} and τ_{1} = W (Set_{1}(τ′_{1})) ref . Consider R′ = R, l: Set_{0}(τ′_{1}) . For l′ ≠ l, since ⊢ ϕ, R ▷ s(l′): R(l′) and R(l′) is imperative, we have by Corollary 6.4, ⊢ ϕ, R′ ▷ s(l′): R(l′) , i.e., ⊢ ϕ, R′ ▷ s′(l′): R′(l′) where s′ = s[l ↦ v] . And, since ⊢ ϕ, R ▷ v: τ′_{1} , by Corollary 6.4, ⊢ ϕ, R′ ▷ v: Imp_{ITV(R′)}τ′_{1} . Clearly, Imp_{ITV(R′)}τ′_{1} = Set_{0}(τ′_{1}) . Hence, ⊢ ϕ, R′ ▷ s′(l): R′(l) and thus s′: R′. Trivially, ⊢ ϕ, R′ ▷ l: τ_{1} , since W (Set_{1}(τ_{1})′) = Set_{0}(τ′_{1}) . Thus, by Lemma 6.9(iii), ⊢ ϕ, R′ ▷ E[l]: τ′ for τ′ = S_{E}(τ) .

• (E[!l], s) ⟼ (E[s(l)], s) . By Lemma 6.9(i), ⊢ ϕ, R▷!l: τ_{1} . Hence, ⊢ ϕ, R ▷ l: τ_{1} ref , i.e., R(l) = τ_{1} . Since s: R, we have that ⊢ ϕ, R ▷ s(l): R(l) , i.e., ⊢ ϕ, R ▷ s(l): τ_{1} . Now, using Lemma 6.9(ii), we get that ⊢ ϕ, R ▷ E[s(l)]: τ .

• (E[l : = v], s) ⟼ (E[v], s[l ↦ v]) . Then ⊢ ϕ, R ▷ l: τ_{1} ref , ⊢ ϕ, R ▷ v: τ_{1} . Hence s[l ↦ v]: R. And since ⊢ ϕ, R ▷ v: τ_{1} , by Lemma 6.9(ii), ⊢ ϕ, R ▷ E[v]: τ_{1} .

• (E[e], s) ⟼ (wrong, s) , where e ⇝ wrong . By Lemma 6.8, since wrong is not typeable, there is no R, τ_{1} such that ⊢ ϕ, R ▷ e: τ_{1} . By Lemma 6.9(i), this implies that ∄R, τ such that ⊢ ϕ, R ▷ E[e]: τ and the Lemma is thus true vacuously.

• (E[!v], s) ↦ (wrong, s) , where v ∉ Loc. By admissibility condition (i) and the (abs) rule, ⊬ ϕ, R ▷ v: τ_{1} ref for any R, τ_{1} . Hence ⊬ ▷ ▷ ϕ: , R: !vτ_{1} for any R, τ_{1} . Then similar to previous case.

• (E[v_{1} : = v_{2}], s) ⟼ (wrong, s) , where v_{1} ∉ Loc. This is similar to previous case.

As a corollary of Lemma 6.10, we can now establish that starting in the initial store, evaluation of any typable user program leads to typable expressions.

Corollary 6.11 Let e be a program, i.e., a closed expression with no location constants. If e is typeable, i.e., ⊢ ϕ, ϕ ▷ e: τ for some type τ then for any e′, s′ such that (e, init) ⟼ (e′, s′) we have that e′ is typeable.

Proof The store init has the empty store typing, i.e., init: ϕ. Now the statement follows from Lemma 6.10.

Finally, we can establish our main theorem, that well-typed programs do not lead to run-time errors.

Theorem 6.12 Let e be a typeable program. Then Eval(e) ≠ wrong , i.e., e does not lead to a run-time error.

Proof There is no R′, τ′ such that ⊢ ϕ, R′ ▷ wrong: τ′. Hence, by Corollary 6.11 we cannot have (e, init) ⟼ (wrong, s′) , for any store s′.

7 Conclusion

We present a type system, in the form of typing rules , using weak type variables. Intuitively, a weak type variable is a variable with a numeric index, indicating the number of function applications needed to produce a reference cell containing a value of this type. Although the Standard ML of New Jersey source code is sufficiently complex to make direct proof difficult, extensive experiments with the compiler and examination of the source code suggest that our type system strictly subsumes the implemented type system. Moreover, as noted in Section 5, our type system is sufficiently flexible to give all benchmark examples listed in [LW91] the correct type, without the more complicated type expressions used in [LW91, TJ92, Wri92]. In light of the comments on the limitations of SML-NJ in [LW91] and elsewhere, our type system shows that simple indexed type variables allow more flexible typing of imperative programs than previously believed. To the extent that our type system subsumes the implemented algorithm, Theorem 6.12 shows not only the semantic soundness of our typing rules, but also the soundness of the SML-NJ algorithm that has been used for several years. Since our type system is more flexible than the one used in the SML-NJ, but requires very little or no change in displayed type expressions, we believe it is a good candidate for later implementations of ML and other polymorphic programming languages that have imperative or control constructs.

References

[AM87] A.W. Appel and D.B. MacQueen. A Standard ML compiler. In Functional Programming Languages and Computer Architecture, pages 301–324. Springer LNCS 274, 1987.

[AM91] A.W. Appel and D.B. MacQueen. Standard ML of New Jersey. In Int’l Symp. Prog. Lang. Implementation and Logic, pages 1–13. Springer-Verlag, 1991.

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

[Dam85] L. Damas. Type assignment in programming languages. PhD thesis, Edinburgh University CST-33-85, 1985.

[Hin69] J.R. Hindley. The principal type-scheme of an object in combinatory logic. Trans. AMS, 146:29–60, 1969.

[HL91] R. Harper and M. Lillibridge. A bug in sml polymorphic typing for continuations. Email

         to types@theory.lcs.mit.edu, 1991.

[JG91] P. Jouvelot and D. Gifford. Algebraic reconstruction of types and effects. In 18th ACM Symposium on Principles of Programming Languages, pages 303–310, 1991.

[KMM91] P.C. Kanellakis, H.G. Mairson, and J.C. Mitchell. Unification and ML type reconstruction. In Computational Logic, Essays in Honor of Alan Robinson, pages 444–478. MIT Press, 1991.

[Koe92] A. Koenig. An anecdote about ml type inference. Unpublished Manuscript, 1992.

[KTU90] A.J. Kfoury, J. Tiuryn, and P. Urzyczyn. ML typability is Dexptime-complete. In Proc. 15th Colloq. on Trees in Algebra and Programming, pages 206–220. Springer LNCS 431, 1990. To appear in J. Assoc. Comput. Machinery under title, ”An Analysis of ML Typability”.

[LW91] X. Leroy and P. Weis. Polymorphis type inference and assignment. In 18th ACM Symposium on Principles of Programming Languages, pages 291–302, 1991.

[Mil78] R. Milner. A theory of type polymorphism in programming. JCSS, 17:348–375, 1978.

[TJ92] J.-P. Talpin and P. Jouvelot. The type and effects discipline. In Proc. IEEE Symp. on Logic in Computer Science, pages 162–173, 1992.

[Tof88] M. Tofte. Operational Semantics and Polymorphic Type Inference. PhD thesis, Edinburgh University, 1988. Available as Edinburgh University Laboratory for Foundations of Computer Science Technical Report ECS–LFCS–88–54.

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

[WF92] A.K. Wright and M. Felleisen. A syntactic approach to type soundness. Technical Report TR91-160, Rice University, 1992.

[Wri92] A.K. Wright. Typing references by effect inference. In Proceedings of the European Symposium on Programming, 1992.