Xavier Leroy
email: xavier.leroy@inria.fr

Applicative functors and fully transparent higher-order modules

We present a variant of the Standard ML module system where parameterized abstract types (i.e. functors returning generative types) map provably equal arguments to compatible abstract types, instead of generating distinct types at each application as in Standard ML. This extension solves the full transparency problem (how to give syntactic signatures for higher-order functors that express exactly their propagation of type equations), and also provides better support for non-closed code fragments.

Introduction

Most modern programming languages provide support for type abstraction: the important programming technique where a named type t is equipped with operations f, g, . . . then the concrete implementation of t is hidden, leaving an abstract type t that can only be accessed through the operations f, g, . . . Type abstraction provides fundamental typing support for modularity, since it enables a type-checker to catch violations of the modular structure of programs.

Type abstraction is usually implemented through generative data type declarations: to make a type t abstract, the type-checker generates a new type t incompatible with any other type, including types with the same structure. From this, it is tempting to explain type abstraction in terms of generativity of type declarations and say for instance that "a type is abstract because it is created each time its definition is evaluated". The Definition of Standard ML [START_REF] Milner | The definition of Standard ML[END_REF][START_REF] Harper | A type discipline for program modules[END_REF] formalizes this approach as a calculus over type stamps that defines when "new" types are generated and when "old" types are propagated. This approach is adequate for specifying a type-checker, but too low-level and operational in nature to help understanding type abstraction and reason about programs using it.

Independently, Mitchell and Plotkin [START_REF] Mitchell | Abstract types have existential type[END_REF] have proposed a more abstract, less operational account of type abstraction based on a parallel with existential quantification in logic. Instead of operational intuitions about type generativity, this approach uses a precise semantic characterization: representation independence [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF][START_REF] Mitchell | On the equivalence of data representations[END_REF], to show that type abstraction is enforced. This abstract approach has since been extended to account for the main features of the Standard To appear in the proceedings of the 22nd symposium Principles of Programming Languages, january 1995.

ML module system: the "dot notation" as elimination construct for abstract types [START_REF] Cardelli | Typeful programming[END_REF][START_REF] Cardelli | Abstract types and the dot notation[END_REF] and the notion of type sharing and its propagation through functors [START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF][START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF].

Unfortunately, some features described by operational frameworks remain unaccounted for in the abstract approach, such as structure sharing and the "fully transparent" behavior of higher-order functors predicted by the operational approach [START_REF] Macqueen | A semantics for higherorder functors[END_REF]. Also, even though the abstract approach is syntactic in nature and therefore highly compatible with separate compilation [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF], code fragments with free functor identifiers could be supported better (see section 2.4 for an example). MacQueen [START_REF] Macqueen | A semantics for higherorder functors[END_REF][START_REF] Appel | Separate compilation for Standard ML[END_REF] claims that the problem with higher-order functors is serious enough to invalidate the abstract approach and justify the recourse to complicated stamp-based descriptions of higher-order functors and separate compilation mechanisms.

The work presented in this paper is an attempt to solve two of these problems (fully transparent higher-order functors and support for non-closed code fragments) in a syntactic framework derived from [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF]. It relies on a modification of the behavior of functors (parameterized modules). In Standard ML and other models based on type generativity, a functor defining an abstract type returns a different type each time it is applied. We say that functors are generative. In this work, we consider functors as applicative: if the functor is applied twice to provably equal arguments, the two abstract types returned remain compatible. Functors therefore map equals to equals, which enables equational reasoning on functor applications during type-checking. In turn, this allows more precise signatures for higher-order functors, thereby solving the full transparency problem.

Applicative functors are also interesting as an example of a module system that ensures type abstraction (the representation independence properties still hold) without respecting strict type generativity (some applications of a given functor may return new types while others return compatible types). In this approach, type abstraction mechanisms are considered from a semantic point of view (how to make programs robust with respect to changes of implementations?) rather than from an operational point of view (when are two structurally identical types compatible?). This work illustrates the additional expressiveness and flexibility allowed by this shift of perspective.

The remainder of this paper is organized as follows. Section 2 introduces informally the applicative semantics of functors and the main technical devices that implement it. Section 3 formalizes a calculus with applicative functors. Section 4 shows that the representation independence property still holds, and section 5 that higher-order functors are fully transparent in this calculus. Section 6 discusses related work and section 7 gives concluding remarks.

Type paths and the propagation of type equalities

Module systems such as SML's allow type expressions of the form x.t, where x is a structure identifier (the name of a module) and t is the name of a type defined in this structure. Since structures can be nested, type expressions such as x1. . . . xn.t are also allowed, denoting the t type component of the xn substructure of . . . the structure x1. These type expressions are called type paths or long type identifiers.

When type bindings are transparent (named types are compared by structure), type paths play no role in typechecking, since they can always be replaced by the type expressions to which they are bound. This is not the case with opaque type bindings, where the definitions of type identifiers are hidden and types are compared by name. Opaque bindings are crucial to implement type abstraction and representation hiding. In SML, they are provided by the abstype and datatype constructs. Type paths play the role of witnesses of opaque types [START_REF] Cardelli | Persistence and type abstraction[END_REF]: although the definition of an opaque type is not available, two occurrences of a type path denoting this opaque type are recognized as compatible types. In other terms, syntactic equality between type paths implements the name equivalence that characterizes type abstraction and type generativity [START_REF] Cardelli | Abstract types and the dot notation[END_REF].

Combined with type definitions in signatures (the ability to specify type equalities in module interfaces), type paths can also express how abstract types are propagated and shared across substructures of a structure, and across the argument and result of a functor. Consider for instance the following Set functor that implements sets over any type equipped with a total ordering:

. end

This combination of type paths and dependent functor types has been used to give complete syntactic accounts of type sharing in the SML module system [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF][START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF][START_REF] Leroy | A syntactic approach to type generativity and sharing (extended abstract)[END_REF].

Restriction of projections to paths

An obvious generalization of type paths is to allow projections of type components from arbitrary structure expressions: then, m.t would be a valid type expression for any structure expression m whose result contains a t component [START_REF] Macqueen | Using dependent types to express modular structure[END_REF][START_REF] Harper | On the type structure of Standard ML[END_REF]. This extension adds considerable expressive power, but raises delicate issues. First, when are two type expressions m.t and m .t compatible? Clearly, we cannot check that m and m reduce to the same structure, since equality of structure expressions is undecidable. Second, even if we compare structures by mere syntactic equality (m.t and m .t are compatible if and only if the structure expressions m and m are syntactically identical), some type abstraction is lost. For instance, two occurrences of the type expression (struct abstype t = τ with decls end).t would be recognized as compatible, while the two abstract type definitions can come from different parts of the program and should create two distinct abstract types t. This problem is particularly apparent in the syntactic module systems [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF][START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF], which have a typing rule (the "self" rule) that transforms abstract types into types "manifestly equal to themselves": if the structure path p has signature To avoid this problem, all module-language constructs whose evaluation can generate new types (by evaluating an abstype or datatype definition) must not occur in type projections. This excludes structure construction (struct...end) and functor application as well (the body of the functor can generate new types at each application). The only constructions that remains are access to a structure identifier (x) and access to a substructure (x 1 .x 2 ), that is, the type paths (p ::= x | p.x), as in SML. The restriction of type projections to paths is therefore equivalent to the strict notion of type generativity found in SML.

Functor applications in paths

In spite of these considerations, there are situations where it would be extremely useful to extend slightly the class of paths (the syntactic class p of structure expressions such that p.t is a legal type expression) to include simple cases of functor applications, where the functor and its argument are themselves paths. Let us therefore take

p ::= x | p.x | p 1 (p 2 )
and illustrate the consequences of this choice, on the expressiveness of the language and on the notion of type abstraction.

Local applications of functors

A first situation where this extension proves useful is to support functors that apply other functors locally.

IntDict.domain d = IntPrioQueue.contents q
However, what appeared to be an incremental change of the program (add some operations to existing functors) has required major changes to the modular structure of the program:

• All other uses of Dict and PrioQueue in the program must be modified to provide the extra Set argument, even if they do not use the new operations.

• Higher-order functors that take Dict or PrioQueue as arguments must also be modified.

• Hoisting the application Set(IntOrder) from the points where it is actually used to a common ancestor of these points in the dependency graph is a non-local program transformation, as in MacQueen's "diamond import" example [START_REF] Macqueen | Using dependent types to express modular structure[END_REF].

Introducing functor applications in paths enables a much more elegant solution: the functors Dict and PrioQueue can apply Set locally, as in the original attempt, and receive the following signatures: From the signatures above, it follows that the two types IntDict.KeySet.set and IntPrioQueue.EltSet.set are equal to Set(IntOrder).set, and therefore compatible.

Full transparency in higher-order functors

As previously mentioned, the combination of dependent functor types and type equalities in signatures makes it possible to give syntactic signatures to first-order functors that characterize exactly the "input-output behavior" of functors: how they propagate type components from their argument structure to their result structure. (See for example the signature for Set in section 2.1.) This property, in turn, enables simple syntactic descriptions of the module system and simple separate compilation mechanisms [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF], with no loss in expressiveness with respect to SML [START_REF] Leroy | A syntactic approach to type generativity and sharing (extended abstract)[END_REF].

