Xavier Leroy
email: xavier.leroy@inria.fr.

Unboxed objects and polymorphic typing

This paper presents a program transformation that allows languages with polymorphic typing (e.g. ML) to be implemented with unboxed, multi-word data representations, more efficient than the conventional boxed representations. The transformation introduces coercions between various representations, based on a typing derivation. A prototype ML compiler utilizing this transformation demonstrates important speedups.

Introduction

It is common saying that statically-typed programs can be compiled more efficiently than dynamically-typed programs. A number of run-time type tests become unnecessary, for instance. In this paper, we study some compilation techniques that rely on the availability of typing information at compile-time. These techniques are connected to the data representation problem: how high-level objects manipulated by the language are mapped onto machine-level objects.

Static typing and data representation

There are many ways in which knowing type information at compile-time can help in selecting better representations for data. First of all, a compiler needs to know the size (required amount of memory) of all objects manipulated by the program, in order to allocate enough space for variable values and intermediate results, and to move the right number of bits from one location to another when performing bindings or assignments. Without static typing, a default size (usually one word) must be assumed for all objects in the program, and all representations must fit in this size. Objects that do not fit naturally in one word, such as records and 64bit floating-point numbers, have to be boxed (allocated in the heap and handled through a pointer). With static typing, objects belonging to different types can have different sizes, as long as all objects of the same type have the same size. The compiler infers the size of an object from its type, and therefore knows how to allocate a variable of that type, or move a value of that type. This makes it possible to have unallocated objects larger than one word: unallocated 64-bit floating-point numbers, and unallocated records, in particular. The former are crucial for numerical-intensive programs. The latter are crucial for languages based on the λ-calculus, such as ML, where functions have only one argument and one result, and functions with several arguments or several results are encoded as functions taking or returning records.

A compiler may also use static typing information to indicate which register class is best suited for a given object. Most architectures distinguish floating-point registers from general-purpose registers; floating-point operations can only be performed between floating-point registers. When an object is statically known to have type float, it is possible to keep this object in a floatingpoint register, instead of a general-purpose register, so that computation on this object will not require register moves. The typical example of this type-based targeting is the use of different calling conventions for functions of different types: a function with result type float can be compiled to return its result in a given floatingpoint register, ready to be used by the caller; a function that returns an object of type int will use a given integer register instead. Static typing guarantees that the caller and the callee agree on the types of the arguments and the results, and therefore on their locations.

The problem with polymorphism

Type-directed compilation, as exemplified above, requires that each object manipulated by the program have one, unique, statically-known type. This holds with simple, monomorphic type systems such as Pascal. But this is not the case with more advanced type systems, notably those providing type abstraction or polymorphism [START_REF] Cardelli | On understanding types, data abstraction, and polymorphism[END_REF]. With type abstraction, the concrete type of an object can remain unknown at compile-time.

With polymorphism, an object can belong to several different types at the same time; again, its actual type is not available at compile-time. This paper focuses on polymorphism, and, more specifically, on the polymorphic type discipline of the ML language [START_REF] Milner | The definition of Standard ML[END_REF]. For instance, the ML identity function function x → x belongs to type α → α for all type expressions α. This type allows the function to be applied to objects of any type. Therefore, when compiling this function, we know neither the size of the argument nor the correct calling convention.

Several solutions to this issue have been considered. (See [START_REF] Morrison | An ad hoc approach to the implementation of polymorphism[END_REF] for a survey.) The first one is to defer the compilation of a polymorphic object until it is actually used. At that time, we can compile a version of this object specialized to the type it is used with. This technique is often used for generics in Ada. It supports efficient data representations, but results in code duplication and loss of separate compilation.

A simpler solution is to assume a default size, common to all objects, and default calling conventions, common to all functions, just as if the language was not statically typed. Most existing ML implementations have taken this approach: they use one-word representations and uniform calling conventions 1 [6, 9, 4, 3]. This approach solves the problem of polymorphism, but results in a serious loss of efficiency. For instance, tuples are always heap-allocated, making passing several arguments to a function quite expensive. This efficiency loss is unfortunate, especially when large parts of a program are monomorphic (types are known at compile-time), as it is the case with most realistic ML programs.

Mixed representations

In this paper, we propose an alternate solution, mixed data representations, that relies on using different representations, boxed as well as unboxed, for the same high-level object, depending on the amount of type information available at compile-time. This solution is both efficient (monomorphic pieces of code are compiled with optimal data representations) and practical (polymorphic functions are compiled once and for all). It relies on introducing coercions between various data representations, based on a typing derivation for the program. Some recent papers also consider mixing boxed and unboxed representations in the implementation of MLlike languages. Peyton-Jones [START_REF] Peyton-Jones | Unboxed values as first-class citizens[END_REF] expresses many optimizations on boxing and unboxing as source-to-source transformations in this setting. To cope with polymor-phism, a simple typing restriction is proposed: type variables in a polymorphic type can only be instantiated by "boxed" types (types whose values are boxed). The work presented here is complementary: our program transformation can be viewed as a translation from ML (unrestricted polymorphism) into Peyton-Jones' language (restricted polymorphism).

Morrison et al. have also used coercions between uniform and specialized representations in the implementation of their Napier88 language [START_REF] Morrison | An ad hoc approach to the implementation of polymorphism[END_REF]. The coercion mechanism we use is similar to theirs, but offers one distinct advantage: whereas coercions in Napier88 involve interpreting type tags at run-time, ours may be entirely compiled, eliminating type information passing at run-time. We also provide a more formal framework to reason about coercion-based compilation techniques, and prove their correctness.

The remainder of this paper is organized as follows: section 2 informally explains mixed data representations and demonstrates the use of coercions. Section 3 formalizes these ideas, as a translation from the core ML language to the core ML language with restricted polymorphism and explicit coercions. We prove that the translation preserves the type and the semantics of the original program. Section 4 shows how the results above extend to concrete data types. Section 5 reports on an implementation of this technique in the Gallium highperformance ML compiler. We give a few concluding remarks in section 6.

Presentation

The approach taken in this paper is to mix two styles of data representation: specialized representations (multiword objects and special calling conventions) when the static types are monomorphic; and uniform representations (one-word objects and default calling conventions) when the static types are polymorphic. Coercions between the two representation styles are performed when a polymorphic object is used with a more specific type. In the case of a polymorphic function, for instance, coercions take place just before the function call and just after the function return.

Polymorphic terms are compiled with the assumption that all terms whose static type is a type variable will be represented at run-time with a uniform representation. Hence the compiler knows their size (one word) and their calling protocol (the default one). Consider the following polymorphic function:

let make pair = λx. (x, x)
Its type is ∀α. α → α × α. Since x has static type α (a type variable), the compiler assumes the value of x fits in one word, and is passed in the default location: typically the first integer register. The returned value has static type α × α. The compiler knows it is a pair, hence it produces code that returns an unallocated pair of one-word, uniformly represented values in the first two integer registers.

Consider now the application make pair (3.14). Here, function make pair is used with the more specific type float → float × float. The compiled code for this application evaluates the argument 3.14 with the specialized representation for objects of type float: an unallocated, two-word floating-point number in a floatingpoint register. Similarly, we expect as a result two unallocated floating-point numbers in two floating-point registers. These choices are not compatible with the hypotheses made when compiling make pair. Therefore, it is not possible to call the code for function make pair directly. The argument 3.14 must be first coerced to the uniform representation for floating-point numbers: the number is boxed, and a pointer to the box is passed to function make pair. The value returned, an unallocated pair of two boxed floating-point numbers, must be coerced back to the specialized representation for pairs of floating-point numbers, by unboxing the two components of the pair.

To express this translation more formally, we introduce two operators: wrap(τ ), the coercion from the specialized representation for objects of type τ to the uniform representation; and unwrap(τ ), the reverse coercion, from the uniform representation to the specialized representation. Often, wrap(τ ) will be implemented by boxing, and unwrap(τ ) by unboxing. Better implementations can be considered for certain types τ , however; hence we stick to the more general terminology wrapunwrap. We will often say that an object is "in the wrapped state", or "in the unwrapped state", to indicate how it is represented. With this notation, the compilation of make pair(3.14) can be expressed as a translation to an expression with explicit coercions: let x = make pair(wrap(float) (3.14)) in (unwrap(float)(fst(x)), unwrap(float)(snd(x)))

followed by a conventional Pascal-like compilation that infers size and calling convention informations from the types.

The next example involves higher-order functions: The important point is that higher-order functions may require their functional arguments to be transformed to accommodate uniform representations instead of specialized representations. This transformation does not require recompilation of the functional, nor of the functional argument. It suffices to put some "stub code" around the functional argument, to perform the required coercions.

let map pair = λf. λx. (f(fst(x)), f(snd(x))) in

Formalization

In this section, we formally define the translation outlined above, in the context of the core ML language. We show that the translated program, evaluated with specialized data representations, computes the same thing as the original program, evaluated with uniform data representations.

The languages

The source language is the core ML language: λ-calculus with constants and the let construct. The only data structures are pairs. The target language is core ML extended with the two constructs wrap(τ ) and unwrap(τ ). The syntax for source terms (ranged over by a), target terms (a ), type expressions (τ ), and type schemes (σ) is as follows:

a ::= i | f | x | λx. a | let x = a 1 in a 2 | a 1 (a 2 ) | (a 1 , a 2 ) | fst(a) | snd(a) a ::= i | f | x | λx. a | let x = a 1 in a 2 | a 1 (a 2 ) | (a 1 , a 2 ) | fst(a ) | snd(a ) | wrap(τ )(a ) | unwrap(τ )(a ) τ ::= α | int | float | τ 1 → τ 2 | τ 1 × τ 2 σ ::= ∀α 1 . . . α n . τ
Here and elsewhere, we write x for an identifier, i for an integer constant, f for a floating-point constant, and α for a type variable. Primitives are presented as predefined identifiers such as add float.

To the source language we apply Milner's type discipline [START_REF] Damas | Principal type-schemes for functional programs[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF]. We recall the typing rules below. They define the familiar predicate E a : τ ("under assumptions E, term a has type τ "). Here, E is a finite mapping from identifiers x to type schemes σ.

