Xavier Leroy

Michel Mauny

Dynamics in ML

Objects with dynamic types allow the integration of operations that essentially require runtime type-checking into statically-typed languages. This article presents two extensions of the ML language with dynamics, based on our work on the CAML implementation of ML, and discusses their usefulness. The main novelty of this work is the combination of dynamics with polymorphism.

Introduction

Static typing (compile-time enforcement of the typing rules for a programming language) is generally preferred over dynamic typing (the production of run-time tests to check the rules), since static typing reports type violations earlier, and allows for the generation of more efficient code. However, one has to revert to dynamic typing for programs that cannot be recognized type-safe at compiletime. This situation often reveals weaknesses of the type system used. Dynamic typing could be avoided, then, by employing more advanced type systems. For instance, it had long been believed that generic functions (functions that can be applied to arguments of different types) can only be supported by dynamically-typed languages, such as Lisp, until the advent of polymorphic type disciplines, such as the one of ML, that permit static typing of such functions.

In contrast, there are programming situations that seem to require dynamic typing in an essential way. A first example is the eval function (and similar meta-level operations), that takes a character string, evaluates it as an expression of the language, and returns its value. The type of the returned value cannot be known at compile-time, since it depends on the expression given as argument. Another example is structured input/output. Some runtime systems provide an extern primitive that takes an object of any type and efficiently outputs a low-level representation of the object to persistent storage. The object can be read back later on, possibly in another process, by the intern primitive. The extern function can easily be typed in a polymorphic type system; but this is not the case for the intern function, since the type of its result depends on the contents of the file being read. In order to guarantee type safety, it is clear that the values returned by eval or by intern must carry some type information at run-time, and that this type information must be dynamically checked against the type expected by the context.

As demonstrated above, dynamic typing cannot be avoided for a few highly specific functions. But we would like to retain static typing for the huge majority of functions that can be typechecked at compile-time. What we need is a way to embed dynamic typechecking within a statically-typed language. The concept of objects with dynamic types, or dynamics, for short, as introduced by Cardelli [START_REF] Cardelli | Amber. In Combinators and Functional Programming Languages[END_REF], is an elegant answer to this need. A dynamic is a pair of a value v and a type expression τ , such that v has type τ . From the standpoint of static typing, all dynamics belong to the built-in type dyn. The type dyn represents those values that are self-described as far as types are concerned; that is, those values on which run-time type checking can be performed.

Continuing the examples above, the function eval naturally returns dynamics, so its static type is string → dyn. Similarly, intern has type io channel → dyn, and the extern function will be made to accept arguments of type dyn only, since the external representation of an object should now include its type.

Two constructs are provided to communicate between type dyn and the other types in the language. One construct creates dynamics by taking an object of any type and pairing it with its static type. The other construct checks the internal type of a dynamic against some static type τ , and, in case of success, gives access to the internal value of the dynamic with type τ .

In this paper, we consider the integration of dynamics, as described above, into the ML language [START_REF] Milner | The definition of Standard ML[END_REF]. The main novelty of this work is the combination of dynamics with a polymorphic type discipline. This combination raises interesting issues that have not been addressed yet. The main published references on dynamics have only considered first-order types [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF], or first-order types with subtyping [START_REF] Cardelli | Amber. In Combinators and Functional Programming Languages[END_REF][START_REF] Cardelli | The Modula-3 type system[END_REF]. Abadi et al. [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF] mention some of the problems involved with polymorphism, but briefly and informally. They reference a draft paper by Mycroft [21] that is said to consider the extension of ML with dynamics; this article has never been published, and we could not get a copy of it. Recently, Abadi et al. have proposed an extension to their earlier work that allows polymorphism and subtyping [START_REF] Abadi | Dynamic typing in polymorphic languages[END_REF]. We compare their proposals to ours in section 5 below.

The two extensions of ML with dynamics we present here are not mere proposals. The simpler one has been fully integrated into the CAML system [START_REF] Weis | The CAML reference manual[END_REF], the ML implementation developed at INRIA, for more than three years. It has grown to the point of stability where dynamics are used inside the CAML system. The second, more ambitious extension was also extensively prototyped in CAML. This practical experience enables us to discuss the main implementation issues involved by dynamics. It also gives some hints on the practical usefulness of dynamics in an ML system, both for user-level programming and system-level programming.

The remainder of this paper is organized as follows. Section 2 presents a first extension of ML with dynamics. After an informal presentation, we formalize typing and evaluation rules for dynamics within a significant subset of ML, show the soundness of typing with respect to evaluation, and discuss type inference and compilation issues. Section 3 extends the system previously described with the ability to destructure dynamics (both the type part and the value part), and rebuild dynamics with the components of the structure. We adapt the typing and evaluation rules of section 2 to this extension. Section 4 discusses the practical usefulness of the two systems, based on some significant uses of dynamics in the CAML environment. Finally, we mention some related work in section 5, and give concluding remarks in section 6.

Simple dynamics

This section describes dynamics as they are implemented in CAML release 2.6 and later [29, ch. 8].

Introduction and elimination constructs

The new construct dynamic a is provided to create dynamics. This construct evaluates a, and pairs it with (the representation of) the type inferred for a. For instance, dynamic 1 evaluates to (1, int), and dynamic true to (true, bool). In any case, the expression dynamic a is of type dyn, without any mention of the internal type of the dynamic.

To do anything useful with a dynamic, we must gain access to its internal value, bringing it back to the statically-typed world. A run-time type check is needed at that point to guarantee type safety. This check must ensure that the internal type of the dynamic does match the type expected by the context. This operation is called coercion of a dynamic. Coercion is traditionally presented as a special syntactic construct, such as the typecase construct in [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF]. This construct binds the internal value of the dynamic to some variable. It also handles the case where the run-time type check fails, and another coercion must be attempted, or an exception raised.

In ML, these two mechanisms, binding and failure handling, are already provided by the patternmatching machinery. Hence, instead of providing a separate coercion construct, we integrate dynamic coercion within pattern-matching. We introduce a new kind of pattern, the dynamic patterns, written dynamic(p : τ ). This pattern selects all dynamics whose internal value matches the pattern p, and whose internal type agrees with the type expression τ . For instance1 , here is a function that takes a dynamic and attempts to print it:

let print = function dynamic(x : int) → print int x | dynamic(s : string) → print string s | dynamic((x, y) : int × int) →
print string "("; print int x; print string ", "; print int y; print string ")" | x → print string "?"

Creation of polymorphic dynamics

The introduction of dynamics in a polymorphic type system raises some issues that do not appear in the case of a monomorphic type system. In this section, we show that some restrictions must be put on dynamic creation; the next section deals with the semantics of type matching during dynamic coercion.

It is allowed to create a dynamic of an object with a polymorphic type, provided the type is closed : none of the type variables free in the type should be free in the current typing environment. For instance, dynamic(function x → x) is perfectly legal, since the identity function has type α → α, and α is a fresh type variable that does not appear anywhere else (in the case of a principal typing). It will be possible to use the internal value of the dynamic with all type instances of α → α.

On the other hand, function x → dynamic x is rejected: dynamic x is typed in the environment x : α, where x does not have a closed type. In this case, it is impossible to determine at compile-time the exact type of the object put into the dynamic: static typing says it can be any instance of α, that is, any type. To correctly evaluate the function above, the actual type to which α is instantiated would have to be passed at run-time. Since polymorphic functions can be nested arbitrarily, this means that all polymorphic functions, even those that do not build dynamics directly, would have to take type expressions as extra parameters, and propagate these types to the polymorphic functions they call.

Besides complicating compilation and raising efficiency issues, passing type information at runtime is essentially incompatible with the ML semantics, because it implies "by-name" semantics for polymorphism instead of ML's "by-value" semantics for polymorphism, in the terminology of [START_REF] Leroy | Polymorphism by name for references and continuations[END_REF]. In other terms, the extra abstractions that must be inserted at generalization points to pass type information around cause the evaluation of polymorphic expressions to be delayed until instantiation-time, and therefore side-effects can occur at different times than in ML. Assume for instance that the following expression is not rejected:

let f = function x → (print"Hi!"; function y → dynamic(x, y)) in let g = f(1) in (g(1), g(true))
To correctly propagate type information, the compiler must insert extra abstractions over type representations and the corresponding applications, as follows:

let f = function τ → function τ → function x → (print"Hi!"; function y → dynamic(x, y : τ × τ )) in let g = function τ → f(int)(τ )(1) in (g(int)(1), g(bool)(true))
No other placement of abstractions and applications is possible, since abstractions and applications must correspond to the points where generalization and instantiation take place. Hence, the program above prints "Hi!" twice, instead of once as in core ML. Besides this change in semantics for the let construct, allowing dynamics to be created with non-closed types also destroys the parametricity properties of the ML type system. It is wellknown that, since polymorphic functions can only operate uniformly over objects whose type is a type variable, all functions with a given polymorphic type obey some algebraic laws that depend only on the type [START_REF] Wadler | Theorems for free! In Functional Programming Languages and Computer Architecture[END_REF][START_REF] Harry | Outline of a proof theory of parametricity[END_REF]. For instance, all functions f with type ∀α. α list → α list are such that, for all functions g and lists l,