Unfortunately, this result does not extend straightforwardly to higher-order functors: some higher-order functors do not possess any syntactic signature that characterizes exactly their behavior. Consider for instance the paradigmatic higher-order functor: signature S = sig type t end functor Apply(functor F(X:S):S; structure A:S) = F(A)

The expected behavior for this kind of functors, called the "fully transparent" behavior in [START_REF] Macqueen | A semantics for higherorder functors[END_REF] and predicted by the models based on strong sums [START_REF] Macqueen | Using dependent types to express modular structure[END_REF][START_REF] Harper | On the type structure of Standard ML[END_REF], is that at applicationtime all type equalities known about its two arguments are combined to deduce the type equality that holds on the t component of the result. For instance, if the F argument is the identity and the A argument has t = int, then the result also has t = int; if F is the constant functor returning t = bool, then the result has t = bool.

functor

: S) = F(A)
The signature for Apply is then functor Apply( functor F(X: S): sig type t=X.t end structure A: S) : sig type t=A.t end From this signature, it follows that B = Apply(Identity Int) has B.t manifestly equal to int. But then the application Apply(Constant Int) is ill-typed, since the functor Constant does not meet the specification of the F argument of Apply. The modified definition of Apply propagates more type equations, but makes the higher-order functor less general. At any rate, full transparency is not achieved.

The introduction of functor applications in type paths provides a simple, elegant solution to this full transparency problem, allowing functors such as Apply to receive syntactic signatures that capture exactly their type propagation behavior. In the case of Apply, this signature is functor Apply(functor F(X:S):S; structure A:S):

sig type t = F(A).t end
This is a correct signature for Apply: since the functor body F(A) belongs to the extended class of paths, it has not only signature S, but also sig type t = F(A).t end by application of the "self" typing rule. Moreover, this signature propagates type equalities correctly, because at application-time F and A in the result signature are substituted by the actual arguments f and a to the functor, and all known equalities about the result of f (a) will also hold for the result of Apply.

end).t end

Unfortunately, this is not a well-formed signature, since the argument to F is not a path. We must therefore revert to the less precise signature functor ApplyProd(functor F(X:S):S; structure A:S): sig type t end which does not propagate type equalities as expected. To achieve full transparency, the program must be rewritten so that the argument to F is a path. Since this argument contains A as a free variable, we must actually "lambda-lift" it as follows: Then, ApplyProd is assigned the fully transparent signature functor ApplyProd(functor F(X:S):S; structure A:S): sig type t = F(G(A)).t end which ensures the proper propagation of type equations. This trick is an instance of a general normalization technique that transforms an arbitrary program to eliminate applications of functors to non-paths, therefore ensuring that type equations are always propagated as expected (see section 5.2).

Applicative semantics of functor application

As recalled in section 2.2, the standard notion of paths (p ::= x | p.x) is the only one that guarantees strict type generativity. In turn, type generativity guarantees type abstraction. The question, then, is: how much type generativity and type abstraction is lost if we allow functor applications in paths? Some generativity, but no abstraction. More precisely, the only difference is that if we have a functor that returns an abstract type, and we apply it twice to syntactically identical paths, then we obtain two compatible abstract types, while with the standard notion of paths we would have generated two distinct types. Consider:

structure IntSet1 = Set(IntOrder) structure IntSet2 = Set(IntOrder)
With the standard notion of paths, we have IntSet1.set = IntSet2.set. If functor applications are allowed in paths, by applying the "self" rule, we obtain IntSet1: sig ... type set = Set(IntOrder).set ... end IntSet2: sig ... type set = Set(IntOrder).set ... end from which it follows that IntSet1.set = IntSet2.set.

In other terms, the consequence of adding functor applications in paths is that functors returning abstract types now map equal structure path arguments to equal abstract types. We call this behavior applicative, by opposition to the usual generative behavior, where each application of such functors generates a new abstract type, whether the arguments are identical or not.

The applicative behavior appears only if the functor arguments are syntactically identical structure paths: in all other cases, the "self" rule does not apply and the abstract types in the functor results are considered different. For instance, if we define structure IntSet3 = Set(IntOrder: ORD) structure IntSet4 = Set(IntOrder: ORD) we obtain IntSet3.set = IntSet4.set, since (IntOrder: ORD) is not a path. This may look unnatural, and more refined syntactic criteria could be used to determine equality of functor arguments; on the other hand, the line has to be drawn somewhere, and equality of structure paths is easily explained and understood.

We claim that the applicative semantics for functor applications does not violate type abstraction and does not weaken the robustness of programs. First, even though the applicative semantics makes some previously incompatible abstract types compatible (IntSet1.set and IntSet2.set in the example above), the representations of these abstract types are still hidden, and outsiders still cannot forge or inspect directly values of these types. Section 4 formalizes this argument as a representation independence property.

Moreover, several module-level construct still generate new types predictably, because they still do not belong to the extended class of paths: structure construction struct...end and restriction of a structure by a signature (strexp : sigexp). The programmer can rely on these constructs to obtain new, incompatible types, if desired for added safety. Continuing the example above, the types IntSet1.set and IntSet2.set can be made different by adding a signature constraint:

structure IntSet1 = (Set(IntOrder): SET) structure IntSet2 = (Set(IntOrder): SET)
The opaque interpretation of constraints in our module calculus guarantees that all equalities known about the set component are forgotten.

Moreover, (Set(IntOrder): SET) is syntactically not a path, hence the "self" rule cannot be used to derive a type equality between IntSet1.set and IntSet2.set. In other terms, functor application can no longer be used to force the generation of new types (as is sometimes done in SML using functors with no arguments), but other constructs such as signature constraints can be used for the same purposes.

Applicative functors and side-effects

In an imperative language such as ML, one may wonder whether the hypothesis that functors map equals to equals is sound. In a language with side-effects and modules as first-class values [START_REF] Cardelli | Typeful programming[END_REF][START_REF] Harper | A type-theoretic approach to higher-order modules with sharing[END_REF], the applicative semantics for functors is actually unsound: The problem is avoided in a stratified language such as SML: type components of structures cannot depend on values, only on types, and the language of types is purely functional; hence, the application of a functor to two structures with identical type components returns two structures with identical type components. The applicative semantics is therefore sound.

It is true, however, that value components of a functor body may depend on the store. It would therefore be incorrect to generalize the applicativity hypothesis to "a functor maps two structures that share (in SML's structure sharing sense) to two structures that share". In this paper, we only consider sharing between type components of structures. (See [START_REF] Crégut | Compilation séparée pour un langage de modules avec types génératifs[END_REF] for a treatment of structure sharing in functor signatures.)

A calculus with applicative functors

In preparation for representation independence and expressiveness results, we now define a module calculus with applicative functors, derived from [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF][START_REF] Leroy | A syntactic approach to type generativity and sharing (extended abstract)[END_REF].

Syntax

In the following grammar, v, t, and x are names (for value, type, and module components of structures, respectively), and vi, ti, and xi are identifiers (for values, types, and modules). All identifiers (e.g. xi) have a name part (here, x) and a stamp part (i) that distinguishes identifiers with the same name. Bound identifiers can be renamed, but α-conversion must preserve the name parts of identifiers and can only change the stamp part. This way, access by name inside structures is meaningful, yet α-conversion can still be performed to avoid name clashes.

t).

At the level of the module language (m), we have structures, functor abstractions and functor applications. Structures are collection of bindings for values, types and modules (either substructures or functors). The corresponding module types M are signatures (collections of declarations for values, types and modules) and functor types (dependent function types). Type components in signatures can be declared either abstractly (type t i ) or transparently (type t i = τ ).

Signatures are treated as opaque for signature matching, meaning that a transparent type binding (type t i = τ ) restricted by an abstract type specification (type t i ) becomes abstract: the type equality t i = τ is forgotten. SML's generative bindings abstype and datatype can therefore be expressed as a transparent type binding followed by a restriction by an abstract signature.

Complete programs P are sequences of definitions s that define an integer-valued field named res, which is the observable result of the program execution.

Typing rules

The typing rules for this calculus are shown in figure 1. The rules define the following judgements:

E m : M The module m has module type M . E M 1 <: M 2
The module type M 1 is a subtype of the module type M 2 . E M modtype The module type M is well-formed.

E P ok

The program P is well-typed.

We write BV (S) for the set of identifiers bound by the signature S, and similarly for typing environments. We assume

Typing of module expressions (E m : M ), structures (E s : S) and programs ( P ok):