E(x) = ∀α 1 . . . α n . τ Dom(ρ) ⊆ {α 1 . . . α n } E x : ρ(τ ) E i : int E f : float E + x : τ 1 a : τ 2 E λx. a : τ 1 → τ 2 E a 2 : τ 1 → τ 2 E a 1 : τ 1 E a 2 (a 1 ) : τ 2 E a 1 : τ 1 E a 2 : τ 2 E (a 1 , a 2 ) : τ 1 × τ 2 E a : τ 1 × τ 2 E fst(a) : τ 1 E a : τ 1 × τ 2 ⇒ a E snd(a) : τ 2 E a 1 : τ 1 E + x : Gen(τ 1 , E) a 2 : τ 2 E let x = a 1 in a 2 : τ 2
In the last rule above, we write Gen(τ, E) for the type scheme generalizing τ in environment E. It is defined by

Gen(τ, E) = ∀α 1 . . . α n . τ
where α 1 . . . α n are the type variables free in τ but not in E.

The translation

The translation of a term from the source language to the target language is based on the types given to the term and to its subterms. More precisely, we define the translation on a typing derivation for the given term. (In an actual compiler, this derivation would be the principal typing derivation for the term.) The translation is presented as the predicate E a : τ ⇒ a , where E a : τ is the typing predicate defined above, and the fourth component a (a term of the target calculus) is the translation for a. This proposition is defined by a set of inference rules, with the same structure as the typing rules. The rules are given in figure 1.

Most rules propagate the translated terms in the obvious way. The hard work is performed by the S ρ function (ρ is a substitution of types for type variables) in the rule for variable specialization. Given a target term a represented according to type τ , function S ρ is responsible for inserting the right wrap and unwrap coercions to transform it into a term represented according to type ρ(τ ). The S transformation is defined as follows:

S ρ (a : α) = unwrap(ρ(α))(a ) S ρ (a : int) = a S ρ (a : float) = a S ρ (a : τ 1 × τ 2 ) = let x = a in (S ρ (fst(x) : τ 1 ), S ρ (snd(x) : τ 2 )) S ρ (a : τ 1 → τ 2 ) = λx. S ρ (a (G ρ (x : τ 1 )) : τ 2 )
where x is not free in a

We also need to define the dual transformation G:

G ρ (a : α) = wrap(ρ(α))(a ) G ρ (a : int) = a G ρ (a : float) = a G ρ (a : τ 1 × τ 2 ) = let x = a in (G ρ (fst(x) : τ 1 ), G ρ (snd(x) : τ 2 )) G ρ (a : τ 1 → τ 2 ) = λx. G ρ (a (S ρ (x : τ 1 )) : τ 2 )
where x is not free in a

The term a given to the S transformation has been compiled assuming uniform representations for all data of static type α, for each type variable α. When a is considered with type ρ(τ ), the context expects these data of static type α to have the same (specialized) representations as data of static type ρ(α). Therefore, the goal of transformation S is to locate all data of static type α in term a , and apply the unwrap(ρ(α)) coercion to them.

The transformation proceeds recursively over τ , the principal type for a . When τ is a type variable α, it simply applies unwrap(ρ(α)) to a . When τ is an atomic type nothing needs to be done, since ρ(τ ) = τ . When τ is a product type τ 1 × τ 2 , the two components of a , fst(a ) and snd(a ), are recursively transformed, and the two results are paired together. Finally, when τ is a function type τ 1 →τ 2 , the transformation returns a function that translates its argument y with type τ 1 , applies a to it, and translates the result with type τ 2 . The processing of the argument requires a different transformation, G, instead of S, because of the contravariance of the arrow type constructor. In other words, the translated function S ρ (a : τ 1 → τ 2 ) should be applicable to data of type ρ(τ 1 ), using the specialized representation for components of type α; before applying a to it, it is necessary to switch to uniform representation for these components. This is performed by the dual transformation G, defined exactly as S, except that in case τ = α, the coercion wrap(ρ(α)) is used instead of unwrap(ρ(α)).

Working out the example make pair(3.14) above, we get the following derivation, where E is the typing environment make pair ← ∀α. α → α × α and ρ is the sub-

E(x) = ∀α 1 . . . α n . τ Dom(ρ) ⊆ {α 1 . . . α n } E x : ρ(τ ) ⇒ S ρ (x : τ ) E i : int ⇒ i E f : float ⇒ f E + x : τ 1 a : τ 2 ⇒ a E λx. a : τ 1 → τ 2 ⇒ λx. a E a 2 : τ 1 → τ 2 ⇒ a 2 E a 1 : τ 1 ⇒ a 1 E a 2 (a 1 ) : τ 2 ⇒ a 2 (a 1 ) E a 1 : τ 1 ⇒ a 1 E + x : Gen(τ 1 , E) a 2 : τ 2 ⇒ a 2 E let x = a 1 in a 2 : τ 2 ⇒ let x = a 1 in a 2 E a 1 : τ 1 ⇒ a 1 E a 2 : τ 2 ⇒ a 2 E (a 1 , a 2 ) : τ 1 × τ 2 ⇒ (a 1 , a 2 ) E a : τ 1 × τ 2 ⇒ a E fst(a) : τ 1 ⇒ fst(a ) E a : τ 1 × τ 2 ⇒ a E snd(a) : τ 2 ⇒ snd(a )
Figure 1: The translation rules stitution α ← float.

E make pair : float → float × float ⇒ S ρ (make pair : α → α × α) E 3.14 : float ⇒ 3.14 E make pair(3.14) : float × float ⇒ S ρ (make pair : α → α × α)(3.14)
By definition of S, we have:

S ρ (make pair : α → α × α) = λx. S ρ (make pair(G ρ (x : float)) : float × float) = λx. let y = make pair(wrap(float)(x)) in (unwrap(float)(fst(y)), unwrap(float)(snd(y)))
After performing the β-reduction x = 3.14 at compiletime, we get the intuitive translation given in section 2.

The translation often introduces many redexes that can be reduced at compile-time.

Type correctness of the translation

In this section, we show that the translation defined above does not introduce type errors: the resulting target term is well-typed. The target language is equipped with a variant of the type system for the source language. (We write for the typing judgements of the target language, instead of .) There are two differences. The first one is the explicit mention of wrapping and unwrapping at the level of types: we introduce a new kind of type expression, [τ ], that represents the type of all wrapped values of type τ . Conversely, other kinds of type expressions, such as float or τ 1 × τ 2 , now stand for unwrapped values of these types. We write τ for the extended type expressions:

τ ::= α | int | float | τ 1 → τ 2 | τ 1 × τ 2 | [τ ]
Then, the typing rules for the wrap and unwrap constructs are, obviously:

E a : τ E wrap(τ )(a ) : [τ ] E a : [τ ] E unwrap(τ )(a ) : τ
The second difference is the restriction of polymorphism. In the source language, a type variable α universally quantified in a type scheme can be substituted by any type expression. In the target language, we only allow substitution by a "wrapped type", that is, a type of the form [τ ]. This restriction reflects the fact that, at compile-time, objects whose type is a type variable are assumed to be in the wrapped state. If type variables can only be instantiated by wrapped types, then the assumption above holds for all well-typed target terms. To implement this restriction on polymorphism, we change the typing rule for variables to:

E (x) = ∀α 1 . . . α n . τ Dom(ρ) ⊆ {α 1 . . . α n } E x : [ρ](τ )
Here, the substitution [ρ] is the substitution defined by [ρ](α) = [ρ(α)] for all α ∈ Dom(ρ). Any substitution of wrapped types for type variables has the the form [ρ] for some ρ.

We can now state the correctness of the translation with respect to the type systems.

Proposition 1 If E a : τ ⇒ a , then E a : τ .
Proof: the proof requires the following lemma.

Lemma 1 1. If E a : [ρ](τ ), then E S ρ (a : τ ) : ρ(τ ). 2. If E a : ρ(τ ), then E G ρ (a : τ ) : [ρ](τ ).
Proof: by induction over τ . In case τ = α, (1) is the typing rule for unwrap, and (2) is the typing rule for wrap.

2

Proposition 1 follows from a simple inductive argument on the translation derivation. The only interesting case is a = x. Then, the translation is:

E(x) = ∀α 1 . . . α n . τ Dom(ρ) ⊆ {α 1 . . . α n } E x : ρ(τ ) ⇒ S ρ (x : τ )
In the type system for the target language, we have E x : [ρ](τ ). By case 1 of lemma 1, we conclude that E S ρ (x : τ ) : ρ(τ ), as expected. 2

Operational semantics

In this section, we give operational semantics for the source language and for the target language, in preparation for a proof of the semantic correctness of the translation. We define two evaluation predicates, mapping terms to values, in the style of [START_REF] Milner | The definition of Standard ML[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF]. The syntax for values is: To be more specific, we assume the following typical size assignment:

v ::= i | f | v | v 1 , v 2 | clos(k,
i = 1 f = 2 v = 1 op = 2 v 1 , v 2 = v 1 + v 2 clos(k, λx. a, e) = 2.
(We consider closures as two pointers, one to the code part, one to the environment part). We also associate a size to type expressions accordingly:

int = 1 float = 2 τ 1 → τ 2 = 2 τ 1 × τ 2 = τ 1 + τ 2 [τ ] = 1 α = 1.
The semantics are given in figure 2. The semantics for the source language uses uniform data representations: all terms are mapped onto values of size one. For instance, the floating-point number f is represented as f ; the pair of two terms, the first evaluating to v 1 , the other to v 2 , is represented as v 1 , v 2 ; and closures are boxed, too.

For the target language, we use specialized representations: floating-point numbers, pairs, and closures are left unallocated. Notice the appearance of a new kind of run-time type errors: applying a closure to a value of the wrong size. Coercions wrap(τ ) and unwrap(τ ) are implemented as boxing and unboxing for types of size greater than one, and as no-ops for types of size one.

Semantic correctness of the translation

In this section, we show that the translation preserves semantics: the translated program (evaluated with mixed representations) computes the same thing as the original program (evaluated with uniform representations).

There is a slight difficulty here: the semantics may assign different values to the two programs, because one object may have different representations in the two semantics. For instance, in the case of a term with type float, the translation is correct if and only if whenever the term evaluates to f , then its translation evaluates to f .

Hence we need to define a notion of equivalence between two values, one corresponding to uniform representations, the other corresponding to mixed representations. Actually, the equivalence is defined between typed values (value-type pairs). We write it Γ |= v : τ ≈ v : τ . Types are needed here to correctly interpret the values, and to ensure the well-foundedness of the definition.

The environment Γ provides an interpretation for type variables in τ and τ . Legal interpretations for type variables are non-empty sets V of pairs of values, such that for all (v, v ) ∈ V, we have v = 1. This restriction over the size of v captures the fact that whenever values are considered with type α, they must use default representations.

The definition of the semantic equivalence is modeled after the "semantic typing" relations used in some proofs of soundness for type systems [START_REF] Tofte | Type inference for polymorphic references[END_REF]. The equivalence relation extends to type schemes, and to environments: We can now state the semantic correctness of the translation:

• Γ |= v : α ≈ v : α iff (v, v ) ∈ Γ(α) • Γ |= i : int ≈ i : int • Γ |= f : float ≈ f : float • Γ |= v : τ ≈ v : [τ ], where τ = 1, iff Γ |= v : τ ≈ v : τ • Γ |= v : τ ≈ v : [τ ], where τ > 1, iff Γ |= v : τ ≈ v : τ • Γ |= v 1 , v 2 : τ 1 × τ 2 ≈ v 1 , v 2 : τ 1 × τ 2 iff Γ |= v 1 : τ 1 ≈ v 1 : τ 1 and Γ |= v 2 : τ 2 ≈ v 2 : τ 2 • Γ |= clos(1, λx.a, e) : τ 1 → τ 2 ≈ clos(k, λx .a , e ) : τ 1 → τ 2 iff τ 1 = k, and for all values v 1 , v 2 , v 1 such that Γ |= v 1 : τ 1 ≈ v 1 : τ 1 and e+x←v 1 a u → v 2 , there exists a value v 2 such that e + x ← v 1 a m → v 2 and Γ |= v 2 : τ 2 ≈ v 2 : τ 2 .
→ v 1 e 0 + x ← v 1 a 0 u → v 0 e a 2 (a 1 ) u → v 0 e a 1 u → v 1 e + x ← v 1 a 2 u → v 2 e let x = a 1 in a 2 u → v 2 e a 2 u → add e a 1 u → f 1 , f 2 f 1 + f 2 = f e a 2 (a 1 ) u → f e a 1 u → v 1 e a 2 u → v 2 e (a 1 , a 2 ) u → v 1 , v 2 e a u → v 1 , v 2 e fst(a) u → v 1 e a u → v 1 , v 2
→ v 1 v 1 = k e 0 + x ← v 1 a 0 m → v 0 e a 2 (a 1 ) m → v 0 e a 1 m → v 1 e + x ← v 1 a 2 m → v 2 e let x = a 1 in a 2 m → v 2 e a 2 m → add e a 1 m → f 1 , f 2 f 1 + f 2 = f e a 2 (a 1 ) m → f e a 1 m → v 1 e a 2 m → v 2 e (a 1 , a 2 ) m → v 1 , v 2 e a m → v 1 , v 2 e fst(a ) m → v 1 e a m → v 1 , v 2 e snd(a ) m → v 2 e a m → v τ = 1 e wrap(τ )(a ) m → v e a m → v τ > 1 e wrap(τ )(a ) m → v e a m → v τ = 1 e unwrap(τ )(a ) m → v e a m → v τ > 1 e unwrap(τ )(a ) m → v
• Γ |= v : ∀α 1 . . . α n . τ ≈ v : ∀α 1 . . . α n . τ iff for all legal interpretations V 1 . . . V n for type variables α 1 . . . α n , we have Γ + α 1 ← V 1 + . . . + α n ← V n |= v : τ ≈ v : τ • Γ |= e : E ≈ e : E iff
Proposition 2 Assume that:

E a : τ ⇒ a , Γ |= e : E ≈ e : E, e a u → v.
Then, there exists a value v such that:

e a m → v and Γ |= v : τ ≈ v : τ.
Proof: the proof makes use of the results below.

Lemma 2 Let ρ be the substitution

{α 1 ← τ 1 . . . α n ← τ n }. Define V i = {(v, v ) | Γ |= v : τ i ≈ v : [τ i ]}.
Then, the V i are legal interpretations for the α i . And the following two results are equivalent:

Γ + α 1 ← V 1 + . . . + α n ← V n |= v : τ ≈ v : τ (1) Γ |= v : ρ(τ ) ≈ v : [ρ](τ ) (2)
Proof: by induction over τ . 2

Lemma 3 1. If e a m → v and Γ |= v : ρ(τ ) ≈ v : [ρ](τ ), then there exists v such that e S ρ (a : τ ) m → v and Γ |= v : ρ(τ ) ≈ v : ρ(τ ). 2. If e a m → v and Γ |= v : ρ(τ ) ≈ v : ρ(τ ), then there exists v such that e G ρ (a : τ ) m → v and Γ |= v : ρ(τ ) ≈ v : [ρ](τ ).
Proof: by induction over τ .

2

The proof of proposition 2 itself is a simple inductive argument on the translation derivation. The only interesting case is a = x. Then, the translation derivation is:

E(x) = ∀α 1 . . . α n . τ Dom(ρ) ⊆ {α 1 . . . α n } E x : ρ(τ ) ⇒ S ρ (x : τ )
The only evaluation possibility is v = e(x). By hypothesis, Γ |= e(x) : ∀α 1 . . . α n . τ ≈ e (x) : ∀α 1 . . . α n . τ.

By definition of |= on type schemes, and by lemma 2, we have:

Γ |= e(x) : ρ(τ ) ≈ e (x) : [ρ](τ ).
Then, the expected result follows from lemma 3 (case 1), taking a = x and v = e (x). 2

Concrete data types

Until now, we have only dealt with simple data structures such as tuples and records. This section discusses more complex data structures: ML concrete data types. Except in degenerate cases, values belonging to concrete data types are best kept boxed at all times, in the unwrapped state as well as in the wrapped state. This conclusion can be drawn separately from two features of the concrete data types: they are sum types; and they can be recursive. Since data types are sum types, we do not know the exact size for values of these types, only an upper bound. Keeping these values unallocated would waste resources (e.g. registers). Since data types can be recursive, values of these types cannot be allocated completely flatly: sub-components of the same type must be handled through pointers.

Therefore, data types are represented by a heap block containing the constructor tag and the argument to the constructor, as usual. However, specialized representations result in a layout of the constructor argument that is flatter than usual, and therefore more space-and time-efficient. For instance, assuming the constructor declaration C of float × float, the value C(3.1415, 2.718) is represented by the 5-word block:

C 3.1415 2.718
This optimized layout is natural when we use mixed representations. We statically know that the constructor argument is of type float × float. Hence the constructor argument is evaluated as an unallocated pair of two unallocated numbers. When applying constructor C to this argument, the components of the argument are not boxed yet, and we are free to choose the most compact memory layout for them.

ML data types can be parameterized by other types, as the familiar list type:

datatype α list = Nil | Cns of α × α list
This raises a subtle issue.

If we naively follow the approach above, a list of floating-point numbers Cns(3.1415, Nil), with static type float list, is represented with the numbers unboxed, as follows.

Cns 3.1415 E Nil

However, generic functions over lists, such as the length function, are compiled without knowing the exact type of the list elements, and therefore they assume wrapped representations for the list elements. Hence, before being passed to a generic function over lists, the list above must be coerced to:

Cns c 3.1415 E Nil
That is, to coerce a τ list to an α list, we would have to apply coercion wrap(τ ) to each list element. More generally, transformation S would be defined on lists as:

S ρ (a : τ list) = map (λx. S ρ (x : τ )) a .

This operation requires time and space proportional to the length of the list, making this approach clearly impractical. To avoid copying, we must require that list elements are in the wrapped state at all times, even if their type is statically known. In other words, all list cells must share the same layout, with only one word allocated for the list element (last format above). This layout is determined once and for all when the list type is defined, assuming wrapped representations for the components of type α (the type parameter). Then, nothing needs to be done when specializing or generalizing a list: S ρ (a : τ list) = a .

Instead, some wrapping and unwrapping steps are required when constructing or accessing lists. To insert them correctly, it suffices to consider constructors and accessors as polymorphic functions that are used with more specific types: the translation given above inserts the right coercions.

To correctly handle lists and other generic data structures, it is not enough to keep list components in the wrapped state. We must also impose some additional compatibility conditions on the wrap and unwrap transformations. Namely, we must ensure that the components of a wrapped object are themselves in the wrapped state. This is what we call "recursive wrapping". Consider the list l = Cns((3.1415, 2.718), Nil), with type (float × float) list. If we don't perform recursive wrapping, the natural representation for list l is:

Cns c 3.1415 2.718 E Nil
This object is not a suitable argument to a function f with type ∀α. (α × α) list → . . . Such a function assumes its list argument to be of the format:

Cns c © d d d E
And no coercion will take place on l before it is passed to f, since l is a list. Hence, the correct representation for l is:

Cns c © 3.1415 d d d 2.718 E Nil
This means that the correct wrapped representation for a pair of floating-point numbers is a boxed pair of two boxed floating-point numbers. Similarly, the wrapped representation for a function with type float → float is not a boxed closure of the original function on unwrapped numbers, but a boxed closure of the corresponding function on wrapped numbers. More generally, the wrapped representation for an object of type τ must be compatible with the wrapped representation for objects of type τ , for all types τ more general than τ . To this end, we redefine the wrap and unwrap coercions on product types and on function types in terms of the S and G translations:

wrap(τ 1 × τ 2 )(a ) = wrap(×)(G {α←τ 1 ,β←τ 2 } (a : α × β)) wrap(τ 1 → τ 2 )(a ) = wrap(→)(G {α←τ 1 ,β←τ 2 } (a : α → β)) unwrap(τ 1 × τ 2 )(a ) = unwrap(×)(S {α←τ1,β←τ2} (a : α × β)) unwrap(τ 1 → τ 2 )(a ) = unwrap(→)(S {α←τ 1 ,β←τ 2 } (a : α → β))
Here, we have introduced primitive coercions wrap and unwrap that are attached to the type constructors × and → themselves, and no more to product types and to function types. These coercions can be implemented arbitrarily, for instance by boxing and unboxing.

Application to ML

The author has implemented the ideas above in Gallium, a prototype high-performance compiler for the ML language.

Representations for ML data types

We first describe the exact data representations used. Tuples, records, and floating-point numbers are represented as described above: unboxed in the unwrapped state, boxed in the wrapped state. Since moving around a large object is expensive, it would be wise to limit the size of an unboxed tuple. We could decide that any tuple requiring more than 4 words, for instance, is always boxed. This can be determined from the type of the tuple.

Concrete data type values are kept boxed at all times, as explained in section 4.

Unwrapped integers are unboxed, 32-bit wide. Even though they fit in one word, they have to be boxed in the wrapped state, for garbage collection reasons (see below). The wrap(int) operation is therefore implemented as boxing, and unwrap(int) as unboxing. An alternative would be tagged, unboxed, 31-bit wide integers both for the unwrapped state and the wrapped state; this would reduce heap allocation, but arithmetic on tagged integers is slower, and interface with C functions is complicated.

The garbage collector allows small, 8-bit wide integers to remain unboxed in the wrapped state. These small integers are used to encode booleans, as well as a built-in char type. The wrap and unwrap operations for these types are no-ops. As an easy generalization of the case for booleans, small integers could also represent enumerated data types (concrete types with constant constructors only).

The only value of type unit, (), is represented in the unwrapped state as the 0-tuple -the absence of any value, actually. Wrapped values of type unit are represented as a given one-word constant. The wrap(unit)(a) operation consists in evaluating a and loading the constant; the unwrap(unit)(a) operation simply evaluates a and throws the result away.

Closures representing functional values are represented by two unallocated words. One word points to the code part of the function. The other word points to a heap block containing the environment part: the values for the free variables of the function. Allocation of the environment part is not performed if it fits in one word. This simple approach already eliminates some closure allocations, especially in the case of simple curried functions. It seems impossible to avoid boxing the environment part in all cases: the type-based techniques proposed for tuples do not apply here, since we do not know the types of the values contained in the environment part. (The type of the function does not say anything about these types.) Arrays are generic data structures that can be arbitrarily large. This makes coercion by copying impractical on arrays. Actually, ML arrays can be physically The access functions coerce the array elements to or from the wrapped representation as needed. References to an array with a known type would directly access the array; references to an array with an unknown type would go through the access functions.

An overview of the implementation

The Gallium system compiles the Caml Light dialect of ML into assembly code for the MIPS R3000 processor [START_REF] Kane | MIPS RISC architecture[END_REF]. It combines the data representation technique presented here with a conventional, non CPS-based back end, using some of the standard techniques from [START_REF] Aho | Compilers: principles, techniques, and tools[END_REF].

A compilation involves two passes that communicate through an intermediate language nicknamed "C--". This is a simple expression-based language, that manipulates unboxed tuples of integers, floating-point numbers, or pointers (either code pointers or heap addresses). C--provides most of the operations and control structures of C, minus the operations on struct and union. In addition, C--directly supports exceptions and garbage collection.

This intermediate language is weakly typed: to each expression is attached a machine-level type expression. A machine-level type is simply a sequence of atomic types: either int, float, or address. Machine-level types contains just enough information for the back-end to determine the sizes and the calling conventions, and for the garbage collector to trace all pointers into the heap.

The front-end performs type inference, expands pattern-matching into decision trees, inserts the wrap and unwrap operations, and explicits closures. The front-end is entirely machine-independent. It embodies all the ML-specific treatments in the compiler. By contrast, the back-end is machine-dependent, but it knows almost nothing about ML. It performs instruction selection, reordering of computations, liveness analysis, register allocation by priority-based coloring of the interference graph [START_REF] Chow | Register allocation by priority-based coloring[END_REF], and emission of MIPS assembly code.

In the run-time system, the main originality is the use of static typing information to supplement the lack of tagging on objects that are not pointers. Traditionally, garbage collectors rely on run-time tags to distinguish pointers into the heap from other objects. Tags are also used to implement certain primitives such as generic equality. This solution is not adequate in our case, since we use native, unallocated 32-bit integers and floating-point numbers, that cannot be tagged. Instead, we make some of the static typing information available at run-time. Namely, each boxed object is adorned with a header giving the machine-level type of the object; each stack frame is associated with a descriptor giving the locations of live objects of type address in the corresponding function; a table contains the locations of all global variables of type address. This information allows the garbage collector to trace all valid pointers into the heap.

It has been pointed out that normally this approach does not work well in the presence of polymorphism [START_REF] Appel | Run-time tags aren't necessary[END_REF], since an object with static type α can be either an address into the heap, or an unboxed integer. In our case, such an object is guaranteed to be in the wrapped state; and we have arranged for all wrapped representations to be valid pointers, by boxing wrapped integers. Hence we can assume that all objects of type α are valid pointers. This fact allows the use of a simple, fast copying collector -at the cost of allocating wrapped integers. The alternative is to keep integers unboxed at all times, and revert to a collector with ambiguous pointers [START_REF] Bartlett | Compacting garbage collector with ambiguous roots[END_REF], which is slower and more complex. The times given are user CPU times, including garbage collection time. "Gallium" is the compiler described above; "Gallium0" is a version of the Gallium compiler that shares the same back-end and code generator, but uses conventional, boxed data representations; "SML-NJ" is Standard ML of New Jersey version 0.66, from Bell Labs and Princeton university; "Caml" is Caml version 3.1, from INRIA; and "cc" is the Ultrix 4.1 C compiler, at optimization level 2.

Benchmarks

These figures indicates that the data representation technique described here lead to important speedups on some programs; have little impact on other programs; and really slow down one (fairly contrived) test program.

The best results are achieved on programs that perform mostly numerical computations (tests 1 and 2): unboxed, untagged integer and floating-point numbers really pay off in this case. For these programs, the execution times for Gallium are comparable to the times for the C compiler. The author believes that this data representation issue was the main bottleneck that prevented C-like code written in ML from being compiled as efficiently as in C.

Programs that perform mostly symbolic computation (tests 5, 6, and 8) also benefit from specialized data representations, although the speedups are less dramatic. This is somehow surprising, since these programs mostly manipulate values of concrete data types, that are always boxed. However, they benefit from having unallocated tuples to communicate with functions with several arguments, and unallocated closures to communicate with higher-order functions.

The most interesting tests are those that make heavy use of polymorphic data structures and polymorphic higher-order functions (tests 3, 4, 6, and 7). Polymorphic higher-order functions tend to execute less effi-ciently with mixed data representations: the stub code inserted around their functional arguments introduces extra function calls. In test 6, this potential slowdown is overcome by the other benefits of mixed representations (unallocated tuples and closures). Tests 3 and 4 shows a slight slowdown; apparently, it could be avoided by performing some compile-time reductions on a local scale. Test 7, however, demonstrates a major slowdown on a highly polymorphic program. The test consists in mapping quad quad (λx. x + 1) on a list of integers, where quad is double double, and double is Church's numeral number two: λf. λx. f(f x). In this example, the closure for double gets considered in rapid succession with different types (α, α → α, and (α → α) → (α → α)). The compiled code spends a lot of time switching between the various representations corresponding to these types. Aggressive compile-time reductions are required to eliminate these unnecessary coercions. The author has not encountered this phenomenon in more realistic examples than test 7, however.

Concluding remarks

The technique presented in this paper, while resulting in important speedups, is essentially local, and based solely on static typing information. This means it remains easy to prove correct, and easy to implement. No extra static analysis is required; such analyses are often quite expensive, to the point of being impractical. Higher-order functions cause no difficulties, while most other systems static analyses fail in this case. And separate compilation remains possible, since all we need are the types of external identifiers -an information provided by any module system.

Mixed data representations not only speed programs up, but also make it easier to interface with libraries written in another language, such as C: it suffices to take unwrapped representations compatible with the C data formats and calling conventions.

Standard ML features type abstraction (at the level of modules) in addition to polymorphism (at the level of terms). From the standpoint of data representation, type abstraction raises the same issues as polymorphism. For instance, there is this nasty restriction in Modula-2 [START_REF] Wirth | Programming in Modula-2[END_REF], that an abstract type can only be implemented by a pointer type or an ordinal type, to ensure values of an abstract type fit in one word. Mixed data representations also work well with type abstraction: we take values of an abstract type to be unwrapped inside the structure that defines the abstract type, and wrapped outside, in the clients of the structure; the right coercions are introduced by applying the G transformation from section 3.2 to the values exported by the structure.

The technique presented in this paper works better in conjunction with compile-time reductions such as function inlining (though the Gallium compiler currently performs no inlining). Reductions can be performed before or after introducing the coercions. In the latter case, inlining a polymorphic function creates redexes of the form wrap(τ )(unwrap(τ )(a )) or unwrap(τ )(wrap(τ )(a )), that can trivially be replaced by a , saving one boxing step and one unboxing step. In the former case, a polymorphic function, once inlined, has a more specific type, and therefore can be compiled more efficiently.

When all polymorphic functions are systematically inlined, the program becomes completely monomorphic, and it can be compiled with optimal data representations. This essentially amounts to the Ada approach referred to in the introduction. The strength of our technique is that it is possible to stop compile-time reductions at any time (when the code becomes too large), and still get a correct program. This paper has only considered simple coercions between the wrapped representations and the unwrapped representations. More elaborate coercion schemes can certainly be found. (Thatte [15] gives interesting examples of complex coercions.) In particular, all coercions considered here are strict; lazy coercions (coercions that would be performed only on demand) could lead to a better utilization of unwrapped data structures inside generic data structures such as lists and arrays. A more axiomatic presentation of the translation proposed here, giving minimal semantic conditions over the coercions, would certainly help in finding good sets of coercions.

  λx. a, e) | op op ::= add | . . . A value is either a constant; a pointer v to a heap cell containing value v; an (unallocated) pair of two values v 1 , v 2 ; a primitive operation op; or a closure clos(k, λx. a, e) of function λx. a by evaluation environment e, with k being the expected size of the function argument (see below). Evaluation environments e are finite mappings from variables to values. This definition for values makes the boxing steps explicit (they are usually left implicit in this kind of semantics), and provides for the fact that values may have different sizes.