map g (f l) = f (map g l).
This captures the fact that a function f with the type above can only reorder, duplicate and remove some elements from the given list, regardless of the actual value of the elements; hence we get the same results if we apply an arbitrary transformation g to each element of the list either before applying f or after. This is no longer true if we add dynamics without typing restrictions: the function f defined by

let f = function l → match (dynamic l) with dynamic(m : int list) → reverse l | d → l would have type ∀α. α list → α list, yet map string of int (f [1; 2]) = ["2"; "1"] f(map string of int [1; 2]) = ["1"; "2"]
The closedness condition on dynamic creation rules out the f function above. More generally, it is conjectured that the closedness condition suffices to guarantee that similar parametricity results hold for ML plus dynamic and for core ML.

Coercion of polymorphic dynamics

For type matching in the presence of polymorphic types, two behaviors can be considered. The first one is to require that the internal type of the dynamic be exactly the same as the expected type, up to a renaming of type variables. The other behavior is to also accept any dynamic whose internal type is more general than the expected type. For instance, dynamic [ ], whose internal type is ∀α. α list, matches the pattern dynamic(x : int list) with the latter behavior, but not with the former. We have retained the latter behavior, since it seems more coherent with the statically-typed part of the ML language (where e.g. the empty list can be used in any context that expects a list of integers). Type patterns are allowed to require a polymorphic type, as in dynamic(f : α → α). This pattern matches any dynamic whose internal type is as general or more general than the type in the pattern (e.g. β → β, or β → γ). As a consequence of this semantics, identifier f can safely be used with different instances of the type α → α in the right-hand side of the pattern-matching, as in:

function dynamic(f : α → α) → f f
The type matching semantics guarantee that f will be bound at run-time to a value that belongs to all instances of the type scheme α → α. (This is the only case in ML where a variable bound by a function construct can be used with several types inside the function body.)

In the example above, the type variable α is not a regular pattern variable such as f: it is implicitly quantified universally by the dynamic pattern, and therefore cannot be instantiated during the matching process. For instance, the pattern dynamic(x : α list) matches only a dynamic of the polymorphic empty list, not any dynamic of any list. As a consequence, a type pattern τ more general than a type pattern τ will match fewer dynamics than τ , in contrast with regular ML patterns. This means that in a dynamic matching, the most general type patterns must come first. To catch polymorphic lists as well as integer lists, one must write In the latter definition, the second case would never be selected, since the first case also matches dynamics with internal type α list.

Syntax

We now formalize the ideas above, in the context of the core ML language, enriched with patternmatching and dynamics. The syntax of the language is as follows:

Type expressions: To precisely define the semantics of dynamic expressions, we need to keep track of the type given to their arguments during typechecking. For this purpose, we introduce annotated expressions (typical element b), that have the same syntax as raw expressions a, except that the dynamic expressions also contain the type of their argument. More precisely, dynamic expressions are annotated by a type scheme: a type expression with some variables universally quantified.

τ ::= int a base type [] α type variable [] τ 1 → τ 2 function type [] τ 1 × τ 2 product
::= x [] function p 1 → b 1 | . . . | p n → b n [] dynamic (b 1 : σ) [] . . .
Type schemes are identified up to a permutation or renaming of bound variables. Trivial type schemes ∀.τ are written τ , and identified with type expressions.

Typechecking

The typing rules for this calculus are given in figure 1. Most of the rules are just those of the core ML language, revised to take pattern-matching into account in function definitions. Two additional rules present the creation and coercion of dynamics.

The rules define the predicate E a : τ ⇒ b, meaning "expression a has type τ in the typing environment E". The b component can be viewed as the typed completion of a (the input expression): b is an annotated expression, with the same structure as a, that records the types

(1) E i : int ⇒ i (2) τ ≤ E(x) E x : τ ⇒ x (3) p k : τ ⇒ E k E + E k a k : τ ⇒ b k (k = 1, . . . , n) E function . . . | p k → a k | . . . : τ → τ ⇒ function . . . | p k → b k | . . . (4) E a 1 : τ → τ ⇒ b 1 E a 2 : τ ⇒ b 2 E a 1 a 2 : τ ⇒ b 1 b 2 (5) E a 1 : τ 1 ⇒ b 1 E a 2 : τ 2 ⇒ b 2 E (a 1 , a 2 ) : τ 1 × τ 2 ⇒ (b 1 , b 2 ) (6) E a 1 : τ 1 ⇒ b 1 E + [x → Clos(τ 1 , F V (E))] a 2 : τ ⇒ b 2 E let x = a 1 in a 2 : τ ⇒ let x = b 1 in b 2 (7) E a : τ ⇒ b F V (τ ) ∩ F V (E) = ∅ E dynamic a : dyn ⇒ dynamic(b, Clos(τ, ∅)) (8) x : τ ⇒ [x → τ ] (9) i : int ⇒ [ ] (10) p : τ ⇒ E p : τ ⇒ E (p, p ) : τ × τ ⇒ E ⊕ E (11) p : τ ⇒ E dynamic(p : τ ) : dyn ⇒ Clos(E, ∅)
Figure 1: Typing rules given to the arguments of dynamic expressions. The rules make use of an auxiliary predicate, p : τ ⇒ E, meaning "pattern p has type τ and enriches the type environment by E". Here, E stands for a finite mapping from variable names to type schemes.

Some notations on maps. The empty map is written [ ]. The map that associates σ to x and is undefined on other variables is written [x → σ]. The asymmetric join of two maps E 1 and E 2 is written E 1 + E 2 ; it is asymmetric in the sense that if x belongs to the domain of E 1 and to the domain of E 2 , we take (E 1 + E 2 )(x) = E 2 (x) and ignore E 1 (x). The symmetric join of E 1 and E 2 is written E 1 ⊕ E 2 ; it is undefined if the domains of E 1 and E 2 are not disjoint.

We write F V (τ ) for the set of all type variables that appear in the type expression τ . For type schemes, we take F V (σ) to be the type variables free in σ:

F V (∀α 1 . . . α n . τ ) = F V (τ )\{α 1 . . . α n }.
Similarly, F V (E) is the union of the free variables of all type schemes in the codomain of E.

We write τ ≤ σ to express that type τ is an instance of type scheme σ; that is, writing σ = ∀α 1 . . . α n . τ , we have τ = τ {α 1 ← τ 1 . . . α n ← τ n } for some types τ 1 . . . τ n .

Finally, Clos(τ, V ) stands for the closure of type τ with respect to those type variables not in the set V . It is defined by

Clos(τ, V ) = ∀α 1 . . . α n .τ , where {α 1 , . . . , α n } is F V (τ ) \ V .
The Clos operator is extended pointwise to type environments.

The only rules that significantly differ from those of the core ML language are rule 7, that deals with dynamic creation, and rule 11, that deals with dynamic coercion. Rule 7 says that the expression dynamic(a) has type dyn, provided that a has a type τ that can be closed: none of the free variables of τ are free in the current typing environment E. The completion of dynamic a is dynamic(b : σ), where b is the completion of a, and σ the type scheme obtained by generalizing all variables free in τ , that is, Clos(τ, ∅).

Rule 11 says that the pattern dynamic(p : τ ) matches values of type dyn, provided that p matches values of type τ . Assume p binds variables x 1 . . . x n to values of types τ 1 . . . τ n . Then, dynamic(p : τ ) binds the same variables to the same values. As described above, all type variables free in τ 1 . . . τ n can be generalized. Hence, we take that dynamic(p : τ ) binds x 1 . . . x n to values of types Clos(τ 1 , ∅) . . . Clos(τ n , ∅).

One might be surprised by the fact that the types τ 1 . . . τ n are generalized independently. For instance, the pattern dynamic(f, g

: (α → α) × (α → α)) results in the environment [f : ∀α. α → α, g : ∀β. β → β]
(after renaming α to β in the second type scheme), and the information that the types of f and g share the same α has been lost. Actually, this makes no difference, because the type schemes ∀α.

(α → α) × (α → α) and ∀α, β. (α → α) × (β → β)
are isomorphic: all terms belonging to one type scheme also belong to the other [START_REF] Di | Type isomorphisms in a type-assignment framework[END_REF]. The isomorphisms between polymorphic product types justify the independent generalization of the components of E in rule 11.

An important property of the ML type system is the stability of typing judgements under substitutions [START_REF] Damas | Principal type-schemes for functional programs[END_REF]. The typing predicate defined above also enjoys this property.