E x i : E(x i ) (
E τ ≈ τ E (val vi : τ ) <: (val vi : τ ) (16) E M <: M E (module xi : M ) <: (module xi : M ) (17)
E (type ti = τ ) <: (type ti) (18) E (type ti) <: (type ti) (19) E τ ≈ τ E (type ti = τ ) <: (type ti = τ ) (20) E t i ≈ τ E (type t i ) <: (type t i = τ ) (21)
Type equivalence (E τ ≈ τ ):

E1; type ti = τ ; E2 ti ≈ τ (22) E p : sig S 1 ; type t i = τ ; S 2 end E p.t ≈ τ {n i ← p.n | n i ∈ BV (S 1 )} (23)
(Rules for congruence, reflexivity, symmetry, transitivity and base language-dependent equivalences omitted.)

Well-formedness of module types (E M modtype): rules omitted.

Denotational semantics

The dynamic semantics of the module calculus is obtained by erasing all type information and mapping structures to records and functors to functions. This is formalized as a standard denotational semantics shown in figure 2. We assume given a domain B of values for the base language, including a constant wrong denoting run-time type errors, and a meaning function [[•]] ρ for expressions of the base language. Writing f in → for partial functions with finite domain, the domain V of values for the module language is defined as:

V = (ValName f in → B) × (ModName f in → V ) + (V → V ) + wrong ⊥
Meaning of module expressions and programs:

[[x i ]] ρ = if x i ∈ Dom(ρ) then ρ(x i ) else wrong [[p.x]]ρ = let d = [[p]]ρ in if x ∈ Dom(d) then d(x) else wrong [[struct s end]]ρ = [[s]]ρ [[functor(x i : M )m]] ρ = λd. if d = wrong then wrong else [[m]] ρ+{x i →d} [[m 1 (m 2 )]] ρ = if [[m 1 ]] ρ ∈ V → V then [[m 1 ]] ρ ([[m 2 ]] ρ ) else wrong [[(m : M )]]ρ = [[m]]ρ [[ε]]ρ = {} [[val v i = e; s]] ρ = let d = [[e]] ρ in if d = wrong then wrong else let d = [[s]] ρ+{v i →d} in if d = wrong then wrong else {v → d} + d [[type t = τ ; s]] ρ = [[s]] ρ [[module xi = m; s]]ρ = let d = [[m]]ρ in if d = wrong then wrong else let d = [[s]] ρ+{x i →d} in if d = wrong then wrong else {x → d} + d [[prog s end]] = let d = [[s]] ∅ in if res ∈ Dom(s) then s(res) else wrong
Extension of the meaning function on value expressions: We now show that applicative functors ensure a suitable notion of type abstraction. Following Reynolds [START_REF] Reynolds | Types, abstraction and parametric polymorphism[END_REF] and Mitchell [START_REF] Mitchell | On the equivalence of data representations[END_REF], we use representation independence as the semantic characterization of type abstraction: a language enforces type abstraction if two implementations of an abstract type can be observationally equivalent (substituting one by the other in any program does not change the outcome of the program), yet use different representation types to implement this abstract type. The proof is an adaptation of Mitchell's proof for the SOL calculus [START_REF] Mitchell | On the equivalence of data representations[END_REF], which relies on logical relations.

[[p.v]] ρ = let d = [[p]] ρ in if v ∈ Dom(d) then d(v) else wrong
We first define binary logical relations for the values and type expressions of the module calculus. Logical relations are presented as the judgement Γ |= v ≈ v : M ⇒ T , read: "under the type interpretation Γ, the values v and v are equivalent when observed under type M and produce the type interpretation T ". The type interpretation Γ assigns a meaning to the type identifiers and type paths appearing in M . The T component records the relations we used to prove the equivalence of v and v . We need T because the elimination construct we use for abstract types (type paths) has open scope, in contrast with Mitchell's open construct, which has closed scope.

Let BaseRel be the set of admissible relation between base values (binary relations over B that do not relate wrong with wrong). Define

M odInterp = (T ypeN ame f in → BaseRel) × (M odN ame f in → M odInterp) + (M odInterp → M odInterp) InterpEnv = (T ypeIdent f in → BaseRel) × (M odIdent f in → M odInterp)
Module interpretations T ∈ M odInterp are either structure interpretations (a record mapping type names to base relations and module names to module interpretations), or functor interpretations (functions from interpretations to interpretations). Interpretation environments Γ ∈ InterpEnv map type identifiers to base relations and module identifiers to module interpretations. An interpretation environment Γ provides a meaning to type paths as admissible relations between base values in the obvious way:

Γ(p.t) = (Γ(p))(t) Γ(p.x) = (Γ(p))(x) Γ(p 1 (p 2 )) = (Γ(p 1 ))(Γ(p 2 ))
We first define a family (R τ Γ ) of logical relations over values of the base language in the usual way:

• (b1, b2) ∈ R int Γ iff b1 and b2 are equal integers • (b 1 , b 2 ) ∈ R t i Γ iff t i ∈ Dom(Γ) and (b 1 , b 2 ) ∈ Γ(t i ) • (b 1 , b 2 ) ∈ R p.t Γ iff Γ(p.t) is defined and (b 1 , b 2 ) ∈ Γ(p.t) • (b 1 , b 2 ) ∈ R τ →σ
(a 1 , a 2 ) ∈ R τ Γ , we have (b 1 (a 1 ), b 2 (a 2 )) ∈ R σ Γ We then define the judgement Γ |= v ≈ v : M ⇒ T by induction over M , as follows. 4. Γ |= s 1 ≈ s 2 : (val v i : τ ; S) ⇒ T iff (s 1 (v), s 2 (v)) ∈ R τ Γ and Γ |= s 1 ≈ s 2 : S ⇒ T 5. Γ |= s 1 ≈ s 2 : (type t i ; S) ⇒ T iff there exists an admissible base relation R and an interpretation T such that Γ + {t i → R} |= s 1 ≈ s 2 : S ⇒ T and T = {t → R} + T 6. Γ |= s 1 ≈ s 2 : (type t i = τ ; S) ⇒ T iff Γ + {t i → R τ Γ } |= s 1 ≈ s 2 : S ⇒ T and T = {t → R τ Γ } + T 7. Γ |= s1 ≈ s2 : (structure xi : M ; S) ⇒ T iff there exists interpretations T and T such that Γ |= s1(x) ≈ s2(x) : M ⇒ T and Γ + {xi → T } |= s1 ≈ s2 : S ⇒ T and T = {x → T } + T
Notice that in the fifth case (declaration of an abstract type ti), we do not require ti to be implemented by the same type expression in the two structures denoted by s and s : we can interpret ti by any admissible relation, not only R τ Γ for some τ , as long as the relation makes the remainder of the two structures related [START_REF] Mitchell | On the equivalence of data representations[END_REF]. We define similarly an equivalence relation Γ |= ρ ≈ ρ : E ⇒ Γ between evaluation environments ρ and ρ viewed under the typing environment E. The Γ component is an extension of Γ with interpretations for the identifiers declared in E.

The fundamental lemma of logical relations for the module calculus is as follows:

Proposition 1 If E m : M and ∅ |= ρ ≈ ρ : E ⇒ Γ, then there exists an interpretation T such that Γ |= [[m]] ρ ≈ [[m]] ρ : M ⇒ T.
Proof: standard inductive argument on the derivation of E m : M . 2

As a corollary, we obtain the representation independence property: two closed module expressions whose meanings are related can be substituted one for the other in any program. The first formulation is as follows:

Proposition 2 Let m1 and m2 be two closed module expressions such that ∅ m1 : M and ∅ m2 :

M . Assume ∅ [[m1]] ∅ ≈ [[m2]] ∅ : M ⇒ T for some T . For all pro- gram contexts C[ ] such that xi : M C[xi] ok, we have [[C[m1]]] = [[C[m2]]]. Proof: Let D[ ] be the structure context such that C[ ] = prog D[ ] end. We have [[C[m1]]] = [[D[m1]]] ∅ (res) and similarly for m2. Let ρ1 = {xi → [[m1]] ∅ } and ρ2 = {xi → [[m2]] ∅ } and E = (xi : M ). By hypothesis on m1 and m2, we have ∅ |= ρ1 ≈ ρ2 : E ⇒ Γ where Γ = {xi → T }.
By hypothesis on C, we have

E (struct D[xi] end) : (sig val res : int end). From the fundamental lemma, it follows that Γ |= [[struct D[xi] end]]ρ 1 ≈ [[struct D[xi] end]]ρ 2 : (sig val res : int end) ⇒ T for some T . It is easy to check that [[D[xi]]]ρ 1 = [[D[m1]]] ∅ ,
and similarly for m2 and ρ2. Extracting the res integer field from the denotations of D[m1] and

D[m2], it follows that ([[D[m 1 ]]] ∅ (res), [[D[m 2 ]]] ∅ (res)) ∈ R int Γ , which means [[C[m1]]] = [[C[m2]]] since R int Γ is the equality relation over integers. 2
Proposition 2 is a relatively weak result, because the assumption x i : M C[x i ] ok requires the program context C[ ] to be parametric with respect to all possible implementations of the signature M and prevents C[ ] from taking advantage of more typing hypothesis that could be derived about a particular implementation. The following reformulation of proposition 2 shows that even without the hypothesis x i : M C[x i ] ok, the applicative functor calculus prevents C[ ] from depending too closely on a particular implementation of M .

In the following statement, we say that a module type M is principal for a module expression m in an environment E if E m : M and for all types M and environments E such that

BV (E ) ∩ BV (E) = ∅, if E; E m : M , then E; E M <: M .
Proposition 3 Let m1 and m2 be two closed module expressions and M be a module type. Assume that M is a principal type for m1 and for m2 in the empty environment. Then, for

all program contexts C[ ], the program C[m1] is well-typed if and only if C[m2] is, and if so, [[C[m1]]] = [[C[m2]]]. Proof: Assume ∅ C[m 1 ] ok.
Using the fact that M is principal for m 1 , we can build a derivation of

x i : M C[x i ] ok. Applying proposition 2, it follows that [[C[m 1 ]]] = [[C[m 2 ]]]. 2
Two closed modules m1 and m2 that have a common principal type and are equivalent at that type are therefore observationally equivalent. Moreover, this condition does not require that the two modules implement their type components by the same representation types. Consider the typical situation: M = sig type t; val x: t end m 1 = (struct type t = τ 1 ; val x = ... end : M) m 2 = (struct type t = τ 2 ; val x = ... end : M) If m 1 and m 2 are well-typed, then M is principal for m 1 and m 2 . (Since signature constraints are not paths, the "self" rule does not apply to m 1 and m 2 , and therefore no type smaller than M can be derived.) Moreover, by definition of logical relations, the denotations of m 1 and m 2 can be related even if τ 1 is incompatible with τ 2 . This would not be the case if the class of paths were extended further, e.g. by allowing any module expression in paths. Then, the "self" rule would apply to the definitions of m 1 and m 2 , allowing the derivation of the following typings: m1 : sig type t = m1.t; val x: t end m2 : sig type t = m2.t; val x: t end and M would no longer be the principal type of m1 and m2. The hypothesis that m1 and m2 have the same principal type would force m1 and m2 to be syntactically identical, hence τ1 and τ2 to be identical as well.

This situation cannot happen in the applicative functor calculus: m1 and m2 in proposition 3 cannot be paths since they must be closed, while paths p ::= xi | p.x | p1(p2) always have at least one free structure identifier. Hence, the "self" rule does not apply to m1 and m2, thus m1 and m2 can have the same principal type while implementing abstract type components differently.

This discussion shows that introducing functor applications in paths does not compromise representation independence as characterized by proposition 3, but further extensions of the class of paths could. Subtyping and type equivalence: (rules omitted: congruence, transitivity and symmetry for ≈, transitivity for <:) E m : EQ(τ )

Typing rules:

E x i : E(x i ) (
E π t (m) ≈ τ (34) E M ≈ M E M <: M (35) E τ type E EQ(τ ) <: TYPE (36) E M1 <: M 1 E; xi : M1 M2 <: M 2 E (Σx i : M 1 . M 2 ) <: (Σx i : M 1 . M 2 ) (37) E M 1 <: M1 E; xi : M 1 M2 <: M 2 E (Πx i : M 1 . M 2 ) <: (Πx i : M 1 . M 2 ) ( 38
)
Type strengthening:

V(τ )/m = V(τ ) TYPE/m = EQ(πt(m)) EQ(τ )/m = EQ(πt(m)) (Σx i : M 1 . M 2 )/m = Σx i : (M 1 /π 1 (m)). (M 2 /π 2 (m)) (Πx i : M 1 . M 2 )/m = Πx i : M 1 . (M 2 /m(x i ))
Figure 3: Typing rules for the manifest sums calculus 5 Full transparency for higher-order functors

In this section, we prove that the module calculus with applicative functors has fully transparent higher-order functors, in the sense of MacQueen and Tofte [START_REF] Macqueen | A semantics for higherorder functors[END_REF]. One way to prove this result is to take their static semantics for higherorder functors and show that all correct programs in this semantics are well-typed in our calculus. We have not been able to show this result due to the complexity of their formalism. Instead, we will show that the calculus with applicative functors can encode a stratified calculus with strong sums similar to MacQueen's DL calculus and Harper and Mitchell's XML calculus [START_REF] Macqueen | Using dependent types to express modular structure[END_REF][START_REF] Harper | On the type structure of Standard ML[END_REF]. Strong sums account for many features of the SML module system, excluding generativity but including transparent type bindings and fully transparent higher-order functors. The existence of a typepreserving encoding into the calculus with applicative functors is therefore a strong hint that the latter ensures full transparency.

The manifest sums calculus

To simplify the encoding, we start from the "manifest sums" calculus, a variant of the strong sums calculus that differs on the way type equalities are propagated (through compiletime reductions of terms in the strong sums calculus, but through enriched types in the manifest types calculus), but has the same expressive power. All terms well-typed with strong sums are also well-typed with manifest sums; we omit the proof, which is along the lines of the proof of proposition 1 in [START_REF] Leroy | Manifest types, modules, and separate compilation[END_REF]. The manifest sums calculus has the following syntax:

Terms: m ::= xi | λxi : M. m | m1(m2) | ιv(e) | ιt(τ ) | xi = m1, m2 | π1(m) | π2(m)
Types:

M ::= V(τ ) | TYPE | EQ(τ ) | Σx i : M 1 . M 2 | Πx i : M 1 .

Path normalization

In preparation for the encoding into the applicative functor calculus, we first show how to rewrite terms to meet the syntactic restrictions imposed by the latter, such as the restriction of projections to paths. Paths p in the manifest sums calculus are described by the grammar

p ::= x i | π 1 (p) | π 2 (p) | p 1 (p 2 ).
To express the rewriting more easily, we extend the syntax of terms and types with a let binding (i.e. explicit substitutions): The first group of rewrite rules introduce names for arguments to projections that are not paths. In the following, mc ranges over terms that are not paths.

Over terms:

ιv(e[πv(mc)])

→ let xi = mc in ιv(e[πv(xi)]) ι t (τ [π t (m c )]) → let x i = m c in ι t (τ [π t (x i )]) π 1 (m c ) → let x i = m c in π 1 (x i ) π 2 (m c ) → let x i = m c in π 2 (x i ) m(mc) → let xi = mc in m(xi) Over types: V(τ [πt(mc)]) → Let xi = m in V(τ [πt(xi)]) EQ(τ [π t (m c )]) → Let x i = m in EQ(τ [π t (x i )])
The let bindings have no equivalent in the applicative functor calculus, unless they occur immediately below a pair construction, in which case they can be translated as extra bindings in a struct...end. The second group of rules lift let bindings upwards until they hit a pair operator.

Over terms:

let σ in let σ in m → let σ; σ in m (let σ in m 1 )(m 2 ) → let σ in m 1 (m 2 ) λx i : M. let σ in m → let λx i : M. σ in σ(m, x i ) λxi : (Let σ in M ). m → let σ in λxi : M. m Over types: Let σ in Let σ in M → Let σ; σ in M Σx i : (Let σ in M 1 ). M 2 → Let σ in Σx i : M 1 . M 2 Σx i : M 1 . (Let σ in M 2 ) → Let λx i : M 1 . σ in Σx i : M 1 . σ(M 2 , x i ) Πxi : (Let σ in M1). M2 → Let σ in Πxi : M1. M2 Πx i : M 1 . (Let σ in M 2 ) → Let λx i : M 1 . σ in Πx i : M 1 . σ(M 2 , x i ) Over substitutions: x i = (let σ in m); σ → σ; x i = m; σ
To express the introduction of abstractions and applications when a let-binding crosses a binder (λ, Σ or Π), we have used the following notations: if σ is the substitution The encoding, written • , is defined as: We then show that this encoding is type-preserving: if E m : M in the manifest sums calculus and E, m, M are normalized, then E m : M in the applicative functor calculus. This completes the proof that our calculus with applicative functors can express strong sums.

y 1 =
x i = x i π1(p) =

Related work

Several semantics for fully transparent higher-order functors have been given, first in type-theoretic frameworks based on strong sums [START_REF] Macqueen | Using dependent types to express modular structure[END_REF][START_REF] Harper | On the type structure of Standard ML[END_REF], then as extensions of SML's stampbased static semantics [START_REF] Macqueen | A semantics for higherorder functors[END_REF][START_REF] Biswas | Higher-order functors with transparent signatures[END_REF]. Only MacQueen and Tofte's formalism [START_REF] Macqueen | A semantics for higherorder functors[END_REF] handles the full SML module language; both the strong sums-based models [START_REF] Macqueen | Using dependent types to express modular structure[END_REF][START_REF] Harper | On the type structure of Standard ML[END_REF] and Biswas's static semantics based on higher-order variables [START_REF] Biswas | Higher-order functors with transparent signatures[END_REF] fail to account for generative type definitions. Unfortunately, MacQueen and Tofte's description is technically involving, in part because it is oriented towards an efficient implementation (functor re-elaboration is minimized). The present paper provides a simpler description of fully transparent higher-order functors with both generative and non-generative type bindings; the main missing SML feature is structure generativity and sharing.

Among the formalisms mentioned above, ours is the only one that provides complete syntactic signatures for higherorder functors (syntactic signatures that captures exactly their transparent behavior), which are required to support Modula-2 style separate compilation. Crégut [START_REF] Crégut | Compilation séparée pour un langage de modules avec types génératifs[END_REF] also attacks the problem of complete syntactic signatures for higherorder functors. His proposal relies on enriching signatures with equalities between structures (ours uses only equalities between types), which has the advantages of accounting for structure sharing and remaining compatible with the standard generative semantics of functor application, and the disadvantage of requiring a rather complex stamp-based formalism.

A notion of functors with applicative semantics appears in Rouaix's Alcool language [START_REF] Rouaix | The ALCOOL 90 report[END_REF], which combines Haskellstyle dynamic overloading with a type abstraction mechanism. In the presence of dynamic overloading, applicative functors arise naturally a generalization of ML's parameterized type constructors such as list: when types are equipped with dictionaries of functions implementing overloaded symbols at that type, parameterized types become functors from types plus dictionaries to types plus dictionaries. Since type constructors are applicative by definition (the types τ 1 list and τ 2 list are equal as soon as τ 1 = τ 2 ), these functors naturally have applicative semantics. The applicative semantics of functors might therefore prove useful to account for type classes or Alcool-style abstract types by translation to a language with structures and functors.

Conclusions

The applicative semantics of functor applications seems useful to increase the expressive power of the SML module system, and has very little impact both on the semantic properties of the language and on the complexity of its type system. It supports precise syntactic signatures for fully transparent higher-order functors, which facilitates separate compilation and provides a simple formalization of full transparency. On the negative side, the applicative semantics precludes modules as first-class values; also, existing stamp-based typecheckers cannot easily be modified to implement it. More practical experience with the applicative semantics is needed to assess its impact on the modular programming style.

  signature ORD = sig type t; val less: t -> t -> bool end functor Set(Elt: ORD): SET = struct type elt = Elt.t datatype set = Leaf | Node of set * elt * set val empty = Leaf ... (* Familiar ordered binary tree implementation omitted *) end The following signature for the Set functor captures the fact that the elt component of the result is the same type as the t component of the argument: functor Set(Elt: ORD): SET = sig type elt = Elt.t type set val empty: set val member: elt -> set -> bool ..

  functor G(A:S) = struct type t = A.t * A.t end functor ApplyProd(functor F(X:S):S; structure A:S) = F(G(A))

  val r = ref false functor F() : sig type t end = (r := not !r; if !r then struct type t = int end else struct type t = bool end) structure A = F() structure B = F() Semantically, A.t is int and B.t is bool, but the applicative semantics for functors assumes A.t = B.t.

Figure 1 :

 1 Figure 1: Typing rules

Figure 2 :

 2 Figure 2: Denotational semantics

Γ iff b 1

 1 and b 2 are functions, and for all base values

  Terms:m ::= . . . | let σ in m Types:M ::= . . . | Let σ in M Substitutions: σ ::= ε | x i = m; σFor the purposes of type-checking and evaluation, let x1 = m1; . . . ; xn = mn in m is treated as the textual substitution m{xn ← mn} . . . {x1 ← m1}.

  p .fst π2(p) = p .snd λx i : M. m = functor(x i : M ) m m(p) = m ( p ) ι v (e) = struct val v i = e end ιt(τ ) = struct type t i = τ end xi = (let σ1 in m1), let σ2 in m2 = struct σ1 ; module fstj = m1 ; σ2 {xi ← fstj}; module snd k = m2 {xi ← fstj} endThe encoding of a substitution is a sequence of module bindings: x1 = m1; . . . ; xn = mn is (module x1 = m1 ; . . . ; module xn = mn ). Types are translated to module types and signatures as follows:V(τ ) = sig val v i : τ end TYPE = sig type t i end EQ(τ ) = sig type t i = τ end Σx i : M 1 . M 2 = sig module fst j : M 1 ; module snd k : M 2 {x i ← fst j } end Πxi : M1. M2 = functor(xi : M1 ) M2Finally, for projections inside values and simple types, we take πv(p) = p .v πt(p) = p .t

  If all structure expressions are allowed in paths, the "self" rule makes abstract types that happen to have the same implementation automatically compatible: structure A = struct abstype t = τ with decls end structure B = struct abstype t = τ with decls end By application of the "self" rule, we obtain the following signatures for A and B:

	p : sig ... type t; ... end
	then it also has signature
	p : sig ... type t = p.t; ... end
	A: sig type t =
	(struct abstype t = τ with decls end).t;
	... end
	B: sig type t =
	(struct abstype t = τ with decls end).t;
	... end
	Hence A.t = B.t, which violates type abstraction.

  Consider the following Dict functor implementing dictionaries: Dict and PrioQueue cannot be used together, because the set types used by the contents and domain functions are not compatible:

		Then, structure IntOrder =
	signature DICT = sig type key	struct type t = int; fun less x y = (x<y) end structure IntDict = Dict(IntOrder) structure IntPrioQueue = PrioQueue(IntOrder)
	type 'a dict val empty: 'a dict val add: key -> 'a -> 'a dict -> 'a dict val find: key -> 'a dict -> 'a end	The types IntDict.KeySet.set and IntPrioQueue.EltSet. set are incompatible, therefore the following expression does not type-check: IntDict.domain d = IntPrioQueue.contents q
	functor Dict(Key: ORD): DICT = struct type key = Key.t datatype 'a dict =	The SML solution to the problem above is to avoid ap-plying locally the Set functor and parameterize instead Dict and PrioQueue by the required Set structure:
	Leaf | Node of 'a dict * key * 'a * 'a dict ... (* Binary tree implementation omitted *) end	functor Dict( structure Key: ORD structure Set: SET sharing Set.elt = Key.t): DICT =
	Assume we need to extend this functor with a domain op-eration that returns the set of keys of a dictionary. To do so, we need a structure implementing sets of keys. The sim-plest approach is to construct this structure inside the Dict functor, using the Set functor:	struct ... structure KeySet = Set ... end functor PrioQueue( structure Elt: ORD structure Set: SET
	signature DICT =	sharing Set.elt = Elt.t): PRIOQUEUE =
	sig	struct
	...	... structure EltSet = Set ...
	structure KeySet: SET sharing KeySet.elt = key	end
	val domain: 'a dict -> KeySet.Set	structure IntSet = Set(IntOrder)
	end	structure IntDict =
	functor Dict(Key: ORD): DICT =	Dict(structure Elt = IntOrder
	struct	structure Set = IntSet)
	...	structure IntPrioQueue =
	structure KeySet = Set(Ord)	PrioQueue(structure Elt = IntOrder
	fun domain dict = ...	structure Set = IntSet)
	end	By hoisting the application Set(IntOrder) outside of Dict
	Unfortunately, the signature above does not reflect that	and PrioQueue, we have made explicit that the KeySet and
	KeySet has been obtained by applying Set to Ord; there-	EltSet substructures of IntDict and IntPrioQueue provide
	fore, the type KeySet.set in the result structure of Dict is	compatible set types. Therefore, the following expression
	assumed incompatible with other set types obtained by ap-	now type-checks:
	plying Set elsewhere to the same ordered type. Continuing
	the example, assume we have another functor, say an im-
	plementation of priority queues, that uses the same trick as
	Dict:
	signature PRIOQUEUE =
	sig
	type elt
	type queue
	val empty: queue
	val add: elt -> queue -> queue
	val extract: queue -> elt * queue
	structure EltSet: SET sharing EltSet.elt = elt
	val contents: queue -> EltSet.set
	end
	functor PrioQueue(Elt: ORD): PRIOQUEUE =
	struct
	...
	structure EltSet = Set(Elt)
	...
	end

  Since the signatures show explicitly how the set types are derived from the functor arguments, the structures obtained by applying Dict and PrioQueue to the same ordered type now interact correctly:

	functor Dict(Key: ORD):
	sig
	type key = Key.t
	type 'a dict
	...
	val domain: 'a dict -> Set(Key).set
	end
	functor PrioQueue(Elt: ORD):
	sig
	type elt = Elt.t
	type queue
	...
	val contents: queue -> Set(Elt).set
	end
	structure IntDict = Dict(IntOrder)
	(* : sig
	...

val domain: 'a dict -> Set(IntOrder).set end *) structure IntPrioQueue = PrioQueue(IntOrder) (* : sig ... val contents: queue -> Set(IntOrder).set end *)

  As in the first-order case, the propagation of type equalities through syntactic functor signatures is limited by the fact that only paths are allowed in type expressions, not type projections from arbitrary structures. Consider the following variant of Apply:

	functor ApplyProd(functor F(X:S):S;
	structure A:S) =
	F(struct type t = A.t * A.t end)
	Its natural signature is:
	functor ApplyProd(functor F(X:S):S;
	structure A:S):
	sig
	type t = F(struct type t = A.t * A.t
	For instance,
	structure B = Apply(Identity Int)
	(* : sig type t = Identity(Int).t end *)

and Identity(Int) has signature sig type t = Int.t end, from which it follows B.t = Int.t = int. Similarly, structure C = Apply(Constant Int) (* : sig type t = Constant(Int).t end *) and Constant(Int).t = bool, hence C.t = bool, as expected.

  | π 1 (p) | π 2 (p) | p 1 (p 2 ) Normalized terms: m ::= p | λxi : M. m | m(p) | ιv(e) | ιt(τ ) | xi = (let σ1 in m1), let σ2 in m2Normalized terms are then encoded as module expressions from the applicative functor calculus by turning injections and pairs into structures with conventional field names (v for values, t for types, fst and snd for pair components).

	Paths:
	p ::= x i Simple terms:
	e ::= . . . | πv(p)
	Simple types:
	τ ::= . . . | π t (p)
	5.3 Encoding
	Moreover, a
	term in normal form with respect to the rules above is such
	that: all projections are applied to paths; all functions ar-
	guments in applications are paths; no Let bindings remain;
	and let bindings occur only in toplevel position or as ar-
	guments to a pair construction. Assuming without loss of
	generality that complete programs have a pair in toplevel
	position, and identifying m with let ε in m as needed, we
	can therefore describe normalized programs by the following
	grammar:

m 1 ; . . . ; y n = m n , we write

λx i : M. σ for y 1 = λx i : M. m 1 ; . . . ; y n = λx i : M. m n σ(m, x i ) for m{y 1 ← y 1 (x i ) . . . y n ← y n (x i )}

It can be shown that the rewrite rules above preserve typing: if E m : M and m → m , then E m : M .

Γ |= s 1 ≈ s 2 : sig S end ⇒ T iff s 1 and s 2 are semantic signatures such that Γ |= s 1 ≈ s 2 : S ⇒ T

2. Γ |=f1 ≈ f2 : functor(xi : M )N ⇒ T iff f1, f2and T are functions such that for all values v1, v2 and interpretations X satisfying Γ |= v1 ≈ v2 : M ⇒ X, we haveΓ + {xi → X} |= f1(v1) ≈ f2(v2) : N ⇒ T (

X) 3. Γ |= s1 ≈ s2 : ε ⇒ {} for all semantic signatures s1 and s2


Damien Doligez

Xavier Leroy

A concurrent, generational garbage collector for a multithreaded implementation of ML

This paper presents the design and implementation of a \quasi real-time" garbage collector for Concurrent Caml Light, an implementation of ML with threads. This two-generation system combines a fast, asynchronous copying collector on the young generation with a nondisruptive concurrent marking collector on the old generation. This design crucially relies on the ML compiletime distinction between mutable and immutable objects.

Introduction

This paper presents the design and implementation of a garbage collector for Concurrent Caml Light, an implementation of the ML language that provides multiple threads of control executing concurrently in a shared address space.

Garbage collection | the automatic reclamation of unused memory space | is one of the most problematic components of run-time systems for multi-threaded languages. The naive \stop-the-world" approach, where all threads synchronously stop executing the user's program to perform garbage collection, is clearly inadequate, since it introduces synchronization between otherwise independent threads. For instance, this can result in all threads being blocked for some time if one thread is in the middle of a lengthy, uninterruptible operation when garbage collection starts. This contravenes one of the main motivations for having multiple threads: to reduce the response time of interactive applications. To achieve this goal, a promising direction is to run the garbage collector concurrently with the threads that execute the user's program, with as little synchronization as possible between the collector and the mutators (the threads executing the user's program).

Authors' address: INRIA Rocquencourt, B. P. 105, 78153 Le Chesnay, France. E-mail: Damien.Doligez@inria.fr, Xavier.Leroy@inria.fr.

A number of concurrent collectors have been described in the literature, such as the concurrent markand-sweep algorithm [START_REF] Cousineau | The categorical abstract machine[END_REF][START_REF] Hickey | Performance analysis of on-the-y garbage collection[END_REF][START_REF] Baker | List processing in real time on a serial computer[END_REF], which requires no synchronization with the mutators, at the price of a moderate overhead on the mutators. However, these designs seem unable to meet the memory demands of typical ML programs. ML programs tend to have high allocation rates, but many allocated objects have a short life span. This is due in part to the ML language itself, which encourages a programming style where many intermediate structures are built; and in part to some compilation techniques 1, 10] that result in heap allocation for large amounts of environments and control structures.

The garbage collection technique most adapted to this allocation pro le is generation scavenging 24], that concentrates reclamation e ort on recently allocated objects. However, the e cient implementation of generation scavenging requires the ability to relocate objects by copying between the memory areas that hold the various \generations" of objects. Performing relocation while the mutators are running is problematic: we must ensure that the mutators are aware of the relocation, and do not try to access a relocated object at its old, invalid address. Some designs rely on tests when dereferencing a heap pointer [START_REF] Reppy | CML: a higher-order concurrent language[END_REF][START_REF] Appel | Virtual memory primitives for user programs[END_REF]; others, on an extra indirection word for each heap object [START_REF] Boehm | Mostly parallel garbage collection[END_REF][START_REF] Morriset | A portable multiprocessor interface for Standard ML of New Jersey[END_REF]; others, on virtual memory page protections 2]. All three approaches entail a signi cant run-time penalty on the mutators, unless special hardware or special system software is used.

The memory management system presented in this paper is an attempt to circumvent this weakness of concurrent copying collectors by relying on speci c features of the ML language. This system has two generations, with a fast, asynchronous copying collector on the young generation, and a non-disruptive concurrent marking collector on the old generation. The aforementioned di culties with copying are avoided by splitting the young generation into areas attached to the mutators, each area being accessed by one mutator only. The performance issue with concurrent mark-and-sweep is avoided by the fact that the allocation rate in the old generation is low, since most short-lived objects are reclaimed by the copying collectors. This combination results in quasi real-time performance for memory allocation, while keeping the overhead on the mutators low.

This design relies crucially on two features of ML. First, the ML type system distinguishes at compile-time between mutable objects (that can be physically modi ed) and immutable objects. Second, duplicating immutable objects is semantically transparent. The rst point makes it possible to have di erent allocation policies for mutable and immutable objects. The second point allows copying the object residing in the private area of a mutator at arbitrary times.

The remainder of this paper is organized as follows. Section 2 brie y describes the Concurrent Caml Light system. Section 3 presents the memory organization; the concurrent aspects of the system (the mark-andsweep major collector) are detailed in section 4. Section 5 comments on some experimental results. Section 6 discusses some directions for further work. Finally, section 7 compares our design with some other concurrent collectors.

Concurrent Caml Light

Concurrent Caml Light is an extension of Caml Light 12,[START_REF] Kung | An e cient parallel garbage collection system and its correctness proof[END_REF], the authors' implementation of the ML language, with concurrency primitives. The concurrency model is lightweight processes (threads) with shared memory. The synchronization tools are locks and conditions. (Figure 1 shows the Caml Light interface to the module providing the concurrency primitives.) This is the model provided by the C Threads library under the Mach operating system 9]. On top of these concurrency primitives, we can to implement higher-level concurrency abstractions such as channels and events [START_REF] Paulson | ML for the working programmer[END_REF][START_REF] Ben-Ari | Algorithms for on-the-y garbage collection[END_REF].

The ML language is a conventional imperative language with functions as rst-class values and strong static typing [START_REF] North | Concurrent garbage collection on stock hardware[END_REF][START_REF] Leroy | The ZINC experiment: an economical implementation of the ML language[END_REF]. From the standpoint of memory management, the ML language has two distinctive features that are crucial to the design described here. The rst feature is that not all ML data structures can be modi ed in-place. That is, the updating primitives provided by the language operate only on speci c data types, either built-in (such as references and arrays) or specially declared (such as the Caml record types with \mutable" elds). This fact, combined with strong static typing, ensures a clear separation at compile-time between mutable objects (that can be physically updated) and immutable objects (that can only be read type process;; value fork : (unit -> 'a) -> process and exit : unit -> 'a and join : process -> unit and detach : process -> unit and yield : unit -> unit and self : unit -> process;; type mutex;; type condition;; value new_mutex : unit -> mutex and new_condition : unit -> condition and lock : mutex -> unit and unlock : mutex -> unit and try_lock : mutex -> bool and signal : condition -> unit and broadcast : condition -> unit and wait : condition -> mutex -> unit;;

Figure 1: The interface to the module thread providing the concurrency primitives once constructed). This permits di erent allocation policies for mutable and immutable objects; our design takes advantage of this fact. Another important feature of ML is that it does not specify any generic physical equality primitive similar to eq in Lisp. The provided equality primitive implements structural equality on immutable objects, and physical equality on mutable objects. Consequently, there is no way to test two immutable objects for physical equality. Combined with the fact that immutable objects cannot be modi ed in-place, this means that it is always semantically correct to duplicate an immutable structure: the original structure and its copy cannot be distinguished by any program. Our collector does indeed duplicate immutable structures and keeps the two copies alive for some time | strange as it may sound for a system that is supposed to reclaim memory space.

Overview of the memory organization

The memory heap is organized as follows. (See gure 2.) First, there is a large, common heap shared between all threads. All threads can allocate, read, and update objects in the shared heap. Then, each thread possesses its own, small, private heap (typically 32K). On a modern shared-memory architecture with large, write-back caches, we expect the private heap to remain in one and only one cache most of the time, thereby causing very little bus tra c when it is accessed. This assumes that the system scheduler is clever enough to tie each thread to a single processor whenever possible. When the private heap becomes full, the corresponding thread stops and performs a minor collection: it copies all live objects in the private heap to the shared heap. Live objects are those that are pointed to by the memory roots of the thread (the registers and the stacks of the machine), as well as their descendents. This copying makes the whole private heap available again for private allocation. Consequently, allocation in the private heap is performed linearly, and requires only one pointer comparison and one pointer increment. A minor collection can be performed at any time, regardless of the status of the other mutator threads. The only synchronization required is when allocating the copied objects in the shared heap.

Major collection on the shared heap is performed by a dedicated thread, which runs concurrently with the mutator (and minor collection) threads. It uses the concurrent mark and sweep algorithm described by Dijkstra et al. 11]. We postpone a complete discussion of the algorithm and the cooperation between the major collector thread and the other threads to the next section. Since the major collector does not move objects, no synchronization is required when accessing or modifying an object in the shared heap, either for the major collector thread or for the mutator threads. Race conditions can result in a dead object not being collected by the current major collection cycle; but they cannot result in a live object being reclaimed.

If the available space in the shared heap drops to zero before the major collection cycle is over, then the muta-tor threads attempt to enlarge the shared heap, by extending the process address space, instead of waiting for the major collection to nish. We want to avoid blocking the mutator threads as much as possible. Blocking is only required in the unlikely case where the virtual memory is exhausted.

Copy on update

The design outlined above assumes that there are no pointers from the shared heap to a private heap, nor from one private heap to another private heap. Otherwise, a private heap could contain objects that are live, but not directly reachable from the roots of the corresponding threads. Without special treatment, a pointer from the shared heap to a private heap can be created by updating an \old" mutable object, residing in the shared heap, with a pointer to a newly created structure, that still resides in a private heap; and a pointer between two private heaps can then be created by reading the mutable object from another thread.

This situation is avoided by copying the transmitted private object to the main shared heap and storing in the old mutable object a pointer to the copy, instead of a pointer to the original private object. The descendents of the transmitted object that reside in the private heap are recursively copied, too. This copying is very similar to a minor collection with only one root, the transmitted object. Indeed, it stores forwarding pointers from the copied objects to their copies, just as the minor collector does, so that the next minor collection will not copy these objects again, but reuse their copies.1 Therefore, this \copy on update" strategy does not waste time: we just do some of the next minor collection right away. Also, it avoids the complexity of maintaining a remembered set of old objects that contain pointers to the young generation 24].

Allocation of mutable objects

Until the next minor collection, the thread that created the transmitted object can access both the original, private object and its copy in shared memory: the original object can still be reached through the memory roots of the thread, since we haven't updated the roots of the thread; the copy can be accessed by dereferencing the mutable object in which it was stored. Therefore, we must ensure that the two objects are semantically equivalent. This is the case if both objects contain only immutable structures; then, as pointed out in the previous section, no constructions in the ML language can distinguish one from the other. This is no longer true if the original object contains a mutable structure, because it would be duplicated during the copying process. This could lead to an update of the two mutable structures by two di erent objects, breaking the equivalence between the transmitted object and its copy.

To avoid this situation, it su ces to allocate mutable objects directly in the main, shared heap. Then, they will never be copied, since they already reside in the shared heap. This makes copying semantically transparent. Of course, a performance penalty is incurred: allocation in the shared heap is more expensive than allocation in the private heap, because of the required synchronization and free-list searching. However, most ML programs allocate relatively few mutable objects, and they tend to have a longer life span than average. This keeps the overhead reasonable.

The concurrent collector

The major collector implements the concurrent mark and sweep algorithm described by Dijkstra et al. 11]. In this section, we recall the basics of the algorithm, adapt it to our situation (Dijkstra et al. made some simplifying assumptions to keep correctness proofs manageable), and show how the mutator threads cooperate with the concurrent collector.