2 u→

 2 clos(1, λx. a 0 , e 0 ) e a 1 u

→ 2 m→

 2 clos( type(x) , λx. a , e) e a clos(k, λx. a 0 , e 0 ) e a 1 m

Figure 2 :

 2 Figure 2: Operational semantics (left: uniform representations; right: mixed representations)

  the domains of e, E, e , E are the same, and for all x ∈ Dom(e), we have Γ |= e(x) : E(x) ≈ e (x) : E (x).

Figure 5 .

 5 Figure 5.1 gives some experimental results obtained with the Gallium compiler. The tests were run on a Dec-Station 5000/200. All tests were limited to 8 megabytes.The times given are user CPU times, including garbage collection time. "Gallium" is the compiler described above; "Gallium0" is a version of the Gallium compiler that shares the same back-end and code generator, but uses conventional, boxed data representations; "SML-NJ" is Standard ML of New Jersey version 0.66, from Bell Labs and Princeton university; "Caml" is Caml version 3.1, from INRIA; and "cc" is the Ultrix 4.1 C compiler, at optimization level 2.These figures indicates that the data representation technique described here lead to important speedups on some programs; have little impact on other programs; and really slow down one (fairly contrived) test program.The best results are achieved on programs that perform mostly numerical computations (tests 1 and 2): unboxed, untagged integer and floating-point numbers really pay off in this case. For these programs, the execution times for Gallium are comparable to the times for the C compiler. The author believes that this data representation issue was the main bottleneck that prevented C-like code written in ML from being compiled as efficiently as in C.Programs that perform mostly symbolic computation (tests 5, 6, and 8) also benefit from specialized data representations, although the speedups are less dramatic. This is somehow surprising, since these programs mostly manipulate values of concrete data types, that are always boxed. However, they benefit from having unallocated tuples to communicate with functions with several arguments, and unallocated closures to communicate with higher-order functions.The most interesting tests are those that make heavy use of polymorphic data structures and polymorphic higher-order functions (tests 3, 4, 6, and 7). Polymorphic higher-order functions tend to execute less effi-

  in the wrapped state, as in the case of lists. Unwrapped array elements are desirable, however, since they lead to flat arrays, that are more compact and have better locality properties. One approach is to represent arrays as a flat block of unwrapped objects, paired with functions to read or write an element.

	Test	Gallium Gallium0 SML-NJ Caml cc -02 What is tested
	1 Takeushi	3.00	5.09	4.47	34.0	1.96 function calls (3 args),
						integer arithmetic
	2 Integral	0.80	2.83	8.46	15.2	0.40 floating-point arithmetic,
						loops
	3 List summation	3.60	3.45	5.12	7.90	list processing, integer
						arithmetic
	4 Sieve	1.00	0.94	2.31	5.74	list processing, functionals,
						polymorphism
	5 Boyer	1.80	2.76	3.60	14.6	term processing, function
						calls
	6 Knuth-Bendix	0.90	0.98	1.11	12.4	0.86 term processing, functionals,
	completion					polymorphism
	7 Church integers	6.58	2.40	2.90	16.1	functionals,
						polymorphism
	8 Solitaire	5.84	10.8	12.6	17.1	0.70 function calls, arrays,
						loops
			Figure 3: Experimental results
	modified, making copying semantically incorrect. Gal-
	lium uses a simple representation for arrays: it always
	keeps array elements