Proposition 1 If E a : τ ⇒ b, then ϕ(E) a : ϕ(τ ) ⇒ b for all substitutions ϕ.
Proof: First, we check that if p : τ ⇒ E, then p : ϕ(τ ) ⇒ ϕ(E). This is an easy inductive argument on p. The case where p is a dynamic pattern follows from the fact that ϕ(Clos(E, ∅)) = Clos(E, ∅), since Clos(E, ∅) has no free variables. Then, proposition 1 follows from a well-known inductive argument on a [20, section 4.7.2]. We give only the new case: a = dynamic a 1 . In this case, the typing derivation is:

E a : τ ⇒ b F V (τ ) ∩ F V (E) = ∅ E dynamic a : dyn ⇒ dynamic(b : Clos(τ, ∅))
By renaming if necessary, we can assume that none of the free variables of τ are (1) in the domain of ϕ, and (2) free in ϕ(E). This renaming does not modify E, since F V (τ )∩F V (E) = ∅. Applying the induction hypothesis, we get a proof of ϕ(E) a : ϕ(τ ) ⇒ b. We have ϕ(τ ) = τ by hypothesis (1), and

F V (τ ) ∩ F V (ϕ(E)) = ∅ by hypothesis (2). Hence we can conclude ϕ(E) dynamic a : dyn ⇒ dynamic(b : Clos(τ, ∅))
, which is the expected result. 2

Evaluation

We now give call-by-value operational semantics for our calculus. Annotated expressions b are mapped to responses (ranged over by r). Responses are either values, or the constant wrong that denotes run-time type violations. Values (v) are terms with the following syntax: Since most rules are similar to those of ML [START_REF] Milner | The definition of Standard ML[END_REF], we only detail the two rules dealing with dynamics. Rule 18 expresses that evaluating dynamic(b : σ) amounts to evaluating b and pairing its value with σ, the static type of b. Rule 29 defines the semantics of pattern matching over dynamics. The internal type scheme σ of the dynamic is required to be more general than the type τ expected by the pattern: the type τ must be an instance of the type scheme σ, in the sense

Values: v ::= cst(i) integer value [] pair(v, v ) value pair [] dynamic(v : σ) dynamic value [] clos(e, p 1 → b 1 | . . . | p n → b n ) function closure
(12) e x * → e(x) (13) e i * → cst(i) (14) e function . . . | p k → b k | . . . * → clos(e, . . . | p k → b k | . . .) (15) e b * → clos(e , . . . | p k → b k | . . .) e b * → v v < p k * → e e + e b k * → r k minimal e b b * → r (16) e b 1 * → v 1 e b 2 * → v 2 e (b 1 , b 2 ) * → pair(v 1 , v 2 ) (17) e b 1 * → v e + [x → v] b 2 * → r e let x = b 1 in b 2 * → r (18) e b * → v e dynamic(b : σ) * → dynamic(v : σ) (19) e b * → v v = clos(e, . . .) e b b * → wrong (20) e b * → wrong e b b * → wrong (21) e b * → clos(e 1 , p 1 → b 1 | . . . | p n → b n ) e b * → v v < p k * → wrong e b b * → wrong (22
(26) v < x * → [x → v] (27) cst(i) < i * → [ ] (28) v 1 < p 1 * → e 1 v 2 < p 2 * → e 2 pair(v 1 , v 2 ) < (p 1 , p 2 ) * → e 1 ⊕ e 2 (29) v < p * → e τ ≤ σ dynamic(v : σ) < dynamic(p : τ ) * → e (30) v = cst(i ) v < i * → wrong (31) v = pair(v 1 , v 2 ) v < (p 1 , p 2 ) * → wrong (32) v 1 < p 1 * → wrong pair(v 1 , v 2 ) < (p 1 , p 2 ) * → wrong (33) v 2 < p 2 * → wrong pair(v 1 , v 2 ) < (p 1 , p 2 ) * → wrong (34) v = dynamic(v : σ) v < dynamic(p : τ ) * → wrong (35) τ ≤ σ v < p * → wrong dynamic(v : σ) < dynamic(p : τ ) * → wrong

Soundness

In this section, we show that the typing rules are sound with respect to the evaluation rules: the evaluation of a well-typed program never stops because of a run-time type error, such as trying to apply an integer as if it were a function. In this situation, the evaluation rules given above associate wrong to the program. We now show that this cannot occur to a well-typed program.

Proposition 2 Let a 0 be a program (a closed expression). If [ ] a 0 : τ 0 ⇒ b 0 for some type τ 0 , then we cannot derive [ ] b 0 * → wrong.
To prove this result, we first define a semantic typing relation, |= v : τ , saying whether the value v semantically belongs to the type τ . The relation is defined by structural induction on v, as follows.

• |= cst(i) : τ if and only if τ = int • |= pair(v 1 , v 2 ) : τ if and only if τ = τ 1 × τ 2 and |= v 1 : τ 1 and |= v 2 : τ 2 • |= clos(e, p 1 → b 1 | . . . | p n → b n ) : τ if and only if τ = τ 1 → τ 2 and
p 1 → a 1 | . . . | p n → a n ) : τ 1 → τ 2 ⇒ (function p 1 → b 1 | . . . | p n → b n ) • |= dynamic(v : σ) : τ if and only if τ = dyn and |= v : σ.
The use of the typing relation to define |= over functional values is taken from [START_REF] Tofte | Type inference for polymorphic references[END_REF]. The semantic typing relation extends to type schemes and to environments: Proof: By induction over p. The cases p = x and p = i are obvious. If p = (p 1 , p 2 ), then the last rule applied in the typing derivation is For the case p = dynamic(p 1 : τ 1 ), the last rule applied in the typing derivation is Proof: By induction over the length of the evaluation, and case analysis over a. We show one base case and two inductive cases; the other cases are similar. If a = x, the rule used in the typing derivation is

• |= v : σ if
p 1 : τ 1 ⇒ E 1 p 2 : τ 2 ⇒ E 2 (p 1 , p 2 ) : τ 1 × τ 2 ⇒ E 1 ⊕ E 2 with τ = τ 1 × τ 2 and E = E 1 ⊕ E 2 . By hypothesis |= v : τ 1 × τ 2 , we have v = pair(v 1 , v 2 ) with |= v 1 : τ 1 and
p 1 : τ 1 ⇒ E 1 dynamic(p 1 : τ 1 ) : dyn ⇒ Clos(E 1 , ∅) with τ = dyn and E = Clos(E 1 , ∅). By definition of |=, we have v = dynamic(v 1 : σ) and
τ ≤ E(x) E x : τ ⇒ x
The only possible evaluation is e x * → e(x). Hence, r = e(x) = wrong. By hypothesis |= e : E, we have |= e(x) : E(x). Since τ ≤ E(x), this implies |= e(x) : τ , which is the expected result. If a = let x = a 1 in a 2 , the last typing rule used is

E a 1 : τ 1 ⇒ b 1 E + [x → Clos(τ 1 , F V (E))] a 2 : τ ⇒ b 2 E let x = a 1 in a 2 : τ ⇒ let x = b 1 in b 2
→ v e + [x → v] b 2 * → r e let x = b 1 in b 2 * → r
Applying the induction hypothesis to the evaluation of b 1 , we get

|= v : τ 1 . By proposition 3, this implies |= v : Clos(τ 1 , F V (E)). Hence |= e + [x → v] : E + [x → Clos(τ 1 , F V (E))],
and we can apply the induction hypothesis to the evaluation of b 2 . This leads to the expected result: r = wrong and |= r : τ 2 .

If a = dynamic a 1 , the last typing rule used is

E a 1 : τ 1 ⇒ b 1 F V (τ 1 ) ∩ F V (E) = ∅ E dynamic a : dyn ⇒ dynamic(b 1 , Clos(τ 1 , ∅))
There

Type reconstruction

Unlike the ML type system, the type system presented above does not possess the principal type property. This fact is due to the closedness condition in the rule for dynamic expressions. Consider the expression function x → dynamic x. It has types int → dyn, and dyn → dyn, and more generally τ → dyn for all closed types τ ; but the lower bound of all these types, α → dyn, is not a valid type for the function, since it corresponds to the construction of a dynamic with a statically unknown type. Such programs must be statically detected, and rejected as ambiguous: they have no well-defined semantics. The programmer must put more type constraints to unambiguously state what the program should do.

P (i) = (int, [ ]) P (x) = (α, [x → α])
where α is a fresh type variable

P (p 1 , p 2 ) = (τ 1 × τ 2 , E 1 ⊕ E 2 )
where (τ 1 , E 1 ) = P (p 1 ) and (τ 2 , E 2 ) = P (p 2 )

P (dynamic(p 1 : τ )) = (τ, θE 1 )
where (τ 1 , E 1 ) = P (p 1 ) and θ is such that