In this section, each thread along with its minor collector is considered a mutator thread by the major collector. The major collector will be called \the collector", and the mutator threads (and their minor collectors) will be called \the mutators".

The major collector does not essentially depend on the existence of the minor collectors. It only needs some way of asking a given mutator to mark the objects pointed to by its roots. In our design, this marking is performed by the minor collectors.

Four-color marking

Each object in the shared heap has one of four colors: white, gray, black, or blue. White denotes objects that have not yet been visited by the marking phase. Gray denotes objects that have been visited, but whose sons have not yet been visited. Black denotes objects that have been visited, and whose sons have been visited too. Blue is used for the free list objects: blue objects are always ignored by the collector. 2The color of a block evolves as summarized in gure 3. The marking phase sets to black all reachable objects. To do so, it sets the roots to gray and repeatedly nds a gray object and marks it. Marking an object means setting it to black, and shading its sons. Shading means setting the object to gray if it is white. The sweeping phase reclaims all white objects, setting them to blue and adding them to the free list. It also resets all black objects to white. Allocation in the heap turns blue objects back to white, gray or black, depending on the relative states of the collector and mutator, as detailed below.

The collection phases

The collector proceeds in three phases: root enumeration, end of marking, and sweeping. The root enumeration and end of marking together constitute the marking phase.

