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

Polymorphism by name for references and continuations

This article investigates an ML-like language with byname semantics for polymorphism: polymorphic objects are not evaluated once for all at generalization time, but re-evaluated at each specialization. Unlike the standard ML semantics, the by-name semantics works well with polymorphic references and polymorphic continuations: the naive typing rules for references and for continuations are sound with respect to this semantics. Polymorphism by name leads to a better integration of these imperative features into the ML type discipline. Practical experience shows that it retains most of the efficiency and predictability of polymorphism by value.

Introduction

Polymorphic type disciplines like that of ML fit well within purely applicative languages. However, polymorphism becomes problematic when imperative features are added to a purely applicative kernel. In this paper, we consider two important imperative features: references (data structures that can be modified in-place); and first-class continuations (objects that capture the control state of the evaluator). In the ML community, it has long been known that the naive polymorphic typing for references is unsound; strong typing restrictions must be put on polymorphic references to ensure soundness [START_REF] Tofte | Type inference for polymorphic references[END_REF]. Recently, it has been shown that the natural polymorphic typing for continuations [START_REF] Duba | Typing first-class continuations in ML[END_REF] is unsound for similar reasons [START_REF] Harper | ML with callcc is unsound[END_REF][START_REF] Harper | Polymorphic type assignment and CPS conversion[END_REF].

In this paper, we show that these difficulties are not inherent to the polymorphic typing of references and continuations, but specific to the ML semantics for generalization and specialization (the two constructs that introduce polymorphism): when generalization and specialization are given alternate semantics, the simple polymorphic typings for references and continuations becomes sound. We call the ML semantics polymorphism by value, and the alternate semantics studied here polymorphism by name.

Generalization is the operation that transforms a term of type τ [α], where α is a type variable standing for an unknown type, into a term of type ∀α. τ [α]. Specialization is the operation that transforms a term of type ∀α. τ [α] into a term of type τ [σ], for some given type expression σ. With ML's polymorphism by value, generalization has strict semantics: it evaluates its argument once and for all, and the resulting value is shared between all specializations of the polymorphic term produced. With polymorphism by name, generalization has lazy semantics: it suspends the evaluation of its argument, and each specialization re-evaluates this suspension in the current context. Polymorphism by name is used in Quest [START_REF] Cardelli | Typeful programming[END_REF]; viewed as a restricted form of polymorphism, the "generics" of Clu or Ada also follows this semantics. Drawing the parallel with function application, polymorphism by value is analogous to call by value, and polymorphism by name is analogous to call by name. These two semantics for polymorphism cannot be distinguished in a purely applicative language without recursion: lambda-calculus with polymorphic typing is strongly normalizing. This is no longer true when we add imperative features to the core language. In particular, polymorphism by value makes it possible to access the same reference object or continuation object with two different types, which can compromise type safety; while this cannot happen with polymorphism by name, since specializations to the two types return two different references or continuations. This semantic difference has major consequences on the polymorphic typing discipline. With polymorphism by value, some typing restrictions must be put on generalization and/or on the constructs that build references and continuations to avoid the inconsistent use of one reference or continuation object with different types. Several polymorphic type systems have been proposed that achieve this goal [START_REF] Damas | Type assignment in programming languages[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Milner | The definition of Standard ML[END_REF][START_REF] Leroy | Polymorphic type inference and assignment[END_REF][START_REF] Wright | Typing references by effect inference[END_REF][START_REF] Talpin | The type and effect discipline[END_REF], but they are either overly restrictive (many useful polymorphic functions that use references or continuations are rejected), or complicated and hard to understand from the programmer's standpoint. In contrast, with polymorphism by name, the simple, intuitive polymorphic type disci-Semantics Implicit syntax Explicit syntax Naive polymorphic typing Polymorphism by value ML FX-87 [START_REF] Gifford | Integrating functional and imperative programming[END_REF] unsound

Polymorphism by name This work Quest, Clu, Ada sound Figure 1: Four approaches to polymorphism plines can be extended straightforwardly to references and continuations, and provide excellent support for the imperative programming style. This fact is folk lore, and the author does not claim originality for noticing it. It is briefly mentioned in several discussions of imperative languages with polymorphic type systems [START_REF] Gifford | Integrating functional and imperative programming[END_REF][START_REF] Cardelli | Typeful programming[END_REF]. This fact is also apparent in Harper and Lillibridge's recent work on CPS conversion for polymorphic languages [START_REF] Harper | Polymorphic type assignment and CPS conversion[END_REF][START_REF] Harper | Explicit polymorphism and CPS conversion[END_REF], which shows that an ML-like language (i.e. one with call by value and polymorphism by value) does not admit any type-preserving CPS transform, in contrast to languages with call by name or polymorphism by name.

The first aim of the present paper is to formally state this folklore result, by giving a soundness proof for Milner's type system with respect to the by-name semantics, including references and first-class continuations. This proof improves over previous soundness proofs for references in the setting of structural operational semantics [START_REF] Tofte | Type inference for polymorphic references[END_REF] by using only elementary techniques instead of more involving techniques such as co-induction.