θτ 1 = τ W (i, E) = (int, id, ∅) W (x, E) = (τ {α 1 → β 1 , . . . , α n → β n }, id, ∅)
where E(x) = ∀α 1 . . . α n . τ and β 1 , . . . , β n are fresh variables

W ((function p 1 → a 1 | . . . | p n → a n ), E) = (τ → τ , ϕ, D) where (τ k , E k ) = P (p k ) for k = 1, . . . , n and µ = mgu(τ 1 , . . . , τ n ) and (τ 1 , ϕ 1 , D 1 ) = W (a 1 , E + µ E 1 ) and (τ 2 , ϕ 2 , D 2 ) = W (a 2 , ϕ 1 (E + µ E 2 )) and . . . and (τ n , ϕ n , D n ) = W (a n , ϕ n-1 . . . ϕ 1 (E + µ E n )) and µ = mgu(ϕ n . . . ϕ 2 τ 1 , . . . , ϕ n τ n-1 , τ n ) and ϕ = µ • ϕ n • • • • • ϕ 1 • µ and τ = ϕτ 1 and τ = µ τ n and D = µ ϕ n . . . ϕ 2 D 1 ∪ . . . ∪ µ ϕ n D n-1 ∪ µ D n W (a 1 (a 2 ), E) = (µα, µ • ϕ 2 • ϕ 1 , µϕ 2 D 1 ∪ µD 2 ) where (τ 1 , ϕ 1 , D 1 ) = W (a 1 , E) and (τ 2 , ϕ 2 , D 2 ) = W (a 2 , ϕ 1 E) and µ = mgu(ϕ 2 τ 1 , τ 2 → α)
with α being a fresh variable

W (let x = a 1 in a 2 , E) = (τ 2 , ϕ 2 • ϕ 1 , ϕ 1 (D 1 ) ∪ D 2 ) where (τ 1 , ϕ 1 , D 1 ) = W (a 1 , E) and (τ 2 , ϕ 2 , D 2 ) = W (a 2 , ϕ 1 E + x → ∀α 1 . . . α n . τ 1 ) with {α 1 . . . α n } = F V (τ 1 ) \ F V (ϕ 1 E) \ F V (D 1 ) W (dynamic(a 1 ), E) = (dyn, ϕ 1 , D 1 ∪ (F V (τ 1 ) ∩ F V (ϕ 1 E))) where (τ 1 , ϕ 1 , D 1 ) = W (a 1 , E) W ((a 1 , a 2 ), E) = (ϕ 2 τ 1 × τ 2 , ϕ 2 • ϕ 1 , ϕ 2 D 1 ∪ D 2 ) where (τ 1 , ϕ 1 , D 1 ) = W (a 1 , E) and (τ 2 , ϕ 2 , D 2 ) = W (a 2 , ϕ 1 E)

Figure 3: The type reconstruction algorithm

There is a slight technical difficulty in detecting ambiguous programs. For the dynamic a construct, it would not be correct to infer the most general type τ for a, and fail immediately if some variables in τ are free in the current typing environment: these variables may later be instantiated to closed types. Consider the expression (function x → dynamic x) [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF]. Assuming the function part of the application is typed before the argument, the function is given type α → dyn, and dynamic x appears to build a dynamic with non-closed type α. But when the application is typed, α is instantiated to int, and we know that the dynamic is created with internal type int. Hence, the closedness check must be delayed until the end of type inference. The idea is as follows: when typing dynamic a, we record all type variables that are free in the inferred type for a and in the current typing environment. At the end of typechecking, all type variables in this set must be instantiated to closed types.

This process can be formalized as a simple extension of the Damas-Milner algorithm W [START_REF] Damas | Principal type-schemes for functional programs[END_REF]. The algorithm is shown in figure 3. It takes as input an expression a and an initial typing environment E. It outputs a type τ (the type inferred for a), a substitution ϕ (recording instantiations performed on E), and a set D of type expressions that keeps track of ambiguous dynamic constructions. 2Each time a dynamic(a) expression is typed, all type variables free in the inferred type for a and in the current typing environment are added to D. For expressions of other kinds, D is simply carried around; the instantiations performed on E are also performed on D. Variables free in D are prevented from being generalized.

If the algorithm fails, the program is not well-typed. If the algorithm succeeds with D containing only closed types, then τ is the most general type for the program. If the algorithm succeeds, but D contains non-closed types, then the program is ambiguous; however, it has type ψ(τ ) for all substitutions ψ such that ψ(D) contains only closed types.

For dynamic patterns dynamic(p : τ ), the expected type τ is given explicitly in the pattern, so there is actually nothing to infer. We just check that the pattern p is of type τ , and record the (polymorphic) types of the variables bound by p. We have considered inferring τ from the pattern p and the right-hand side a of the pattern-matching, but this seems quite difficult, since variables bound by p can be used with several different types in a.

Compilation

In the current CAML implementation, internal types of dynamics are represented by the following term-like structure:

type gtype = Gvartype of int | Gconsttype of int × gtype list
Type constructors are identified by unique stamps instead of names to correctly handle type redefinition. Type variables are also encoded as integers. All type variables are assumed universally quantified. The code generated for dynamic(b : σ) simply pairs the value of a with the structured constant representing a trivial instance of σ as a gtype. For pattern matching, CAML provides a library function ge gtype, that takes two types and tests whether the first one is more general than the second one. The code generated for pattern matching on dynamics simply calls ge gtype with the internal type of the dynamic, and the expected type (again, a structured constant of type gtype). The sequence of tests matching the internal value against the pattern is entered only when ge gtype returns true. Those tests were compiled assuming that the value being tested belongs to the expected type for the dynamic; therefore, it would be incorrect to match the internal value first, and then the internal type.

To speed up run-time type tests, we could switch to the following representation for internal types of dynamics:

type gtype = Gvartype of gtype option ref | Gconsttype of int × gtype list
This representation makes it possible to perform instantiations by physical modifications on the type, which is more efficient than recording them separately as a substitution [START_REF] Cardelli | Basic polymorphic typechecking[END_REF]. These physical modifications are reversed at the end of matching.

To make dynamic coercions even faster, we could perform partial evaluation on the ge gtype predicate, since its second argument is always known at compile-time. Conventional patternmatching compilation techniques [START_REF] Peyton-Jones | The implementation of functional programming languages[END_REF] do not apply directly, however, since they consist in specializing term-matching predicates on their first argument (the more general term), not on the second one (the less general term). Specializing a matching predicate such as ge gtype on its second argument is actually just as difficult as the more general problem of specializing a unification predicate on one of its arguments. The latter problem has been extensively studied in the context of Prolog compilation. A popular solution is the Warren Abstract Machine and its compilation scheme [START_REF] David | An abstract Prolog instruction set[END_REF][START_REF] Maier | Computing with logic: logic programming with Prolog[END_REF][START_REF] Aït-Kaci | The WAM: a real tutorial[END_REF]. Most of the techniques developed there apply to our problem. We shall detail this issue at the end of section 3.6

Non-closed types in dynamic patterns

This section presents an extension of the system presented above that makes it possible to match dynamic values against dynamic patterns with incomplete type information. This enables destructuring dynamics without specifying their exact type.

Presentation

With the previous system, the internal value of a dynamic can only be extracted with a fixed type. This turns out to be insufficient in some cases. Let us continue the print example of section 2.1. For product types, we would like to have a single case that matches all dynamics of pairs, prints the parentheses and comma, and recursively calls the print function to print the two components of the pair. This cannot be done with the system above: the pattern dynamic((x, y) : α × β) will only match dynamics whose internal type is at least as general as ∀α∀β. α × β, definitely not all dynamics whose internal type is a pair type. What we need is to have type variables in dynamic patterns that are not universally quantified, but rather existentially quantified, so that they can be bound to the corresponding parts of the internal type of the dynamic.

We now give a more complete version of the print function, with explicit universal and existential quantification for type variables in dynamic patterns. We will use it as a running example in this section. static type contains a variable α existentially bound, it is possible to build a dynamic from this object. The internal type of the dynamic will be the "true" type for a: its static type where the binding of α has been performed. Cases (3) and ( 5) in the print function illustrate this feature: when the matching with ∃α. dynamic(x :: l : α list) succeeds, two dynamics are created, dynamic x with internal type the type τ bound to α; and dynamic l with internal type τ list. This transforms a dynamic of a non-empty list into the dynamic of its head and the dynamic of its tail, thus allowing recursion on the list.

Mixed quantifications

Existentially quantified variables can be freely mixed with universally quantified variables inside type patterns. Then, the semantics of the matching depends on the relative order in which these variables are quantified. This is illustrated by cases ( 7) and (8) in the print example -two modest attempts at printing functional values.