At the beginning of the root enumeration phase, the collector sets a global ag to signal the beginning of the marking phase. It then shades the global variables, and asks each mutator to shade its roots. During this phase, the collector also begins to nd gray objects and mark them as described above. 3 The root enumeration ends when the collector has obtained the roots of the last mutator. The collector then completes the marking phase by repeatedly marking gray objects until no more remain.

When the marking phase is nished, the collector examines each heap object in turn. All black objects are set to white. All white objects are free; they are set to blue and inserted into the free list (or collapsed with the preceding free object, if adjacent). Some objects might have been set to gray by the mutators since the end of the marking phase. These objects are also set to white.

The marking phase assumes that no object is black when it starts, and it ensures that all reachable objects are black or gray when it stops. More precisely: all objects that are reachable from the roots of a mutator at the time the mutator shades its roots, or that become reachable after that time, are black at the end of the marking phase. Objects can become reachable by allocation and by inplace modi cation, which are performed by the mutators concurrently with the collection. These operations therefore require some cooperation with the collector, as described below. The sweeping phase assumes that all reachable objects are black or gray when it starts, and it ensures that only unreachable objects are inserted into the free list, and that no black objects remain when it stops. Again, allocation and in-place modi cation require some cooperation with the collector, in order to avoid setting objects to black. These preconditions and postconditions ensure the correctness of the collector: only unreachable objects are ever inserted into the free list. The completeness (all unreachable objects are eventually inserted into the free list) stems from the following facts: no unreachable object ever becomes reachable again there are no blue objects outside of the free list all white objects unreachable at the start of the marking phase remain white all white objects are inserted into the free list by the sweeping phase gray objects that are unreachable at the beginning of the mark phase become black during marking, then white during sweeping, and are reclaimed by the next collection cycle.