The second aim is to clarify a confusion that appears in some of the works mentioned above: the confusion between the fact that polymorphism is given by-name semantics and the fact that polymorphism is explicit in the syntax. The explicit presentation of polymorphism consists in providing special syntactic constructs for generalization and specialization: for instance, abstraction over a type variable (Λα. e) and application of a term to a type (e τ ) in Girard's and Reynold's second-order lambda-calculus. Ada, Clu, Quest follow this approach. The alternate presentation consists in leaving these operations implicit in the source program, and to perform them silently at conventional program points. In the ML language, generalization is performed by the let construct, and specialization by referencing a variable. All existing languages with polymorphism by name have polymorphism explicit in the syntax. This leads Cardelli to write [START_REF] Cardelli | Typeful programming[END_REF]: Mutability [in Quest] interacts very nicely with all the quantifiers, including polymorphism [. . . ] The problems encountered in ML are avoided by the use of explicit polymorphism. This is misleading: mutable objects cause no difficulties in Quest because polymorphism follows the by-name semantics, not because it is explicit in the syntax. Indeed, the two semantics and the two syntactic presentations for polymorphism can be combined independently (see figure 1); but the fact that the simple polymorphic typing is sound is specific to the by-name semantics. To clearly make this point, this paper investigates a calculus with implicit polymorphism and by-name semantics for generalization and specialization. This calculus remains very close to the ML language, much closer than languages with explicit polymorphism, yet it safely supports the polymorphic typing of references and continuations without putting complicated restrictions over typing.

Our final aim is to discuss the practicality of polymorphism by name. Polymorphism by name is sometimes rejected a priori on the grounds of inefficiency [START_REF] Gifford | Integrating functional and imperative programming[END_REF], and also on the grounds that an imperative language with non-strict constructs is error-prone. The author's experience with a prototype implementation of ML with polymorphism by name suggests that these problems are minor in practice: polymorphism by name can be compiled just as efficiently as polymorphism by value in the most frequent cases; and programs that behave differently under the two semantics are quite rare.

The remainder of this paper is organized as follows. Section 2 informally introduces polymorphism by name, and shows how it interacts with references and continuations. Section 3 gives an operational semantics for this calculus, and shows the soundness of Milner's type system with respect to this semantics. Section 4 reports on the practicality of polymorphism by name.

Informal development

The let name binding

The let binding plays two roles in ML: type generalization and sharing of subcomputations. On the one hand, the expression let x = a in b generalizes the type of a, allowing x to be used in b with different instances of the type of a. On the other hand, this expression evaluates a once and for all, and shares the resulting value between all occurrences of x in b. The other ML binding construct, function abstraction, also performs sharing on the value of the function argument, but does not generalize its type (for reasons relevant to the type inference problem).

MLN, the variant of ML with polymorphism by name proposed in this paper, separates type generalization from value sharing. The let construct is replaced by the let name construct:

let name x = a in b.
This construct generalizes the type of a, giving a polymorphic type to x in b. In contrast with the usual let binding, the let name binding does not evaluate a immediately. Instead, the evaluation of a is suspended and is restarted each time x is referenced in b. In other terms, the MLN expression let name x = a in b behaves exactly like the ML expression

let x = λ(). a in b{x ← x()},
or equivalently like the textual substitution b{x ← a}.

Hence, in MLN, the two roles of the ML let are provided by separate constructs: the let name binding performs type generalization but does not share the corresponding value, while function abstraction performs value sharing, but does not generalize the corresponding type. The parallel is more apparent if we introduce the derived form let val x = a in b, which is syntactic sugar for (λx. b)(a). The let val binding shares the value of a between all occurrences of x in b, but does not generalize the type of a; hence, all occurrences of x in b are given the same type.

The semantics for let name are consistent with a well-known property of the ML type system [START_REF] Mitchell | Type systems for programming languages[END_REF]: that the expression let x = a in b has type τ if and only if the substitution b{x ← a} has type τ , provided x occurs in b. The let name construct carries this equivalence one step further: let name x = a in b not only typechecks but also behaves like the textual substitution b{x ← a}.

What have we gained by separating type generalization and value sharing into distinct constructs? In a purely applicative setting, nothing. Worse, we lose the ability to define polymorphic objects that are computed only once and shared among all their invocations. We shall discuss later how serious this restriction is for purely applicative programs. However, when we add imperative features such as references and continuations, the restriction has important benefits, as we shall see.