In case [START_REF] Cardelli | The Modula-3 type system[END_REF], the pattern is ∃α.∀β. dynamic(f : α → β). Since α is bound before β, the variable α matches only type expressions that do not depend on β. For instance, a dynamic with internal type ∀γ. γ → γ is rejected. The functions selected by the pattern above are exactly those returning a value of type β for all β. Since no such value exists in ML, the selected functions never terminate normally, hence they are printed as function x → ⊥.

In case ( 8), the pattern is ∀α.∃β. dynamic(f : α → β). Here, β is bound after α; hence β can be instantiated to type expressions containing α. For instance, this pattern matches a dynamic with type ∀γ. γ → γ list, binding β to α list. This pattern catches a class of functions that operate uniformly on arguments of any type [START_REF] Wadler | Theorems for free! In Functional Programming Languages and Computer Architecture[END_REF]. These functions cannot test or destructure their arguments, but only put them in data structures or in closures. Therefore, if we apply such a function to a symbolic name x, and recursively print the result, we get a representation of the function body, with x standing for the function parameter. 3 (More exactly, the printed function is extensionally equivalent to the original function, assuming there are no side-effects.)

In the presence of mixed quantification, the rules for typing the right-hand side of patternmatchings outlined above have to be strengthened: it is not always correct to treat an existentially quantified type variable as a new abstract atomic type. Consider:

function ∀α.∃β. dynamic(f : α → β) → f(1) = f(true)
Assuming f : ∀α. α → β, the expression f(1) = f(true) typechecks, since both applications of f have type β. Yet, when applying the function above to dynamic(function x → x), the matching succeeds, f(1) evaluates to 1, f(true) evaluates to true, and we end up comparing 1 with truea run-time type violation. Since the actual value of β is allowed to depend on α, static typechecking has to assume that β does depend over α, and treat two occurrences of β corresponding to different instantiations of α as incompatible. This is achieved by considering β in the right-hand side of the matching as a type constructor parameterized by α. (This transformation is known in logic as Skolemization.) To avoid confusion, we shall write S β for the type constructor associated to the type variable β. Therefore, we now assume f : ∀α. α → S β (α) for the typing of f(1) = f(true), and this leads to a static type error, since the two sides of the equal sign have incompatible types S β (int) and S β (bool). However, f(1) = f( 2) is well-typed, since both sides have type S β (int). The general rule is: for the purpose of typing the right-hand side of a pattern-matching, an existentially quantified type variable β is replaced by the type expression S β (α 1 , . . . , α n ), where α 1 . . . α n is the list of those type variables that are universally quantified before β in the pattern.

Multiple dynamic matching

Type variables are quantified at the beginning of each case of the pattern-matching, not inside each dynamic pattern. This makes no difference for universally quantified variables (because of the type isomorphisms). However, existentially quantified variables can be shared among several dynamic patterns, expressing sharing constraints between the internal types of several dynamics. For instance, the "dynamic function application" example of [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF] can be written as:

function ∃α.∃β. (dynamic(f : α → β), dynamic(x : α)) → dynamic(f x)
This function takes a pair of two dynamics, applies the first one (which should contain a function) to the second one, and returns the result as a dynamic. It ensures that the type of the argument is compatible with the domain type of the function.

Type variables can be shared among two dynamic patterns of the same matching; but we shall prohibit sharing between patterns belonging to different matchings (curried dynamic matching). In other terms, all cases in a pattern matching are required to be closed: all type variables contained in dynamic patterns should be quantified at the beginning of the corresponding matching. For instance, it is not possible to write the dynamic apply function as it appears in [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF]:

function ∃α.∃β. dynamic(f : α → β) → function dynamic(x : α) → dynamic(f x)
This violates the requirement above, since α is bound by the outermost matching, and mentioned in the innermost one. The reasons for this restriction are mostly pragmatic: curried dynamic matching, in conjunction with polymorphic dynamics, can lead to ambiguities in the bindings of types to existentially quantified type variables. Consider:

let f = function ∃α. dynamic(x : α) → let d = dynamic(x) in function dynamic(y : α) → d in f(dynamic [ ])(dynamic [1])
The first type matching succeeds with α bound to ∀β. β list, but the second matching requires α to be narrowed to int list. It is unclear whether the dynamic d created between the two matchings should have internal type ∀β. β list or int list. This problem does not arise if we require the actual type bound to α to be determined by only one matching. This is ensured by the closedness condition on pattern matching, without significantly reducing the expressive power of the language: curried dynamic application can still be written as function df → function dx → match (df, dx) with . . . at the cost of a later error detection, if df is not a dynamic of a function.

(36

) E i : int ⇒ i (37) τ ≤ E(x) E x : τ ⇒ x (38) Q k p k : τ ⇒ E k E + E k a k : τ ⇒ b k F SC(τ ) ∩ BV (Q k ) = ∅ E function . . . | Q k .p k → a k | . . . : τ → τ ⇒ function . . . | Q k .p k → b k | . . . (39) E a 1 : τ → τ ⇒ b 1 E a 2 : τ ⇒ b 2 E a 1 a 2 : τ ⇒ b 1 b 2 (40) E a 1 : τ 1 ⇒ b 1 E a 2 : τ 2 ⇒ b 2 E (a 1 , a 2 ) : τ 1 × τ 2 ⇒ (b 1 , b 2 ) (41) E a 1 : τ 1 ⇒ b 1 E + [x → Clos(τ 1 , F V (E))] a 2 : τ ⇒ b 2 E let x = a 1 in a 2 : τ ⇒ let x = b 1 in b 2 (42) E a : τ ⇒ b F V (τ ) ∩ F V (E) = ∅ E dynamic a : dyn ⇒ dynamic(b, Clos(τ, ∅)) (43) Q x : τ ⇒ [x → τ ] (44) Q p 1 : τ 1 ⇒ E 1 Q p 2 : τ 2 ⇒ E 2 Q (p 1 , p 2 ) : τ 1 × τ 2 ⇒ E 1 ⊕ E 2 (45) Q i : int ⇒ [ ] (46) F V (τ ) ⊆ BV (Q) Q p : τ ⇒ E θ = S( , Q) Q dynamic(p : τ ) : dyn ⇒ Clos(θ(E), ∅)

Syntax

The only syntactic change is the introduction of a sequence of quantifiers in front of each case in pattern matchings.

Expressions:

a ::= . . . [] function Q 1 .p 1 → a 1 | . . . | Q n .p n → a n Annotated expressions: b ::= . . . [] function Q 1 .p 1 → b 1 | . . . | Q n .p n → b n
Quantifier prefixes:

Q ::= [] ∀α.Q [] ∃α.Q
We will always assume that variables are renamed so that quantifier prefixes Q never bind the same variable twice. We write BV (Q) for the set of variables bound by prefix Q.

Typechecking

We introduce the Skolem constants at the level of types. To each type variable α, we associate the type constructor S α , with variable arity.

τ ::= . . . [] S α (τ 1 , . . . , τ n ) Skolem constants appear only inside inferred types: they cannot appear in the type part of dynamic patterns, nor in the internal type of dynamic values. We shall write τ , σ for types that do not contain Skolem constants. We define F SC(τ ), the free Skolem constants of type τ , as the set of all variables α such that the type constructor S α appears in τ .

The new typing rules for functions and for patterns are shown in figure 4. For each case Q.p → a in a function definition, the pattern p is typed taking Q into account. The proposition p : σ ⇒ E now takes Q as an extra argument, becoming Q p : σ ⇒ E. The Q prefix is carried unchanged through all rules, and it is used only in the rule for dynamic patterns. There, in the types of all identifiers bound by the pattern, we replace existentially quantified type variables by the corresponding Skolem functions. This is performed by the substitution θ = S( , Q), defined inductively on Q as follows:

S(α 1 . . . α n , ) = id S(α 1 . . . α n , ∀α.Q) = S(α 1 . . . α n α, Q) S(α 1 . . . α n , ∃α.Q) = {α → S α (α 1 , . . . , α n )} • S(α 1 . . . α n , Q)
The typing of the action a proceeds as previously. We simply check that the type of a does not contain any Skolem constants corresponding to variables bound by Q. This is ensured by the side-condition F SC(τ

) ∩ BV (Q k ) = ∅ in rule 38.

Evaluation

The introduction of existential type variables in dynamic patterns significantly complicates the semantics of the language, both for dynamic creation and for dynamic matching. The modified evaluation rules are shown in figure 5. The value space used is: For dynamic creation, the evaluation of dynamic(b, τ ) now has to transform the static type τ inferred for a before pairing it with the value of a (rule 53). Skolem constants representing existentially bound type variables are replaced by the actual types bound to these variables, properly instantiated. These bindings of type variables are recorded in the evaluation environment e. Since existential type variables may depend upon universal variables, an existential variable is actually bound to a type context (a type expression with holes) instead of a simple type expression. We write type contexts as λα 1 . . . α n . τ , where the type variables α 1 . . . α n are names for the holes in τ . The T function defined below is the evaluation function on types. It maps a type expression τ to a type expression τ not containing Skolem constants, interpreting the Skolem constants according to an environment e.