Concurrent allocation and modi cation

As explained in 11], the mutators have to take the collector state into account when performing in-place modi cation on heap objects. Otherwise, updating an already black object could result in a reachable object that remains white at the end of marking. This problem is further complicated by the fact that the set of roots is not xed during the collection: mutators can push and pop pointers on their local stacks without any cooperation with the collector.

To avoid this kind of situations, the modi cation operation must shade both the old and the new value of the modi ed eld. Shading the new value ensures that it will be recognized as reachable by the collector, even if all other pointers to the new value disappear (e.g., by popping the last pointer from a stack). Shading the old value ensures that it will be recognized as reachable by the collector, in case some pointers to the old value are still kept on some stack.

In the simpli ed setting described in 11] (a xed set of roots), shading either the old or the new value is sufcient. This is not true in our case. Assume we do not shade the new value. Since the collector starts marking objects before having obtained all roots, a mutator can modify a black object by storing a pointer to a white object which is only reachable from the local stack, then pop all pointers to this white object before shading its roots. This results in a reachable object that remains white. This kind of pointer smuggling is illustrated in gure 4. Now, assume we do not shade the old value. The mutator could give its roots, then push a white eld of a white object onto its stack, then overwrite that eld. This results in a white object that is reachable from the stack. (See gure 5.) This coloring at modi cation time is only necessary during the marking phase. For the sake of e ciency, we do not perform it during the sweeping phase, avoiding the creation of gray objects that would survive a complete collection cycle before being reclaimed.