References are indirection cells whose contents can be physically updated. They model data structures that can be modified in-place. References are presented through the primitive operations ref(a), to create a fresh reference to a; and !a to access the contents of reference a; and a := b to update the contents of reference a by b. For typechecking, we introduce the type τ ref of references containing an object of type τ . The obvious typings for the operations over references are: With polymorphism by value, type safety can be compromised when a reference is given a non-trivial polymorphic type. Several restrictions of the ML type system have been proposed that rule out this situation [START_REF] Damas | Type assignment in programming languages[END_REF][START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Leroy | Polymorphic type inference and assignment[END_REF][START_REF] Wright | Typing references by effect inference[END_REF][START_REF] Talpin | The type and effect discipline[END_REF]. However, finding "the" right type system for ML with references is still an active research topic. The main difficulty is to give a type system that is correct but not overly restrictive.

τ → τ
On the one hand, it is not easy to statically control the propagation of references in a program. Since references are first-class values, they can be returned as function results, stored into data structures, passed through polymorphic functions, and even hidden inside function closures as in the following example.

let functional ref = λx. let r = ref x in (λ(). !r), (λy. r := y)
The function functional_ref creates a reference and disguises it as two functions, one for access, the other for update. The two functions returned seem totally unrelated, and there is not even a ref in their types. It is difficult to keep track of the reference hidden in these two functions.

On the other hand, the type system should not put overly strong restrictions over references whose types contain type variables. Otherwise, many useful polymorphic functions that use references are rejected, and the imperative programming style is poorly supported. Because of the two local references that hold intermediate results, most extensions of the ML type system give a more restrictive type to this function than to its purely applicative counterpart, even though the two functions compute exactly the same result. The most advanced extensions [START_REF] Leroy | Polymorphic type inference and assignment[END_REF][START_REF] Talpin | The type and effect discipline[END_REF] succeed in giving the same type to the two functions, but they require complex type algebras, where types reflect many operational properties of the functions. This conflicts with the use of types as partial specifications in module interfaces.

Polymorphism by name provides an indirect way to resolve this tension. With polymorphism by name, it is semantically impossible to create a reference and consider it with two different types. Consider again the first example above, with let replaced by let name: These examples show that polymorphism by name avoids type violations when polymorphic references are inconsistently used. However, it perfectly supports the consistent sharing of references inside polymorphic functions, even if these references have statically unknown types. For instance, in the case of the function reverse, the desired behavior is obtained by: The let val bindings for arg and res ensure that these identifiers are bound to the same references throughout the while loop. This causes no typing difficulties because arg and res are consistently used with the same type inside the loop. The outermost let name binding ensures that reverse is polymorphic. The fact that the closure representing this function will be rebuilt each time reverse is used, instead of being shared between all uses, is semantically transparent.

let name r = ref(λx. x) in r := (λx. x + 1); if (!r)(true) then . . . else . . . The test if (!r)(

First-class continuations

We now consider the addition of continuations as firstclass values to the core ML language. We closely follow the presentation adopted in the Standard ML of New Jersey implementation. This presentation and some alternatives are thoroughly discussed by Duba, Harper and MacQueen [START_REF] Duba | Typing first-class continuations in ML[END_REF], to which the reader is referred for a more gentle introduction to continuations in ML.

In SML-NJ, continuations are presented through the type τ cont of continuations expecting a value of type τ , and the two operations callcc(a), to capture the current continuation and pass it to the function a, and throw(a 1 , a 2 ), to restart the continuation a 1 on the value a 2 . The typings for these operations are, for all types τ and τ :

(τ cont → τ ) → τ for callcc τ cont × τ → τ for throw
These typings are sound in a simply-typed language [START_REF] Duba | Typing first-class continuations in ML[END_REF]. It had long been believed that they were also sound in the polymorphic type system of ML, until Harper and Lillibridge came up with a counterexample [START_REF] Harper | ML with callcc is unsound[END_REF]:

let later = callcc(λk. (λx. x, λf. throw(k, (f, λg. ()))
)) in print(first(later)("Hello world")); second(later)(λx. x + 1)

Everything typechecks with the typings above: later is given type ∀α, β. (α → α) × (α → α) → β, and therefore can be used with α instantiated to string in the first part of the sequence and with α instantiated to int in the second part. At run-time, the callcc construct binds k to the continuation later → print(first(later) . . .). Execution proceeds by applying the identity function to the string "Hello world", then by restarting the continuation k on the value v = ({λ}x{. }x + 1), ({λ}g{. ()}). A run-time type violation follows when trying to apply the first component of v to the string "Hello world". The reason is that the type of value v is less general than the type statically assumed for later in the body of the let. This situation is quite similar to the first example with references above: in both cases, static typing assumptions about identifiers bound to polymorphic objects are violated after the binding has changed, either because a reference was updated, or because a continuation was restarted.

This problem with polymorphic continuations can be avoided by typing restrictions similar to those for polymorphic references [START_REF] Wright | A syntactic approach to type soundness[END_REF][START_REF] Leroy | Typage polymorphe d'un langage algorithmique[END_REF]

Formalization

In this section, we formalize the calculus presented above, give its operational semantics, and show the soundness of Milner's typing rules with respect to the semantics.

Syntax

The language we consider is the core ML language enriched with references and continuations. We assume given a countable set of variable identifiers, ranged over by x. The terms of the calculus, ranged over by a, are described by the grammar below.

Expressions:

a ::= i integer constant | x variable identifier | λx. a function abstraction | a 1 (a 2 ) function application | let name x = a 1 in a 2 suspended binding | op(a)
unary operator application | op(a 1 , a 2 ) binary operator application Operators:

op ::= ref creation of a reference | deref access to a reference | assign modification of a reference | callcc capture the current continuation | throw invocation of a continuation
For the sake of simplicity, we have omitted conditional constructs and fixpoint operators in the calculus above.

It is straightforward to add typing and evaluation rules for conditionals. As for recursive functions, there is no need to introduce a built-in fixpoint operator, since recursive functions can be defined (albeit painfully) in terms of references and continuations. For instance, the expression below computes the fixpoint Y (λf. λx. a):

let val r = ref(λx. throw(k, 1
)) in r := λx. a{f ← !r}; !r (Here, k is assumed to be some dummy integer continuation previously captured. The function {λ}x{. }throw(k, 1) has type τ → τ for all types τ and τ , and therefore provides an initial value with the right type for the reference.)

Operational semantics

We now give a continuation semantics to the language above, in structured operational style. The rules in figure 3 define the evaluation predicate e/s a; k ⇒ r, meaning "in evaluation environment e and initial store s, the evaluation of the term a followed by the continuation k terminates on the answer r". The rules also define the auxiliary predicate s v k ⇒ r, meaning "in the initial store s, the value v passed to the continuation k produces the answer r". An answer is either a value and a modified store, or the constant wrong denoting a run-time type error. Evaluation environments map variables to values. These semantic objects are represented Values:

v ::= i integer constant | (x,
s[ ← v] k ⇒ r s v unop(ref, k) ⇒ r ∈ Dom(s) s( ) k ⇒ r s unop(deref, k) ⇒ r ∈ Dom(s) s[ ← v] v k ⇒ r s v binop2(assign, , k) ⇒ r e[x ← k]/s a; k ⇒ r s (x, a, e) unop(callcc, k) ⇒ r s v k 1 ⇒ r s v binop2(throw, k 1 , k) ⇒ r
If none of the conclusions of the rules above match:

e/s a; k ⇒ wrong s v k ⇒ wrong
E i : int E(x) = ∀α 1 . . . α n . τ E x : τ {α 1 ← τ 1 , . . . , α n ← τ n } E[x : τ ] a : τ E λx. a : τ → τ E a 1 : τ → τ E a 2 : τ E a 1 (a 2 ) : τ E a 1 : τ F V (τ ) \ F V (E) = {α 1 . . . α n } E[x : ∀α 1 . . . α n . τ ] a 2 : τ E let name x = a 1 in a 2 : τ E a : τ E ref(a) : τ ref E a : τ ref E deref(a) : τ E a 1 : τ ref E a 2 : τ E assign(a 1 , a 2 ) : τ E a : τ cont → τ E callcc(a) : τ E a 1 : τ E a 2 : τ cont E throw(a 1 , a 2 ) : τ Figure 4:
The typing rules as terms from the algebra defined by the grammar in figure 2. Store locations, ranged over by , are taken from a given infinite set of locations.

The evaluation rules can almost be read as the transitions of an abstract machine such as the CEK-machine [START_REF] Reynolds | Definitional interpreters for higherorder programming languages[END_REF][START_REF] Felleisen | Control operators, the SECD machine and the λ-calculus[END_REF] enriched with a store: the terms a represent the code component of the machine, the environments e represent the environment component, and the continuation terms k represent the stack. The judgement e/s a; k ⇒ r can be read as "initiate the computation of a, pushing the current state of the computation on k if necessary". The judgement s v k ⇒ r can similarly be read as "resume the saved computation on top of k over the value v".

The only rule that does not correspond closely to a transition of a CEK-like machine is the rule for let name. For the sake of simplicity, we have expressed the evaluation of let name x = a 1 in a 2 as the evaluation of the textual substitution a 2 {x ← a 1 }. An alternate presentation, closer to an actual execution model, is to bind x to the suspension (a 1 , e) during the evaluation of a 2 , and to evaluate this suspension each time x is referenced; this presentation is detailed in [12, chapter 6].

Type system

We now apply Milner's polymorphic type discipline to the language above. The typing rules are well known; we recall them in figure 4. The rules define the predicate E a : τ , meaning "under the assumptions E, the expression a has type τ ". Type expressions, type schemes and typing environments are defined by the grammar:

Type soundness

We are now in a position to show a Milner's style soundness result for the proposed calculus: no closed, welltyped term can evaluate to wrong. That is, a welltyped term either diverges or terminates with a normal response, but does not terminate on a run-time type violation.

Proposition 1 If [ ] a : τ and [ ]/[ ] a; stop ⇒ r, then r = wrong.
A simple, indirect proof of this claim is as follows. By rewriting all let name nodes in a by the rule

let name x = a 1 in a 2 ⇒ let x = λ(). a 1 in a 2 {x ← x()}
we transform a into a term a of ML with polymorphism by value that evaluates to wrong if and only if a evaluates to wrong. Moreover, the translation a is welltyped in Tofte's type system [START_REF] Tofte | Type inference for polymorphic references[END_REF], with all type variables taken to be imperative type variables. The main reason is that all let expressions bind non-expansive expressions. Then, proposition 1 follows from the "well-known fact" that Tofte's type system is sound for the core ML language extended with references and continuations.

Unfortunately, while the soundness of Tofte's system has been shown for ML plus references [START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Wright | A syntactic approach to type soundness[END_REF] and separately for ML plus continuations [START_REF] Wright | A syntactic approach to type soundness[END_REF], no formal soundness proof has been given for the combination of references and continuations. Hence this indirect argument is not satisfactory. A direct proof of the soundness claim is given in appendix. The proof is a considerable simplification over previous proofs of type soundness in the presence of a store, which rely either on complicated domain constructions [START_REF] Damas | Type assignment in programming languages[END_REF], or on definitions by greatest fixpoints and proofs by co-induction [START_REF] Tofte | Type inference for polymorphic references[END_REF].

The key idea, due to Tofte, is to appeal to the typing relation to define what it semantically means for a functional value to belong to a function type: instead of the usual condition "closure (x, a, e) belongs to type τ 1 → τ 2 iff it maps values of type τ 1 to values of type τ 2 ", we take that "closure (x, a, e) belongs to type τ 1 → τ 2 iff we can derive the typing judgement E λx. a : τ 1 → τ 2 for some typing environment E that agrees with the evaluation environment e".

We have extended this idea to the semantic typing of continuations: instead of the usual condition "continuation k belongs to type τ cont iff it never produces wrong when applied to a value of type τ ", we use structural induction over k and appeal to the typing rules. The resulting proof is elementary: it proceeds only by structural induction over the terms representing values and evaluation derivations. In particular, there is no need for proofs by co-induction [START_REF] Tofte | Type inference for polymorphic references[END_REF][START_REF] Milner | Co-induction in relational semantics[END_REF]. The proofs also easily extend to other polymorphic type systems for references and continuations [START_REF] Leroy | Typage polymorphe d'un langage algorithmique[END_REF].

Assessment

Polymorphism by name supports references and continuations in a type-safe way, while retaining the ML type algebra and typing rules, that are familiar and easy to understand. This is a strong advantage over the restricted type systems proposed for references and continuations in the setting of by-value semantics, which generally use richer type algebras and more complex typing rules. MLN, the variant of ML with polymorphism by name proposed in this paper, is therefore an interesting alternative to ML when imperative features are considered. However, MLN is not semantically equivalent to ML: since value sharing and type generalization are performed by distinct constructs in MLN, it is not possible to share the value of a polymorphic object. In this section, we discuss the practical consequences of this fact.

Differences in semantics

First of all, programs where polymorphic objects are computed by expressions with observable side-effects do not behave the same in ML and in MLN: the side-effects are performed once at creation-time in ML, but several times in MLN -once for each specialization. Example:

let name f = print("Hi!"); λx. x in f(f(f))
Evaluating this MLN phrase prints "Hi!" three times; the corresponding ML phrase prints "Hi!" only once. Here is another example, which assumes defined a stamp generator gensym:

let stamper = let stamp = gensym() in λx. (x, stamp) in . . .
In ML, the stamper function takes arguments of arbitrary types and pairs them with the stamp obtainedthe same stamp for all applications of stamper. The straightforward translation to MLN behaves differently:

let name stamper = let val stamp = gensym() in λx. (x, stamp) in . . .
Each application of stamper re-evaluates the expression defining stamper, and therefore calls gensym each time; hence, a different stamp is paired with each argument. To preserve the original behavior, the program must be rewritten as follows: let val stamp = gensym() in let name stamper = λx. (x, stamp) in . . . For more complex examples, deeper transformations might be required. However, these examples are rather artificial. In practice, polymorphic objects are most often defined by expressions that are side-effect free and that do not depend on the state, such as lambdaabstractions. In this case, the translation from ML to MLN is straightforward: it suffices to replace the let bindings by let name for polymorphic objects and let val otherwise, and the behavior of the program is preserved. For the experiments described below, the author translated about 10000 lines of ML programs to MLN this way, without encountering a single case where non-trivial transformations (as in the stamper example) were required.

Differences in efficiency

Even in the cases where it is safe to re-evaluate the expressions defining polymorphic objects, we may fear that this recomputation is a major source of inefficiency.

In practice, this is not the case, because in most programs the vast majority of polymorphic objects are defined as functions λx. a. The evaluation of these objects reduces to the construction of a closure, which is cheap. Moreover, the standard uncurrying techniques [1, section 6.2] can be used to avoid re-building the function closure when a polymorphic function is immediately applied. Consider the typical code fragment:

let name f = λx. a in . . . f(1) . . . f(true) . . .
This MLN program is compiled exactly as the following ML program:

let f = λ(). λx. a in . . . f()(1) . . . f()(true) . . .
That is, f is compiled as a curried function with two arguments, () and x. After uncurrying, the two curried applications are transformed into simple calls to a function with two arguments, which is as efficient as the direct application f(1) or f(true). (The extra cost of passing the unit argument can easily be avoided.)

However, there are some situations where a polymorphic object is expensive to compute. These situations correspond to the partial application of a curried function that performs a significant amount of computation between the passing of its first and second arguments. Binding the function returned by the partial application allows the sharing of this computation between all subsequent applications of the function. With polymorphism by name, this sharing is impossible if the result of the partial application must remain polymorphic.

Here is an example of this situation. Consider a function that sorts key-data pairs in increasing order for the keys. Assume that the keys and the associated data are not provided together, as a list of pairs, but separately, as a list of keys and a list of associated items. The function result is the permuted list of items. To take advantage of partial applications, the clever way to write this function is to compute the sorting permutation (e.g. a list of integers) as soon as the list of keys is given, and to return a function that simply applies the sorting permutation to the given list of items: Hence, the benefits of partial application are lost.

let

Experimental results

To evaluate more precisely the impact of polymorphism by name on real programs, the author has implemented a prototype compiler for ML with polymorphism by name, derived from his Caml Light system [START_REF]The Caml Light system, release 0.6. Software and documentation distributed by anonymous FTP on ftp[END_REF], which implements polymorphism by value. Deriving an MLN compiler from an ML compiler is straightforward: it suffices to transform the MLN expressions

let name x = a in b into ML expressions let x = λ(). a in b{x ← x()}
early in the compilation process; the remainder of the compiler need not be modified. Good performance crucially depend on the efficiency of the subsequent uncurrying phase, however. In the case of the Caml Light execution model [11, chap. Figure 5 gives some preliminary benchmark results for the Caml Light-based ML and MLN compilers. The test programs comprise, in addition to the usual toy programs, two medium-sized programs performing mostly symbolic processing, Boyer's simplified theorem prover and an implementation of the Knuth-Bendix completion algorithm, and two pieces of the Caml Light environment, adapted to polymorphism by name and bootstrapped, the lexical analyzer generator (1000 lines) and the compiler itself (8000 lines). Some of these programs are completely monomorphic (Fibonacci, word count). Others use polymorphic functions intensively (Church integers). The more realistic programs operate mostly on monomorphic data structures, but make frequent use of generic functions over lists, hash tables, etc.

The experimental results show that all programs, even the purely monomorphic ones that do not use Adapting such an ML compiler to MLN is straightforward: it suffices to transform let name x = a in b expressions into let val x = λ(). a in b{x ← x()} early in the compilation process, and let the uncurrying mechanisms work on this intermediate form.

These experimental results are encouraging: they show that an ML compiler with uncurrying mechanisms can easily be adapted to polymorphism by name, without major efficiency loss. The author believes that these results are not specific to the Caml Light implementation, but should apply to any ML compiler equipped with uncurrying mechanisms. Polymorphism by name cannot be dismissed easily on the grounds of inefficiency.

Conclusions

We have shown that by-name semantics for polymorphism can be integrated with an ML-like language, resulting in a simple solution to the problems raised by the polymorphic typing of references and continuations. This solution has two major advantages over the traditional "restricted polymorphism by value" approach, which consists in keeping polymorphism-by-value semantics and putting suitable typing restrictions over references and continuations. First of all, the type system assigns the same types to applicative and imperative implementations of the same function, which is crucial in the context of modular programming (in Standard ML, for instance, most polymorphic functions specified with an applicative type cannot be implemented in an imperative style). Moreover, this result is achieved while keeping the simple, familiar ML type algebra, in contrast with the most recent type systems for restricted polymorphism-by-value, such as effect systems [START_REF] Talpin | The type and effect discipline[END_REF] and closure typing [START_REF] Leroy | Polymorphic type inference and assignment[END_REF][START_REF] Leroy | Typage polymorphe d'un langage algorithmique[END_REF], which achieve the same results at the cost of complicated type algebras where type expressions are so informative that their use as specifications in module interfaces becomes problematic.

It is true that the polymorphism-by-name approach has some unfortunate drawbacks, such as its inability to express the sharing of some subcomputations of polymorphic values, but these drawbacks seem relatively minor in practice, compared with the drawbacks of the restricted polymorphism-by-value approach. We have presented some experimental evidence of this fact; more experience with polymorphism by name is needed to confirm the practicality of this approach.

A Proof of soundness

In this appendix, we sketch the proof of soundness of Milner's type system with respect to the semantics given in section 3.2.

We first formalize what it means for a value to semantically belong to some type, and for a continuation to semantically accept values of some type. We write these conditions S |= v : τ and S |= k :: τ , respectively. 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. The semantic typing relations are defined by structural induction over the terms representing values, continuations and evaluation environments, as follows: A store typing S extends a store typing S if Dom(S ) ⊇ Dom(S), and S ( ) = S( ) for all ∈ Dom(S). The semantic typing relations defined above are obviously stable under store extension; that is, if S |= v : τ and S extends S, then S |= v : τ , and similarly for the other semantic typing relations.

• S |= i : int • S |= (x, a, e) : τ 1 → τ 2 if
Proposition 2 Let a be a term, E a typing environment, τ a type expression, S a store typing, k a continuation, s a store, and r an answer. Proof. The proof is a simple, but tedious induction on the height of the evaluation derivation (the derivation of e/s a; k ⇒ r for (1); the derivation of s v k ⇒ r for (2)), and case analysis on a and k, respectively. We give the main cases; the remaining cases are similar.

Case (1) when a is let name x = a 1 in a 2 . From the typing derivation of E a : τ , we can construct a typing derivation of E a 2 {x ← a 1 } : τ [16, section 4.7.2]. The result follows from induction hypothesis (1) applied to the evaluation of a 2 {x ← a 1 }.

Case (1) when a is a 1 (a 2 ).

Let τ → τ be the type of a 1 . By definition of |= over apply1 continuations, we have S |= apply1(a 2 , e, k) :: τ → τ , taking E for the required typing environment. Applying the induction hypothesis (1) to the evaluation e/s a 1 ; apply1(a 2 , e, k) ⇒ r, we get r = wrong as expected.

Case (2) when k is apply1(a 2 , e 2 , k).

By hypothesis S |= k :: τ , we have τ = τ 1 → τ 2 and E 2 a : τ 1 and S |= e 2 : E 2 and S |= k :: τ 2 , for some τ 1 , τ 2 , E 2 . By hypothesis S |= v : τ , the value v is a closure (x, a 0 , e 0 ), and (3) E 0 λx. a 0 : τ 1 → τ 2 and ( 4) S e 0 : E 0 for some E 0 . Since v is a closure, the elimination rule for apply1 closures matches. From ( 3) and ( 4), we get S |= apply2(x, a 0 , e 0 , k) :: τ 1 . The expected result follows from induction hypothesis (1) applied to the evaluation e/s a 2 ; apply2(x, a 0 , e 0 , k) ⇒ r.

Case (2) when k is apply2(x, a, e, k).

By hypothesis S |= k :: τ , we have ( 5

  Consider the following function, which reverses a list iteratively: let reverse = λl. let arg = ref l in let res = ref [ ] in while not null(arg) do res := head(!arg) :: !res; arg := tail(!arg) done; !res

  true) re-evaluates ref({λ}x{. }x), resulting in a new reference to the identity function, different from the reference that was assigned the successor function in the previous line. Hence !r evaluates to the identity function, and no run-time type violation occurs. With let val instead of let name, the reference r would be given type (α → α) ref, where α is not generalized. Hence α is instantiated to int when typing the assignment, and typing the test leads to a static type error.The functional ref example proceeds similarly: the only way to do something harmful with functional ref is to apply it to a polymorphic object (e.g. the identity function), bind the two returned functions to variables, and use them with two different instantiations of their types:let (read, write) = functional ref(λx. x) in . . .Either the let is a let val, and identifiers read and write remain monomorphic; or the let is a let name, and functional ref({λ}x{. }x) is re-evaluated each time read or write are referenced, creating fresh, nonaliased references to the identity function each time.

  let name reverse = λl. let val arg = ref l in let val res = ref [ ] in while not null(arg) do res := head(!arg) :: !res; arg := tail(!arg) done; !res

Figure 3 :

 3 Figure 3: The evaluation rules

  Type expressions: τ ::= int the type of integers | α type variable | τ 1 → τ 2 function type | τ ref reference type | τ cont continuation type Type schemes: σ ::= ∀α 1 . . . α n . τ Typing environments: E ::= [x 1 : σ 1 , . . . , x n : σ n ]

  3], the very same code is generated for the MLN expression let name f = λx. a in . . . f(a ) . . . f(a ) . . . and for the corresponding ML expression let f = λx. a in . . . f(a ) . . . f(a ) . . . which is about the best we can expect.

1 .

 1 If E a : τ and S |= e : E and S |= k :: τ and |= s : S and e/s a; k ⇒ r, then r = wrong. 2. If S |= v : τ and S |= k :: τ and |= s : S and s v k ⇒ r, then r = wrong.

  ) E λx. a : τ → τ and (6) S |= e : E and S |= k :: τ for some E and some τ . Consider the environments e 1 = e[x ← v] and E 1 = E[x ← τ ]. By (6) and the hypothesis S |= v : τ , we have S |= e 1 : E 1 . Moreover, E 1 a : τ since this is the premise of the only typing rule that concludes (5). Hence we can apply induction hypothesis (1) to the evaluation e 1 /s a; k ⇒ r. Case (2) when k is unop(ref, k ). Let be the new location chosen by the evaluation rule. Consider the store typing S = S[ ← τ ]. We have |= s[ ← v] : S . Since / ∈ Dom(s) = Dom(S), the store typing S extends S. Hence S |= k :: τ implies S |= k :: τ , which means S |= k :: τ ref. The result follows by induction hypothesis (2) applied to the evaluation s[ ← v] |= k ⇒ r and to the store typing S . Case (2) when k is binop2(assign, v, k ). By hypothesis S |= k :: τ , we have S |= k :: τ , and the value v is a location such that S( ) = τ . Since |= s : S, it follows that ∈ Dom(s). By hypothesis S |= v : τ , we have |= s[ ← v] : S. Hence we can apply the induction hypothesis (2) to the evaluation s[ ← v] v k ⇒ r. It follows that r = wrong, as desired. Case (2) when k is unop(callcc, k ). By hypothesis S |= k :: τ , we have τ = τ cont → τ and S |= k :: τ . By hypothesis S |= v : τ , we have v = (x, a, e), with E λx. a : τ cont → τ and S e : E for some typing environment E. Consider the environments e = e[x ← k] and E = E[x ← τ cont]. We have S |= e : E and, given the typing rule for

  -with the same drawbacks: the corresponding type systems are either too restrictive or too complicated. Again, polymorphism by name provides an alternate solution. With by-name semantics for generalization, it is impossible to capture a continuation that generalizes the type of the value received by the continuation, as in Harper and Lillibridge's example, because polymorphism by name does not generalize the type of values, but only of suspended expressions. In the setting of polymorphism by name, Harper and Lillibridge's example becomes:

	let name later =
	callcc(λk. (λx. x,
	λf. throw(k, (f, λg. ()))))
	in print(first(later)("Hello world"));
	second(later)(λx. x + 1)

(Binding later with a lambda abstraction would result in a static type error.) The callcc expression defining later is evaluated twice, once for each reference to later, capturing different continuations than in the case of by-value semantics. In particular, the application second(later) binds k to the continuation later → second(later)({λ}x{. }x + 1), and the throw k restarts the program at that point, with second(later) bound to the harmless function {λ}g{. ()}. No run-time type violation occurs.

  Here, the intermediate function f is polymorphic (with type ∀α. α list → α list), and therefore can be applied to item lists of different types -without sorting again the list of keys each time. This last point holds in ML, but not in MLN. If f is to remain polymorphic, it must be bound by a let name construct; then, each application f(l) evaluates as

	weird sort (<) (lots of integers) (l)
	weird sort =
	λorder. λkeys.
	let permut = . . .
	in λitems. apply permut(permut, items)
	This is more efficient if several lists of items are to be
	ordered on the same list of keys:
	let f = weird sort (<) (lots of integers) in
	. . . f(lots of strings) . . .
	. . . f(lots of booleans) . . .

  there exists a typing environment E such that E λx. a : τ 1 → τ 2 and S e : E. |= apply1(a, e, k) :: τ 1 → τ 2 if there exists a typing environment E such that E a : τ 1 and S |= e : E and S |= k :: τ 2 .

	• S |= apply2(x, a, e, k) :: τ if there exists a typing
	environment E and a type τ such that E λx. a :

• S |= : τ ref if ∈ Dom(S) and S( ) = τ . • S |= k : τ cont if S |= k :: τ . • S |= stop :: τ for all types τ . • S τ → τ and S |= e : E and S |= k :: τ . • S |= unop(ref, k) :: τ if S |= k :: τ ref. • S |= unop(deref, k) :: τ ref if S |= k :: τ . • S |= binop1(assign, a, e, k) :: τ ref if there exists a typing environment E such that E a : τ and S |= e : E and S |= k :: τ . • S |= binop2(assign, v, k) :: τ if S |= v : τ ref and S |= k :: τ . • S |= unop(callcc, k) :: τ cont → τ if S |= k : τ . • S |= binop1(throw, a, e, k) :: τ cont if there exists a typing environment E such that E a : τ and S |= e : E. • S |= binop2(throw, v, k) :: τ if S |= v : τ cont. • S |= e : E if for all x ∈ Dom(e), E(x) is a simple type τ such that S |= e(x) : τ . • |= s : S if Dom(s) = Dom(S), and for all ∈ Dom(s), we have S |= s( ) : S( ).

Acknowledgments

The author is indebted to Didier Rémy for many discussions of the ideas in this paper. Many thanks to Benjamin Pierce for his editorial help.

function abstraction, E a : τ . The result follows by induction hypothesis (1) applied to the evaluation of e /s a; k ⇒ r.

By hypothesis S |= k :: τ , it follows that S |= k :: τ . Applying the induction hypothesis (2) to the evaluation S |= v k ⇒ r, we get the expected result.

2

Proposition 1 in section 3.4 immediately follows from property (1) in proposition 2, taking the empty map for e, E, s and S.