Values: v ::= cst(i) integer value [] pair(v, v ) value pair [] dynamic(v : σ) dynamics value [] clos(e, Q 1 .p 1 → b 1 | . . . | Q n .p n → b n ) function closure
(49) e function . . . | Q k .p k → b k | . . . * → clos(e, . . . | Q k .p k → b k | . . .) (50) e b * → clos(e , . . . | Q k .p k → b k | . . .) e b * → v Q k v < p k * → (e , Γ) e + e + Solve(Q k , Γ) a k * → r k minimal e b b * → r (51) e b 1 * → v 1 e b 2 * → v 2 e (b 1 , b 2 ) * → pair(v 1 , v 2 ) (52) e b 1 * → v e + [x → v], t b 2 * → r e let x = b 1 in b 2 * → r (53) e b * → v e dynamic (b : σ) * → dynamic(v : T (σ, e)) (54) Q v < x * → ([x → v], ∅) (55) Q i < i * → ([ ], ∅) (56) Q v 1 < p 1 * → (e 1 , Γ 1 ) Q v 2 < p 2 * → (e 2 , Γ 2 ) Q (v, v ) < (p, p ) * → (e ⊕ e , Γ 1 ∪ Γ 2 ) (57) Q v < p * → (e, Γ) σ = ∀α 1 . . . α n . τ {α 1 . . . α n } ∩ BV (Q) = ∅ Q dynamic(v : σ) < dynamic(p : τ ) * → (e, Γ ∪ {τ = τ })
T (int, e) = int T (dyn, e) = dyn T (α, e) = α T (τ 1 × τ 2 , e) = T (τ 1 , e) × T (τ 2 , e) T (τ 1 → τ 2 , e) = T (τ 1 , e) → T (τ 2 , e) T (S α (τ 1 . . . τ n ), e) = τ [α 1 ← T (τ 1 , e), . . . , α n ← T (τ n , e)] if e(α) = λα 1 . . . α n . τ
The T function straightforwardly extends to type schemes:

T ((∀α 1 . . . α n . τ ), e) = ∀α 1 . . . α n . T (τ, e) if {α 1 . . . α n } ∩ Dom(e) = ∅
For dynamic matching during function application (rule 50), it is no longer possible to perform dynamic type matching separately for each dynamic pattern, since patterns may share existentially quantified variables. Therefore, all dynamic type constraints are collected first, as a set of equations τ 1 = τ 2 , where τ 1 is the internal type of a dynamic, and τ 2 a type pattern. Hence the response m returned by the pattern-matching predicate is either wrong, or a pair (e, Γ) of a set e of bindings and a set Γ of equations between types. In addition, the pattern-matching predicate is now parameterized by Q, the quantifier prefix for the matching, becoming Q v < p * → m (rules 54-57). The Q prefix is used in rule 57 to select a trivial instance of the internal type of the dynamic whose free variables do not clash with the variables bound by Q. In a second phase, the function Solve is called to resolve the set Γ of equations on types, taking then prefix Q into account. (The next section precisely defines Solve.) When the type matching succeeds, Solve returns the correct bindings for existentially quantified type variables. Then, the evaluation of the right-hand side of the matching proceeds as usual.

Unification

The run-time matching between type patterns and internal types of dynamics amounts to a certain kind of unification problem, called unification under a prefix. This problem is studied extensively in [START_REF] Miller | Unification under a mixed prefix[END_REF], though in the very general setting of higher-order unification, while we only deal with firstorder terms here. The first-order problem also appears in [START_REF] Miller | Lexical scoping as universal quantification[END_REF]. In our case, the problem consists in checking the validity of propositions of the format

q 1 α 1 . . . q n α n .(τ = τ )
where the q k are either universal or existential quantifiers, and τ , τ are first-order terms of a free algebra. Unification under mixed prefix generalizes the well-known matching problem ("given two terms τ and τ , find a substitution θ such that θ(τ ) = τ ") and the unification problem ("given two terms τ and τ , find a substitution θ such that θ(τ ) = θ(τ )"): writing α 1 . . . α n for the variables of τ and β 1 . . . β n for the variables of τ , the matching problem is equivalent to

∀β 1 . . . ∀β n ∃α 1 . . . ∃α n .(τ = τ ),
and the unification problem to

∃β 1 . . . ∃β n ∃α 1 . . . ∃α n .(τ = τ ).
For the purpose of dynamic matching, we not only want to know whether the proposition Q.(τ = τ ) holds (where Q is a quantifier prefix), but also to find minimal assignments for the variables existentially quantified in Q that satisfy the proposition. From now on, we shall treat variables universally bound in Q as constants. That is, we add these variables as term constructors with arity zero to the initial signature (int and dyn of arity zero, → and × of arity two).

Definition 1 A substitution θ is a Q-substitution if for all variables α, all constants β contained in the term θ(α) are bound before α in prefix Q.

Definition 2 A substitution θ is a Q-unifier of τ and τ if θ(τ ) = θ(τ ) and θ is a Q-substitution.
If such a substitution exists, τ and τ are said to be Q-unifiable.

Clearly, the formula Q.(τ = τ ) is valid if and only if τ and τ are Q-unifiable. The following proposition gives a simple way to check whether two terms are Q-unifiable. Proposition 6 Two terms τ and τ are Q-unifiable if and only if τ and τ are unifiable, and their most general unifier is a Q-substitution.

Proof:

The "if" part is obvious. For the "only if" part, let θ be a Q-unifier of τ and τ . Since θ(τ ) = θ(τ ), the terms τ and τ are unifiable. Let µ be their most general unifier. There exists a substitution ϕ such that θ = ϕ • µ. Hence, for all variables α, the constants contained in µ(α) are a subset of those contained in θ(α). Since θ is a Q-substitution, all constants in µ(α) are also bound before α in Q. It follows that µ is a Q-substitution.

2

Proposition 6 shows that if two terms are Q-unifiable, then they possess a most general Qunifier. Moreover, we immediately get an algorithm to compute the most general Q-unifier of τ and τ : compute the most general unifier of τ and τ , using e.g. Robinson's algorithm, and check that it is a Q-substitution.

We can now define the function Solve used in evaluation rule 50. It takes a prefix Q and a set Γ of equations τ 1 = τ 1 , . . . , τ n = τ n . The types τ 1 . . . τ n are trivial instances of the internal types of dynamic values. The types τ 1 . . . τ n are the type parts of dynamic patterns. Since the prefix Q binds the variables in τ 1 . . . τ n only, we first complete Q to bind the variables in τ 1 . . . τ n also. Let α 1 . . . α m be the variables free in τ 1 . . . τ n . We take Q = Q.∃α 1 . . . ∃α m . This existential quantification means that the variables α 1 . . . α m can be freely instantiated during type matching, since they are universally quantified in the internal types of dynamic values. Because of the renaming constraint in rule 46, the variables α 1 . . . α m are not already bound by Q.

Let µ be the most general Q -unifier of τ 1 × . . . × τ n and τ 1 × . . . × τ n . The substitution µ is transformed into an evaluation environment, by adding bindings for the variables that are existentially quantified in Q. More precisely, we take Solve(Q, Γ) to be s(µ, , Q), where s is defined as follows:

s(µ, α 1 . . . α n , ) = [ ] s(µ, α 1 . . . α n , ∀α.Q) = s(µ, α 1 . . . α n α, Q) s(µ, α 1 . . . α n , ∃α.Q) = [α → (λα 1 . . . α n .µ(α))] + s(µ, α 1 . . . α n , Q)
The transformation s is the run-time counterpart of the Skolemization function S used for static typing in section 3.3. It turns the substitution µ into an evaluation environment that reflects the instantiations performed on the existentially quantified variables during the type matching process.

Compilation

The semantics given above are quite complicated, so it is no surprise their implementation turns out to be delicate. The main difficulty is unification under a prefix Q. Efficient algorithms are available for the regular unification phase. It remains to quickly check that the resulting substitution is a Q-substitution. This check can actually be integrated with the occur check, at little extra cost. The idea is to reflect dependencies by associating ranks (integers) to type variables. Variables bound by Q are statically given ranks 0, . . . , n from left to right. Other variables (i.e. those in the internal types of dynamics) are considered bound at the end of Q, and are therefore given rank ∞. When identifying two variables α and β, the resulting variable is given rank min(rank(α), rank(β)). Then, binding an existential variable α to a constructed type τ is legal if and only if:

1. (occur check) α does not occur in τ 2. (rank check) τ does not contain any universal type variable whose rank is greater than the rank of α.