Concurrent allocation raises similar issues: the newly allocated objects must be assigned the right color, depending on the collector status. During the marking phase, objects are allocated black. This is justi ed by the fact that the allocated objects become reachable, and their sons were already reachable, hence will eventually be set to black. Setting the allocated objects to gray would also be correct, but the marking phase might not terminate.

During the sweeping phase, objects are allocated

Synchronization issues

The coloring scheme described above has one interesting property: it is always safe to set an object to gray. Of course, setting many objects to gray is ine cient, since an unreachable gray object will not be reclaimed at the end of the current collection cycle, but only at the end of the next cycle. However, this fact allows us to avoid synchronization whenever the resulting race condition can only end up in making an object gray instead of the intended color.

This trick is used in the modi cation and allocation procedures, to test the collector status without locking. For instance, the coloring of newly allocated blocks is implemented as follows:

1. if phase = marking then 2.

set the object to black; 3.

if phase = sweeping then 4.

set the object to gray; 5. else 6. if address(object) < sweep pointer then 7.

set the object to white; 8. else [START_REF] Brooks | Trading data space for reduced time and code space in real-time garbage collection on stock hardware[END_REF].

set the object to gray;

There are two race conditions between this code and the collector. First of all, the collector may enter the sweeping phase between lines 1 and 2. Then, the object could incorrectly be set to black after being swept. In this case, lines 3 and 4 set the object back to gray, which meets the preconditions of the next marking phase. The collector must synchronize with all mutators before entering the marking phase, hence line 4 is guaranteed to complete before the next marking cycle. The other race condition is that the sweep pointer can change after the test in line 6. However, the sweep pointer is monotonically increasing, hence the race condition can only result in executing line 9 instead of line 7, i.e. in setting the object to gray instead of white, which is safe.