The New Jersey compiler utilizes better calling conventions when applying a known function[START_REF] Appel | Compiling with continuations[END_REF]. However, this optimization does not work when calling functions that are passed as arguments, or defined in another compilation unit.

Acknowledgments

Many thanks to Ian Jacobs, Damien Doligez and Luc Maranget for their comments.


Xavier Leroy
email: xleroy@margaux.inria.fr

Pierre Weis
email: weis@margaux.inria.fr

Polymorphic type inference and assignment

We present a new approach to the polymorphic typing of data accepting in-place modification in ML-like languages. This approach is based on restrictions over type generalization, and a refined typing of functions. The type system given here leads to a better integration of imperative programming style with the purely applicative kernel of ML. In particular, generic functions that allocate mutable data can safely be given fully polymorphic types. We show the soundness of this type system, and give a type reconstruction algorithm.

Introduction

Polymorphic type disciplines originate in the study of λcalculus and its connections to constructive logic [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur[END_REF][START_REF] Reynolds | Toward a theory of type structure[END_REF], so it is no surprise it fits very nicely within purely applicative languages, without side effects. However, polymorphism becomes problematic when we move toward conventional imperative languages (Algol, Pascal), and allow physical modification of data structures. The problem appeared at an early stage of the design of ML [8, p. 52], when assignment operators were provided for the primitive data types of references and vectors. Consider the following example, in ML 1 : let r = ref [ ] in r := [START_REF] Appel | Standard ML reference manual (preliminary)[END_REF]; if head (!r ) then . . . else . . .

If we naively give type ∀α. α list ref to the reference r,

we can first use it with type int list ref , and store in it the list with 1 as single element -an int list, indeed.

Given its type, we can also consider r as having type bool list ref , hence head (!r ) has type bool, and the if statement is well-typed. However, head (!r ) evaluates to 1, which is not a valid boolean. This example shows that physical modification of data compromises type safety, since it can invalidate static typing assumptions.

As demonstrated here, the use of polymorphic mutable data (that is, data structures that can be modified in place) must be restricted. An obvious way to tackle this problem, used in early implementations of ML [START_REF] Cousineau | The CAML primer[END_REF], is to require all such data to have monomorphic, statically-known types. This restriction trivially solves the problem, but it also makes it impossible to write polymorphic functions that create mutable values. This fact has unfortunate consequences.

A first drawback is that it is not possible to provide generic, efficient implementations of most data structures (vectors, hash tables, graphs, B-trees, . . . ), as they require physical modification. Even a trivial function such as taking a vector of an arbitrary type and returning a copy of it is not well-typed with the policy above, since it creates a vector with a statically unknown type.

Another drawback is that polymorphic mutable values are prohibited even if they are not returned, but used for internal computation only. As a consequence, most generic functions cannot be written in an imperative style, with references holding intermediate results. Consider the familiar map functional: let rec applicative map f l = if null l then [ ] else f (head l ) :: applicative map f (tail l )

Here is an alternate implementation of map in imperative style:

let imperative map f l = let argument = ref l and result = ref [ ] in
while not (null !argument) do result := f (head !argument) :: !result; argument := tail !argument done; reverse !result Some ML type systems reject imperative map as illtyped. Others give it a less general type than its purely applicative version. In any case, the imperative version cannot be substituted for the applicative one, even though they have exactly the same semantics. As demonstrated here, the programming style (imperative vs. applicative) interferes with the type specifications. This clearly goes against modular programming. Some enhancements to the ML type system have been proposed [START_REF] Damas | Type assignment in programming languages[END_REF][START_REF] Tofte | Operational semantics and polymorphic type inference[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Appel | Standard ML reference manual (preliminary)[END_REF], that weaken the restrictions over polymorphic mutable data. Standard ML [START_REF] Milner | The definition of Standard ML[END_REF] incorporates some of these ideas. These enhanced type systems make it possible to define many useful generic functions over mutable data structures, such as the function that copies a vector. However, these systems are still not powerful enough: they fail to infer the most general type for the imperative map example above; and they do not work well in conjunction with higher-order functions. Because of these shortcomings, Standard ML does not provide adequate support for the imperative programming style. This is a major weakness for a general-purpose programming language.

In this paper, we present a new way to typecheck mutable data within a polymorphic type discipline. Our type system is a simple extension of the one of ML. It permits type reconstruction and possesses the principal type property. It requires minimal modifications to the ML type algebra. Yet it definitely improves the support for imperative programming in ML. It allows generic functions over mutable data structures to have fully polymorphic types. It is powerful enough to assign to a function written in imperative style the same type as its purely applicative counterpart. For example, in this system, the imperative implementation of map cannot be distinguished from the usual, applicative one, as far as types are concerned.

The remainder of the paper is organized as follows.

In section 2, we introduce informally our type system, and show the need for a more precise typechecking of functions. Section 3 formalizes the ideas above. We state the typechecking rules, show their soundness, and give a type reconstruction algorithm. Section 4 briefly compares our approach with previous ones. We give a few concluding remarks in section 5.

Informal presentation

In this section, we informally introduce our typing discipline for mutable data, focusing on references to be more specific. Unlike the Standard ML approach, we do not attempt to detect the creation of polymorphic references. What we prohibit is the use of a reference with two different types. The only way to use a value with several types is to generalize its type first, that is, to universally quantify over some of its type variables. (In ML, the only construct that generalizes types is the let binding.) Hence, what we restrict is type generalization: we never generalize a type variable that may be free in the type of a reference. Such a type variable is said to be dangerous. Not generalizing dangerous type variables ensures that a mutable value always possesses a monotype.

It remains to detect dangerous type variables at generalization-time. Though this suggests a complex and expensive static analysis, this turns out not to be the case: dangerous variables can be determined by mere examination of the type being generalized, as we shall now illustrate.

Datatypes

Consider the example given in introduction: References may be embedded into more complex data structures (pairs, lists, concrete datatypes). Fortunately, the type of a data structure contains enough information to retrieve the types of the components of the structure. For instance, a pair with type A × B contains one value of type A and one value of type B. Therefore, any variable which is dangerous in A or in B is also dangerous in A × B. For instance, in

let r = ref [ ] in r := [1]; if head (!
let r = ([ ], ref [ ]) in e the expression ([ ], ref [ ]) has type α list × β list ref ,
where β is dangerous but not α. Hence in e, variable r has type ∀α. α list × β list ref .

The treatment of user-defined datatypes is similar. Parameterless datatypes cannot contain polymorphic data, so there is no dangerous variable in them. Parameterized datatypes come in two flavors: those which introduce new ref types (such as type α foo = A | B of α ref ), and those which don't. The former are treated like ref types: all variables free in their parameter(s) are considered dangerous. The latter are treated like product types: their dangerous variables are the dangerous variables of their parameter(s). The analysis above is based solely on the type of the function result. Hence, the usage of a polymorphic function is unrestricted if the function does not return any references, as witnessed by the absence of ref types in its codomain type. This holds even if the function allocates references with statically unknown types for internal purposes, but does not return them. For instance, this is the case for the imperative map functional given in the introduction: it is given type ∀α, β. (α → β) → α list → β list, the very same type as its purely applicative counterpart applicative map. The imperative map functional can be substituted for applicative map in any context. In particular, it can be applied to highly polymorphic arguments: the expression imperative map (function x → x ) [ ] is well-typed, and returns the fully polymorphic empty list, even though two references were created with type α list ref . The type system guarantees that these references are used consistently inside the function, and are not exported outside.

Functions

Another strength of this type-based analysis is its good handling of higher-order functions and partial applications.

Consider the partial application of applicative map to make ref : our type system correctly recognize it as harmless, and gives it the fully polymorphic type ∀α. α list → α ref list. This is not the case for ML type systems that attempt to control the creation of references (see section 4).

Functions with free variables

The careful reader may have noticed a flaw in the discussion above: we have neglected the fact that a func-tion may possess free variables. Suppose that a function f has a free variable r which is bound to a reference outside the function. Function f can access and update the reference, yet the type of r does not necessarily appear in the type of f . A classic example is the functional presentation of references as a pair of functions, one for access, the other for update:

let functional ref x = let r = ref x in (function ( ) → !r ), (function z → r := z ) The expression functional ref [ ] has type (unit → α list) × (α list → unit),
where no type variable is dangerous, so it is fully polymorphic, yet it breaks type safety just as ref [ ] does. The problem is that the types of the free variables of a function do not appear in the type of the function. In this context, it is useful to think of functions as closures. Closures, in contrast with any other data structure, are not adequately described by their (functional) type: we do not know anything about the types of the values contained in the environment part of a closure.

Our solution is to keep track of what is inside a closure. We associate with any function type a set of types, the types of all variables free in the function. We could put this set of types as a third argument to the arrow type constructor. For technical reasons, we find it more convenient to add an extra level of indirection in recording this set of types. Therefore, each function type is adorned with a label. Labels are written L, M , and labeled function types are written A L → B. Separately, we record constraints on those labels. Constraints have the format A L, meaning that objects of type A are allowed to occur in environments of type L. An environment of type L is not required to contain a value of type A. It is not allowed to contain a value of a type B unless B L is one of the recorded constraints.

This way, function type labels allow typings of the environment parts of closures.

For instance, functional ref now has type:

α L → (unit M → α) × (α N → unit) with α ref M, α ref N hence functional ref [ ] has type: (unit M → β list) × (β list N → unit) with β list ref M, β list ref N
thus revealing the presence of a polymorphic reference in each function of the pair, and preventing the generalization of β. The rule is that in a functional type

A M → B, a variable α is dangerous iff there exists a constraint C M with α dangerous in C.
This typing of closures gives a precise account of the interleaving of internal computation and parameter passing in (curried) functions, and of the possible data sharing between invocations. For instance, it succeeds in distinguishing the following two functions:

function ( ) → ref [ ] : unit L → α list ref let r = ref [ ] in function ( ) → r : unit L → α list ref with α list ref L
The former is harmless, since it returns a fresh reference each time, so it can be generalized. The latter always return the same reference, which is therefore shared between all calls to the function. It must remain monomorphic, which is indeed the case, since α is a dangerous variable in its type.

Before presenting the type system formally, we now give the main intuitions behind the typing of closures. Constraints are synthesized during the typing of abstractions, as follows: when giving type A Finally, to give the most general type to functionals, we must be able to generalize over labels, in the same way as we generalize over regular type variables. Consider the functional:

function f → 2 + (f 1)
It must be possible to apply it to any function mapping integers to integers, whatever its closure may contain. Yet if we give it the type (int L → int) M → int without generalizing over L, we could only apply it to functions without free variables, assuming there is no constraint over L in the current environment. Instead, the right typing is ∀L. (int

L → int) M → int.
In more complex situations, the current environment contains constraints over the label to be generalized. These constraints are discharged in the type schema, and reintroduced at specialization time. Type schemas therefore have the format ∀V 1 . . . V n . A with Γ, where the V i are either labels or type variables, and Γ is a sequence of constraints.

Formalization

In this section, we formalize a calculus based on the ideas above.

Syntax

The language we consider is the core ML language, λcalculus plus a distinguished let construct. We shall assume a built-in int type, with integer constants. The store is presented through the type A ref of references to a term of type A, and the operations ref(a), to allocate a new reference to term a, !a to get the contents of the reference a, and a := b to update the content of a by b.

We assume given a countable set Var of term variables, with typical elements x, y. In the following, i ranges over integers. The syntax of terms, with typical elements a, b, is as follows:

a ::= x | i | λx. a | (b a) | let x = a in b | ref(a) | !a | a := b

Typechecking

Type expressions, with typical elements A, B, have the following syntax:

A ::= X | int | A L → B | A ref
In the definition above, X stands for a type variable, ranging over a given countable set TVar . Function types A L → B are annotated by a label L, taken from a countable set Lbl . Labels are distinct from term variables and type variables.

Type schemas, with typical element Σ, are composed of type expressions with some type variables and some labels universally quantified. They also contain a sequence of constraints Γ. Constraints have the format Σ L. Given a type A in the context of a constraint sequence Γ, we define its free variables (labels as well as type variables) F V (A with Γ) and its dangerous free variables DV (A with Γ) as follows. The intuition behind the definition of F V is that the components of a functional type A L → B are not only A, B and L, but also any type expression C such that C L is one of the recorded constraints.

Σ ::= A | ∀V 1 . . . V n . A with Γ Γ ::= | Σ L, Γ V ::= X | L (int) E i : int with Γ (varspec) E(x) = ∀X 1 . . . X n , L 1 . . . L m . A with Γ E x : A{X i ← B i , L j ← M j } with Γ{X i ← B i , L j ← M j } ∪ Γ (fun) E[x ← A] b : B with Γ for all y free in λx. b, (E(y) L) ∈ Γ E λx. b : A L → B with Γ (app) E b : A L → B with Γ E a : A with Γ E (b a) : B with Γ (letgen) E a : A with Γ (Σ, Γ ) = Gen(A, E, Γ) E[x ← Σ] b : B with Γ ∪ Γ E let x = a in b : B with Γ ∪ Γ (ref) E a : A with Γ E ref(a) : A ref with Γ (deref) E a : A ref with Γ E !a : A with Γ (assign) E a : A ref with Γ E b : A with Γ E a := b : A with Γ
F V (X with Γ) = {X} F V (int with Γ) = ∅ F V (A ref with Γ) = F V (A with Γ) F V (A L → B with Γ) = {L} ∪ F V (A with Γ) ∪ F V (B with Γ) ∪ (Σ L)∈Γ F V (Σ with Γ) DV (X with Γ) = ∅ DV (int with Γ) = ∅ DV (A ref with Γ) = F V (A with Γ) DV (A L → B with Γ) = (Σ L)∈Γ DV (Σ with Γ)
To complete the definition above, we extend F V and DV to type schemas and to typing environments in the obvious way:

F V (∀V 1 . . . V n . A with Γ ) with Γ = F V (A with Γ ∪ Γ ) \ {V 1 . . . V n } DV (∀V 1 . . . V n . A with Γ ) with Γ = DV (A with Γ ∪ Γ ) \ {V 1 . . . V n } F V (E with Γ) = x∈Dom(E) F V (E(x) with Γ)
The typing rules are given in figure 1. They are very similar to the rules for ML, except for the additional handling of constraints, reminiscent of the treatment of subtyping hypotheses in type inference systems with subtypes [START_REF] Mitchell | Coercion and type inference[END_REF][START_REF] Fuh | Type inference with subtypes[END_REF].

The rules define the proposition "term a has type A under assumptions E and constraints Γ", written E a : A with Γ. The typing environment E is a partial mapping from term variables to type schemas. We write E[x ← A] for the environment identical to E, except that x is mapped to A. We assume the usual set operations are defined over constraints Γ in the obvious way.

As in Standard ML [11, p. 21], the Gen operator used in the (letgen) rule is responsible for generalizing as many type variables as possible in a type. Here, we also generalize over labels whenever possible. In addition, we prohibit generalization over dangerous type variables. A tentative definition would therefore be

Gen(A, E, Γ) = ∀V 1 . . . V n . A where the set {V 1 . . . V n } is F V (A with Γ) \ DV (A with Γ) \ F V (E with Γ).
However, it would be incorrect to generalize over a variable which remains free in the constraint sequence used

i[s] e =⇒ int(i)[s] x[s] e =⇒ e(x)[s] (λx. a)[s] e =⇒ clos(x, a, e |F V (a) )[s] b[s] e =⇒ clos(x, c, e 1 )[s 1 ] a[s 1 ] e =⇒ v 2 [s 2 ] c[s 2 ] e 1 [x←v 2 ] =⇒ v 3 [s 3 ] (b a)[s] e =⇒ v 3 [s 3 ] a[s] e =⇒ v 1 [s 1 ] b[s 1 ] e[x←v1] =⇒ v 2 [s 2 ] (let x = a in b)[s] e =⇒ v 2 [s 2 ] a[s] e =⇒ v[s ] / ∈ Dom(s ) ref(a)[s] e =⇒ loc( )[s [ ← v]] a[s] e =⇒ loc( )[s ] !a[s] e =⇒ s ( )[s ] a[s] e =⇒ loc( )[s 1 ] b[s 1 ] e =⇒ v[s 2 ] (a := b)[s] e =⇒ v[s 2 [ ← v]]
Figure 2: The evaluation rules later. Therefore, Gen also discharges in the schema all "generic" constraints, i.e. the constraints in Γ where one of the V i is free, and returns the remaining constraints, to be used further in the typing derivation.

Definition 1 (Generalization) Let A be a type expression, E be a typing environment, Γ be a constraint sequence. Define:

{V 1 . . . V n } = F V (A with Γ) \ DV (A with Γ) \ F V (E with Γ).
Let Γ be the sequence of those constraints Σ L in Γ such that L is one of the V i . Then:

Gen(A, E, Γ) = (∀V 1 . . . V n . A with Γ ), (Γ \ Γ )

Evaluation

We give here an evaluation mechanism for terms of our calculus, using structural operational semantics. The evaluation relation a [s] e =⇒ v[s ] maps a term a, in the context of an evaluation environment e and a store s, to some value v, and a modified store s . Values have the following syntax:

v ::= int(i) | clos(x, a, e) | loc( )
Here, ranges over a countable set Loc of locations. Stores are partial mappings from locations to values. Since we assume call-by-value, evaluation environments are partial mappings from term variables to values. The rules given in figure 2 define precisely the evaluation relation, assuming standard left-to-right evaluation order.

To account for run-time type errors, we introduce the special result wrong, and state that if none of the evaluation rules match, then a[s] e =⇒ wrong. This way, we can distinguish between type errors and nontermination.

Soundness of typing

The type system presented here is sensible with respect to the evaluation mechanism above: no well-typed term can evaluate to wrong.

Proposition 1 Let a be a term, A be a type, Γ be a sequence of constraints such that we can derive ∅ a : A with Γ. Then, for all stores s 0 , a[s 0 ] does not evaluate to wrong; that is, we cannot derive a[s 0 ] ∅ =⇒ wrong.

The proof can be found in appendix. It closely follows Tofte's [16, chapter 5]. The crucial point is that closure labels and constraints give a better control over the types of store locations than in ML. As a consequence, a variable cannot be free in the type of a location reachable from a value without being dangerous in the type of that value. This guarantees the soundness of type generalization.

Type reconstruction

In this section, we consider an adaptation to our language of the well-known Damas-Milner type reconstruction algorithm for ML (algorithm W of [START_REF] Damas | Principal type-schemes for functional programs[END_REF]). In the following, we write mgu(A, B) for the principal unifier of types A and B, if A and B are unifiable. (Otherwise, the type inference algorithm fails.) Type expressions are terms of a two-sorted free algebra, hence this ensures the existence of a principal unifier, that can be obtained by the classical unification algorithm between terms of a free algebra.

Let a be a term, E be a typing environment, and Γ be an initial sequence of constraints. We define infer (E, a, Γ) as the triple (A, σ, ∆), where A is a type expression, σ a substitution and ∆ a constraint sequence, as follows:

infer (E, i, Γ) = (int, Id, Γ) infer (E, x, Γ) = let (∀X 1 . . . X n , L 1 . . . L m . A with ∆) = E(x) let Y 1 , .
. . , Y n be fresh type variables (not free in E nor in A) and M 1 , . . . , M m be fresh labels

let σ = {X i ← Y i , L j ← M j } in (σA, Id, Γ ∪ σ∆) infer (E, λx. b, Γ) = let X, L be fresh variables let Θ = {E(y) L | y free in λx. b} let B, σ, ∆ = infer (E[x ← X], b, Γ ∪ Θ) in (σX L → B, σ, ∆) infer (E, (b a), Γ) = let B, ρ, Θ = infer (E, b, Γ) let A, σ, ∆ = infer (ρE, a, Θ) let X, L be fresh variables let µ = mgu(σB, A L → X) in (µX, µσρ, µ∆) infer (E, let x = a in b, Γ) = let A, σ, ∆ = infer (E, a, Γ) let Σ, ∆ = Gen(A, σE, ∆) let B, ρ, Θ = infer ((σE)[x ← Σ], b, ∆ ) in (B, ρσ, Θ) infer (E, ref(a), Γ) = let A, σ, ∆ = infer (E, a, Γ) in (A ref , σ, ∆) infer (E, !a, Γ) = let A, σ, ∆ = infer (E, a, Γ) let X be a fresh variable let µ = mgu(A, X ref ) in (µX, µσ, µ∆) infer (E, a := b, Γ) = let A, σ, ∆ = infer (E, a, Γ) let B, ρ, Θ = infer (σE, b, ∆) let µ = mgu(ρA, B ref ) in (µB, µρσ, µΘ)
This algorithm enjoys the good properties of the Damas-Milner algorithm: it is correct and complete with respect to the typing rules, and the inferred type is the most general one. The proof is very similar to Damas' proof [START_REF] Damas | Type assignment in programming languages[END_REF].

Relation to ML

We have introduced closure typing as a way to keep track of mutable values embedded in functions. As a consequence, two expressions having the same functional type in ML may now be distinguished by their closure type, and we may fear that this leads to a type system more restrictive than the one of ML. Ideally, we would like the purely applicative fragment of our calculus (that is, without the ref type constructor, and the ref, := and ! term constructors) to be a conservative extension of ML: any pure, closed term that is well-typed in ML should also be well-typed in our calculus. Unfortunately, this is not the case -but for more subtle reasons than the one outlined above.

Actually, two type expressions in our system cannot be distinguished by their closure labels only. The reason is that unification cannot fail because of the labels: given the syntax of type expressions, a label can only be matched against another label, and labels are treated as variables as far as unification is concerned. Therefore, in our system, unification between types is conservative with respect to unification between the corresponding ML types. To be more precise, we introduce the "strip" operator ↓, that maps type expressions in our calculus to ML type expressions, by erasing the labels from function types:

int↓ = int X↓ = X (A ref )↓ = A↓ ref (A M → B)↓ = A↓ → B↓
Then, two type expressions A and B are unifiable if and only if A↓ and B↓ are, and in this case, taking σ = mgu(A, B) and ρ = mgu(A↓, B↓), we have (σC)↓ = ρ(C↓) for all types C. This lemma, along with the close resemblance between our algorithm infer and Damas-Milner's W algorithm, lead us to believe that, given the same pure term, both algorithms infer the same type, modulo closure labels. However, this does not hold because of the generalization step in the case of a let construct. Consider the typing of let x = a in b. Assume that, starting from typing environment E, algorithm infer infers type A with Γ for a, while algorithm W , starting from the corresponding ML typing environment E↓, infers the corresponding ML type A↓. We must check that both algorithms generalize exactly the same type variables, so that they will type b in compatible environments. This could be not the case for two reasons.

The first reason is that algorithm infer does not generalize dangerous type variables, while W does. But this is no problem here, since we consider only the pure fragment of our calculus, without the ref type constructor, hence the set of dangerous variables of any type is always empty.

The second, more serious reason is that closure typing introduces additional free variables in a given type. In general, F T V (A with Γ), the set of free type variables in A with Γ, is a superset of F V (A↓). (Take for instance A = int L → int and Γ = X L.) So it is not obvious that F T V (A with Γ) \ F T V (E with Γ), the set of type variables generalized by infer , is the same as F V (A↓) \ F V (E↓), the set of type variables generalized by W . Indeed, there are cases where infer does not generalize some type variable X, while W does, because X is free in E with Γ, but not in E↓. Consider: λz . let id = λx . if . . . then z else (λy. x ; y) ; x in id id Assuming x : X and y : Y , the term (λy. x ; y) is given type Y M → Y with X M , and the if construct forces z to have the same type. Therefore, when we attempt to generalize X L → X (the type of λx. . . . ; x), we have

E(z) = Y M → Y under constraints Γ = X M, Y M →
Y L, and we cannot generalize over X, since it is free in the type of z. Hence, id remains monomorphic, and the application id id is ill-typed. In ML, we would have z : Y → Y , so we could freely generalize over X, getting id : ∀X. X → X, and the whole term would be well-typed.

The example above is quite convoluted, and it is the simplest one we know that exhibits this "variable capture through labels" phenomenon. We need more experience with the proposed type system to find whether this phenomenon happens in more practical situations. However, in case this turns out to be a serious flaw of our closure typing system, we are investigating two possible improvements that seem to avoid variable captures.

One direction is to record less constraints when typing a λ-abstraction. In the example above, one could argue that the constraint X M should not be recorded, on the grounds that x is "not actually used" in the body of the function, as witnessed by the fact that the type variable X is not free in the type of the function result, nor in the type of the parameter.

The other direction is to check that two function types are compatible without actually identifying their closure types. This way, we could avoid the propagation of the constraint X M to the type of z.

Pragmatics of constraint handling

Practically, the main concern with the type inference algorithm above is the additional overhead introduced by the handling of constraints. First, it is possible to simplify sequences of constraints. Here are some possible simplification rules:

Σ M, Σ M → Σ M Σ M → if Σ is closed A × B M → A M, B M
These three simplifications are obviously sound with respect to the computation of free and dangerous variables. The third rule actually generate more constraints, but this may open the way to further simplifications, e.g. if A = B, or if A is closed.

In addition, constraint handling becomes quite cheap if we distribute constraints inside types, instead of handling a single list of constraints. We suggest grouping together all constraints over the same label L, arranged as a list of type schemes. This list represents the label L itself. To identify two labels, we just have to concatenate the two lists, and this can be done in constant time, using e.g. difference lists. Hence, when unifying two type expressions A and B, the additional work of identifying labels takes time at most proportional to the size of A, B. Therefore, unification can be performed in linear time, as in ML.

Comparison with other type systems

In this section, we compare our type system with previous proposals of polymorphic type systems for languages featuring physical modification.

Standard ML

We consider first the systems proposed for ML. All these systems rely on detecting the creation of mutable values (e.g. by special typechecking rules for the ref construct), and ensuring that the resulting mutable values have monomorphic types.

The first system we consider is the one proposed by Tofte [START_REF] Tofte | Operational semantics and polymorphic type inference[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF], and adopted in Standard ML [START_REF] Milner | The definition of Standard ML[END_REF]. It makes use of weak type variables (written with a * superscript) to prohibit polymorphic references. Weak type variables cannot be generalized by a let binding, unless the corresponding expression is guaranteed to be non-expansive, i.e. that it does not create any references. Damas [START_REF] Damas | Type assignment in programming languages[END_REF] proposed a related, but slightly different scheme, that gives similar results in most cases.

The other system is an extension of Tofte's, used in the Standard ML of New Jersey implementation [START_REF] Appel | Standard ML reference manual (preliminary)[END_REF]. In this scheme, type variables are no longer partitioned into weak and non-weak variables; instead, each type variable has an associated integer, its "degree of weakness", or "strength". This degree measures the number of abstractions that have to be applied before the corresponding reference is actually created. Regular, unconstrained type variables have strength infinity. Variables with strength zero cannot be generalized. Variables with strength n > 0 can be generalized, but each function application decrements the strength of variables.

Standard ML SML-NJ Our system make ref α * → α * ref α 1 → α 1 ref α L → α ref make ref [ ] rejected rejected rejected imperative map (α * → β * ) → α * list → β * list (α 2 → β 2 ) → α 2 list → β 2 list (α L → β) M → α list N → β list with α L → β N imperative map id [ ] rejected rejected α list applicative map make ref rejected rejected α list L → α ref list id make ref rejected rejected α L → α ref (raise Exit : α ref ) α ref α ref rejected
The comparative results are given in figure 3. For each test program, we give its most general type in each system. We assume these are top-level phrases. As in most ML implementations, we reject top-level phrases whose types cannot be closed (because some free variables cannot be generalized).

The first test is the make ref function, defined as function x → ref x . It exercises the possibility of writing generic functions that create and return updatable data structures. Most functions over vectors, matrixes, doubly linked lists, . . . are typed similarly. All type systems considered here capture the fact that make ref should be applicable to monomorphic values only.

The second test is the imperative map functional given in the introduction. It illustrates the use of polymorphic references as auxiliaries inside a generic function. Our type system is the only one which gives a fully polymorphic type to imperative map. The others restrict it to be used with monomorphic type.

The third test is the partial application of applicative map, defined in the introduction, to the make ref function. It exercises the compatibility between functions that create mutable data and higherorder functions. SML and SML-NJ refuse to generalize its type, hence reject it. They are unable to detect that applicative map does not apply make ref immediately, hence that applicative map make ref does not create any polymorphic reference.

A simplified version of this test, shown below, is to apply the identity function id to the make ref function.

Our type system gives the same type to id make ref and to make ref .

The others don't, and we take this as strong evidence that they do not handle full functionality correctly.

The last example illustrates a weakness of our typebased approach. By using exceptions, for instance, one may mimic the creation of a reference as far as types are concerned, without actually creating one. In the expression (raise Exit : α ref ), our type system considers that α is dangerous and does not generalize it. Other type systems recognize that no references are created, hence they correctly generalize it. This flaw of our method has little impact on actual programming, however.

Quest

In our system, we made no attempt at restricting the creation of mutable values, and concentrated on type generalization instead. We were inspired by Cardelli's Quest language [START_REF] Cardelli | Typeful programming[END_REF], which departs significantly from ML, but features mutable data structures and polymorphic typing.

Quest makes almost no typing restrictions for mutable values. Soundness is ensured by different semantics for type specialization. Namely, an expression with polymorphic type is evaluated each time its type is specialized, in contrast with ML, where it would be evaluated only once. This is consistent with the fact that polymorphism is explicit in Quest programs: polymorphic objects are actually presented as functions that take a type as argument and return a specialized version of the object. But these semantics are incompatible with ML, where generalization and specialization are kept implicit in the source program.

FX

The FX effect system [START_REF] Lucassen | Polymorphic effect systems[END_REF] is a polymorphic type system that performs purity analysis as well: the type of an expression indicates what kind of side-effects its evaluation can perform. This provides a simple way to deal with the problem of mutable values: the type of an expression cannot be generalized unless this expression is referentially transparent. It is easy to see that such "pure" expressions can safely be used with different types.

Though this approach is attractive for other purposes (e.g. automatic program parallelization), it definitely does not address the main issue considered here: how to give the same type to semantically equivalent functions, whether written in applicative style or in imperative style. The reason is that the purity analysis of FX makes it apparent in the types whether a function allocates mutable data for local purposes. For instance, imperative map and applicative map do not have the same type in FX.

Conclusion

We have presented herein an extension of the ML type system that considerably enhances the support for data accepting in-place modification. This is a significant step toward the integration of polymorphic type discipline and imperative programming style. We have introduced the notion of closure typing, which is essential to the soundness of this approach. We have given one type system that performs this closure typing, based upon labels and constraints. Our system is simple, but falls short of being a conservative extension of ML. Further work includes investigating alternate, more subtle ways to typecheck closures, that would not reject any well-typed ML program, while correctly keeping track of mutable data.

The scope of this work is not strictly limited to the problem of mutable data structures. For instance, it is well-known that polymorphic exceptions raise the same issues as references, and can be handled in the same way. More generally, similar problems arise in the integration of polymorphic typing within several other programming paradigms. For instance, one approach to the integration of functional and logic programming is to allow partially defined values containing logical variables within a conventional functional language [START_REF] Smolka | FRESH: a higher-order language with unification and multiple results[END_REF]. Polymorphic logical variables break type safety just as polymorphic references do, and are amenable to the same treatment. In object-oriented programming, status variables of objects can be seen as references systematically encapsulated in functions (the methods). Closure typing seems relevant to the polymorphic type-checking of such objects. Finally, some calculi of communicating systems feature channels as first-class values [START_REF] Milner | A calculus of mobile processes: part 1[END_REF]. Polymorphic typing of these channels must guarantee that senders and receivers agree on the types of transmitted values, and this is similar to ensuring that writers and readers of a reference use it consistently [START_REF] Reppy | First-class synchronous operations in Standard ML[END_REF].

Similarly, let s be a store. We say that |= s : S with Γ if Dom(s) ⊆ Dom(S) and for all ∈ Dom(s), we have S |= s( ) : S( ) with Γ.

In the proof of soundness, we will use the fact that the semantic typing judgement is stable under substitution. Starting from a given value v, it is not possible in general to access any location in the store. The set R(v) of locations reachable from v is defined by induction on v, as follows.

Definition 3 (Reachable locations) R(int(i)) = ∅ R(loc( )) = { } R(clos(x, a, e)) = y∈Dom(e)

R(e(y))

In the definition of S |= v : A with Γ, the types of the locations that cannot be reached from v are irrelevant. We can actually assume any other type for those locations:

Lemma 2 (Garbage collection) Let S, S be two store typings such that S( ) = S ( ) for all ∈ R(v). If S |= v : A with Γ, then S |= v : A with Γ Our type expressions are informative enough to allow us to connect the type of a location reachable from a value v with the type A of v. More precisely, we have the following key lemma which relates the variables free in the type of with the dangerous variables of A. To apply the induction hypothesis to the last premise, we need to show that: To do so, we must prove that, for any substitution µ over the V i , (3) By lemma 3, for any location reachable from v a , we have F V (S a ( ) with Γ) ⊆ DV (A with Γ), and none of the V i is dangerous in A with Γ, hence none of the V i is free in S a ( ). Therefore,

S a |=

M→

  B to the abstraction e = function x → . . ., for each variable y free in e, we look up the type C y of y in the typing environment and record the constraint C y M . It is always safe to add new constraints, since the constraints over a label L are intended to give an upper bound for what can go inside closures of type L. (This may lead to less general types, however, since more variables will be declared dangerous.) Unifying two labeled function types A L → B and C M → D is easy: it suffices to identify both labels L and M , resulting in a single label which bears the previous constraints on M as well as those on L. For instance, assuming f : int L → int, the expression if . . . then f else let z = 1 in function x → x + z has type int L → int as well, with the additional constraint that int L.

Figure 1 :

 1 Figure 1: The typing rules.

Figure 3 :

 3 Figure 3: Comparison with other type systems

Lemma 1 (

 1 Semantic substitution) If S |= v : A with Γ, then µS |= v : µA with µΓ for all substitutions µ.

Lemma 3 ( 1 L→ A 2 , 2

 3122 Store typing control) Assume S |= v :A with Γ. Let be a location in R(v). Then F V (S( ) with Γ) ⊆ DV (A with Γ).Proof: By induction on v.Case 1: A = int and v = int(i). Obvious, since there are no locations reachable from v.Case 2:A = B ref , v = loc( ),and S( ) = B. By definition of the reachable locations, = . Hence F V (S( ) with Γ) = F V (B with Γ) = DV (A with Γ).Case 3: A = A and v = clos(x, a, e). Let y be a variable such that is reachable from e(y). Let Σ be a type scheme such that S |= e(y) : Σ and (Σ L) ∈ Γ. We write ∀V 1 . . . V n . B with Γ for Σ. For all substitutions µ over V 1 . . . V n , since S |= e(y) : µB with Γ ∪ µΓ , we get by induction hypothesis:F V (S( ) with Γ ∪ µΓ ) ⊆ DV (µB with Γ ∪ µΓ )Taking well-chosen substitutions µ, it follows that:F V (S( ) with Γ) ⊆ DV (B with Γ ∪ Γ ) \ {V 1 . . . V n }Hence the desired result: F V (S( ) with Γ) ⊆ DV (Σ with Γ) ⊆ DV (A with Γ)We are now ready to show the soundness of the typing rules.Proposition 2 (Soundness) Assume E a : A with Γ. Let e be an evaluation environment, s a store, S a store typing such that:S |= e : E with Γ |= s : S with Γ.Assume a[s]e =⇒ w. Then, w = v[s ], and there exists a store typing S extending S, such that:S |= v : A with Γ |= s : S with ΓProof: By induction on the length of the evaluation. All cases proceed as in Tofte's proof[16, chapter 5], except when a is a let binding. Then, the last step of the typing derivation is:E a : A with Γ (Σ, Γ ) = Gen(A, E, Γ) E[x ← Σ] b : B with Γ E let x = a in b : B with ΓApplying the induction hypothesis to the first premise, we get v a , s a , S a extending S such that: a[s] e =⇒ v a [s a ] S a |= v a : A with Γ |= s a : S a with Γ.

S

  a |= v a : µA with Γ ∪ µΓ . (1) Since S a |= v a : A with Γ, we have, by lemma 1, µS a |= v a : µA with µΓ. (2) By definition of Gen, none of the V i appears in any constraint of Γ , hence µ(Γ) = µ(Γ ∪ Γ ) = Γ ∪ µΓ .

(

  µS a )( ) = S a ( ) for all ∈ R(v a )[START_REF] Damas | Type assignment in programming languages[END_REF] and the claim (1) above follows from (2), (3), (4), and lemma 2. Therefore, we can apply the induction hypothesis to the right branch of the typing derivation, getting v b , s b , S b extending S a such that:b[s a ] e[x←v a ] =⇒ v b [s b ] S b |= v b : B with Γ |= s b : S b with Γwhich is the expected result. 2

  Function types are treated specially. The reason is that a value with type A → B does not contain a value of type A, nor a value of type B, in contrast with regular datatypes such as A × B or A list. Hence it seems there are no dangerous variables in type A → B, even if A or B contain dangerous variables themselves. For instance, the function let make ref = function x → ref x

	has type α → α ref , and α is not dangerous in it,
	so it is fully polymorphic. It is actually harmless by
	itself. What's harmful is to apply make ref to a poly-
	morphic argument such as [ ], bind the result with a
	let construct, and use it with two different types. But
	this is not possible in the proposed type system, since
	make ref [ ] has type β list ref , and this type will not be
	generalized, as β is dangerous in it. In our approach,
	generic functions that create and return mutable ob-
	jects are given very general types. Type safety is en-
	sured by controlling what can be done with the result
	of their application, as described above.

  Γ), and ∀V 1 . . . V n . A with Γ for Σ. Since S a extends S, and V 1 . . . V n are not free in E, we already have S a |= e : E with Γ as a corollary of lemma 2. It remains to show that:S a |= v a : (∀V 1 . . . V n . A with Γ ) with Γ .

e[x ← v a ] : E[x ← Σ] with Γ

where we write (Σ, Γ ) for Gen(A, E,

Acknowledgments

Didier Rémy suggested the use of constraints in the typing rules. We also benefited from his expertise in type inference and unification problems. Many thanks to Brad Chen for his editorial help.

A Proof of soundness

In this appendix, we sketch the proof of soundness of the type system with respect to the operational semantics given in section 3.3.

We formalize the fact that a value v semantically belongs to a type expression A under constraints Γ. We write this S |= v : A with Γ. The hypothesis S is a store typing, that is, a partial mapping from locations to type expressions. The store typing is needed to take into account the sharing of values introduced by the store. -and there exists a typing environment

The predicate above is extended to type schemas by taking S |= v : (∀V 1 . . . V n . A with Γ ) with Γ iff for all substitutions µ over V 1 . . . V n , we have S |= v : µA with Γ ∪ µΓ Let e be an evaluation environment, and E be a typing environment. We say that S |= e : E with Γ iff Dom(e) ⊆ Dom(E) and for all x ∈ Dom(e), we have S |= e(x) : E(x) with Γ.