As in the case of simple dynamics (section 2.9), the easiest way to implement type matching is to call at run-time a unification primitive, with the type pattern (annotated by rank information) as a constant argument. Partial evaluation of the unification primitive on the type pattern is desirable, not only to speed up type matching, but also to provide a cleaner handling of runtime type environments: after specialization, the bindings for the existential type variables can be recorded on the stack or in registers, as if they were regular variables; without specialization, the unification primitive returns a data structure containing these bindings, and less efficient code is generated to access these bindings.

Specializing unification on one of its arguments is not much harder than specializing matching on its second argument (section 2.9). The techniques developed for the Warren Abstract Machine directly apply [START_REF] David | An abstract Prolog instruction set[END_REF][START_REF] Maier | Computing with logic: logic programming with Prolog[END_REF][START_REF] Aït-Kaci | The WAM: a real tutorial[END_REF], with the exception of the extra rank check. For instance, the WAM does not perform occur check for the initial binding of an existential variable, while we have to check ranks even in this case. Another difference is that backtracking is always "shallow", in the WAM terminology, since ML pattern-matching is deterministic. This simplifies the handling of the trail.

Following the ideas above, the first author has integrated a prototype unification compiler in the CAML system. The CAML pattern-matching compiler was modified to implement unification semantics as well as matching semantics, depending on flags put on the patterns. This low-level mechanism allows performing unification on some parts of a data structure, and regular patternmatching on the other parts. Then, dynamic patterns dynamic(p : τ ) are simply expanded after type inference into product patterns (p, repr(τ )), where repr(τ ) is the pattern that matches all internal representations of types matching τ . The pattern repr(τ ) is marked to use unification semantics.

The only missing feature from what we have described above was rank check. At that time, we considered only dynamic patterns where all universal type variables come first, followed by all existential variables. Rank check could have been added with little modifications.

Dynamic matching benefited from all optimizations performed by the pattern-matching compiler, including factorization of tests between cases, and utilization of typing informations. As a consequence, dynamic matching was quite efficient. However, we agreed that this efficiency was not worth the extra complication of the compiler, and this prototype was not merged with the CAML release.

Assessment

This section discusses the practical usefulness of the two propositions above, drawing from our experience with the CAML system.

Structured input-output

The CAML system provides the two library functions extern : extern channel × dyn → unit and intern : intern channel → dyn, to efficiently write and read data structures on persistent storage, preserving sharing inside the structure. 4 A typical use is, for a separate compiler, to communicate relocation information with its linker, and to save and reload symbol tables representing compiled module interfaces.

The ML type system uses name equivalence for concrete data types. This causes some difficulties with dynamics written to persistent storage: the program reading a dynamic can define some data types with different names than the program that wrote the dynamic, or define data types with the same name, but different structures. There are two solutions to this problem. The first one is to revert to structural equivalence for dynamic type matching. That is, the data type definitions are expanded both in dynamic values and in dynamic type patterns, and structural equivalence is used during matching. The CAML implementation of intern/extern takes another approach: when writing a dynamic to persistent storage, extern also writes the definitions of all concrete data types whose names appear in the type part of the dynamic. When the object is read back, intern checks that the reader program defines data types with the same names and structurally similar definitions, and raises an exception if this is not the case. The latter implementation allows for faster dynamic coercion than the former, but it requires information on data type definitions to be available at run-time.

In conjunction with character-based communication channels such as Unix sockets, the intern and extern primitives provide a simple implementation of remote procedure calls (RPC). Here is a sample RPC server for the monomorphic function f : τ → τ . The first proposed system supports only remote calls to a monomorphic function. Existential variables, as in the second system, are required to provide a remote interface to a polymorphic function. For instance, here is an RPC server for a sorting function:

while true do let (inchan, outchan) = accept connection(. . .) in match intern inchan with ∃α. dynamic(order, arg : (α × α → bool) × α list) → extern outchan (dynamic(sort order arg)) done

Interfacing with system functions

Dynamics makes it possible to provide an interface with a number of system functions that cannot be given a static type in ML. Without dynamics, these functions could not be made available to the user in a type-safe way. In the CAML system, these functions include:

• eval syntax : ML → dyn, to typecheck, compile, and evaluate a piece of abstract ML syntax (type ML). This makes it easy to provide CAML as an embedded language inside a program. For instance, the Coq system [START_REF] Dowek | The Coq proof assistant user's guide: version 5[END_REF], a proof development environment based on the Calculus of Constructions, provides the ability to interactively define proof tactics written in CAML, and to apply them on the fly. The CAML macro facility [29, chapter 18] also makes use of eval syntax, since a macro body is an arbitrary CAML expression whose evaluation leads to the substituted text.

• MLquote : dyn → ML, which is one of the constructors of the data type representing abstract syntax trees. This constructor embeds constants of arbitrary types inside syntax trees. These constants are produced by compile-time evaluations (e.g. macro expansion and constant folding).

• print : dyn → unit, to print a dynamic value in ML syntax. CAML cannot provide a polymorphic printing function with type α → unit, due to some optimizations in the data representation algorithm, that make it impossible to decipher the representation of a data without knowing its type.

In these examples, the returned dynamics are generally coerced to fully known types, usually monomorphic. Therefore, we do not see the need for existential type variables there, and the simpler dynamic system presented in section 2 seems largely sufficient. In practice, the restriction encountered first is not that dynamics can only be coerced to closed types, but that dynamics can only be created with closed types. This prevents the print function from being called by a polymorphic function to print its polymorphic argument, for instance. This is often needed for debugging purposes.

Ad-hoc polymorphism

ML polymorphism is uniform: polymorphic functions operate in the same way on arguments of several types. In contrast, ad-hoc polymorphism consists in having generic functions that accept arguments of several types, but operate differently on objects of different types. Prime examples are the print function or the equal predicate: different algorithms are used to print or compare integers, strings, lists, or references. Several extensions of functional languages have been proposed, that support the definition of such generic functions, including type classes [START_REF] Wadler | How to make ad-hoc polymorphism less ad-hoc[END_REF] and run-time overloading [START_REF] Rouaix | Safe run-time overloading[END_REF].

Dynamics provide a naive, but easy to understand, way to define generic functions. As demonstrated above in the print example, dynamics permit joining predefined functions on atomic types (print int, print string) and functions on data structures (pairs, lists), that recurse on the components of the structures -the main operation in defining generic functions. Another important aspect of generic functions is extensibility: whenever a new data type is defined, these functions should be extended to deal with objects of the new type as well. This can also be supported in the dynamic implementation, by keeping in a reference a list of functions with type dyn → unit, to be applied until one succeeds whenever none of the standard cases apply. For instance, assuming that the type α foo = A of α | B of α × α foo has been defined, we could add a printer for type foo as follows:

new printer (function ∃α. dynamic(A : α foo) → print string "A" | ∃α. dynamic(B(x, y) : α foo) → print string "B("; print (dynamic x); print string ", "; print (dynamic y); print string ")" | x → raise Cannot print); ; It should be pointed out that this implementation of ad-hoc generic functions with dynamics has major drawbacks. First, because of the restrictions on dynamic creation, polymorphic functions that need to call print have to take dynamics themselves. This is not too serious for print, but would be prohibitive for heavily used functions such as equal: all functions on sets, association lists, . . . , would have to operate on dynamics, thus dramatically reducing accuracy of static typing and efficiency of compiled code. Moreover, we cannot statically check that print is never applied to objects that have no printing method defined. This important class of type errors will only be detected at run-time. Finally, such an implementation of generic functions is rather inefficient, since dynamics are built and coerced at each recursive call.

Type classes and run-time overloading techniques seem more realistic in these respects. They statically guarantee that generic functions can only be applied to objects on which they are defined. They perform type matching at compile-time whenever possible. And run-time type information can usually be arranged as dictionaries of methods, allowing faster method selection than dynamic type matching.

Related work

A number of recent studies have considered languages with dynamic types. Some of these studies deal with the automatic insertion of dynamic creations and coercions that turn "ambivalent" programs (programs that cannot be recognized type-safe nor type-erroneous at compile time) into equivalent programs with run-time type checks [START_REF] Satish | Quasi-static typing[END_REF][START_REF] Henglein | Dynamic typing[END_REF]. One motivation is to integrate more transparently dynamically-typed and statically-typed objects; another motivation is the efficient compilation of programs written in dynamically-typed languages such as Scheme. In our proposal, we insist on keeping the coercions to and from dynamics explicit in the source code and under the programmer's responsibility: serious programming errors can go unnoticed at compile-time if run-time type checks are automatically inserted, therefore reducing the robustness of programs.

The work on dynamics most closely related to ours is that of Abadi, Cardelli, Pierce, Plotkin and Rémy. Their first paper [START_REF] Abadi | Dynamic typing in a statically-typed language[END_REF] studies a simply-typed calculus enriched by objects with dynamic type. Dynamics can be coerced to partially unknown types: type patterns in the dynamic coercion construct can contain "pattern variables", that correspond in our second system to existentiallyquantified variables. Since there is no polymorphism, type matching is straightforward.