Interface with the minor collector

The shading of roots is performed by a variant of the minor collector that sets to gray all objects copied to the major heap, as well as all root objects that are already in the major heap. This requires little extra work compared with a normal minor collection. Hence, the least disruptive technique for getting the roots is to set a ag telling the minor collectors to shade the roots, and wait for all the mutators to complete a minor collection. However, a mutator can execute a program that does not allocate; it can also be blocked on a lock, or waiting for input or output. In the former case (looping mutator), the major collector interrupts the mutator and forces a premature minor collection. In the latter case (blocked mutator), the major collector performs the copying and shading itself; this is similar to a minor collection, except that the minor heap is not emptied. The major collector also has to make sure the mutator does not resume execution before the copying and shading is complete. This is the most disruptive interaction between the collector and a mutator, but it is infrequent.

Experimental results

We have implemented the collector described above in a prototype ML system derived from Caml Light release 0.4. It runs on an Encore Multimax with fourteen NS32532 processors, under the Mach operating system. Each processor is rated at about 6 MIPS, and has a 256 K write-back cache. The Caml Light system is a fast bytecode interpreter; it runs 4 to 8 times slower than the SML of New Jersey native-code compiler. To put the timings below in perspective, an application of the identity function takes about 15 s. The measurements used 32 K private heaps, that easily t into the In this section, we comment on some measurements performed on this implementation. We have used the following test programs:

A parallel implementation of the Knuth-Bendix completion algorithm. The program comprises fteen threads, and performs lots of interprocess communication via shared mutable data structures.

A pipelined version of the Caml Light compiler, with one thread for the lexical analyzer, one for the parser, and one for the remainder of the compiler. This program is a typical example of the producerconsumer model. The parallel version relies on \futures", that is, lazy structures with speculative evaluation. The measurements have two goals: rst, estimate the latency of memory operations such as allocation and inplace modi cation; second, determine whether the major collector keeps up with a high number of active mutators. For the rst point, we have measured how long the mutators are interrupted by (1) minor collections, (2) copy on update operations, and (3) direct allocation in the major heap, which requires synchronization. For the second point, we take advantage of the fact that the major collector does not run continuously, but only when the amount of free space in the shared heap drops below a certain threshold (15% of the total heap size, in the experiments). Hence, the running time of the major collector compared with the execution time of the whole program gives an estimate of the load of the major collector.

The results are given in gure 6. The load of the major collector appears to be below 5% per mutator. This suggests that our design should scale to about 20 mutators. These results hold for the four realistic programs considered here. However, on arti cial examples that do nothing but allocate mutable objects, the major collector cannot keep up with as few as four mutators. This is an experimental con rmation of the initial assumption that real ML programs do not allocate much mutable data.

The average latency times are remarkably low. Most minor collections complete in less than 10 ms. The copyon-update strategy makes the cost of an assignment proportional to the size of the assigned value (with the size of the private heap as upper bound) in the worst case; in practice, assignment remains reasonably e cient, even in programs such as the Knuth-Bendix benchmark, that transmit large structures through mutable objects. Finally, the last case where a mutator can be delayed on a memory operation is when it accesses the free list to allocate objects directly in the shared heap: free list accesses must be mutually exclusive. To lower contention, each thread maintains its own small, private free list. The private free lists are replenished from the main free list when a request cannot be satis ed. Transfers from the main free list to a private free list are performed a large chunk at a time, to keep their frequency low. This strategy works well on three of our test programs, but does not avoid a certain amount of contention for the parallel compiler. From these results, we conclude that our design achieves good response time, and is adequate for interactive applications. However, it does not achieve true real-time performance: there is no guaranteed upper bound on the time taken by memory operations. A small number of these operations take much longer than the average time. This can be seen on gure 7, which plots the distribution of execution times for the three memory operations. For instance, a minor collection can take as much as 360 ms, in the worst-case where all objects in the minor heap are alive. Similarly, some copy-on-update operations may need to copy (almost) all objects from the minor heap. There is a trade-o between maximallatency and garbage collection overhead: the worst-case latency can be lowered by reducing the size of the private heaps, but this results in more time spent in minor collections, and an increased load on the major collector.

Extensions

The memory management system described above can be extended in several ways. The rst direction is to parallelize the major collection, in order to keep up with more active mutators. The sweeping phase can straightforwardly be parallelized, since the heap is already divided in medium-sized chunks (256 K), which can be swept by independent threads. The marking phase can also be performed concurrently by several threads, though achieving good balance is more delicate.

Another area of improvement is the \weight" of threads. Since each thread has its own stack and its own private heap, thread creation is a relatively expensive operation: starting a Concurrent Caml Light thread takes about 3 ms, which is commensurate with the time it takes to start a Mach thread (about 1 ms), but still too important for applications that spawn a large number of short-lived threads. For these applications, a promising direction is to adopt the two-level scheme outlined in 19], where the user-level threads are multiplexed on top of a small number of kernel threads. Each kernel thread has its own private heap, and timeshares between a number of user-level threads. Userlevel threads can freely share a private heap, provided that the memory operations on the private heap are mutually exclusive, which the user-level scheduler can easily guarantee.

Finally, the concurrent collector described above can be simpli ed into an incremental, generational collector for uniprocessors. The idea is to perform a small part of the major collection at each minor collection. Since there is only one private heap, copy-on-update is no longer mandatory, and we can maintain a remembered set instead. We have integrated this incremental collector in the release 0.5 of the Caml Light system.

Related work

The system described in this paper is related to two trends in research on garbage collection. The rst trend deals with concurrent variants of the classical marksweep algorithm, with as little synchronization as possible between the mutator and the collector [START_REF] Hickey | Performance analysis of on-the-y garbage collection[END_REF][START_REF] Cousineau | The categorical abstract machine[END_REF][START_REF] Baker | List processing in real time on a serial computer[END_REF]. The emphasis here is on proving the correctness of the proposed algorithms, rather than on practicality and efciency. To our knowledge, none of these designs has made its way into an actual run-time system. There are good reasons to believe that collectors based on these designs would not be able to keep up with typical ML programs. Hickey and Cohen 14] provide some theoretical evidence of this problem. This problem is avoided in our system by the use of generation scavenging, that greatly reduces the allocation rate as viewed by the concurrent mark-and-sweep collector.

A di erent approach to the parallelization of the mark-sweep algorithm is described by Boehm et al. 7]. Their algorithm requires no cooperation from the mutators; instead they rely on virtual memory protections to keep track of modi cations performed by the mutators. Their collector overlaps most of its work with the mutator activity but it has to stop the mutators to nish the marking phase. The resulting pauses are short (about 100 ms) but still one order of magnitude longer than in our system on average. Moreover, their technique must stop all mutators simultaneously, introducing a spurious global synchronization point between all threads. Avoiding this phenomenon was one of our main goals.

The second trend is the practical implementation of concurrent or incremental copying collectors. The rst such collectors were described by Steele 23] and Baker 4], and later extended to generations 18] and to multiple mutators 13]. This algorithm requires a test on each heap pointer dereferencing, which imposes considerable overhead on the mutator, unless special hardware is used. A variant proposed by Brooks 8] replaces this test by a systematic indirection. On stock hardware, this technique slightly reduces the overhead, at the expense of one extra word per heap object. North and Reppy 20] have extended this technique with generations. Appel, Ellis and Li 2] propose to use virtual-memory protections to implement Baker's algorithm without tests on stock hardware. Their technique relies on sophisticated virtual memory primitives, which most widespread operating systems do not provide in an e cient way 3]. Thus, concurrent purely copying garbage collection has not yet been implemented on stock hardware and standard operating systems without major overhead on the mutators. Our mixed design avoids this di culty by restricting the copying to unshared objects, which cannot be accessed concurrently.

Conclusions

We have described a memory management system for a multithreaded implementation of ML that achieves quasi real-time performance with low overhead on the mutators. This system relies crucially on the compiletime separation of mutable and immutable objects. In the case of ML-like languages, this separation is ensured by the type system, therefore demonstrating an unexpected spin-o of strong, static typing in the area of garbage collection. This technique can also be applied to dynamically-typed languages such as Scheme, as long as separate allocation primitives are provided for mutable cons cells and immutable cons cells, and similarly for other data types.

Figure 3 :

 3 Figure 3: Color transitions

Figure 4 :

 4 Figure 4: What happens if we do not shade the new value

Figure 5 :

 5 Figure 5: What happens if we do not shade the old value

Figure 6 :

 6 Figure 6: Average performance

Figure 7 :

 7 Figure 7: Latency distribution

To implement this, the objects in the private heaps have one extra header word, to store a forwarding pointer without destroying the object. This extra word is stripped when the object is copied to the major heap.

In theory, the color blue is not needed: it su ces to consider the free-list head as a memory root, and the free-list blocks as regular reachable blocks. However, the blue color avoids the extra cost of tracing and coloring the free-list blocks.

To quickly nd the next gray object, a cache of recently shaded objects is maintained, avoiding the cost of an actual scanning of the heap in most cases.

Acknowledgments

We would like to thank Ian Jacobs for his careful proofreading, and Greg Morriset for sending us the SIMPLE benchmark.