Abadi et al. have recently extended this system to polymorphic types [START_REF] Abadi | Dynamic typing in polymorphic languages[END_REF]. The main difference between their latest system and our second system is in the format of type patterns in dynamic coercions. Their approach to polymorphic type matching is to allow higher-order pattern variables into type patterns: variables that range over type contexts. For instance, the type pattern ∀α.∃β. α → β in our second system corresponds, in their system, to the pattern ∀α. α → F [α], where F is a pattern variable ranging over operators from types to types. Their algebra of type patterns is strictly more expressive than ours: mixed quantification introduces a linear ordering on 29 the dependencies between existential and universal variables, while pattern variables can express arbitrary dependencies; also, their patterns can select polymorphic functions (e.g. functions that can be applied to integer lists and boolean lists), and these patterns have no equivalent in our second system. On the other hand, mixed quantification has a simple interpretation in first-order logic, and therefore possesses a simple and efficient type matching algorithm; while some ad-hoc restrictions must be put on pattern variables to keep type matching manageable.

Conclusions

We have presented two extensions of ML with dynamic objects. The simpler one has proved quite successful for interfacing user code with some important system functions in a type-safe way. Its implementation cost remains moderate. The other extension, which generalizes the dynamic patterns to include both universal and existential variables in the type part, makes it possible to work on dynamics without coercing them to fixed types. Its semantics are more delicate, and it is considerably harder to implement. We have presented one promising application of this extension: the use of dynamics for data persistence or interprocess communication. The first proposed system does not allow to operate on persistent data in a generic way, or to perform remote calls to polymorphic functions; the second system supports these operations. More practical experience is needed to determine how expressive a polymorphic type system with dynamics needs to be in order to correctly support these applications.

  function dynamic(x : α list) → . . . | dynamic(x : int list) → . . . instead of the more intuitive definition function dynamic(x : int list) → . . . | dynamic(x : α list) → . . .

  Type schemes: σ ::= ∀α 1 . . . α n .τ Annotated expressions: b

  Evaluation environments: e ::= [ . . . , x → v, . . . ] Evaluation responses: r ::= v normal response (a value) [] wrong type error response Pattern-matching responses: m ::= e normal response (an environment) [] wrong type error response The type schemes in dynamic values are required to be closed: all variables are universally quantified. The evaluation rules are given in figure 2. They closely follow the structure of the typing rules. The first two sets of rules define the predicate e b * → r, meaning "in environment e, expression b evaluates to response r". The last two sets of rules define the auxiliary predicate v < p * → m, meaning "the matching of value v against pattern p results in m". Here, m is either an evaluation environment, describing the bindings performed on p variables in case of successful matching, or the constant wrong if a run-time type violation occurred.

) e b 1 e let x = b 1 in b 2

 12

Figure 2 :

 2 Figure 2: Evaluation rules 10

  Two evaluation rules lead to the conclusion e b * → r. The first one is e b 1 * → wrong e let x = b 1 in b 2 * → wrong By induction hypothesis, we cannot derive e b 1 * → wrong, since E a 1 : τ 1 ⇒ b 1 . Hence the last evaluation step must be e b 1 *

1 * → v 1 e

 11 are two evaluation possibilities. The first one (rule 25) concludes r = wrong because e b 1 * → wrong; but this contradicts the induction hypothesis. Hence the last evaluation step must be e b dynamic(b 1 : Clos(τ 1 , ∅)) * → dynamic(v 1 : Clos(τ 1 , ∅)) Applying the induction hypothesis to the evaluation of b 1 , we get |= v 1 : τ 1 . By proposition 3, this implies |= v 1 : Clos(τ 1 , ∅). Hence |= dynamic(v 1 : Clos(τ 1 , ∅)) : dyn, as expected. 2

Figure 4 :

 4 Figure 4: Typing rules with mixed quantification in type patterns

21 (

 21 Evaluation environments: e ::= [ . . . , x → v, . . . , α → (λα 1 . . . α n . τ ), . . . appearing in dynamic values are required to be closed, and not to contain any Skolem constant. 47) e x * → e(x) (48) e i * → cst(i)

Figure 5 :

 5 Figure 5: Evaluation rules with mixed quantification in type patterns (error rules similar to rules 19-25 and 30-35 have been omitted)

  while true do let (inchan, outchan) = accept connection(. . .) in match intern inchan with dynamic(arg : τ ) → extern outchan (dynamic (f arg)) done The corresponding client stub function is: let f arg = let (inchan, outchan) = establish connection(. . .) in extern outchan (dynamic arg); match intern inchan with dynamic(res : τ ) → res

exception

  Cannot print; ; let printers = ref ([ ] : (dyn → unit) list); ; type fun arg = Arg of string in let rec print = function dynamic(i : int) → print int i | . . . | d → let rec try print = function f :: rest → try f d with Cannot print → try print rest | [ ] → print string "?" in try print !printers; ; let new printer f = printers := f :: !printers; ;

  The two claims below are the inductive steps that establish proposition 2.

and only if |= v : τ for all types τ ≤ σ

• |= e : E if and only if e and E have the same domain, and |= e(x) : E(x) for all x in their domain.

The following property shows that semantic typing is stable under substitution; hence, type generalization is always semantically correct. Proposition 3 Assume |= v : τ . Then, |= v : ϕ(τ ) for all substitutions ϕ. Hence |= v : ∀α 1 . . . α n . τ for all variables α 1 . . . α n . Proof: By induction on v. The case where v is a closure is settled by proposition 1. The remaining cases are obvious. 2 Proposition 4 Assume p : τ ⇒ E and v < p * → m. If |= v : τ , then m = wrong; instead, m is an evaluation environment e such that |= e : E.

  |= v 2 : τ 2 . The last rule used in the evaluation derivation is one of 28, 31, 32 or 33. Rule 31 does not apply, since v is a pair. Rule 32 requires v 1 < p 1 ⇒ wrong, but this contradicts the induction hypothesis applied to v 1 . Rule 33 is similarly excluded. Hence the last evaluation rule used must be v 1 < p 1 *

	→ e 1	v 2 < p 2	* → e 2

pair(v 1 , v 2 ) < (p 1 , p 2 ) * → e 1 ⊕ e 2

with e = e 1 ⊕ e 2 . Applying the induction hypothesis to the matching of v 1 against p 1 and to the matching of v 2 against p 2 , we get |= e 1 : E 1 and |= e 2 : E 2 . Hence |= e 1 ⊕ e 2 : E 1 ⊕ E 2 , which is the expected result.

All examples in this article are written in the CAML dialect of ML[START_REF] Cousineau | The CAML primer[END_REF][START_REF] Mauny | Functional programming in CAML[END_REF].

Algorithm W should also produce an annotated expression b. This extra result has been omitted for the sake of simplicity. It is easy to reconstruct b from the principal typing derivation built by the algorithm.

To avoid any confusion between the formal parameter and constants mentioned in the function body, formal parameters are represented by a local type fun arg = Arg of string. This ensures that the given function cannot create any terms of type fun arg, unless it is the print function itself. Fortunately, the self-application print(dynamic print) selects case[START_REF] Di | Type isomorphisms in a type-assignment framework[END_REF] of the definition.

The current implementation of extern does not handle functional values, because the CAML compiler generates position-dependent machine code. Even with position-independent code, the persistent objects produced would not be portable across architectures. However, there is no problem with defining extern over functions in a byte-coded implementation[START_REF] Cardelli | Amber. In Combinators and Functional Programming Languages[END_REF].

type fun arg = Arg of string in let rec print = function dynamic(i : int) → (1) print int i | dynamic(s : string) →

(2) print string "\""; print string s; print string "\"" | ∃α.∃β.dynamic((x, y) : α × β) →

(3) print string "("; print(dynamic x); print string ", "; print(dynamic y); print string ")" | ∃α.dynamic([ ] : α list) → (4) print string "[ ]" | ∃α.dynamic(x :: l : α list) →

(5) print(dynamic x); print string " :: "; print(dynamic l)

Typing existential quantification

We first show how existentially quantified type variables behave when typing the right-hand side of the pattern-matching. An existentially quantified variable can be bound to any actual type at run-time. Hence, at compile-time, we should make no assumptions about the type α, and treat it as an abstract type. That is, the type α does not match any type except itself; and α must not escape the scope of the pattern-matching that binds it: α is not allowed to be free in the type of the returned value. As a consequence, the following two functions are rejected:

while this one is perfectly legal:

and can be applied to dynamic(succ, 2) as well as to dynamic(int of string, "3").

There is one important difference between existentially bound type variables and abstract types: the actual type bound to such a type variable is available at run-time. Given an object a whose