Keywords: System F, ML F, Unification, Types, Graphs, Binders, Inference Recasting Système F, ML F, Unification, Types, Graphes, Lieurs, Inférence

Le langage ML F a été conçu comme une alternative au Système F permettant l'inférence partielle de type à la ML. Il diffère du Système F par la nature de ses types et par sa relation d'instance sur les types. Malheureusement, la définition de l'instance de type est purement syntaxique et n'est pas soutenue par une sémantique sous-jacente. Jusqu'à présent elle n'a été justifiée qu'a posteriori par le résultat de correction.

Dans ce travail nous réexaminons ML F en suivant une approche plus progressive en s'appuyant sur le Système F. Nous soutenons que le Système F n'est pas bien adapté pour l'inférence de type à la ML parce qu'il ne réussit pas à factoriser des dérivations de typage étroitement reliées. Nous résolvons ce problème dans la présentation de ML F à la Curry en enrichissant les types avec une nouvelle forme de quantification qui permet de représenter une collection tout entière de types du système F. Cela conduit à une interprétation naturelle des types de ML F comme des ensembles de types du système F et à en déduire la relation d'instance par inclusion des interprétations. Nous donnons également une définition syntaxique équivalence de l'instance de type sous la forme d'un ensemble de règles d'inférences.

Nous en dérivons une présentation à la Church de ML F en raffinant encore les types de façon à distinguer l'information de type inférée de celle fournie par l'utilisateur. Le langage résultant est plus canonique que celui initialement proposé. Nous montrons un plongement de ML dans ML F ainsi qu'un codage du Système F dans ML F . De plus, comme ML F est plus expressif que le Système F, un codage de ML F est fourni vers une extension du Système F avec des liaisons locales.

Contents

Introduction 3

An intuitive introduction to ML F 10 2.1 A generic Curry-style second-order type system . .

Introduction

The design of programming languages is often an area of difficult compromises. In the end, programming languages must help programmers write correct, maintainable and reusable programs quickly. This implies, in particular, that programming languages must be expressive, so as to write algorithms concisely and directly, avoiding code duplication and acrobatic programming patterns, modular, so as to increase readability, to ease code reuse and to be robust to small code changes, and typed. Types are indeed a key towards program correctness, as they ensure, with very little overhead and without relying on the programmer's skill, that a certain class of errors will never occur at runtime; moreover most common and stupid programming mistakes may so be trapped as type errors.

Simple types, and in particular ground types, are still in use in many languages such as Pascal, C, Java, etc. to categorize values between basic values such as integers, strings, etc., named structured values, and functions. Most basic values and primitive functions have a unique ground type. However, higher-order functions, which receive among their arguments other functions typically used to transform other arguments, are usually polymorphic. That is, they work uniformly for a whole collection of ground types. Unfortunately, this property cannot be described using simple types. As a result, higher-order functions must often be artificially specialized to one or, worse, several instances, introducing duplication, worsening maintainability, and preventing code reuse.

A well-known solution is of course parametric polymorphism, which extends simple types with type variables that may be universally quantified. The simplest form of parametric polymorphism is known as ML-style polymorphism [START_REF] Milner | A theory of type polymorphism in programming[END_REF]: quantifiers are limited to the outermost position of types and the use of polymorphism is limited to definitions, as opposed to parameters of functions. For example, the application-the function that takes two arguments and apply the first one to the second one-may be given type ∀(α, β) (α → β) → (α → β). A whole collection of types obtained by instantiating universal variables by arbitrary types can thus be captured as a single polymorphic type. In this view, types can be thought of as the set of all their instances, which makes them about as easy to understand as simple types. This also eases type inference, as each well-typed program may be characterized by a principal type, i.e. a type whose instances are exactly all types of the program. ML-style polymorphism has been extremely successful for several decades and is still at the core of the most widely used implementations of statically typed functional languages, such as OCaml or Haskell. The advantages of parametric polymorphism over simple types are now widely recognized, as shown by its introduction in C # and the language Java, version 5.

However, polymorphic higher-order functions sooner or later need themselves to be passed as arguments to other functions.

Because of its limited form of polymorphism, ML is well suited for programming abstractions over known data-structures, such as the fold iterator over lists, but it does not allow to abstract iterators over arbitrary collections because it is not possible to write a function that visits a structure without knowing its constructors exactly. Another related limitation is that the Church encoding of data-structures does not usually work in ML.

A crux of Haskell is the use of monads, but the lack of first-class polymorphism prevents the abstraction over monads. This has motivated the introduction of arbitrary-rank polymorphism in Haskell (Jones and Shields, 2004b), but its limitation to predicative polymorphism is too restrictive and makes it inconvenient to use. While row variable polymorphism allows for a rather expressive object-oriented programming style in OCaml, the lack of polymorphic methods that sooner or later arise has motivated the introduction of a limited form of first-class polymorphism, based on Poly-ML (Garrigue and Rémy, 1999). Unfortunately, it remains contrived and ad hoc.

Many situations where first-class polymorphism is useful have been described in the literature. For instance, a series of examples in the context of Haskell are presented in [START_REF] Simon | Practical type inference for arbitrary-rank types[END_REF]. Many of these particular cases are in fact similar and often involve in a way or another taking as argument a function that is applied to heterogeneous data, hence that has to be polymorphic. One may still wonder how often such situations arise. We believe that they are in fact unavoidable, for reasons explained below.

Perhaps, the most convincing and agreed limitations of ML is its inability to represent heterogeneous collections-except via explicit tagging which then prevents their treatment in a uniform way. Indeed, the other way to represent an heterogeneous collection is to give its elements an existential type of the form ∃α.τ , where in fact each element taken separately has a type of the form τ [τ ′ /α] (the type τ in which α has been replaced by τ ′ ) for some type τ ′ . Existential types are also needed to represent closures, i.e. delayed computations that, for instance, are to be run on some remote computation server.

It is well-known that an expression a of existential type ∃α.τ may be encoded as the function λ(f ) f a taking as argument an arbitrary polymorphic function f of type ∀(β) (∀(α) τ → β) → β, so that it can be applied to a but ignoring the part of a that is to be hidden. We write ∀(α) τ for ∀-quantification of variable α in type τ . The scope of α extends to the right as far as possible. The arrow → is right associative and of lower priority than other type constructors such as the product ×. That is,

∀(α) τ × τ ′ → τ → τ ′ means ∀(α) ((τ × τ ′ ) → (τ → τ ′ )).
Quite interestingly, providing existential types as primitive does not alleviate but, on the contrary, reinforces the need for passing polymorphic functions as arguments. Indeed, an expression a 1 of existential type must be opened before it can be used inside an expression a 2 , which is usually written open a 1 as x, β in a 2 . The type variable β stands for the witness of the existential type of a 1 and its scope is the expression a 2 . When the body of a 2 is parametrized over some function f received as argument, the program becomes of the form λ(f ) open a 1 as x, β in a 2 where f is used in a 2 , typically with a type that involves β. In order for β not to escape from its scope, the function f must be polymorphic in some other variable that will be instantiated to some type containing β.

Such examples require quantifiers to appear within types-here on the left-hand side of arrow types, but more generally at any position within types. That is, polymorphic types should be treated as any other types, which is called first-class polymorphism. System F, the second-order polymorphic λ-calculus, is the reference for first-class polymorphism [START_REF] Girard | Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur[END_REF][START_REF] Reynolds | Second-order unification and type inference for Church-style polymorphism[END_REF].

In Curry's view, terms of System F are unannotated and types are left implicit, as in ML. However, as opposed to ML, type inference for System F is undecidable [START_REF] Wells | Typability and type checking in System F are equivalent and undecidable[END_REF]. Moreover, System F does not have principal types1 . That is, the types of an expression in a given typing context cannot be captured as the set of all instances of a particular (principal) type. Of course, the notion of principal types depends on a suitable definition of type instance.

Therefore, in practice, one rather uses Church's view, where source programs contain explicit type information, so as to make type checking straightforward and decidable. More precisely, function arguments come with explicit type annotations and polymorphism is both explicitly introduced by type abstractions and explicitly eliminated by type applications.

For example, the following function maps its argument-a list of pairs-to a list obtained by applying the first coordinate of each pair to the second coordinate.

We write ∀(αα ′ ) σ for ∀(α) ∀(α ′ ) σ. We write λ(x) a for the function that maps x to the expression a. We write Λα. a and a[τ ] for type abstraction and type application, respectively.

Assume we are given a function listmap of type ∀(αβ) (α → β) → list(α) → list(β), as well as the projections fst and snd from pairs of respective types ∀(αβ) α × β → α and ∀(αβ) α × β → β.

Λα . Λβ . λ(pairlist : list((α

→ β) × α)) listmap [( α → β) × α] [β] (λ(p : (α → β) × α) (fst [α → β] [α] p) (snd [α → β] [α] p))
pairlist As illustrated by this example, explicit type information may be quite intrusive sometimes obfuscating and often a pain to write and read, while most of this information is rather obvious from context. By contrast, the very same example, written in ML, looks as follows:

λ(pairlist ) listmap (λ(p) (fst p) (snd p)) pairlist Annotations in ML are unnecessary because the language enjoys full type inference. That is, polymorphism is implicitly introduced and eliminated. This is made possible in ML because type inference does not have to look for first-class polymorphic types, hence it never needs to guess polymorphism. On the opposite, type inference in System F should also consider solutions where the argument of a function, e.g. p in the example above, may have a polymorphic type, such as (∀(α) α × α → list(α)) × (∀(β) τ × τ ), where τ is a type that may mention β. Finding all such solutions is undecidable in the general case. Hence, in System F, one must also annotate programs that are typable in ML if only to say not to look for other types. While System F is attractive for its expressiveness, its poor treatment of the common simple case has limited its use as the core of a programming language, which indirectly benefited to the long life of ML dialects.

Searching for the grail. In the last two decades, considerable research has been carried out to reduce the gap between ML and System F. Unfortunately, all solutions that have been proposed so far are unsatisfactory, from both a theoretical and-worse-practical point of view. The problem has naturally been tackled from two opposite directions.

Starting with System F, one may allow some type annotations to be omitted and attempt to rebuild them, hopefully accepting more ML programs. One theoretically very attractive solution of this kind is to reduce type inference to second-order unification [START_REF] Frank | Partial polymorphic type inference and higher-order unification[END_REF]. This approach does not need type annotations at all, but still requires placeholders for type abstractions and type applications, which unfortunately, are not very convenient to write. Furthermore, type inference remains undecidable, as it then amounts to secondorder unification. Other less ambitious approaches rely on local type information to rebuild omitted type information [START_REF] Pierce | Local type inference[END_REF][START_REF] Odersky | Colored local type inference[END_REF], by contrast with unification which is based on global computational effects. However, places where the user must provide type annotations are not always so obvious [START_REF] Hosoya | How good is local type inference?[END_REF]. Worse, these approaches appear to be fragile with respect to small program transformations; moreover, all of them fail to type a significant subset of useful ML programs.

Conversely, starting with ML, polymorphic types can be embedded into first-class monomorphic types via explicit injection and projection functions. This technique, known as boxed polymorphism [START_REF] Didier | Programming objects with ML-ART: An extension to ML with abstract and record types[END_REF][START_REF] Odersky | Putting type annotations to work[END_REF] may be improved in several ways and has been implemented in both Haskell and ML. While it is useful as a default solution, and acceptable when polymorphic types are used occasionally, the solution does not scale up to intensive use of polymorphism.

In fact, all approaches have somehow assumed that the solution was to be found between ML and System F. Indeed, in Church's view, hence in theory, ML is a subset of System F. However, in practice, ML is implicitly typed while System F is explicitly typed. This makes the previous comparison misleading-if not meaningless. Maybe the solution lies outside of System F, as a more expressive type system that combines implicit let-polymorphism with explicit second-order types.

Our main contribution is a proposal for a new type system, called ML F , that supersedes both ML and System F, allows for simple, efficient, predictable, and complete type inference for partially annotated terms. The language ML F has been introduced in previous works (Le [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]), which we shall below refer to as Full ML F to avoid ambiguity. In this work, we focus on a simplified version, here called ML F for conciseness-or Shallow ML F when there is ambiguity. While Shallow ML F is less expressive than Full ML F , it is still more expressive than both ML and System F, it retains interesting theoretical properties and practical applications, and it has a significantly less technical and more intuitive presentation.

For another simplification, we first consider a Curry-style version of ML F , called2 iML F . This implicitly typed version requires an extension of System-F types with only flexible quantification, written ∀(α ≥ σ) σ ′ . Remarkably, we may interpret types of iML F as sets of System-F types. Roughly, ∀(α ≥ σ) σ ′ may be seen as the collection of all System-F types τ ′ [τ /α] where τ ′ and τ range in the interpretation of σ ′ and σ, respectively. This interpretation induces an instance relation on types. It can also be used to exhibit a translation of expressions into a small extension of System F with local bindings. This shows that the additional expressive power of ML F is theoretically small, although practically important as it increases modularity in an essential way. For the sake of comparison, one may also consider a weaker version, called3 Simple ML F , that has exactly the same expressiveness as System F. Although it retains most theoretical properties of ML F , it is no longer an extension of ML and, as a result, has little practical interest.

Unsurprisingly, full type inference for iML F is undecidable. We thus also devise a Church-style version of ML F , called4 eML F , with optional type annotations. For the purpose of type inference we enrich types with rigid quantification ∀(α ⇒ σ) σ ′ , which, in contrast with flexible bindings, indicates that the polymorphic type σ cannot be instantiated. Rigid quantification may at first be viewed as a notation for representing inner polymorphism σ ′ [σ/α] within type schemes. More importantly, it keeps track of sharing by distinguishing between ∀(α ⇒ σ, α ′ ⇒ σ) σ ′ and ∀(α ⇒ σ) σ ′ [α/α ′ ], which is essential for type inference, as explained next.

Indeed, the ML F type system maintains a clear separation between polymorphism that can be inferred and polymorphism that cannot (more precisely, that we choose not to infer).

Usual ML-style polymorphism belongs to the former category. It is represented by type schemes : the typing of the body of let x = a in a ′ is of the form x : σ ⊢ a ′ : σ ′ for some type σ ′ to be inferred. That is, x is known to have a polymorphic type σ while typing a ′ . For instance, if a is λ(y) y, which we write id, then x is known to have type ∀(α) α → α, which we write σ id .

On the contrary, the type of x in λ(x) a belongs to the latter, and is represented by an abstract type while typing a. The typing of the body is of the form (α ⇒ σ) x : α ⊢ a : σ ′ (1). That is, x is only known to have an abstract type α, which is bound to σ in the prefix (α ⇒ σ), but which cannot be instantiated to σ or to anything else5 . The binding (α ⇒ σ) can be discharged on the right of the typing judgement only when α does not appear in the typing environment, as prescribed by the usual generalisation rule. As an example, if a is x, then (1) becomes (α ⇒ σ) x : α ⊢ x : α. We may derive (α ⇒ σ) ⊢ λ(x) x : α → α and the binding (α ⇒ σ) may now be discharged into ⊢ λ(x) x : ∀(α ⇒ σ) α → α. As a consequence (λ(x) x) ω † is typable without any type annotation on x, where the identifier ω † stands for the function λ(y : σ id ) y y. However, λ(x) x is not typable with type ∀(α ⇒ σ, α ′ ⇒ σ) α → α ′ , as this would have required typing (α ⇒ σ, α ′ ⇒ σ) x : α ⊢ x : α ′ (2), which does not hold.

Conversely, the type of an annotated argument belongs to the former category. The typing of a in λ(x : σ) a involves a judgment of the form x : σ ⊢ a : σ ′ . The annotation is intuitively discharged as ⊢ λ(x : σ) a : σ → σ ′ . However, this is not quite correct because type schemes may not appear under arrow types: instead, we write ⊢ λ(x : σ) a : ∀(α ⇒ σ, α ′ ⇒ σ ′ ) α → α ′ . For example, we have x : σ ⊢ x : σ, and therefore, ⊢ λ(x : σ) x : ∀(α ⇒ σ) ∀(α ′ ⇒ σ) α → α ′ . Here, the type α ′ of the result, and the type α of the argument are decoupled, which is possible since the known type of x is σ and not a type variable abtracting σ.

The problem of type inference with partial type annotations is to find for a program, given with some type annotations, the set of all its types that respect the type annotations. In eML F , solvable type inference problems have principal solutions, which indeed depends on the program type annotations-as illustrated above by the two versions of the identity function that differ only on their type annotations.

The richer types and the let-polymorphism of eML F make it significantly superior to Church-style System F as a programming language: programs admit more general types and require fewer type annotations. More precisely, removing all type abstractions and type applications from a term of System F, leaving only type annotations on function parameters produces a term that is well-typed in eML F and with a more general type than its original type in System F-modulo a straightforward translation of types. Moreover, annotations on function parameters may often be omitted. Precisely, only those that are used polymorphically need to be annotated. In particular, ML programs need no type annotations.

Although type inference is not addressed in this paper, it can be reduced to a first-order unification algorithm for (a form of) second-order types, combined with let-polymorphism a la ML, as shown in previous works by Le Botlan andRémy (2003) and[START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]. While worst-case complexity is at least as hard as in ML, i.e. exponential-time complete, it seems to be quite reasonable in practice. In fact, type inference for ML F has recently been shown to be as efficient as for ML (Rémy and Yakobowski, 2008a;[START_REF] David | A logical algorithm for ML type inference[END_REF].

Notice that both iML F and eML F are typed languages, of equivalent expressiveness, and only differ by whether (some) types are explicitly written in terms. We use the name iML F and eML F when this point of view matters. For instance, only eML F makes sense as a programming language. Otherwise, ML F refers to either view, indifferently.

The full picture. Of course, something must have been lost while going from Full ML F to Shallow ML F . That is, it may be the case in Shallow ML F that a local binding let x = a 1 in a 2 is typable while its operationally equivalent form (λ(x) a 2 ) a 1 is not. Technically, Shallow ML F polymorphism is second-order, yet not first-class.

To see the practical consequences of this limitation, we shall proceed by comparison with ML. We use unannotated terms by default, so as to ease the comparison between the different languages. Consider the following expression in ML: let f = λ(x) x in (f 42, f "foo") The polymorphic type ∀(α) α → α, say σ id , is inferred for the identity function and bound to the identifier f, which may then be used at different type instances, namely int → int and string → string. One may consider replacing the let-binding by an abstraction followed by an immediate application:

(λ (f ) (f 42, f "foo")) (λ(x) x) This expression is not typable in ML, as it would require the function parameter f to be assigned a polymorphic type. In contrast, this expression is typable in iML F , which features second-order polymorphism. (In eML F , one need only add an explicit type-annotation, e.g. σ id , on the parameter f .) However, this is only a simplistic example. For instance, consider a small variant of the previous expression: let f = choose id in (f succ, choose f ω) The identifier succ stands for the successor function of type int → int. The identifier choose stands for a function that takes two arguments and returns either one, which could be defined as λ (x) λ (y) if true then x else y, of (principal) polymorphic type ∀(α) α → α → α. The identifier ω corresponds to the unannotated version of ω † , that is, λ(x) x x. The expression above is not typable in System F. A formal proof of this fact is beyond the scope of this paper-see (Pierce, 2002, Chapter 23) for hints on how to conduct such proofs. Interestingly, this expression is typable in eML F , taking the annotated version ω † instead of ω. Indeed, the expression choose id can be typed with ∀(α ≥ σ id ) α → α, which intuitively stands for all types σ → σ where σ is any instance of σ id . The parameter f can then be used with two peculiar instances, namely (int → int) → (int → int) and σ id → σ id , which are incompatible in System F.

Unfortunately, replacing the local-binding by an abstraction followed by an immediate application leads to the program (λ (f ) (f succ, choose f ω)) (choose id) which is not typable in iML F . The problem is that the required flexible type ∀(α ≥ σ id ) α → α that could previously be assigned to the let-bound variable f, cannot be assigned to a λ-bound variable, as only System Ftypes are allowed for λ-bound variables in Shallow ML F . This restriction is relaxed in Full ML F , which allows flexible quantification at arbitrary positions in types. Hence, the previous example is typable in Full ML F . (In Full eML F , it suffices to add the type annotation ∀(α ≥ σ id ) α → α to the parameter f .)

The main outcomes of staying within Shallow ML F are a more comprehensive presentation of the language and the connections drawn with existing systems, using the semantics of types as a tool not only to convey strong intuitions but also to recover the syntactic instance relation as set containment on semantic types.

The meta-theoretical study of Shallow ML F presented hereafter builds on this semantic support and is thus significantly simpler than-and mostly independent from-the previous study of the full version [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF].

The remaining gap between Shallow ML F and Full ML F is a small step for the user but another big step for a theoretician: the typing rules are exactly the same in both languages except that we unlock the restriction that is imposed on the occurrences of flexible quantification in the shallow version. Hopefully, the intuitions built

Variant

let-∀ λ-∀ let-≥ λ-≥ Simple Types - - - - ML √ - - - System F √ √ - - Simple ML F √ √ - - Shallow ML F √ √ √ - Full ML F √ √ √ √
for the shallow version should carry over to the full version. Unfortunately, our semantics of types cannot be easily extended to cope with the full version.

The different versions of ML F are summarized and put in close correspondence with existing languages in Table 1 and Figure 2.

All languages are presented in order of increasing expressiveness in the table. The first group, on the top of the table and also appearing on the left-hand side of the figure, is composed of three well-known languages where polymorphism is based on the standard ∀-quantification. The second group, on bottom of the table and also appearing on the right-hand side on the figure, is composed of three variants of ML F where polymorphism is based on the peculiar ≥-bounded quantification.

The correspondence between these two groups is explicitly represented on the figure by the horizontal dotted arrows and on the table by the equality of the two submatrices left in white background on the diagonal (and the two constant submatrices in gray background). In this correspondence, the standard ∀-quantification in the first-group becomes the ≥-bounded quantification in the second group. In each group, expressiveness is successively gained by added quantification to the type of let-bound parameters and, then, to that of λ-bound parameters.

As mentioned earlier, Simple ML F is exactly as expressive as System F. This is represented by the identity of the two lines at the junction of the two groups in the table and the double-line arrow relating them in the Figure .  The reason for this coincidence is that Simple ML F is obtained by adding flexible quantification to System F, yet without any construction to exploit it. In this respect, Simple ML F is to Shallow ML F what simply-typed λ-calculus is to ML: simply-typed λ-calculus has universal type variables but no type-instantiation mechanism! Restated in the other direction, Shallow ML F is to Simple ML F what ML is to simply typed λ-calculus, as both enable the underlying polymorphism on local-bindings in the very same manner. Pursuing the analogy, Full ML F is to Shallow ML F what System F is to ML-it enables flexible polymorphism on function parameters and, more generally, to appear at arbitrary position in types: quantification is first-class-but of different power-in both Full ML F and System F. By contrast, it can only be used at local bindings in both Shallow ML F and ML.

The Systems F ∧ (right-hand side of Figure 2) is an extension of System F with intersection types [START_REF] Pierce | Programming with Intersection Types and Bounded Polymorphism[END_REF], while F let below is the restriction of F ∧ to rank-1 intersection types (see §3.6). Equivalently, F let is the closure of Simple ML F by let-expansion. The arrows between F let and F ∧ and Simple ML F and F let are materializing these inclusions. The inclusion of Shallow ML F into F let , which is proved below ( §3.6), implies the correctness of Shallow ML F . The inclusion between Full ML F and F ∧ also holds but is not shown in this paper.

For completeness, two small remarks can also be made. First, Shallow ML F and F let are two extensions of Simple ML F with local-bindings that differ significantly in the way these are typed: In ML F , local-bindings can be typed with Simple-ML F types and generalized afterward, while in F let , they must either use intersection types or be typed after performing let-reduction. Second, the difference between let-∀ extension and let-∧ vanishes when replacing Simple ML F with Simple Types; that is, ML is both the let-∀ extension and let-∧ extension of Simple Types.

We believe that a programming language should be based on the full rather than the shallow version of ML F . However, other extensions such as higher-order types may be easier to explore in the simple version. Hence, the shallow version is not only a pedagogical restriction, but also an interesting and solid point in the design space, from which further investigations may be started.

INRIA

F Full ML F F ∧ ML Shallow ML F F let Simple Types Simple ML F Standard ∀(α) Flexible ∀(α ≥ σ) + let-∀ + λ-∀ + let-∀ ≥ + λ-∀ ≥ + ∀ ≥ +let-∧ +λ-∧
Type inference is not addressed here, as it is a technically orthogonal issue and is not significantly easier for Shallow ML F than for Full ML F . The reader is referred to [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF] or independent study in subsequent work [START_REF] Didier | A graphical presentation of MLF types with a linear-time unification algorithm[END_REF]. As ML F was designed with first-order type inference and let-polymorphism in mind, polymorphism need never be guessed: it is only picked at local bindings or user-provided type annotations, and it is propagated to use sites by first-order unification. The difficulty, and in fact the whole design of ML F , lies in the specification of its type system, and in particular, how every use of polymorphism that would imply guessing has been ruled out. So, although we do not develop type inference here, all the key ingredients can already be found in the Church-style version eML F .

Outline of the paper. While previous studies focused on Full eML F , this work is limited to the study of Shallow ML F (Simple ML F is only introduced as a tool).

The paper is organized as follows. A gentle introduction to ML F exposing successively its Curry's and Church's views, can be found in §2. The Curry's view is explored in details, including discussions of type soundness and of expressiveness in §3. The Church's view is studied formally in §4: although the Church's view has been designed especially for type inference, we focus on its fundamental properties here and leave out type inference for reasons explained above. We also address expressiveness of the Church's view by showing that it subsumes both ML and System F. Related works are discussed in §5 before concluding remarks. For clarity of exposition, all proofs have been moved to appendices.

Figure 3 summarizes the seven encodings presented in §3 and §4. Encoding are represented by edges and labeled with the corresponding theorem. (The interest of the direct encoding of System F to eML F is to introduce fewer annotations than the composition of encodings via iML F , and in particular, fewer type annotations than present in the original term.) The encoding from eML F to ML is partial, defined on the subset of eML F programs that do not contain any annotations.

Notations. We write A # B to mean that the two sets A and B are disjoint. We write ē for a sequence of elements e 1 , . . . e n . We use standard notions of variables, terms, binders, and free variables. The simultaneous capture-avoiding substitution of a sequence of variables ū by a sequence of objects ē′ in an object e is written e[ē ′ /ū].

We use numerical labels in bold face such as (3) as a binding annotation in text or formulas and normal font as (3) to refer to the corresponding binding occurrence. The scope of such labels is the current proof, paragraph, or inner section, and is left implicit. 2 An intuitive introduction to ML F

This section is primarily an informal introduction to ML F . The only prerequisite is a good knowledge of ML and some knowledge of System F. We first remind Curry-style System F. However, we use a generic presentation G so as to emphasize the strong relations between all type systems described here. In particular, we present both Curry-style and Church-style versions of ML F as instances of G. We provide intuitions on the flexible and rigid quantification that are at the heart of ML F , by means of examples. We also discuss-still informally-some of the advantages of ML F compared to System F, besides type inference. This section may also be read back after some technical knowledge of ML F has been acquired to deepen one's understanding.

A generic Curry-style second-order type system

Expressions are the pure λ-terms with optional local definitions. Their BNF grammar is:

a ::= x | λ(x) a | a 1 a 2 Terms | let x = a 1 in a 2
Local bindings (optional)

That is, terms are variables x, functions λ(x) a where the parameter x is bound in a, applications a 1 a 2 , and optionally, local definitions let x = a in a ′ where the variable x is bound (to a) in a ′ . Terms are always taken up to α-equivalence, that is, up to (capture avoiding) renaming of bound variables. Local definitions let x = a in a ′ can always be seen as a way of marking immediate applications (λ(x) a ′ ) a. The intention is to type them in a special way, much as in ML, which is often easier and more general than typing the function and the application independently. In some cases, we may however exclude local definitions in order to either simplify the language, when local definitions do not actually increase expressiveness, or intentionally restrict the language. In either case, we may still use local bindings in examples but only see them as syntactic sugar for immediate applications.

Types

Throughout this paper, we use several related but different notions of second-order types. For simplicity, we use the same countable set of type variables ϑ for all notions of types and letters α, β, or γ to range over type variables.

The generic presentation, summarized in the following BNF grammar, abstracts over the exact sets of first-class types T and type schemes S, which are only partially specified.

τ ∈ T ::= α | τ → τ | . . . Types | ∀(q) τ Polymorphic types (optionally) σ ∈ S ::= τ | ∀(q) σ | . . .

Type schemes

q ∈ Q ::= α :: k Bindings Types should at least contain type variables α and arrow types τ → τ , but may also contain other forms represented by the ellipsis. Of course, types could also contain other type constructors such as products, sums, etc., without any technical complication. For conciseness, we do not include these in the formal presentation. Depending on the particular instance, types may also contain polymorphic types ∀(q) τ where q is a binding of the form (α :: κ). For the sake of generality, quantified type variables are constrained by kinds k ∈ K where INRIA the set of kinds K is left unspecified for the moment. We write dom(q) to refer to α. Type schemes σ extend types with outermost quantification, as in ML. Still, as in ML, types are first-class while type schemes will appear only in typing environments and typing judgments.

In simple cases, such as ML or System F, K is a singleton {⋆}. We may then abbreviate α :: ⋆ as α. The level of generality allows both for multi-kinded type expressions, e.g. taking for K a set of atomic kinds and for more complex forms of quantification, such as subtyping. Note, that K may contain type schemes as subexpressions (see, for instance, types of F <: described below). We write ftv(k) for the free type variables of types expressions that appear in k. In ∀(α :: k) σ, the ∀ quantifier binds α in σ but not in k. Free type variables are defined as usual:

ftv(α) = {α} ftv(τ → τ ′ ) = ftv(τ ) ∪ ftv(τ ′ ) ftv(∀(α :: k) τ ) = ftv(k) ∪ (ftv(τ ) \ {α})
Indeed, this definition must be completed to cover the possible extra forms in the definition of T . The extra cases are usually obvious. We always consider types up to α-conversion. The scope of ∀-quantification extends to the right as far as possible and → is right associative. That is,

∀(q) τ → τ → τ means ∀(q) (τ → (τ → τ )).
We may write ∀(qq ′ ) σ for ∀(q) ∀(q ′ ) σ.

For example, ML types and type schemes are defined as follows:

τ ∈ T ML ::= α | τ → τ ML types σ ∈ S ML ::= τ | ∀(q) σ ML type schemes q ∈ Q ML ::= α :: ⋆ ML bindings
This is indeed the simplest notion of generic types, as all options in the definition have been turned off. Types of System F, which we call F-types, may also be described by an instance of the generic grammar:

t ∈ T F ::= α | t → t | ∀(q) t F types σ ∈ S F ::= t F type schemes q ∈ Q F ::= α :: ⋆ F bindings
Quantifiers may appear in types directly and thus at arbitrary positions in F-types-as expected. In this case, types are closed by outermost quantification and coincide with type schemes. We use letter t instead of letter τ to range over F-types. This will be useful below in iML F to distinguish F-types from other forms of τ -types. Types of F <: are yet another example, that uses kinds in a more interesting way:

τ ∈ T F<: ::= α | τ → τ | ∀(q) τ | ⊤ F <: types σ ∈ S F<: ::= τ F <: type schemes q ∈ Q F<: ::= α <: τ F <: bindings
Types and type schemes still coincide, but contain an extra element ⊤ and kinds are now types. Bindings are written α <: τ rather than α :: τ .

Prefixes

As type variables come with bounds, most operations on types will be defined under a type environment, called a prefix, that assigns bounds to their free type variables. A prefix Q is a sequence of bindings q 1 ..q n . Its domain, written dom(Q) is the set {α 1 , .., α n }. We write ∅ for the empty prefix. A prefix Q binds all type variables of dom(Q) (defined as the union of the pointwise domains). However, they may themselves have free type variables written ftv(Q) that are defined recursively as ftv(∅) = ∅ and ftv(Q, q) = ftv(Q) ∪ (ftv(q) \ dom(Q)). Hence, for a closed prefix q 1 ..q n , dom(q i ) may only intersect ftv(q j ) for j > i. A prefix q 1 ..q n is often used to build types of the form ∀(q 1 ) ..∀(q n ) τ , which we simply write ∀(q 1 ..q n ) τ . Prefixes may also be used as type environments in judgments under prefix, e.g. as type instance defined next. We assume that the following well-formedness condition holds: for each prefix Q of the form q i∈1..n i and for each i and j in 1..n,

• i = j implies dom(q i ) = dom(q j ), and

• i ≥ j implies dom(q i ) /
∈ ftv(q j ).

Type instance

The type-instance relation is meant to capture the idea that some types are better than others, in the sense that some types can be automatically deduced from those of which they are instances. This may be specified directly using a specific typing rule. For example, an expression of System F that has a polymorphic type ∀(α) σ may be applied to any type τ resulting in an expression of type σ[τ /α]. That instantiation may also be left implicit, i.e. without markers such as type abstraction and type application in expressions, as in Curry-style type systems.

The instance relation for Curry-style System F, written ≤ F , is the binary relation composed of exactly all pairs of the form ∀(ᾱ) σ ≤ F ∀( β) σ[τ / ᾱ]) such that none of the variables β is free in ∀(ᾱ) σ. The quantification ∀( β) is used to generalize some of the type variables that might have been introduced in τ .

The definition of type instance relation ≤ ML for ML is exactly the same except that it applies to weaker sets of types and type schemes. Interestingly, the relation ≤ ML is also the restriction of ≤ F to ML type schemes.

We may abstract over the precise definition of the instance relation . For the sake of generality, we assume that the instance relation is taken under some prefix Q. That is, is a ternary relation (Q) σ σ ′ between a prefix Q and two type schemes σ and σ ′ . We say that is a relation under prefix or also that is a prefixed relation. We use letter R to range over such relations. We may view (ternary) prefixed relations as binary relations by treating the relation as a family of relations R Q indexed by prefixes Q ranging in the set of all prefixes. That is R is reflexive (respectively symmetric, transitive, etc.) if relations R Q are reflexive (respectively symmetric, transitive, etc.) for all prefixes Q. The inverse of a prefixed relation R is the relation R -1 defined by taking the inverse of (R Q ) for (R -1 ) Q . (We often write ≻ for (≺) -1 when R is a symbol ≺.)

The System-F type-instance relation ≤ F happens to be a particular case where the relation is actually independent of the prefix (hence, treated as a binary relation on types).

Another type instance relation that generalizes ≤ F in an interesting way is type-containment ≤ η , introduced by Mitchell in the late 80's [START_REF] John | Polymorphic type inference and containment[END_REF]. As for ≤ F , type containment is independent of prefixes and can thus also be treated as a binary relation. It is congruent but propagates contravariantly on the left-hand side of arrow types (and covariantly everywhere else) and distributes ∀-quantifiers over arrows (see [START_REF] John | Polymorphic type inference and containment[END_REF]). Type containment allows to capture deep instantiations, e.g. σ id → σ id ≤ η σ id → (σ id → σ id ), as well as extrusion of quantifiers, e.g.

∀(α ′ ) α ′ → (∀(α) α → α) ≤ η ∀(α ′ , α) α ′ → α → α.
A truly ternary type-instance relation is the subtyping relation <: used in F <: . The prefix is used to assign upper bounds to free type variables of the types being compared. As for type containment, this relation propagates contra-variantly on the left-hand side of arrows.

Both ≤ η and <: treat the arrow type asymmetrically, covariantly on the right-hand side and contra-variantly on the left-hand side. When generalizing the language of types to arbitrary types constructors, they would require type constructors to be declared with a signature defining their variance in each of their argument. By contrast, the type-instance relations of ML or System F are symmetric and need not know about variance of type-constructors.

Type equivalence

We assume that any suitable instance relation is a preorder. Then, an instance relation induces an equivalence under prefix, defined as the kernel of , i.e.

∩ . In the only case of F-types where the equivalence does not depend on prefixes, we actually consider types up to equivalence, i.e. up to commutation of adjacent binders and removal of redundant binders (in addition to α-conversion). That is, ∀(αα ′ ) α → α ′ , ∀(αα ′ ) α ′ → α, and ∀(αα ′ α ′′ ) α ′ → α are thus considered as equal in System F.

The generic Curry-style second-order type system

The generic Curry-style second-order type system, written G(T , S, Q, ), is parametrized by a set of types T , type schemes S, bindings Q, and an instance relation over type schemes.

Typing contexts are partial mappings with finite domains from program variables to type schemes. The free type-variables of a typing context are the union of the free type variables of its codomain. We write ∅ the empty mapping and Γ, x : t the mapping that sends x to t and behaves as Γ everywhere else.

Typing judgments are of the form (Q) Γ ⊢ a : σ where Γ is a typing context and Q a closed prefix that binds all type variables that appear free in σ or Γ. Hence, we must have ftv(σ) ∪ ftv(Γ) ⊆ dom(Q) (and ftv(Q) empty).

Typing rules are given in Figure 4. Rules for variables, abstractions, and applications are standard, modulo

x : σ ∈ Γ (Q) Γ ⊢ x : σ Fun (Q) Γ, x : τ ⊢ a : τ ′ (Q) Γ ⊢ λ(x) a : τ → τ ′ App (Q) Γ ⊢ a 1 : τ 2 → τ 1 (Q) Γ ⊢ a 2 : τ 2 (Q) Γ ⊢ a 1 a 2 : τ 1 Inst (Q) Γ ⊢ a : σ (Q) σ σ ′ (Q) Γ ⊢ a : σ ′ Gen (Q, q) Γ ⊢ a : σ dom(q) / ∈ ftv(Γ) (Q) Γ ⊢ a : ∀(q) σ Let (Q) Γ ⊢ a : σ (Q) Γ, x : σ ⊢ a ′ : σ ′ (Q) Γ ⊢ let x = a in a ′ : σ ′
the explicit mention of the prefix. As terms are unannotated, instantiation and generalization are left implicit, as in ML. Hence, rules Inst and Gen are not syntax-directed: in each case, the expression a appears identically in the premise and the conclusion. Rule Gen is standard and introduces polymorphism by discharging type abstraction from the judgment hypothesis into the type of the expression. Rule Inst is a type-containment rule that generalizes the more traditional forall-elimination step. This approach is preferable in a Curry-style type system as it moves instantiation from the typing derivation into a type-instance sub-derivation.

Rule Let is used for typechecking local definitions in a special way. This rule is indeed inspired from ML and reproduces the very same mechanism for typing local-derivations within System G. In particular, the bound expression is assigned a type scheme rather than a type. This improves over the default rule that would consist in typechecking let x = a 1 in a 2 as the immediate application (λ(x) a 2 ) a 1 . In cases where types and type schemes coincide, e.g. as in System F, we could simply view local definition as syntactic sugar for immediate applications. In other cases, Let is actually the key rule that truly empowers System G.

If G 1 is an instance of System G, we write G 1 :: J to mean without ambiguity that judgment J refers to the system G 1 . However, we usually leave the underlying type system implicit from context.

Renamings.

A renaming is a finite bijective mapping from type variables to type variables. As usual, dom(φ) is {α | φ(α) = α}. Note that if φ is a renaming, then dom(φ) and codom(φ) are equal and φ is a permutation of its domain. We extend renamings to bindings, taking (φ(α) ≥ φ(σ)) for φ(α ≥ σ) and to prefixes, taking (φ(q i )) i∈I for φ(q i i∈I ).

Notice that if dom(φ) is disjoint from dom(Q), then dom(φ(Q)) is equal to dom(Q) but φ(Q) is not, in general, equal to Q.
Hypotheses. In order for the type system to have interesting properties, the instance relation is assumed to satisfy some conditions.

Let extension over well-formed prefixes be the smallest order ⊇ that contains all pairs QqQ ′ ⊇ QQ ′ for any prefixes Q and Q ′ . We say that a prefix Q 2 extends a prefix

Q 1 whenever Q 2 ⊇ Q 1 holds. Intuitively, Q 2 just contains more bindings than Q 1 .
In the rest of the paper, we only consider instance relations that satisfy the following two axioms:

Renaming (Q) σ 1 σ 2 φ renaming (φ(Q)) φ(σ 1 ) φ(σ 2 ) Extra-Bindings Q ⊇ Q ′ (Q ′ ) σ 1 σ 2 (Q) σ 1 σ 2
Then, we can prove that typing judgments can be renamed and prefixes can be extended:

Lemma 2.1.1 i) Renaming of typing derivations: If (Q) Γ ⊢ a : σ holds and φ is a renaming, then (φ(Q)) φ(Γ) ⊢ a : φ(σ) holds. ii) Prefix extension: If (Q) Γ ⊢ a : σ holds and Q ′ ⊇ Q, then (Q ′ ) Γ ⊢ a : σ holds.
Both proofs are by induction on the derivation and indeed rely on both axioms.

Particular instances of System G.

Curry-style System F and ML are two by-design immediate instances of System G, namely G(T F , T F , Q F , ≤ F ) and G(T ML , S ML , Q ML , ≤ ML ). Notice that we slightly depart from the tradition to view ML as a subcase of System F and instead view both as special cases of System G.

An interesting extension of System F, introduced by Mitchell and called F η is the closure of System F by η-contraction [START_REF] John | Polymorphic type inference and containment[END_REF]. It may be concisely described as G(T F , T F , Q F , ≤ η ). As noticed by Mitchell, F η allows more terms to have principal types. For instance, σ id , which is an abbreviation for ∀(α) α → α, is a principal type for the identity function. Other correct types σ id → σ id or σ id → σ id → σ id are ≤ η -instance of σ id . In fact, this is also the case for any possible type of the identity. Hence, σ id captures all types of the identity up to ≤ η -instantiation. For that reason Mitchell has suggested that F η could be a better candidate than System F for type inference. Still, many expressions do not have principal types in F η . Somehow, F η is simultaneously too expressive (we do not really need contra-variance of type instance) and too weak for our needs (it lacks simultaneous instantiation constraints).

The language F <: proposed by Cardelli (Cardelli, 1993) can also be defined as the generic type system G(T F<: , S F<: , Q F<: , <:). Note however, that this is a Curry-style presentation while F <: is usually presented in Church style.

2.2 i ML F : Curry-style ML F .

Returning to our goal, we seek for a language eML F with partial type annotations that is at least as expressive as System F (each term of Curry-style System F is the type erasure of some term of eML F ), supersedes ML (all terms of ML are in eML F , without any annotation), and for which we can perform type inference using a form of first-order unification. Based and improving on previous experiences, we wish to manipulate second-order types transparently, so as to bypass inelegant and verbose boxing and unboxing operations and avoid annotations for all ML programs. Indeed, we seek for the fusion of ML-style implicit polymorphism with explicit F-style polymorphism, rather than just their juxtaposition, so that the best of each approach also strengthens the other one.

The inadequacy of F-types

Our goal implies that type instantiation must be left implicit, as in ML. Implicit instantiation is easy and rather natural in ML. The main reason is that polymorphism is not first-class. That is, only type schemes can be polymorphic. Types which may appear on the left of arrows cannot be polymorphic. Therefore, polymorphic values must always be instantiated before being passed as arguments to functions. This is no more true in System F-or any other language with first-class polymorphism, where a polymorphic value may also be passed as argument. Moreover, implicit polymorphism, as in Curry's style, brings an additional difficulty: the application of a polymorphic function to a polymorphic value may become ambiguous, as a result of permitting any polymorphic expression e of type τ to be considered as an expression of any type τ ′ that is an instance of τ .

For example, consider a value v of type τ and a function choose of type ∀(α) α → α → α (choose could either be a polymorphic comparison returning the greatest of two arguments or just a function randomly returning one of two arguments). What should be the type of choose v in System F? Should v be kept as polymorphic as τ or instantiated to some type τ ′ -but which one? Indeed, any type τ ′ → τ ′ is a correct one for choose v as long as τ ′ is an instance of τ . In other words, the correct types for choose v form a set {τ ′ → τ ′ | τ ≤ τ ′ }6 . Unfortunately, this set does not have a greatest lower bound that could be used as a principal type to represent all others.

This very simple example raises a crucial issue whose solution is really the key to understanding ML F from both the intuitive and formal perspectives.

One may be tempted to use infinite intersection types {τ ′ → τ ′ | τ ≤ τ ′ }, as suggested by Leivant in another context [START_REF] Leivant | Discrete polymorphism[END_REF]. However, this is pernicious from a logical point of view. Moreover, this would ignore the underlying structure of such sets, which are always instantiation upward closed.

Flexible quantification-the Key

Since intersection types are too powerful for our purposes, we introduce a new form of type scheme ∀(α ≥ σ) α → α to describe the set of all types τ → τ such that τ is an instance of σ. We may indeed interpret such type schemes as sets of System-F types ( §3.1). The instance relation ≤ between type schemes is then defined as set inclusion on their interpretations. This makes ∀(α ≥ σ ′ ) α → α an instance of ∀(α ≥ σ) α → α whenever σ ′ is an instance of σ and thus really makes ∀(α ≥ σ) α → α a principal type for the expression choose v where v has principal type scheme σ. Type schemes contain types, but all type schemes are not types. Types may still be polymorphic. For instance, σ id shall remain a type in iML F .

The binding (α ≥ σ) is called a flexible binding, as the bound σ may be soundly replaced by a type scheme σ ′ or a type τ that are instances of σ, producing an instance of the whole type. The occurrence of σ in (α ≥ σ) is also called a flexible occurrence.

By contrast, we call rigid occurrences of a type below an arrow, as those of σ id in σ id → σ id . Rigid occurrences may not be instantiated, as this could be unsound. For example, the function λ(x) x x has type σ id → σ id , where σ id is ∀(α) α → α, but does not have type τ ′ → τ nor even type τ ′ → τ ′ for arbitrary instances τ ′ of σ id . In particular, it does not have type ∀(α) (α → α) → (α → α). Although it would always be safe to instantiate types on the right-hand side of arrow types (or more generally on positive occurrences in types), we do not do so. We may always use a type scheme ∀(α ≥ τ ) τ ′ → α instead of τ ′ → τ to explicitly allow instances of τ to be taken for α.

For the sake of uniformity, we introduce a special trivial bound ⊥ (read bottom) to mean any type. We may then see ∀(α) α → α as syntactic sugar for ∀(α ≥ ⊥) α → α. Intuitively, ⊥ could itself be seen as representing the set of all types and, indeed, ⊥ is equivalent to ∀(α ≥ ⊥) α in our setting. In this view, ∀(α ≥ σ id ) α → α is an instance of ∀(α) α → α: since the bound σ id of the former is an instance of the bound ⊥ of the latter, the interpretation of the former contains the interpretation of the latter.

One may wonder what is the meaning of a type such as (∀(α ≥ τ ) α → α) → τ ′ when a flexible type appears under an arrow type. We just forbid such types. This is achieved by restricting the use of flexible quantification to type schemes and only allow quantification with trivial bounds in types. More precisely, types and type schemes for iML F (Curry-style ML F ) are defined as follows:

τ ∈ T i ::= α | τ → τ | ∀(α ≥ ⊥) τ iML F types σ ∈ S i ::= τ | ∀(q) σ | ⊥ iML F types schemes q ∈ Q i ::= α ≥ σ iML F bindings
Type schemes that are not types are called proper type schemes; they may not appear under arrows. A consequence of this stratification is that proper type schemes cannot be assigned to parameters of function. Therefore, local definitions let x = a 1 in a 2 play a key role, exactly as in ML. Indeed, one may first assign a type scheme σ to a 1 and use σ as the type for the parameter x while typechecking a 2 . By contrast, this assignment of type σ to variable x would be forbidden in the immediate application (λ(x) a 2 ) a 1 whenever σ is a proper type scheme, as x would be λ-bound and its type would have to appear under the arrow type of the function (see Rule Fun).

We thus consider the instance G(T i , S i , Q i , ≤) of Generic Curry-style System F with flexible quantification and local definitions. This intermediate language is in Curry style and all type information is still left implicit. For this reason, we also call it iML F (read implicit ML F ). Remarkably, the power of iML F only lies in its type, type scheme, and type-instance definitions and not in its typing rules, as it is just an instance of System G.

eML

F : Church-style ML F .
The language iML F is our stepping stone to eML F . By comparison with System F, more expressions have principal types and many expressions have more general types. However, iML F does not allow for type inference yet, even though it was designed with type inference in mind, as all type information is still left implicit. We now devise eML F -a Church-style version of iML F that enables type inference7 .

First-order type inference with second-order types Our goal is to perform type inference based on first-order unification but in a language with second-order types. In addition, we wish to reach all ML programs without type annotations and all System F programs via suitable type annotations.

This has immediate consequences in terms of examples that we should or should not type. For example, we should infer a type for the identity function id, or the expression let x = id in x x, as both are already typable in ML. Conversely, we should not type the self-application ω, defined as λ(x) x x (1), unless we explicitly annotate the parameter as in the expression λ(x : σ id ) x x (which we write ω † ).

Our goal is to design the system so that the second-order polymorphism is never guessed. But what does guessing exactly mean? How can we combine ML style implicit polymorphism with second-order explicit polymorphism? The difficulty may be seen by comparing the expressions a 1 defined as (λ(z) z) ω † and a 2 defined as (λ(x) x x) id. Should we reject both, as their function parameters carry values of polymorphic types-σ id → σ id for z in a 1 and σ id for x in a 2 ? Indeed, a 1 may be typed as (λ(z : σ id → σ id ) z) ω † . Here, it seems that σ id → σ id must be guessed as the type of the parameter z. However, one may also type λ(z) z in a 1 as α → α, generalize the resulting type to ∀(α) α → α, and finally instantiate it to (σ id → σ id ) → (σ id → σ id ), which may be more concisely summarized by its fully annotated form (Λα. λ(z : α) z) [σ id → σ id ] ω † in Churchstyle System F. In this expression, σ id → σ id need not be guessed as the type of the parameter z, but as the type for specializing the universal variable α to obtain the polymorphic type (σ id → σ id ) → (σ id → σ id ) of λ(z) z. Fortunately, we may-and must, as argued in §2.2-devise ML F to fully infer type abstractions and type applications (and never guess polymorphic types for function parameters). Thus we accept a 1 (2). Conversely, we reject a 2 for the very same reason we rejected ω (1). Indeed, any closed subterm of a well-typed term must also be well-typed. Thus a 2 , which contains the ill-typed closed subterm ω will also be ill-typed.

Of course, we distinguish a function parameter whose type is inferred from one whose type is given. We do so much as in ML, by distinguishing between types τ (also called monotypes), which do not contain any quantifier and can be inferred, and proper type schemes σ, also called polytypes for emphasis. The parameters z and x of a 1 and a 2 may only be assigned monotypes. This justifies the rejection of a 2 , as λ(x) x x may not be typed when x is a monotype. Conversely, a 1 may be typed by assigning z a monotype, as explained above (2). By contrast with a 2 , the parameter x of λ(x : σ id ) x x may be assigned the polytype σ id , since it is explicitly annotated.

Unfortunately, this distinction is not sufficiently permissive. Consider the expression a 3 defined as λ(z) (z ω † ), which somehow lies between a 1 and a 2 . The parameter z of a 3 must have a polymorphic type while typechecking the body of the function, exactly as in the expression a 2 . However, this polymorphism is not used in the body of a 3 but only carried through. Wishfully, it should thus also be accepted. As another hint, remark that a 3 is the β-reduction of (λ(y) λ(z) z y) ω † , which we refer to as a 4 . Arguing as for a 1 , it is clear that a 4 must be typable. As the β-expanded form is typable, we may expect the β-reduced form to also be-subject reduction will hold when the redexes are let-bindings or applications of unannotated λ-abstractions. As a crosschecking final example, should the expression a 5 defined as λ(z) ω † z be accepted? We may reason by analogy with the previous example and either check that z is not used polymorphically in the body of the function or check that its β-expansion (λ(x) λ(y) x y) ω † is typable.

It is actually a remarkable and essential property of ML F that whenever a 1 a 2 is typable, then apply a 1 a 2 also is, with the same type, where indeed apply stands for the expression λ(x) λ(y) x y-with no type annotation on its parameters. As a remarkable and important corollary, if a function a is typable with some type σ, then so is its η-expanded form λ(z) a z. In practice, such properties ensure that well-typed programs are stable under some minor but useful program transformations. More type-preserving program transformations are given in §4.5.

Abstracting second-order polymorphism into first-order types

To solve this last series of examples, our solution is very much inspired by boxed polymorphism, which allows second-order polymorphism to hang under monotypes (Garrigue and Rémy, 1999). We retain the very same idea of boxing polymorphism, but make boxes virtual, by abstracting (instead of boxing) second-order polymorphism as a first-order type variable. For instance, abstracting σ id as α allows the polymorphic type σ id → σ id to be represented by the monotype α → α.

Technically, we keep abstractions in the prefix Q that appears in front of typing judgments (Q) Γ ⊢ a : σ, using a new form of bindings (α ⇒ σ), which should be read "α abstracts σ." Resuming with the typechecking of a 5 , we may write (α ⇒ σ id ) z : α ⊢ ω † z : α (3). The hypothesis that α abstracts σ id allows to abstract the INRIA type σ id → σ id of ω † as α → α. We may then assign the type α → α to ω † and type α to the application of ω † z when z is assumed to be of type α. Note that abstraction is an asymmetric relation and it is not the case that σ id abstracts α. In particular, (α ⇒ σ) z : α ⊢ z : σ id does not hold. This would reveal hidden information and it is not allowed implicitly, but only explicitly via a type annotation. Discharging the assumption on z in the judgment (3) (like in Rule Fun), leads to (α ⇒ σ id ) ⊢ a 5 : α → α. Finally discharging the prefix (like in Rule Gen), we may conclude ⊢ a 5 : ∀(α ⇒ σ id ) α → α. This can be read as "a 5 has type α → α where α is σ id ." Notice both the analogy and the difference with flexible bounds. Here, the bound of α means exactly σ id and cannot be instantiated. We call (α ⇒ σ id ) a rigid binding and the position of σ id in this type scheme a rigid occurrence.

Although σ id is the only possible meaning for α, it cannot be substituted inside α → α. That is, σ 1 defined as ∀(α ⇒ σ id ) α → α is not equivalent to σ id → σ id , nor to ∀(α ⇒ σ id , α ′ ⇒ σ id ) α → α ′ , which we refer to as σ 2 . Maybe surprisingly, σ 1 is more abstract than σ 2 , which we write σ 2 ⊏σ 1 . To see this, one may read the latter as

∀(α ⇒ σ id ) (∀(α ′ ⇒ σ id ) α → α ′ ) and abstract σ id as α in the binding (α ′ ⇒ σ id ), leading to ∀(α ⇒ σ id ) (∀(α ′ ⇒ α) α → α ′ ), which is equivalent to ∀(α ⇒ σ id ) α → α.
The later step holds because monotype bounds, which have no other instances but themselves, are "transparent" and can always be inlined, i.e. substituted for the variable that binds them.

Intuitively, polytype bounds may also be expanded. For instance, ∀(α ⇒ σ id , α ′ ⇒ σ id ) α → α ′ intuitively stands for σ id → σ id . However, this is not technically correct as in general the position of quantifiers would be ambiguous. For example σ id → σ id → σ id could be read either as

∀(α ⇒ σ id , α ′ ⇒ σ id , α ′′ ⇒ σ id ) α → α ′ → α ′′ or ∀(α ⇒ σ id , α ′ ⇒ σ id → σ id ) α → α ′
where σ id → σ id need in turn to be expanded. However, both are not considered equivalent in iML F . Thus, we simply forbid polytypes to appear under arrow types, and instead force them to be abstracted as variables in auxiliary bindings. Consistently, and by contrast with iML F , we restrict types to monotypes and force all polytypes to be type schemes.

Type annotations are used to reveal abstractions. For instance, λ(x) (x : σ id ) x, is typed as follows: the annotation (x : σ id ) requires that x has some type α where α is an abstraction of σ id ; the annotation then reveals σ id as the type of (the annotated) x instead of the (weaker) abstract type α. We thus have (α ⇒ σ id ) x : α ⊢ (x : σ id ) : σ id , using a derived rule of the form

(α ⇒ σ id ) x : α ⊢ x : α (α ⇒ σ id ) α ⊐ -σ id (α ⇒ σ id ) x : α ⊢ (x : σ id ) : σ id
Once the type σ id has been revealed, it may be instantiated, e.g. into α → α. Therefore, we have (α ⇒ σ id ) x : α ⊢ (x : σ id ) x : α and, finally, ⊢ λ(x) (x : σ id ) x : ∀(α ⇒ σ id ) α → α. There is still one subtlety when typechecking the simpler program λ(x) (x : σ id ). From the intermediate step (α ⇒ σ id ) x : α ⊢ (x : σ id ) : σ id we may not conclude (α ⇒ σ id ) ⊢ (x : σ id ) : α → σ id as α → σ id would be an ill-formed type scheme. Moreover, this would just be one solution among many others, as σ id could also have been instantiated. The solution is to use a flexible binding (α ′ ≥ σ id ) to represent any type of x through the type variable α ′ leading to the judgment (α ⇒ σ id , α ′ ≥ σ id ) ⊢ (x : σ id ) : α ′ . We may then discharge both the context and the prefix and conclude that λ(x : σ id ) x has type ∀(α ⇒ σ id , α ′ ≥ σ id ) α → α ′ . This captures all possible types-given the annotation. Retrospectively, we may see the annotation (a : σ id ) as the application ( : σ id ) a, where the notation ( : σ) stands for the expression λ(x) (x : σ) and may be provided as a (collection of) primitive(s) with type scheme(s)

∀(α ⇒ σ, α ′ ≥ σ) α → α ′ .
Fitting it together into eML F

The type system eML F we have devised so far does not fit directly into the Curry-style System G that does not permit any annotations on source terms. As type abstractions and type instantiation remain implicit in eML F , the only new construction is, for the moment, a new form of abstraction λ(x : σ) a where the parameter x is annotated with a type scheme σ. We shall see below how this construction can be explained in terms of a more atomic simple term annotation.

In fact, we restrict the bounds of rigid bindings to a subset of type schemes, ranged over by letter ρ, that correspond to System-F types as defined by the following grammar.

τ ∈ T e ::= α | τ → τ eML F types σ ∈ S e ::= τ | ∀(q) σ | ⊥ eML F type schemes q ∈ Q e ::= α ≥ σ | α ⇒ ρ eML F bindings ρ ∈ R e ::= τ | ∀(α ≥ ⊥) ρ | ∀(α ⇒ ρ) ρ F-like type schemes
As a consequence, non-trivial flexible bounds may not appear under a rigid bound. This is only to keep eML F in exact correspondence with iML F . Of course, we must adapt the instance relation ≤ of iML F to an instance relation ⊑ on eML F type schemes. In fact, ⊑ is recursively defined together with a subrelation ⊏that captures the notion of type abstraction mentioned above, which is the essential difference between iML F and eML F . There is some degree of liberty in the definition of these two relations, which is discussed at the end of this section, while the precise definition can be found in §4.

From a typing point of view, we may hide type annotations into a collection of primitives ( : ρ) as suggested above and see λ(x : ρ) a as syntactic sugar for λ(x) let x = (x : ρ) in a. This encoding will be explained in detail below. In short, it works as follows. On the one hand, the annotation on ( : ρ) requests its argument x to have type α where α abstracts the type scheme ρ. Thus, the λ-bound variable x has type α, which is a monotype as requested. On the other hand, the annotation returns a value of (concrete) type σ as opposed to the abstract type α-we may say that it reveals the concrete type σ of α. Hence, the let-bound variable x has type σ and may be used within a with different instances. Of course, we may derive the following typing rule for annotated abstractions:

Fun ⋆ (Q) Γ, x : ρ ⊢ a : τ α / ∈ ftv(τ ) (Q) Γ ⊢ λ(x : ρ) a : ∀(α ⇒ ρ) α → τ
Following this approach, eML F remains an instance of System G-at least from a typechecking viewpoint. However, this solution requires ρ to appear at a rigid occurrence in the type ∀(α ⇒ ρ) ∀(α ′ ≥ ρ) α → α ′ , which prevents ρ to be an arbitrary type scheme σ. While this restriction is not a problem in practice, it is more restrictive than necessary and does not allow to directly map derivations of iML F programs to eML F programs.

Therefore, we give a direct account of type annotations, moving slightly out of System G, and introduce the following typing rule:

Annot (Q) Γ ⊢ a : σ ′ (Q) σ ′ ⊐ -σ (Q) Γ ⊢ (a : σ) : σ
This allows all type schemes to be explicitly coerced along the inverse of type abstraction, called revelation. There is still no surprise in the typing rules of eML F : the power of eML F lies in its types, the enforcement of a clear separation between types schemes and types, and the decomposition of the instance relation of iML F into a smaller implicit instance relation and explicit revelation, which we explain below in more details.

Design space

The semantics of eML F is given by translation into iML F by both dropping type annotations and inlining rigid bindings. For the sake of comparison between the instance relation ⊑ of eML F and the instance relation ≤ of iML F , we may always see types of eML F as types of iML F by inlining all rigid bindings. While ≤ is uniquely determined by the encoding of its types into sets of System-F types (given in §3.2), the relation ⊑ is only a subrelation of ≤, so as to allow type inference in eML F . Although type inference is out of the scope of this paper and described elsewhere [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]Rémy and Yakobowski, 2008a), we may explain the choice of ⊑ as follows.

A design choice for eML F is to treat polymorphism as first-class, as in iML F , but never have to guess it. Furthermore, typable expressions must have principal types, so that type inference is both tractable and practical. Concretely, types of eML F are enriched so as to distinguish between types ∀(α ⇒ σ id ) α → α and ∀(α ⇒ σ id , α ′ ⇒ σ id ) α → α ′ , say σ 1 and σ 2 , that are confounded in iML F . In other words, the equivalence relation ⊏ -⊐ -, the kernel of ≤, which is too coarse, is replaced by the asymmetric, more discriminative abstraction relation ⊏ -, whose kernel ≡, is smaller than ⊏ -⊐and such that (⊏ -∪ ⊐ -) * is ⊏ -⊐ -(1), where ⊐ -, called revelation, is the inverse of ⊏ -. This ensures that nothing is really lost: type abstraction is implicitly used to abstract (forget) type information, i.e. to replace a concrete type scheme σ by a type variable α that abstracts σ; conversely, type annotations are explicitly used to reveal (actually, recover) the concrete type scheme that a variable abstracts over. Hence, we may also use revelation in eML F via explicit type annotations.

Therefore, the design space mainly lies in the choice of the preorder ⊏ -, which is already constrained by (1), so that eML F and iML F coincide up to type annotations. The abstraction must not be too coarse, as otherwise eML F would coincide with iML F exactly, require type annotation and have undecidable type inference. The abstraction must not be too discriminative either, as in order for eML F to be a conservative extension of ML, ≡ should at least contain the restriction of ⊏ -⊐to ML type schemes. For instance, if ≡ were the identity relation,

INRIA then eML F would distinguish types such as two representations ∀(α ⇒ τ ) α → α and ∀(α ⇒ τ, α ′ ⇒ τ ) α → α ′ of the same type τ → τ .
We may remove some degrees of freedom in the definition of ⊏ -, by requiring revelation to be confluent, i.e. ⊏ -; ⊐ -(one step of ⊏followed by one step of ⊐ -) to be a subrelation of ⊐ -; ⊏ -. This also implies that ⊏ -⊐is in fact equal to ⊐ -; ⊏ -(2). When splitting ⊏ -⊐into ⊐ -; ⊏ -, there is in fact a natural orientation of the rules that is induced by ≤. For example, consider the type schemes σ ′ 1 , defined as ∀(α ≥ σ id ) α → α, and σ ′ 2 , defined as ∀(α ≥ σ id , α ′ ≥ σ id ) α → α ′ , obtained from the types σ 1 and σ 2 (defined two paragraphs above) by replacing rigid bounds with flexible ones. Type σ ′ 1 is an instance of σ ′ 2 in iML F . That is, flexible bindings can be shared along the instance relation in iML F . Therefore, we choose the same direction for rigid bindings and let σ 2 ⊏σ 1 hold in eML F .

We thus seek for a confluent pre-order ⊐ -, such that ⊐ -; ⊏is ⊏ -⊐and ⊏ -∩ ⊐ -, i.e. ≡, contains at least the equivalence of ML type schemes. In addition, we should minimize ⊐ -\ ⊏which determines when explicit type annotations are required. That is, maximize ≡ within ⊏ -⊐ -(so as preserve type soundness) while retaining both the decidability of type inference and the existence of principal types (3).

Finally, once ⊏is determined, the relation ⊑ must be such that ⊑ ∩ ⊒ is ≡ and (⊑ ∪ ⊐ -) * is ≤. In addition, ⊑ should be chosen as large as possible, so as to minimize the number of type annotations.

Beyond this point, we may only provide hints, as a detailed discussion of type inference is out of the scope of this paper. The preservation of principal types requires the commutation of ≡ with type inference rules (Rémy and Yakobowski, 2008a) and imposes further constraints on ≡. While the original choice for ≡ (Le Botlan and Rémy, 2003) does verify the criteria (3) above, it is not the largest such relation. The relation proposed in this work is more general. It also verifies the criteria (3), as shown in recent works based on graphs by Rémy andYakobowski (2008a, 2007), although with a different presentation. Whether it is optimal-if we exclude considering special cases-is a difficult question, although the graph presentation, which exposes the commutation properties between type inference and type instance more clearly, might help find an answer.

In summary, there is actually little choice for the definition of ⊑, except changing the relation ≤ itself-or considering arbitrary special cases. The design choice made in this paper is ultimately justified by type inference for Full eML F , shown in two other works with minor differences-a slightly weaker relation in the original work or a slight difference in the definition of the relation in the more recent works based on graphs. Interestingly, while Full ML F uses a richer set of types (where rigid bounds can be arbitrary σ-types rather and not only ρ-types), the restriction of its type instance relation to ML F types is exactly the type instance relation of ML F . Hence, the semantics of types of iML F determines type instance ≤ in iML F which in turn leaves little freedom for ⊑ and ⊏in eML F and also strongly constraints their generalization to Full eML F .

i ML F , Curry-style ML F

In this section we study iML F , that is G(T i , S i , Q i , ≤) and, in particular, the type-instance relation ≤ introduced in §2.2. For that purpose, we define an interpretation of iML F types as sets of F types that induces a semantic definition of type instance ( §3.2). An alternative syntactic definition of type instance is given next ( §3.3). We also provide an encoding of iML F terms into terms of F let ( §3.6 and §3.5), which reduces type safety of iML F to that of F let . The expressiveness and modularity of iML F are discussed in §3.7.

Types and prefixes

Flexible bindings are the main novelty of iML F . So as to be self-contained, we remind their definition here:

τ ∈ T i ::= α | τ → τ | ∀(α ≥ ⊥) τ Types σ ∈ S i ::= τ | ∀(q) σ | ⊥ Type Schemes q ∈ Q i ::= α ≥ σ Bindings
The arrow is a type constructor. For simplification, it is the only type constructor but there is no difficulty in generalizing types with other type constructors. The types τ 1 and τ 2 in τ 1 → τ 2 are called type arguments. Type schemes are used as bounds for variables, which limits the way those variables may be instantiated. The special type scheme ⊥ (read bottom) is the most general bound, also called the trivial bound. A variable with a trivial bound is said to be unconstrained. We define ∀(α) σ as syntactic sugar for ∀(α ≥ ⊥) σ. We recall that free (type) variables are defined in § 2.1 (page 11).

Inert types. In iML F , a type is inert if and only if it is a type variable or an arrow type (that is, of the form τ 1 → τ 2 for some types τ 1 and τ 2 ). The set of inert types is written I i . Intuitively, inert types have no other instance but themselves (up to equivalence), i.e., if τ is in I i and τ is an instance of τ ′ then τ ′ is an instance of τ -and so equivalent to τ .

Polytypes. The set T i of iML F types contains only types with trivial bounds ⊥. Notice that ⊥ is not a type but a type scheme. However, ∀(α) α, which as we shall see shortly is equivalent to ⊥, is a type.

Types of T i can be mapped to T F in a trivial way, just by exchanging the trivial bound with the unique kind ⋆. If τ is in T i , we write ⌈τ ⌉ for the counter-part of τ in T F . F-substitutions. We call F-substitutions and write θ for idempotent substitutions mapping type variables to F-types.

Interpretation of types and prefixes

Intuitively, the type scheme ∀(α ≥ σ) σ ′ is meant to represent all types σ ′ where α is any instance of σ. We formalize this intuition by giving a formal interpretation of types and type schemes as sets of F-types. If S is a set of F-types, we write ∀(α) S for the set {∀(α) t | t ∈ S} and θ(S) for {θ(t) | t ∈ S}. Definition 3.2.1 (Semantics of types) The semantics of a type τ , written { {τ } } is the instance closure of its translation to System F, i.e. {t ∈ T F | ⌈τ ⌉ ≤ F t}. The semantics of type schemes, written { {σ} }, is recursively

defined by t ∈ { {σ} } if and only if σ is ⊥ or of the form ∀(α ≥ σ ′ ) σ ′′ and t is of the form ∀( β) t ′′ [t ′ /α] with β # ftv(σ), t ′ ∈ { {σ ′ } }, and t ′′ ∈ { {σ ′′ } }.
Note that the semantics of ⊥ and ∀(α) α are both equal to T F , as suggested earlier, although the former is only a type scheme and not a type. A type of the form ∀(α) τ can be seen both as a type and as a type scheme. In the following lemma, we check that both views lead to the same interpretation.

Lemma 3.2.2 (Consistency) For any type τ , the semantics of τ seen as a type and the semantics of τ seen as a type scheme are equal.

Example 3.1 The interpretation of the polymorphic type σ id , defined as ∀(α) α → α, is the set composed of all types of the form ∀(ᾱ) t → t. In turn, the interpretation of ∀(α ≥ σ id ) α → α is the set composed of all types of the form ∀( β) (∀(ᾱ) t → t) → (∀(ᾱ) t → t). Although both sides of the arrow may vary, they must do so in sync and always remain equal. Note also that ∀(ᾱ) t → t is not necessarily closed, hence the quantification over variables β in front.

The instance relation of System F induces an instance relation in iML F . However, as type instance is defined under prefixes, we must first give a meaning to prefixes.

In a typing judgment, a prefix is meant to capture the possible types that may be substituted for the variables in the domain of the prefix. Thus, the interpretation of a prefix is a set of substitutions. As usual, the composition operator is written

•. That is, f • g is the function x → f (g(x). Given a family of functions (f i ) i∈1..n , we write • i∈1..n f i for f 1 • . . . • f n . Definition 3.2.3 (Semantics of prefixes) The semantics of a prefix Q of the form (α i ≥ σ i ) i∈1..n , written { {Q} } is the set of all F-substitutions of the form • i∈1..n (α i → t i ) where t i ∈ { {σ i } } for i in 1.
.n. As a particular case, { {∅} } is the singleton composed of the identity function.

In fact, we may restrict to certain decompositions that are canonical. Definition 3.2.4 A canonical decomposition of an F-substitution is a decomposition of the form • i∈1..n θ i where all θ i 's are F-substitutions (hence idempotent) and have disjoint domains.

Notice, that given the idempotence of individual substitutions and disjointness of their domains, the idempotence of the composition is then equivalent to the property codom(θ i ) # dom(θ j ) for all i < j.

Lemma 3.2.5 Given a prefix of the form

Q i∈1..n i , any member of { {Q i∈1..n i } } has a canonical decomposition • i∈1..n θ i with θ i ∈ { {Q i } }.
Canonical decompositions are interesting because any grouping (by associativity) is also canonical. Moreover, they enjoy the following property:

INRIA Figure 5: Type Congruence in iML F . iCon-AllLeft (Q) σ 1 R σ 2 (Q) ∀(α ≥ σ 1 ) σ R ∀(α ≥ σ 2 ) σ iCon-AllRight (Q, α ≥ σ) σ 1 R σ 2 (Q) ∀(α ≥ σ) σ 1 R ∀(α ≥ σ) σ 2 iCon-Arrow (Q) τ 1 R τ 2 (Q) τ ′ 1 R τ ′ 2 (Q) τ 1 → τ ′ 1 R τ 2 → τ ′ 2 Lemma 3.2.6 If θ 1 • θ 2 is a canonical decomposition of an F-substitution, then θ 2 • (θ 1 • θ 2 ) = (θ 1 • θ 2 ) • θ 1 = (θ 1 • θ 2 ). Definition 3.2.7 (Type instance) The instance relation ≤ in iML F is defined by (Q) σ 1 ≤ σ 2 if for all θ ∈ { {Q} }, we have θ{ {σ 1 } } ⊇ θ{ {σ 2 } }. The equivalence relation ⊏ -⊐ -is the kernel of ≤.
Remarkably, type instance treats both sides of the arrow symmetrically. Thus, the generalization of types to allow arbitrary type constructors would not need a notion of variance for type constructors. Technically, type instance does not directly operate under arrow types, similarly to ≤ F and by contrast with both <: and ≤ η . However, it does operate inside bindings, which may indirectly affect arrow types. For instance,

∀(α≥σ id ) τ → α can be instantiated into ∀(α≥σ id → σ id ) τ → α which is equivalent to τ → (σ id → σ id ). However, τ → (σ id → σ id )
is not an instance of τ → σ id . Thus, the replacement of τ → σ id by ∀(α ≥ σ id ) τ → α is a way to tell explicitly within types that the right-hand side of the arrow may be instantiated. We could also write ∀(α ≥ σ id ) α → τ to allow instantiation on the left-hand side of the arrow, although such a type may not be more useful than ∀(α) α → τ . Much more interesting, we may allow instantiation on several occurrences simultaneously, as in the type ∀(α ≥ σ id ) α → α (of choose id). It is actually essential that type instantiation be allowed under arrow types and simultaneously in several occurrences, so that programs such as choose id have principal types. It is also important that this mechanism does not depend on variances of type constructors, which would prevent the use of first-order unification for type inference.

Expanding the definition of equivalence, we have

(Q) σ 1 ⊏ -⊐ -σ 2 if and only if for all θ ∈ { {Q} }, we have θ{ {σ 1 } } = θ{ {σ 2 } }. We simply write σ 1 ⊏ -⊐ -σ 2 , when (∅) σ 1 ⊏ -⊐ -σ 2 .
If ⌈τ 1 ⌉ and ⌈τ 2 ⌉ are equal, their semantics { {τ 1 } } and { {τ 2 } } are also equal, hence τ 1 ⊏ -⊐τ 2 . (The only reason why τ 1 and τ 2 may not coincide exactly is that F-types are taken modulo equivalence-see page 12.) We may thus invert the definition ⌈•⌉ into a function from T F to T i . For any type t in T F , we write ⌊t⌋ the type τ of T i defined up to equivalence such that t is ⌈τ ⌉. We extend the ⌊•⌋-mapping pointwise to F-substitutions, writing ⌊θ⌋ for the substitution α → ⌊θ(α)⌋.

Type instance may also be defined on prefixes as follows.

Definition 3.2.8 (Prefix instance) We say that Q 2 is an instance of Q 1 and we write

Q 1 ≤ Q 2 if { {Q 1 } } ⊇ { {Q 2 } }.

Syntactic versions of instance and equivalence

The semantic definition of type instance is not constructive, as it involves quantification over infinite sets. A first step towards an algorithm for checking type instance is to provide an equivalent but syntactic definition of type instance. While semantic type equivalence is defined after type instance, as its kernel, it is simpler (and more intuitive) to define syntactic type equivalence first, and syntactic type instance as a larger relation containing type equivalence.

A judgment for a prefixed relation R is a triple written (Q) σ 1 R σ 2 . It is closed if free type variables of σ 1 and σ 2 are included in dom(Q) and Q is closed. We also say that the prefix Q is suitable for the judgment. Definition 3.3.1 (Congruence) A relation R is ≥-congruent when it satisfies both iCon-AllLeft and iCon-AllRight (Figure 5). It is congruent if it is ≥-congruent and moreover satisfies iCon-Arrow (Figure 5). Lemma 3.3.2 Type instance is ≥-congruent. Type equivalence is congruent.

6: Syntactic type equivalence ⊏ -⊐ -in iML F . iEqu-Comm α 1 / ∈ ftv(σ 2 ) α 2 / ∈ ftv(σ 1 ) (Q) ∀(α 1 ≥ σ 1 ) ∀(α 2 ≥ σ 2 ) σ ⊏ -⊐ -∀(α 2 ≥ σ 2 ) ∀(α 1 ≥ σ 1 ) σ iEqu-Free α / ∈ ftv(σ) (Q) ∀(α ≥ σ ′ ) σ ⊏ -⊐ -σ iEqu-Inert (α ≥ σ ′ ) ∈ Q (∅) σ ′ ⊏ -⊐ -τ τ ∈ I i (Q) σ ⊏ -⊐ -σ[τ /α] iEqu-Var (Q) ∀(α ≥ σ) α ⊏ -⊐ -σ
Definition 3.3.3 (Syntactic type equivalence) Syntactic type equivalence is the smallest reflexive, transitive, symmetric, and congruent relation on closed judgments satisfying the rules of Figure 6.

We intendedly use the same symbol ⊏ -⊐for syntactic and semantic equivalence, because the two definitions coincide, as explained below.

Rule iEqu-Comm allows for commutation of bindings with disjoint domains; Rule iEqu-Free allows for removal of useless bindings; Rule iEqu-Inert allows for inlining of inert bindings (inert types are defined on page 20). Rule iEqu-Var identifies ∀(α ≥ σ) α and σ, i.e. it states that a (possibly polymorphic) type σ stands for all of its instances.

Interestingly, Rule iEqu-Inert allows for reification of a substitution [τ /α] as a prefix (α ≥ τ ). Actually, any substitution can be represented as a prefix. This is a key technical point that is used in the presentation of type inference and unification, where the solution of a unification problem is not a substitution but rather a prefix, which is more general-see [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF] or (Le Botlan, 2004, Chapter 3) for more details.

Rules iEqu-Inert, iEqu-Free and iEqu-Var may be oriented from left to right and used as rewriting rules to transform every type scheme σ into a normal form, up to commutation of binders-see [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF] or (Le Botlan, 2004, Chapter 1) for details.

Syntactic and semantic definitions of type equivalence coincide, as shown by Theorem 3.3.9 and Conjecture 3.3.13 below. Although these results will follow from similar results for type instance, they are easier to prove in the case of type equivalence, hence we prove them independently. We first establish a few lemmas. We remind the notation ∀(α) S introduced at the beginning of §3.2.

Lemma 3.3.4 If α / ∈ ftv(σ), then ∀(α) { {σ} } ⊆ { {σ} } holds.
Lemma 3.3.5 For any F-substitution θ and type scheme σ, we have θ({ {σ} }) ⊆ { {⌊θ⌋(σ)} }.

The converse inclusion only holds under some hypotheses on the occurrences of free type variables of σ that are in dom(θ), which must not be exposed.

Definition 3.3.6 (Exposed type variables) Exposed type variables in a type scheme σ are free type variables etv(σ) that are reachable from the root of σ without crossing any type constructor (i.e. the arrow in our setting), recursively defined as follows:

etv(α) = α etv(τ → τ ) = ∅ etv(⊥) = ∅ etv(∀(α ≥ σ) σ ′ ) = (etv(σ ′ ) \ {α}) ∪ etv(σ) For example α is exposed in ∀(β ≥ α) σ, but not in α → ∀(β) α. Lemma 3.3.7 If α is not exposed in σ, then etv(σ) = etv(σ[τ /α]) holds for any τ .
Our interest is more in type variables that are not exposed, as substituting them is sound.

Lemma 3.3.8 Let σ be a type scheme and θ a substitution

[t/α] such that either t is inert or α is not exposed in σ. If t ′ ∈ { {⌊θ⌋(σ)} } and α / ∈ ftv(t ′ ), then t ′ ∈ θ({ {σ} }).
This lemma is stated in the particular case of a singleton substitution. This is only to simplify its presentation.

Similarly, the condition α / ∈ ftv(t ′ ) may always be satisfied by appropriate renaming of σ and θ. On the opposite, the two conditions on θ are more important and prevent cases where the lemma would not hold.

(Proof p. 55) INRIA Figure 7: Syntactic Type Instance ≤ in iML F . iIns-Equiv (Q) σ 1 ⊏ -⊐ -σ 2 (Q) σ 1 ≤ σ 2 iIns-Bot (Q) ⊥ ≤ σ iIns-Hyp (α ≥ σ) ∈ Q (Q) σ ≤ α iIns-Subst α / ∈ etv(σ) (Q) ∀(α ≥ τ ) σ ≤ σ[τ /α]
Lemma 3.3.9 (Soundness of syntactic equivalence) The semantic type equivalence relation satisfies all rules of Figure 6. We intendedly use the same symbol for syntactic and semantic type instance because the two definitions coincide, as explained below.

Rule iIns-Equiv ensures that type instance contains type equivalence. Rule iIns-Bot states that ⊥ is the most general type. Rule iIns-Hyp is obvious as a logical rule, as it just uses an hypothesis. Its effect is to replace a type scheme by a variable that stands for an instance of that type scheme. As it can be used repeatedly, its effect is often to join two flexible bindings that have the same bound (when used in combination with flexible-congruence rules). iIns-Subst inlines a flexible binding (α ≥ τ ) with a type bound τ , thus settling the choice made for τ . Type scheme bounds must be instantiated to types using flexible congruence before they can be inlined. The side condition requires that variable α is not exposed in σ. This is to prevent cases where α would appear in σ as a flexible bound. For example, without the side condition, one could derive

(Q) ∀(α ≥ τ ) ∀(β ≥ α) ∀(γ ≥ α) β → γ ≤ ∀(β ≥ τ ) ∀(γ ≥ τ ) β → γ, which implies (Q) ∀(α ≥ τ ) α → α ≤ ∀(β ≥ τ ) ∀(γ ≥ τ ) β → γ
and is certainly false: the semantics ensures that β and γ are substituted by the same instance of τ on the left-hand side, but not on the right-hand side. Note that this condition also prevents the case where σ is itself α, as in the type instance (Q) ∀(α ≥ τ ) α ≤ τ . However, this judgment is a particular case of equivalence, and thus still provable using rule iIns-Equiv.

Instance derivations can be renamed, prefixes can be extended, and substitutions by equivalent types preserve equivalence, as stated by the following Lemma.

Lemma 3.3.11 Assume R is ⊏ -⊐ -or ≤.
i) The relation R satisfies both axioms Renaming and Extra-Bindings of page 13.

ii)

If (Q) τ 1 ⊏ -⊐ -τ 2 holds, then (Q) σ[τ 1 /α] ⊏ -⊐ -σ[τ 2 /α] holds.
(Proof p. 56)

Lemma 3.3.12 (Soundness of syntactic instance) The type instance relation satisfies all rules of Figure 7.

(Proof p. 57)
An obvious question is whether the syntactic definitions of type equivalence and type instance are complete for the corresponding semantic definitions.

Conjecture 3.3.13 (Completeness of syntactic relations) Any type equivalence relation can be derived with rules of Figure 6. Any type instance relation can be derived with rules of Figure 7.

A proof of this conjecture has only been sketched, using an intermediate semantics of types based on a graphic representation to factor all of their instances as a single and simple object-see discussion in §5. While showing the equivalence of the two semantics should not be difficult, a description of the graph representation of types is beyond the scope of this paper (see [START_REF] Didier | A graphical presentation of MLF types with a linear-time unification algorithm[END_REF]) and a direct proof using the semantics of this paper without referring to graphs would be too long and tedious.

This conjecture combined with Lemma 3.3.9 justifies our semantics of types. In the rest of the paper we do not distinguish between syntactic and semantic relations and only say type equivalence or type instance. However, we do not actually rely on this conjecture: we only use the soundness of the syntactic definitions with respect to their semantics definitions, not their completeness. Therefore, reading type equivalence and type instance as the syntactic versions hereafter is always technically correct and never relies on the conjecture.

Typing rules

As iML F is an instance of System G, its typing rules are as described in Figure 4. Some examples of typings have been introduced informally in §1. Other examples will be presented with more details in §3.7.

There is an interesting admissible rule in iML F that helps typing abstractions:

iFun ⋆ (Q) Γ, x : τ ⊢ a : σ α / ∈ ftv(τ ) (Q) Γ ⊢ λ(x) a : ∀(α ≥ σ) τ → α
To see this, assume (Q) Γ, x : τ ⊢ a : σ. Let α be a variable that does not appear free in (Q). We have (Q, α ≥ σ) Γ, x : τ ⊢ a : σ (1) by lemma 2.1.1.ii. We have (Q, α ≥ σ) σ ≤ α (2) by iIns-Hyp. By Rule Inst with (1) and ( 2), we get (Q, α ≥ σ) Γ, x : τ ⊢ a : α. We conclude by Rule Fun followed by Rule Gen.

Generalized application

Rule Gen generalizes a binding by moving a binding from the prefix to the right-hand side. The converse rule is in fact admissible.

UnGen ⋆ (Q) Γ ⊢ a : ∀(α ≥ σ) σ ′ α / ∈ dom(Q) (Q, α ≥ σ) Γ ⊢ a : σ ′ Indeed, assume (Q) Γ ⊢ a : ∀(α ≥ σ) σ ′ holds. Then, by Lemma 2.1.1.ii, we get (Q, α ≥ σ) Γ ⊢ a : ∀(α ≥ σ) σ ′ . We conclude by Rule Inst and (Q, α ≥ σ) ∀(α ≥ σ) σ ′ ≤ σ ′ , as shown below: (Q, α ≥ σ) ∀(α ≥ σ) σ ′ = ∀(β ≥ σ) σ ′ [β/α] by α-conversion ≤ ∀(β ≥ α) σ ′ [β/α] by iIns-Hyp and iCon-AllLeft ⊏ -⊐ -σ ′ by iEqu-Inert
More interestingly, the following generalized application rule is also admissible-it is actually derivable with repeated applications of admissible Rule UnGen ⋆ on both premises, and an application of rule App followed by an application of rule Gen:

App ⋆ (Q) Γ ⊢ a 1 : ∀(Q ′ ) τ 2 → τ 1 (Q) Γ ⊢ a 2 : ∀(Q ′ ) τ 2 (Q) Γ ⊢ a 1 a 2 : ∀(Q ′ ) τ 1
We refer to typing rules extended with App ⋆ as generalized typing rules. We presented the system with Rule App, rather than Rule App ⋆ for economy of the formalization as well as for emphasizing the generic presentation of the type system. However, the generalized typing rules, while defining the same judgments allow for more derivations and so have actually more interesting modularity properties. In particular, we use the generalized presentation in §3.7.

Recursion

There is no explicit construction for recursion in iML F . From a typing point of view, recursion can always be treated as the application of a fixed point combinator, given as a constant with its type scheme in the initial typing environment. For instance, let rec f = λ(x) a 1 in a 2 in ML may be seen as let f = fix (λ(f ) λ(x) a 1 ) in a 2 where fix behaves, for instance, as

λ(f ) (λ(x) f (λ(y) x x y)) (λ(x) f (λ(y) x x y)).
and is assigned the type scheme ∀(γ ≥ ∀(αβ) α → β) (γ → γ) → γ. The derived typing rule is:

Rec ⋆ (Q, Q ′ ) Γ, f : τ ⊢ λ(x) a 1 : τ (Q) Γ, f : ∀(Q ′ ) τ ⊢ a 2 : τ 2 (Q) Γ ⊢ let rec f = λ(x) a 1 in a 2 : τ 2
This view implies that f must be assigned a type τ and not a type scheme while type checking a 1 . Thus, f may be used polymorphically during the recursion, but only with System-F polymorphism.

INRIA

Using a primitive construct for recursion would allow f to be assigned a type scheme, which would be slightly more general. However, this extension would break the encoding of ML F into System F, described below in §3.6.

The key is that where f is assigned a type, the recursion itself can be seen as monomorphic, as every occurrence of f in a 1 sees f with the same polymorphic type, which may then be instantiated appropriately. By contrast, when f is a type scheme σ, several occurrences of f in a 1 may view f with different types (that are all instances of σ, of course).

System F as a subset of (Simple) i ML F

We recall that Simple ML F is iML F without terms with local bindings. Before showing the inclusion of System F in Simple ML F , we show the inclusion of their instance relations.

Lemma 3.5.1 Assume t ≤ F t ′ holds. Then, (Q) ⌊t⌋ ≤ ⌊t ′ ⌋ holds under any suitable prefix Q.

(Proof p. 57)
The next lemma states the inclusion of System F into Simple ML F .

The translation ⌊Γ⌋ of a typing context Γ into one of Simple ML F , is the pointwise translation of types, i.e. ⌊x : t⌋ is x : ⌊t⌋.

Theorem 1 Assume F :: Γ ⊢ a : t holds. Then, the judgment iML F :: (Q) ⌊Γ⌋ ⊢ a : ⌊t⌋ holds under any prefix Q binding the free variables of Γ and t.

(Proof p. 57) 3.6 Type soundness, by viewing i ML F as a subset of F let

In this section, we introduce a new type system, called F let that extends System F with let-bindings a la ML, which is already large enough to contain iML F . The language F let is actually a subset of the more notorious extension of System F with intersection types F ∧ . The type soundness of F ∧ , which is folklore knowledge, ensures the type soundness of iML F .

From ML and System F to F let The language ML extends simple types with type schemes, which can be used to factor out all the simple types of an expression, and a specific rule for typechecking local bindings that takes advantage of type schemes. Namely, while typechecking let x = a in a ′ , the locally bound variables x may be assigned a type scheme ∀(α) τ rather than a simple type τ , which amounts to assigning x the whole collection of simple types τ [τ ′ /α] where τ ′ ranges over all types. This is the essence of the ML type system. Its simplicity lies in the fact that type schemes may not be assigned to function parameters, hence, ML retains nearly the simplicity of simple types. Actually, it is well-known that an expression is typable in ML if (and only if) it is typable with simple types after reduction of all its local bindings, i.e. the replacement of let x = a in a ′ by a ′ [a/x] in any context. This reduction always terminates but the resulting expression may be exponentially larger than the original one. Hence, this operational view of ML is inefficient. It is not very modular either. Thus, it is never used in practice. However, it provides ML with a very simple specification: ML is the closure of simple types by let-expansion8 .

Unfortunately, the empowering effect of the Let-Gen typing rule for local bindings becomes inoperative in (the generic presentation of) System F. That is, it does not allow more programs to be well-typed than by seeing local bindings let x = a 1 in a 2 as immediate applications (λ(x) a 2 ) a 1 . This is not a weakness of System F. It simply follows from the fact that types are first-class (or, in our generic setting, that type schemes and types are identical).

One may then consider the alternative definition of ML-the closure of simple types by let-expansion-and apply it to System F. More precisely, we define F let as the smallest superset of System F that contains all terms let x = a 1 in a 2 such that both a 1 and a 2 [a 1 /x] are in F let . The requirement that a 1 also be in F let is to reject terms such as let x = a 1 in a 2 where x would not appear in a 2 and a 1 could be any expression.

This definition is equivalent to adding the following typing rule to System F:

Let-Expand (Q) Γ ⊢ a 1 : σ 1 (Q) Γ ⊢ a 2 [a 1 /x] : σ (Q) Γ ⊢ let x = a 1 in a 2 : σ
Since let-reduction may duplicate let-redexes but not create new ones, it must terminate (by Levy's finite development theorem for the λ-calculus (Barendregt, 1984)). That is, a term of F let may always be let-reduced to a term of System F.

As for ML, this operational specification is not quite satisfactory. Fortunately, there is also a more direct specification based on a very restricted use of intersection types, where intersections are only allowed in types schemes. Consider the following instance of generic types:

τ ∈ T F let ::= α | τ → τ | ∀(q) τ F let types σ ∈ S F let ::= τ | σ ∧ σ F let type schemes q ∈ Q F let ::= α :: ⋆ F let bindings
and the instance relation F let defined as the smallest transitive relation that treats ∧ as associative, commutative, contains ≤ F and all pairs σ ∧ σ ′ F let σ. Then, F let may be equivalently defined by the generic system G(T F let , S F let , Q F let , ) extended with the following typing rule:

Inter (Q) Γ ⊢ a : σ 1 (Q) Γ ⊢ a : σ 2 (Q) Γ ⊢ a : σ 1 ∧ σ 2
This system is a particular case of the extension of System F with intersection types studied by [START_REF] Pierce | Programming with Intersection Types and Bounded Polymorphism[END_REF] 9 , which we refer to as F ∧ . The language F let is significantly weaker-but simpler-than F ∧ . However, to the best of our knowledge it has not be considered on its own.

Our main interest in F let is that although it has a very simple and intuitive specification and is only a small extension to System F, it is already a superset of ML F as we shall see in the next section.

Type soundness of F let

Type soundness relates the static semantics of programs, i.e. well-typedness, to their dynamic semantics, i.e. evaluation. In pure λ-calculus where all values are functions, evaluation may never go wrong except by looping. Type soundness of System F ensures that well-typed programs are strongly normalizable.

However, most real languages allow loops or arbitrary recursion and contain interesting programs that may not terminate. In this setting, well-typedness cannot ensure termination any longer. Simultaneously, real languages also introduce non-functional values, and therefore other sources of errors such as applying a non-functional value to some argument. Well-typedness must then prevent such errors from happening.

In this paper we do not define the dynamic semantics of expressions. We do not address type soundness directly, but only indirectly by showing that well-typed expressions are also well-typed in F let .

The type soundness of F let follows from type soundness of F ∧ . To the best of our knowledge, the type soundness of F ∧ , which is folklore knowledge, has never been published. While proving type soundness for F let directly should not raise any difficulty, this is out of the scope of this paper.

Encoding i ML F into F let

We show that iML F is a subset of F let by translating typing derivations of iML F into typing derivations of F let . For that purpose, we instrument typing judgments of iML F (Q) Γ ⊢ a : σ into judgments of the form (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ to mean "given an F-substitution θ in { {Q} }, and a type t in { {σ} }, the judgment (Q) Γ ⊢ a : σ requires a context ∆". These judgments may also be read as an algorithm that takes θ, t, and a typing derivation of a (regular) typing judgment iML F :: (Q) a ⊢ σ and returns a context ∆. These judgments are defined by typing rules of Figure 8.

In the translation, we distinguish let-bound variables, written x, from λ-bound variables, written y. Hence, the two rules iF-Var-Let and iF-Var-Fun corresponding to the usual unique rule for variables. Notice that only the iF-Var-Let inserts a binding in ∆. The context ∆ maps let-bound variables to intersection types, written ∧t i∈I i . We write ∆ 1 ∧ ∆ 2 for the environment that maps x to ∆ 1 (x) ∧ ∆ 2 (x) when x is in both dom(∆ 1 ) and dom(∆ 2 ) or as ∆ 1 or ∆ 2 when x is in either dom(∆ 1 ) or dom(∆ 2 ). There are two rules for local bindings. Rule iF-Let assumes that variable x appears free in a ′ . The bound expression is typechecked as many times as there are occurrences of x in a ′ , which enables each occurrence to pick a different instance t of σ via rule iF-Var-Let. Rule iF-Let-0 is for the degenerate case where x does not appear free in a ′ . We must still typecheck

8: Translating iML F to F let . iF-Var-Let x : σ ∈ Γ (Q ∋ θ) Γ ⊢ x : σ ∋ t ⇒ (x : t) iF-Var-Fun y : τ ∈ Γ (Q ∋ θ) Γ ⊢ y : τ ∋ t ⇒ ∅ iF-Fun (Q ∋ θ) Γ, y : τ ⊢ a : τ ′ ∋ ⌈τ ′ ⌉ ⇒ ∆ (Q ∋ θ) Γ ⊢ λ(y) a : τ → τ ′ ∋ ⌈τ → τ ′ ⌉ ⇒ ∆ iF-App (Q ∋ θ) Γ ⊢ a 1 : τ 2 → τ 1 ∋ ⌈τ 2 → τ 1 ⌉ ⇒ ∆ 1 (Q ∋ θ) Γ ⊢ a 2 : τ 2 ∋ ⌈τ 2 ⌉ ⇒ ∆ 2 (Q ∋ θ) Γ ⊢ a 1 a 2 : τ 1 ∋ ⌈τ 1 ⌉ ⇒ ∆ 1 ∧ ∆ 2 iF-Inst (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ (Q) σ ≤ σ ′ (Q ∋ θ) Γ ⊢ a : σ ′ ∋ t ⇒ ∆ iF-Gen α / ∈ ftv(Γ) β # dom(Q) (Q, α ≥ σ ∋ θ • [t/α]) Γ ⊢ a : σ ′ ∋ t ′ ⇒ ∆ (Q ∋ θ) Γ ⊢ a : ∀(α ≥ σ) σ ′ ∋ ∀( β) t ′ [t/α] ⇒ ∆ iF-Let-0 x / ∈ ftv(a ′ ) (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ (Q ∋ θ) Γ, x : σ ⊢ a ′ : σ ′ ∋ t ′ ⇒ ∆ ′ (Q ∋ θ) Γ ⊢ let x = a in a ′ : σ ′ ∋ t ′ ⇒ ∆ ∧ ∆ ′ iF-Let ((Q ∋ θ) Γ ⊢ a : σ ∋ t i ⇒ ∆ i ) i∈I I = ∅ (Q ∋ θ) Γ, x : σ ⊢ a ′ : σ ′ ∋ t ′ ⇒ ∆, x : ∧(t i ) i∈I (Q ∋ θ) Γ ⊢ let x = a in a ′ : σ ′ ∋ t ′ ⇒ ∆ ∧ (∧∆ i i∈I )
the premise once to ensure that a is well-typed-since in a call-by-value strategy a is evaluated even if its result is to be discarded. Other rules are straightforward. By convention, all judgments

(Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ carry the implicit side-conditions θ ∈ { {Q} } and θ(t) ∈ θ({ {σ} }).
The following lemma justifies our suggestion to read these judgments as an algorithm.

Lemma 3.6.1 If the judgment (Q) Γ ⊢ a : σ holds, then for any θ in { {Q} } and t in { {σ} }, there exists a context

∆ such that (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ holds.
Notice that, by construction, neither { {Q} } nor { {σ} } may be empty.

(Proof p. 57)

The next two lemmas show the soundness of iML F by translation into F let , which is itself sound. We define { {Γ} } as {y : ⌈τ ⌉ | y : τ ∈ Γ}. Notice that bindings with true type schemes are not in { {Γ} }; they will be replaced by bindings with conjunctive types in some additional environment ∆.

Lemma 3.6.2 If the judgment (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆ holds, then F let :: θ({ {Γ} }), ∆ ⊢ a : θ(t) holds. (Proof p. 58)
Theorem 2 iML F is a subset of F let . More precisely, if the judgment iML F :: (Q) Γ ⊢ a : σ holds, then for any θ in { {Q} } and τ in { {σ} }, there exists a context ∆ such that the judgment F let :: θ({ {Γ} }), ∆ ⊢ a : θ(t) holds.

(Proof p. 58) Type Soundness. Type soundness is a corollary of Theorem 2, as it ensures that iML F is as safe as F let , which is itself as safe as F ∧ , which is safe.

Discussion. As a particular case of the previous lemma, Simple ML F is a subset of System F, since terms of F let without local bindings are also in F. The converse is also true, as shown in the previous section. In particular, Simple ML F and F coincide-regarding the sets of typable terms. We may summarize this section and the previous one with the inclusions

Simple iML F ⊆ F ⊆ Simple iML F ⊂ iML F ⊂ F let .
We already know that at least one of the two last inclusions is strict, as the term a ω IK defined as let y = ω in K (y I) (y K) is in F let (as it let-reduces to a term in F) but it is not in F [START_REF] Giannini | Characterization of typings in polymorphic type discipline[END_REF]. (Notice that a ω IK is in any higher-order extension F n of F for n > 2, hence also in F ω .)

In fact, the two inclusions are strict. We shall show an example that is typable in ML F but not in System F in the following subsection. We now argue (informally) that a ω IK is not in ML F . Intuitively, Rule Inter is much more powerful than rule iF-Let since a conjunctive type may be an arbitrary (finite) set of types in Inter, whereas iF-Let only allows to form conjunctions between types that belong to a common type scheme. To see that a ω IK is not in ML F , we may reproduce the argument used for F by [START_REF] Giannini | Characterization of typings in polymorphic type discipline[END_REF] by analyzing all possible derivations of a ω IK in ML F . In fact, the parameter y will be assigned a type σ that must be a type for ω. In turn, as the parameter x of ω is used polymorphically, it must be assigned an exact type, hence σ is of the form ∀(α 1 ⇒ σ 1 ) ∀(α 2 ⋄ σ 2 ) α 1 → α 2 where σ 1 must be a System-F type ⌊t⌋. Reproducing the reasoning of [START_REF] Giannini | Characterization of typings in polymorphic type discipline[END_REF] (see also Pierce (2002, §23) and [START_REF] Wells | Typability and type checking in System F are equivalent and undecidable[END_REF]), t must be of the form ∀(α) .(. . . (α → t n ) → . . . t 1 ) → t 0 . However, no type of this form can be simultaneously a type for I and K, as required by the two uses of y. In fact, the term a ω IK is not typable in Full ML F either.

Subject reduction. The subject reduction property holds in Simple iML F as a consequence of the twodirectional encoding between System F and Simple iML F . We expect subject reduction to hold in iML F , since it holds in Full ML F (Le Botlan, 2004). However, we did not check this result, as type soundness has already been established by encoding iML F into F let in §3.6.

Expressiveness and modularity

As typing derivations of System F can be mapped directly to typing derivations of iML F , the language iML F performs at least as well as System F with regard to typechecking. We claim that iML F is strictly more expressive than System F in a rather unusual but practically meaningful sense, as it is more modular than System F. Indeed, we show that constructing data structures containing polymorphic values is not modular in System F, while it is in iML F .

For that purpose, we exhibit an unannotated expression b, which, as far as typing is concerned, can be compared to a data structure, say a list, containing a polymorphic value, say id. This expression is typable in System F, hence also in iML F . Then, b is inserted 10 both into a monomorphic data structure (for the sake of conciseness, we use constants in expressions) and into a (truly) polymorphic data structure. In System F, though, two typing derivations are necessary for b, depending on the type of the data structure it will be inserted into. Worse, the number of differences between both typing derivations is proportional to the size of b. On the contrary, in iML F , we show that the very same derivation can be used for b in both cases. (This is of course simply a consequence of principal types.)

We actually consider the generalized presentation of iML F , using Rule App ⋆ rather than App. We could also argue in the original system, but with a more careful definition of modularity. For fairness of comparison, we consider the implicit version of System F. The result can only be (significantly) worsened in explicit System F, as not only typing derivations of progams will have to be changed, but also some of their type abstractions and type applications.

Although our statement is based on a particular example-we do not actually prove that changes in the derivation must be non local but argue informally-it is also seconded by formal results in Le Botlan's thesis [START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF] where it is shown how a single type of eML F captures all type abstractions and type applications of a given expression in System F. However, this formal result uses the principal type property of eML F , which we do not show here, as we do not address type inference-hence, our informal, but simpler explanation.

Although the following example is presented in iML F and based on the modularity of typing derivations, it can be reproduced in eML F since only type annotations on function parameters are needed in eML F and all other type information can be reconstructed in a principal manner.

In fact, we exhibit a sequence of expressions (a n ) n∈I N of increasing size, defined inductively. So as to ease the presentation, we assume that the core language is extended with a ground type i (such as int) and that the initial environment Γ 0 contains the functions choose, id, comp, and ω that satisfy the following signature in iML F (their signature in System F follows by translation).

choose

:

∀(α) α → α → α id : ∀(α) α → α △ = σ id comp : (i → i) → (i → i) △ = σ comp ω : σ id → σ id △ = σ ω
10 Insertion is modeled by mere application.

INRIA

For instance, comp could be the expression λ(g) (λ(x) g (succ x)) where succ is the successor function for integers. From a typing point of view, we claim that choose is similar to a datatype constructor. Indeed, choose v w can be compared to the two-element list [v; w], since v and w are required to have the same type.

Of course, choose v w does not behave as a list, since it forgets its elements after application (at least one of them). Similarly, choose v can be compared to the singleton list [v]. In particular, the typing of choose id raises the same difficulties than the typing of [id] as far as the position of quantifiers is concerned : namely, is its type list(σ id ), or ∀(α) list(α → α), or even ∀(α) list(∀(β) (α → β) → (α → β)?

We now define a sequence of expressions a n and a sequence of types σ n parametrized by an initial expression a for a 0 and an initial closed type σ for σ 0 .

a 0 △ = a a n+1 △ = choose a n σ 0 △ = σ σ n+1 △ = ∀(α ≥ σ n ) α → α
(From a typing point of view, a n behaves as [.. [a]..], the nested singleton list ending at depth n with a as a leaf.) Assume Γ 0 ⊢ a n : σ n (1). By lemma 2.1.1.i (page 13), we have (α ≥ σ n ) Γ 0 ⊢ a n : σ n (2). Then, we have the following derivation of Γ 0 ⊢ a n+1 : σ n+1 (3) in iML F :

Inst (α ≥ σ n ) Γ 0 ⊢ choose : ∀(α) α → α → α (α ≥ σ n ) Γ 0 ⊢ choose : α → α → α (2) (α ≥ σ n ) σ n ≤ α (α ≥ σ n ) Γ 0 ⊢ a n : α Inst (α ≥ σ n ) Γ 0 ⊢ choose a n : α → α (3) Gen App
Hence, by induction judgement (1) holds for every integer n provided Γ 0 ⊢ a : σ holds. Observe that, by construction, we have Γ 0 ⊢ id : σ id (4), Γ 0 ⊢ comp : σ comp (5), and Γ 0 ⊢ ω: σ ω (6). Assume moreover that σ id ≤ σ. Using Rule iCon-AllLeft repeatedly, we obtain σ n id ≤ σ n . In particular,

σ n+1 id ≤ ∀(α ≥ σ n ) α → α (7). Let b be id n+1 . We have Γ ⊢ b : σ n+1 id , which gives Γ ⊢ b : ∀(α ≥ σ n ) α → α by Rule
Inst and (7). Using generalized Rule App ⋆ we have Γ 0 ⊢ b a n : σ n (8). As both σ ω and σ comp are instances of σ id , we may thus conclude that both applications b ω n and b comp n are typable in iML F . More importantly, the typing derivations of b are the same for both terms-only the typing of the arguments and final application differs. The key point here is that the instantiation of the type of b may be delayed as much as possible. This is possible only because of the expressiveness of types and of the instance relation of iML F .

In System F, both applications are typable as well, but unlike in iML F , the typing derivations of b are significantly different. In particular, each node of the typing derivation tree differs up to the leaves, i.e. up to the typing of the expression id. Indeed, the type applications required at each application node are always different in both derivations. We see that a single difference in the unannotated term occurring at an arbitrary depth in the argument of the application id n+1 ω n (compared to id n+1 comp n ) induces changes in the typing of the body of the function a n+1 up to depth n.

As explained above, this example can easily be read back with lists. More generally, it shows that when incrementally building a collection of objects in ML F , each intermediate collection may be kept as polymorphic as possible, since it can be seen as a collection of a less polymorphic values at any time and at no cost. In particular, a new element that is less polymorphic than the previous elements of the collection may later be added to the collection. By contrast, in System F, one must know the best common type of all the elements before collecting the very first one.

To wrap up the example, it follows that the expressions a n let defined as let x = id n+1 in let z = x ω n in x comp n for any n, and, as a particular case, the expression let x = choose id in let z = x ω in x comp are not typable in System F. They are all typable in iML F , indeed.

Notice that although F let is larger than iML F , it is not necessarily better: while a n let is also typable in F let its typing derivation in F let is still problematic as the typing derivation for id contains two similar sub-derivations specialized for ω and comp, respectively, and joined with ∧ rather than a principal typing derivation independent of further applications, as could be done in iML F . The analysis of the open world modular problem described by a n when n increases is more informative about modularity than that of the closed expression a n let . Remark also that a n λ defined as app (λ(x) let z = x ω n in x comp n ) id n+1 does not typecheck in iML F , as the argument id n+1 must be assigned a type scheme and not a type. However, this example typechecks in Full ML F .

In summary, the main benefit of iML F over System F is that its types are more principal, so that typing derivations of iML F are more modular than typing derivations in System F. This is a key for the design of eML F that permits simple type inference. In fact, many modularity properties of iML F are kept in eML F (see type preserving transformations in §4.5).

eML F , Church-style ML F

In this section, we step on modular typechecking properties of iML F to design a version with optional type annotations, called eML F , that has a clear and intuitive specification of where and when to put type annotations. After a presentation of eML F types ( §4.1) and relations between them, we introduce terms, typing rules and show type safety ( §4.2) by translation of well-typed programs into iML F . We also exhibit a translation of System F into eML F that shows the intrinsic expressiveness of eML F and its very low demand on the amount of explicit type information ( §4.3). We show that eML F is a conservative extension to ML ( §4.4). Finally, we present a few useful program transformations that are type preserving in eML F ( §4.5).

Specifying where and when to put type annotations

In iML F , no type annotation is ever given. As a consequence, type inference is undecidable, just like in implicit System F. In order to make type inference decidable, we need some annotations to be mandatory. Our guideline is:

Only function parameters that are used polymorphically need an annotation.

This implies that types of annotated arguments are distinguishable from those of unannotated arguments. The solution is to have two different ways of representing a given type: one for explicit type information and another one for inferred type information. Unlike previous works, no explicit coercion is however needed to cast the former into the latter. Types that are explicitly introduced with type annotations are represented directly with a type scheme σ, as usual. On the contrary, types that have been inferred are represented indirectly via a variable α that is rigidly bound to a type scheme σ in the prefix. This means that α stands for the type σ, but α may not be freely replaced by σ or an instance of σ. Still, values of type α can be merged with other values of type σ, by "weakening them to the abstract type α"-and not conversely. This operation, called abstraction and written ⊏ -, plays a crucial role with respect to type inference. The converse relation, implicitly recasting an abstract variable α to its bound σ is not permitted, as it would allow-and hence force-type inference to guess (impredicative) polymorphic types and, as a result, make it undecidable. However, as this operation is always sound, it may be performed explicitly via a type annotation.

Types, prefixes, and type relations

We remind the definition of types and prefixes below, so as to make this section self-contained:

τ ∈ T e ::= α | τ → τ eML F types σ ∈ S e ::= τ | ∀(q) σ | ⊥ eML F type schemes q ∈ Q e ::= α ≥ σ | α ⇒ ρ eML F bindings ρ ∈ R e ::= τ | ∀(α ≥ ⊥) ρ | ∀(α ⇒ ρ) ρ F-like type schemes
As in ML, monotypes are simple types, for the purpose of type inference. This contrasts with System F or iML F , for which type inference is not considered. We use the symbol ⋄ as a meta-variable that denotes either ≥ or ⇒. For example, (α ⋄ σ) stands for either (α ⇒ σ) or (α ≥ σ), which are called rigid (resp. flexible) bindings. We also say that α is rigidly (resp. flexibly) bound. A prefix that contains only rigid bindings is called rigid. The rigid domain of a prefix Q, written dom = (Q), is the set of α such that α is rigidly bound in Q.

Notice that eML F types do not form a superset of iML F types, since for type inference purposes, they cannot have quantifiers. This may be surprising. However, all of iML F types have a counterpart in eML F (as implied by Theorem 4). For instance, the iML F type (∀(α 1 ) τ 1 ) → (∀(α 2 ) τ 2 ) is not an eML F type. However, it can be represented as the eML F type ∀(β 1 ⇒ σ 1 , β 2 ⇒ σ 2 ) β 1 → β 2 via extra rigid bindings. In fact, eML F types are more precise as there may be several types of eML F mapped to the same iML F type. This refinement of types is used in eML F to distinguish polymorphism that is given from polymorphism that is assumed.

Inert types I e . A type is inert if it is of the form ∀(Q) τ , where τ / ∈ ϑ and Q is rigid. The set of inert types is written I e . This definition is indeed the counterpart of inert types I i in iML F .

INRIA

-FlexLeft (Q) σ 1 R σ 2 (Q) ∀(α ≥ σ 1 ) σ R ∀(α ≥ σ 2 ) σ eCon-AllLeft (Q) σ 1 R σ 2 (Q) ∀(α ⋄ σ 1 ) σ R ∀(α ⋄ σ 2 ) σ eCon-AllRight (Q, α ⋄ σ) σ 1 R σ 2 (Q) ∀(α ⋄ σ) σ 1 R ∀(α ⋄ σ) σ 2 Figure 10: Type Equivalence in eML F . eEqu-Comm α 1 / ∈ ftv(σ 2 ) α 2 / ∈ ftv(σ 1 ) (Q) ∀(α 1 ⋄ 1 σ 1 ) ∀(α 2 ⋄ 2 σ 2 ) σ ≡ ∀(α 2 ⋄ 2 σ 2 ) ∀(α 1 ⋄ 1 σ 1 ) σ eEqu-Free α / ∈ ftv(σ) (Q) ∀(α ⋄ σ ′ ) σ ≡ σ eEqu-Mono (α ⋄ τ ) ∈ Q (Q) σ ≡ σ[τ /α] eEqu-Var (Q) ∀(α ⋄ σ) α ≡ σ eEqu-Inert σ ∈ I e (Q) ∀(α ≥ σ) σ ′ ≡ ∀(α ⇒ σ) σ ′
Relations between types. The equivalence and instance relations in iML F are adapted to eML F to deal with rigid bindings. As explained earlier 2.3, type equivalence ⊏ -⊐in iML F is too large to permit type inference and has been split into two inverse relations: abstraction ⊏and revelation ⊐ -. More precisely, type equivalence ⊏ -⊐in iML F corresponds to the transitive closure of ⊏ -∪ ⊐ -, while type equivalence ≡ in eML F is ⊏ -∩ ⊐ -. Moreover, ⊏is a subrelation of type instance, and may be left implicit in programs. Conversely, uses of ⊐must be made explicit, via type annotations.

We now present the equivalence, abstraction, and instance relations formally and in this order, from the smaller to the larger relations, as their definitions depend on these inclusions. Rules of Figure 10 are straightforward adaptations of those on Figure 6. The only difference is the replacement of single ≥ bound in iML F by the two possible bounds ≥ or ⇒ in eML F . Rule iEqu-Inert is split into two rules : eEqu-Mono inlines directly monotypes, whereas eEqu-Inert uses a rigid binding as an alias for an inert type σ (since direct substitution would not be possible in general).

We remind that ϑ is the set of type variables. We write V for the set of type schemes that are ≡-equivalent to a variable under the empty prefix. In fact, it is convenient to have a notation for the top-most structure of a type scheme.

Definition 4.1.3 (Head) The head of a type scheme σ is the symbol or variable, written head(σ), defined inductively as follows:

head(α) △ = α head(τ 1 → τ 2 ) △ = → head(⊥) △ = ⊥ head(∀(α ⋄ σ 1 ) σ 2 ) △ = head(σ 1 ), if head(σ 2 ) = α head(σ 2 ), otherwise
The head of a type scheme is preserved by equivalence under an empty prefix. Hence, the heads of all elements of V are type variables. We can show the converse-a type scheme σ, the head of which is a type variable, is in V-by an easy structural induction on σ. Hence, V is also the set {σ ∈ S | head(σ) ∈ ϑ} of type schemes the head of which are type variables. Rigid bindings are used to abstract explicit type schemes as implicit ones, by storing and sharing their definition via the prefix. The abstraction relation ⊏describes whenever a type scheme is more abstract than another one.

-Equiv (Q) σ 1 ≡ σ 2 (Q) σ 1 ⊏ -♯ σ 2 eAbs-Hyp (α ⇒ σ) ∈ Q (Q) σ ⊏ -α eAbs-Left (Q) σ 1 ⊏ -♯ σ 2 (Q) ∀(α ≥ σ 1 ) σ ′ ⊏ -♯ ∀(α ≥ σ 2 ) σ ′ eAbs-SharpLeft (Q) σ 1 ⊏ -σ 2 σ ′ / ∈ V (Q) ∀(α ⇒ σ 1 ) σ ′ ⊏ -♯ ∀(α ⇒ σ 2 ) σ ′ eAbs-SharpDrop (Q) σ 1 ⊏ -♯ σ 2 (Q) σ 1 ⊏ -σ 2
To explain abstraction, we introduce type scheme contexts, written S, as a type scheme with a single hole " • ", which may be defined by the following BNF grammar:

S ::= • | ∀(α ⋄ S) σ | ∀(α ⋄ σ) S
Abstraction is essentially structural, except for the key axiom that retrieves an assumption from the prefix (Rule eAbs-Hyp of Figure 11). However, a peculiarity of abstraction is that it is congruent only in all contexts ending with a true rigid binding, that is, type scheme contexts of the form ∀(α ⇒ • ) σ where σ is not equivalent to α. This condition is ensured by the stronger requirement σ / ∈ V of Rule eAbs-SharpLeft. Omitting the condition would allow pathological contexts such as ∀(β ≥ ∀(α ⇒ • ) α) τ , which are equivalent to ∀(β ≥ • ) τ . In particular, this would allow to conclude (Q)

∀(α ≥ σ 1 ) τ ⊏ -∀(α ≥ σ 2 ) τ from (Q) σ 1 ⊏ -σ 2 . For example, we would have (α⇒σ) ∀(β≥σ) τ ⊏ -∀(β≥α) τ , which implies ∀(α⇒σ) ∀(β≥σ) τ ⊏ -∀(α⇒σ) ∀(β≥α) τ , i.e. ∀(α ⇒ σ) ∀(β ≥ σ) τ ⊏ -∀(α ⇒ σ) τ [α/β],
by Rule eCon-AllRight. However, this is unsound with respect to its counter-part in ≤. To see this, take σ id for σ and β → α for τ . We would have

∀(α ⇒ σ id ) ∀(β ≥ σ id ) β → α ⊏ -∀(α ⇒ σ id ) α → α in eML F while ∀(β ≥ σ id ) σ id → β ≡ σ id → σ id does not hold in iML F . This is indeed incorrect, as it would allow the other direction ∀(α ⇒ σ id ) α → α ⊐ -∀(α ⇒ σ id ) ∀(β ≥ σ id ) β → α
to be used explicitly via an annotation, and so make (ω † : σ id ) ω † well-typed, which is of course incorrect as its evaluation loops. (Perhaps, another more intuitive example using primitive integers is (ω † : σ id ) succ.)

Intuitively, a rigid binding behaves as a protection that prevents the underlying type from ever being instantiated and, as a consequence, allows it to be abstracted. Technically, we need to keep track of protected abstractions, as only those can be used in unprotected flexible contexts. For that purpose, we use an auxiliary relation ⊏ -♯ , called protected abstraction, that is recursively defined with the (unprotected) abstraction relation ⊏ -. Rules may be read by first ignoring the difference between ⊏and ⊏ -♯ , then realizing that the distinction only prevents uses of eAbs-Hyp in pathological contexts for the reason explained above.

In fact, an alternative presentation is to remove Rule eEqu-Inert from the equivalence, and instead add a rule eAbs-Inert

eAbs-Inert σ ∈ I e (Q) ∀(α ≥ σ) σ ′ ⊏ -♯ ∀(α ⇒ σ) σ ′
This only slightly weakens the equivalence relation (inert types can then only be changed from flexible to rigid bound and not conversely). It changes the set of types a program has, but does not change the set of typable programs. The advantage of this alternate presentation is a simplification of equivalence which then only deals with commutation and removal of useless binders and inlining of monomorphic nodes. It also seems more natural in the graphical presentation of ML F (Yakobowski, 2008)-as all other operations on inert types must remain part of abstraction. However, we prefer here to stay with the (slightly) larger equivalence relation.

Whereas the abstraction relation ⊏can abstract a type scheme into a variable (see Rule eAbs-Hyp), the protected abstraction ⊏ -♯ cannot do the same, except in degenerate cases:

Lemma 4.1.5 If (Q) σ 1 ⊏ -♯ σ 2 and either σ 1 ∈ V or σ 2 ∈ V, then (Q) σ 1 ≡ σ 2 . INRIA Figure 12: Type Instance in eML F . eIns-Abstract (Q) σ 1 ⊏ -σ 2 (Q) σ 1 ⊑ σ 2 eIns-Hyp (α ≥ σ) ∈ Q (Q) σ ⊑ α eIns-Bot (Q) ⊥ ⊑ σ eIns-Rigid (Q) ∀(α ≥ ρ) σ ′ ⊑ ∀(α ⇒ ρ) σ ′
The instance relation differs from the one of iML F in only two minor ways. Firstly, it extends not only the equivalence but also the abstraction relation. Secondly, Rule iIns-Subst, which would no longer be wellformed, has been replaced by eIns-Rigid, introducing a rigid binding instead of performing the substitution in the conclusion. Other rules in Figure 12 are directly taken from those of iML F (Figure 7). The next lemma shows that instantiating (and a fortiori abstracting) a type τ has no effect up to equivalence, in contrast with abstraction of type schemes.

Lemma 4.1.7 For any type τ and type scheme σ, if (Q) τ ⊑ σ holds, then (Q) τ ≡ σ. Besides, there exists a type τ ′ such that (∅) σ ≡ τ ′ .

Soundness of instance and abstraction relations

The type soundness of eML F is shown below by a translation of well-typed eML F programs into well-typed iML F ones, which in turn requires a translation of types and relations on types.

Trivial bindings such as (β ≥ α) often lead to pathological cases, as they are just redirections. As a consequence, we often need to consider type schemes of V in a special way. While we write σ ∈ V (or σ ≡ β when the identifier β is meaningful) for conciseness and clarity, this can always be understood-and computed-as head(σ) ∈ ϑ (or head(σ) = β). Definition 4.1.8 (Type projection) The projection of an eML F type into an iML F type is defined as follows:

τ △ = τ ⊥ △ = ⊥ ∀(α ⇒ σ 1 ) σ 2 △ = σ 2 [ σ 1 /α] ∀(α ≥ σ 1 ) σ 2 △ = σ 2 [β/α] if σ 1 ≡ β ∀(α ≥ σ 1 ) σ 2 if σ 1 / ∈ V
The projection of a monotype τ is τ itself and the projection of ⊥ is ⊥. A binding (α ⇒ σ 1 ) is translated to a substitution [ σ 1 /α], which is well-formed as σ 1 is an F-like type. A binding (α ≥ σ 1 ) is translated to (α ≥ σ 1 ), unless it is a trivial one, in which case the corresponding substitution is performed. An important property of the projection is, intuitively, that the projection of a type that is not itself a type variable never contains exposed type variables (defined in §3.3.6).

Lemma 4.1.9 The set of exposed type variables of σ is included in the singleton {head(σ)}.

Whereas the projection of an eML F type is an iML F type, the projection of an eML F prefix Q is a pair composed of an iML F prefix that corresponds to flexible bindings of Q and a substitution that captures the rigid bindings of Q. Special care is again needed for trivial bindings.

Definition 4.1.10 (Prefix projection) The projection of a prefix Q is a pair (Q, θ), defined inductively as follows:

∅ △ = (∅, id) Q = (Q ′ , θ) (Q, α ⇒ σ) △ = (Q ′ , θ • [ σ /α]) Q = (Q ′ , θ) σ / ∈ V Q, (α ≥ σ) △ = ((Q ′ , α ≥ θ σ ), θ) Q = (Q ′ , θ) σ ≡ β Q, (α ≥ σ) △ = (Q ′ , θ • [β/α]) RR n°6228
The following lemma states that type equivalence, type abstraction, and type instance relation are all preserved by projections into iML F .

Lemma 4.1.11 Let (Q ′ , θ) be Q . We have the following implications i)

If (Q) σ 1 ≡ σ 2 , then (Q ′ ) θ σ 1 ⊏ -⊐ -θ σ 2 . ii) If (Q) σ 1 ⊏ -σ 2 , then (Q ′ ) θ σ 1 ⊏ -⊐ -θ σ 2 . iii) If (Q) σ 1 ⊑ σ 2 , then (Q ′ ) θ σ 1 ≤ θ σ 2 .
(Proof p. 58)

Properties 4.1.11.ii and 4.1.14.i show that the relations ⊏ -⊐and (⊏ -∪ ⊐ -) * are in correspondence. They were also used indirectly to show Property 4.1.11.iii. Only Property 4.1.11.iii is further used, namely to show the close correspondence between iML F and eML F .

Completeness of instance and abstraction relations

We may conversely show that type instance and type abstraction in eML F capture no more than type instance and type equivalence in iML F . Let us first introduce a translation from iML F types to eML F ones, written σ , defined inductively as follows:

α △ = α ⊥ △ = ⊥ ∀(α ≥ σ) σ ′ △ = ∀(α ≥ σ ) σ ′ τ 1 → τ 2 △ = ∀(α 1 ⇒ τ 1 , α 2 ⇒ τ 2 ) α 1 → α 2
The translation of variables, ⊥, and flexible bindings are by a direct mapping. The translation of an arrow type τ 1 → τ 2 uses auxiliary bindings (α 1 ⇒ τ 1 , α 2 ⇒ τ 2 ), since τ 1 and τ 2 are guaranteed to be ρ-types, but not necessarily monotypes. In case they are monotypes, the extra indirection is not problematic, as it can always be eliminated by type-equivalence in eML F . The translation of an iML F binding (α ≥ σ) is a binding (α ⋄ σ ) that is rigid if and only if σ is equivalent to an inert type. Formally,

(α ≥ σ) = (α ⇒ σ ) if there exists τ ∈ I i such that (∅) σ ⊏ -⊐ -τ (α ≥ σ ) otherwise
Checking if a type scheme σ is equivalent to an inert type can be performed quite easily, for example by taking normal forms-see Le Botlan ( 2004) for details. The translation of a prefix Q is the pointwise translation of its bindings.

As a preliminary result, we show that inert substitution in iML F is captured by the symmetric closure of abstraction in eML F : Lemma 4.1.12 Let σ be an iML F type scheme and Q be an iML F prefix such that (α

≥ σ ′ ) ∈ Q with (∅) σ ′ (⊏ -♯ ∪ ⊐ -♯ ) * τ and τ ∈ I i . Then, we have ( Q ) σ (⊏ -♯ ∪ ⊐ -♯ ) * σ[τ /α] in eML F . (Proof p. 59)
Lemma 4.1.13 Let τ be an iML F type, σ be an iML F type scheme, and Q an eML F prefix. Then, we have

(Q) ∀(α ⇒ τ ) σ (⊏ -♯ ∪ ⊐ -♯ ) * σ[τ /α] in eML F .
We may now show that type instance and type equivalence in iML F map to type instance and the symmetric closure of type abstraction in eML F .

Lemma 4.1.14 i) If (Q) σ 1 ⊏ -⊐ -σ 2 , then ( Q ) σ 1 (⊏ -♯ ∪ ⊐ -♯ ) * σ 2 . ii) If (Q) σ 1 ≤ σ 2 , then ( Q ) σ 1 (⊑ ∪ ⊐ -) * σ 2 .
(Proof p. 59)

Terms, typing rules, and type soundness

Terms of eML F are those of iML F extended with a new primitive construction for type annotations (a : ∃ (ᾱ) σ).

Notice that the existential ∃ (ᾱ) σ is not an existential type, but a syntactic notation for introducing metavariables ᾱ standing for some types σ′ appearing in σ to be inferred, as can be done in the language ML (Pottier and Rémy 2003, page 102;Jones and Shields 2004a). That is, the BNF grammar of expressions of eML F is:

a ::= x | λ(x) a | a 1 a 2 | let x = a 1 in a 2 Expressions of iML F (a : ∃ (ᾱ) σ) Type annotations INRIA Figure 13: eML F typing rules Var Fun App Gen Let Inst (Q) Γ ⊢ a : σ (Q) σ ⊑ σ ′ (Q) Γ ⊢ a : σ ′ Annot ᾱ ⊆ dom(Q) (Q) Γ ⊢ a : σ ′ (Q) σ ⊏ -σ ′ (Q) Γ ⊢ (a : ∃ (ᾱ) σ) : σ
The typing rules of eML F , given in Figure 13, include all rules from the generic system G(T e , S e , Q e , ⊑) and a new rule for type annotations. Notice, that the generic rule Inst is specialized, accordingly, using the relation ⊑ for type instance. Rule Annot is thus the only interesting rule in eML F . The existentially quantified variables ᾱ in annotations are used to allow annotations to partially specify the type of the expression they annotate: their bounds are left unspecified (equivalently ᾱ could be given a flexible bottom bound in the annotation) and thus must be inferred. Free type variables of σ must all be listed in ᾱ, so that the annotation ∃ (ᾱ) σ is itself closed. Variables ᾱ are required to appear in the prefix Q, as specified by the premise ᾱ ⊆ dom(Q). The judgment (Q) σ ⊏σ ′ allows to reveal σ, but no more. In particular, the bounds assigned to ᾱ are shared between σ ′ and σ, which prevents from revealing more than explicitly specified in σ through implicit instantiation of its free type variables ᾱ. As a particular case, annotating an expression with ∃ (α) α is useless. Conversely, all inner bound variables of σ must be matched exactly-up to abstraction. Syntactic sugar. When σ is closed, we may simply write the annotation σ instead of ∃ (∅) σ. We so recover the simplified rule given in the introduction ( § 2.3, page 18). In fact, by abuse of notation, we could also write (a : σ) when σ is not closed to mean (a : ∃ (ftv(σ)) σ), but we prefer to remain more explicit about bound variables.

We also see abstractions λ(x : σ) a as syntactic sugar for λ(x) let x = (x : σ) in a. Rebinding x to its annotated version (x : σ) avoids repeating the annotation on each occurrence of x in a. The effect is that λ(x : σ) a is typed as if it were λ(x) a[(x : σ)/x], but our syntactic sugar is more local. The annotated abstraction may also be typed directly, with the following derivable typing rule:

Fun ⋆ (Q) Γ, x : ρ ⊢ a : τ ᾱ ⊆ dom(Q) (Q) Γ ⊢ λ(x : ∃ (ᾱ) ρ) a : ∀(β ⇒ ρ) β → τ
In practice, most uses of annotations are actually in abstractions. The reason not to make annotated abstraction the primitive form and the annotations the derived form is that annotations are much simpler to deal with, technically.

Furthermore, for F-like type annotations, (a : ρ) can just be seen as the application of a retyping primitive function (ρ) to the expression a. In Full ML F , all annotations can be treated as such. We could restrict eML F to F-like annotations. However, because types are stratified in Shallow ML F , we would then not reach all type annotations and eML F would loose its close correspondence with iML F .

Example. We first show that the (unannotated) identity function λ(x) x is typable with type ∀(α ⇒ ρ) α → α for any F-like type scheme ρ, which type would be written ρ → ρ in iML F . Notice that ρ may be polymorphic. In the following, we write σ id for ∀(α) α → α.

Inst Gen Fun Var (α ≥ ⊥) x : α ⊢ x : α (α ≥ ⊥) ∅ ⊢ λ(x) x : α → α (∅) ∅ ⊢ λ(x) x : σ id (∅) σ id ⊑ ∀(α ⇒ ρ) α → α (∅) ∅ ⊢ λ(x) x : ∀(α ⇒ ρ) α → α
Notice that a more direct derivation is also possible:

Gen Fun Var (α ⇒ ρ) x : α ⊢ x : α (α ⇒ ρ) ∅ ⊢ λ(x) x : α → α (∅) ∅ ⊢ λ(x) x : ∀(α ⇒ ρ) α → α
For comparison, here is a derivation when the argument is annotated.

Gen Fun ⋆ Inst Var (α ⇒ ρ) x : ρ ⊢ x : ρ (α ⇒ ρ) ρ ⊏ -α (α ⇒ ρ) ρ ⊑ α (α ⇒ ρ) x : ρ ⊢ x : α (α ⇒ ρ) ∅ ⊢ λ(x : ρ) x : ∀(β ⇒ ρ) β → α (∅) ∅ ⊢ λ(x : ρ) x : ∀(α ⇒ ρ) ∀(β ⇒ ρ) β → α
Here, the variable x has a polymorphic F-like type ρ, which is directly accessible with Rule Var. In the previous derivation, x had only a type α, which was bound to ρ in the prefix, hence not directly available. This is a crucial difference between the two derivations. Indeed, in the latter derivation, the polymorphism can be instantiated, so that for example λ(x : σ id ) x x is typable. On the contrary, we will show below ( §4.3) that λ(x) x x is not typable when the type annotation is missing. Another important remark is the use of abstraction (and Rule Inst) to hide the polymorphic type ρ of x as the abstract type α (rigidly bound to ρ in the prefix). This is to prepare for rule Fun ⋆ that requires the codomain of the type of λ(x : ρ) x to be a monotype and not a polytype ρ.

To see the role of existential quantification in type annotations, compare the two expressions λ(x : ∃ (β) ρ) x and λ(x : ∀(β) ρ) x where ρ is ∀(α) α → β → α-with a free single type variable β. Their respective types are

∀(β) ∀(γ ⇒ ρ) ∀(γ ′ ⇒ ρ) γ → γ ′ and ∀(γ ⇒ ∀(β) ρ) ∀(γ ′ ⇒ ∀(β) ρ) γ → γ ′ .
In the later case, the annotation requires the argument to be polymorphic in β-hence the result is also polymorphic in β. Conversely, in the former case, β is shared between the argument type and the result type and cannot be polymorphic within the expression, but only generalized afterward. Less polymorphism is required on the argument and so less polymorphism is claimed on the result-namely just as much as promised on the argument.

Derivable rules. Rules App ⋆ and UnGen ⋆ (defined page 24) remains admissible in eML F -with types and type schemes now taken in eML F , of course.

Recursion. Viewing recursion as a fixed point combinator means that the identifier f of let rec f = λ(x) a 1 in a 2 is treated as the argument of a function and must have a ρ type. Then, f needs an annotation if it is used polymorphically in the body of a 1 . This treatment of recursion allows for polymorphic recursion but with explicit type annotations.

Using a primitive construct for recursion would allow f to be assigned a type scheme instead of a type, via an explicit annotation. Omitting the annotation would amount to inferring polymorphic recursion, which would be undecidable in ML F , as it is already undecidable in ML.

Expressiveness

We show that eML F and iML F are in close correspondence, and thus exactly as expressive. Dropping type annotations directly maps eML F programs to iML F ones.

Theorem 3 Assume eML F :: (Q) Γ ⊢ a : σ holds. Let a ′ be the erasure of a and (Q ′ , θ) be Q . Then, iML F ::

(Q ′ ) θ(Γ) ⊢ a ′ : θ( σ ) holds. (Proof p. 59)
Conversely, all iML F programs can always be mapped to eML F ones by inserting explicit type annotations.

Theorem 4 If iML F :: (Q) Γ ⊢ a : σ holds, then there exists a term a ′ , such that a is a type-erasure of a ′ and eML F :: ( Q ) Γ ⊢ a ′ : σ holds.

(Proof p. 60)
Noticeably, the translation of an iML F program is based on its typing derivation. It introduces a type annotation on every λ-abstraction, and possibly several ones on type instances and generalizations.

INRIA

Type soundness

Type soundness is a corollary of Theorem 3, which ensures that eML F is as safe as iML F , and Theorem 2, which states type soundness of iML F .

Translating System F into eML F

The composition of theorems 2 and 4 states that there is a mapping of System-F terms to eML F terms that proceeds only by insertion of well-chosen type annotations. Those theorems do not tell us where and what annotations to insert. However, their proofs are constructive-given a type derivation of the input term, or equivalently, an explicitly typed input term. That is, we could have used the typed derivation given as input to explicitly produce a type derivation in eML F as output.

However, the resulting term would contain many duplicated or scattered type annotations, unless we change the proof and show stronger (and difficult) lemmas that typed derivations could be rearranged in certain ways, so that for instance, type annotations can always be moved to function parameters.

Instead, we propose a direct translation of explicitly typed System-F programs to eML F that keep (actually translate) the type annotations on λ-abstractions, and throws away all type abstractions and type applications. Therefore, it returns an eML F program that contains at most as much, and in general fewer, type information than the original System-F term.

The first step of the translation is the translation of types. Let us explain an important design choice of this translation, informally. Rigid bindings are interpreted as substitutions (Definition 4.1.8). For example,

∀(α ⇒ σ id ) α → α (1) is interpreted as the F-type σ id → σ id . However, ∀(α 1 ⇒ σ id , α 2 ⇒ σ id ) α 1 → α 2 (2)
is also interpreted likewise. Therefore, there are two candidates for the converse translation of σ id → σ id into eML F , namely (1) and ( 2). Observe that ( 2) is more general than (1) in eML F (the latter is an instance of the former). Taking ( 2) is the approach chosen in § 4.1 to translate iML F types. Maybe surprisingly, we choose (1) to be the translation of σ id → σ id . That is, we always share similar bindings as much as possible, as formalized in Definition 4.3.3 below. The opposite choice, which would associate (2) to the translation of σ id → σ id , is also possible. Although this alternative is perhaps more elegant, its correctness proof is longer and much more involved [START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]. We present the first approach here for the sake of simplicity. Despite this choice, this section remains the most technical part of the paper. It happens that proving the soundness of the translation from System F to eML F is subtle and needs meticulous instrumentation. Let us explain why.

A single System-F type, such as σ id → σ id , corresponds to possibly many types in eML F , as a result of the inlining of rigid bindings in System F. Consequently, eML F types are more discriminatory, i.e. contain more information, than System-F types, which is crucial for permitting type inference. The downside is that, given a typing derivation in System F, we have to reconstruct the missing information and show that it is consistent with eML F typing rules. The purpose of the instrumentation is exactly to reconstruct and trace this information in a safe way.

As the rest of the paper does not depend on the technical details of this section, the user may skip them and directly jump to theorems 6 and 7 at the end of this section.

Auxiliary definitions

We first define a few operators that are used to translate F-types into eML F -types. The translation introduces rigid bindings and unconstrained flexible bindings, but never uses constrained flexible bindings.

As a first step, we translate an F-type into a pair of a prefix and a variable used as an entry point into that prefix. Following our design choice (exposed above), prefixes are maintained in shared form.

Definition 4.3.1 A prefix Q is shared when for all σ, (α 1 ⇒ σ) ∈ Q and (α 2 ⇒ σ) ∈ Q imply α 1 = α 2 .
Sharing is purely syntactic, based on type equality. While it would have been more natural to define sharing up to equivalence, this would require more technical machinery-and at least to present an algorithm for testing equivalence (as, for instance, the one of Le Botlan ( 2004)). The syntactic definition suffices and is simpler.

As a result of sharing, the insertion of a new binding into a prefix depends on bindings that are already present. Insertion, which is defined next, maintains another invariant: prefixes are ordered in the sense that rigid bindings are inserted as far to the left as possible. For example, the prefix (α, β ⇒ γ → γ) is not ordered because the rigid bound of β does not depend on α. The ordered, equivalent prefix is (β ⇒γ → γ, α). Intuitively, ordering may move rigid bindings, but not flexible ones. This is a form of extrusion, which we enforce to ensure maximal sharing of rigid bounds. Indeed, this maximal sharing requires rigid bindings to have the wider possible scope. Formally, the bounds of a prefix Q, written bnds(Q), is the set of all σ such that there exists a binding (α ⇒ σ) in Q.

Definition 4.3.2 The insertion of a type scheme σ into a prefix Q at variable α, written Q α σ, is a prefix defined in the two following cases:

If (α ⇒ σ)∈ Q, then Q α σ is Q. If α /
∈ dom(Q) and σ / ∈ bnds(Q), then Q α σ is defined recursively as follows:

• ∅ α σ is (α ⇒ σ), • (Q ′′ Q ′ ) α σ is (Q ′′ α σ)Q ′ if ftv(σ) # dom(Q ′ ), • (Q ′ , β ′ ⋄ σ ′ ) α σ is (Q ′ , β ′ ⋄ σ ′ , α ⇒ σ) if β ′ ∈ ftv(σ).
We write Q α σ for the pair (Q α σ), α.

Notice that insertion is partial. For example, (β ⇒ σ) α σ is undefined. When defined, it returns the original prefix either exactly or with the binding α = σ inserted "at the right place" while preserving the ordering of other bindings.

We define an algorithm that computes the translation of an F-type t in two steps. We first define a relation that takes a prefix Q and the type t as input and returns a pair of a new prefix Q ′ that extends Q and a type variable α as output. This is written (Q) t : (Q ′ , α) (read "under prefix Q, a translation of t is the pair (Q ′ , α)"). We then define the translation of t, written t as a set of eML F types.

The use of an auxiliary relation instead of simply a function is to capture non-determinism that results from the choice of fresh variables during the translation. Lemma 4.3.6 below shows that a given input yields outputs that are similar, up to renaming.

Below, we use the notation (Q) t : Q ′ σ (without any variable on ) to mean that there exists α such that Q ′ α σ is defined and (Q) t : Q ′ α σ holds. This exposes the witness α in the relation (Q) t : (Q ′ , α) and so introduces a source of non-determinism in the definition-the only one. where Q and Q ′ are well-formed shared prefixes and t a type such that ftv(t) ∩ dom(Q ′ ) ⊆ dom(Q) satisfying the following rules:

(Q) α : (Q, α) (Q) t 1 : (Q 1 , α 1 ) (Q 1 ) t 2 : (Q 2 , α 2 ) (Q) t 1 → t 2 : Q 2 α 1 → α 2 (Qα) t : (Q 1 αQ 2 , β) (Q) ∀(α) t : Q 1 ∀(αQ 2 ) β
The restriction on the free type variables of t and the domains of the prefixes can always be satisfied by an appropriate choice of fresh variables. The only possible translation of a type variable α under prefix Q is the pair (Q, α), whether α belongs to dom(Q) or not. A translation of an arrow type t 1 → t 2 under Q is built using the translation (Q 1 , α 1 ) of t 1 under Q and (Q 2 , α 2 ) of t 2 under Q 1 . It is defined as the insertion of α 1 → α 2 into Q 2 . Finally, the translation of a quantified type ∀(α) t is built using the translation of t under Qα. Then, the resulting prefix is split into Q 1 and Q 2 and the result is the insertion of ∀(αQ 2 ) β into Q 1 . Since Q 1 αQ 2 is ordered, all the bindings of Q 2 actually depends on α, possibly indirectly. This means that the prefix Q 2 to appear in the quantification (αQ 2 ) is as small as possible.

The inclusion of prefixes, written

Q ⊆ Q ′ , means that Q ′ is obtained from Q by none or several insertions. When (Q) t : (Q ′ , α) holds, we have Q ⊆ Q ′ and ftv(Q ′ ) ⊆ ftv(Q) ∪ ftv(t). (This easily follows from the observation that Qα ⊆ Q 1 αQ 2 implies Q ⊆ Q 1 .) Another invariant of the definition is that all bindings that are in Q ′ but not in Q are rigid.
Definition 4.3.4 (Translation of types and prefixes) The translation of an F-type t, written t is the set of all eML F type schemes ∀(Q) α such that there exists a rigid, shared prefix Q ′ with domain disjoint from ftv(t) verifying (Q ′ ) t : (Q, α). The translation of an F-typing environment A, written A , is the set of typing environments Γ that maps each x in dom(A) to some type scheme in A(x) .

The prefix Q must actually be rigid and shared. This follows from definition of the translation relation and the fact that Q ′ is itself rigid.

Note that σ id is both a type of System F and of eML F . We have (∅) σ id : (β ⇒ σ id ), β. We then have

(β ⇒ σ id ) σ id → σ id : (β ⇒ σ id ) (γ ⇒ β → β), γ.
We shall see below that all type schemes in the translation of an F-type are in fact equivalent (Corollary 4.3.10), and similarly for the translation of typing environments. We call rigid an eML F type scheme that is in the translation of an F-type.

INRIA

Auxiliary results. We now establish several properties about the translation algorithm that will be used to prove the main result of this section, Lemma 5, from which theorems 6 and 7-two variants of the same result-immediately follow. All of these properties address the following informal question: How can the output vary for some small changes to the input? For instance, the following lemmas answer this question in particular cases:

• Lemma 4.3.5 states that inputs and outputs can be consistently renamed.

• Lemma 4.3.6 characterizes non determinism: the outputs can be renamed while leaving the input unchanged provided that some capture-avoiding side conditions hold.

• Lemma 4.3.7 states a form of idempotence: i) the input may be replaced by the output (leaving the output unchanged); ii) once the input and output are equal, they may be extended simultaneously.

• Lemma 4.3.9 states that the relation is closed by equivalence.

• Lemma 4.3.12 characterizes the effect of applying a substitution to the input type: the output prefix must be substituted and shared again-along a sharing relation defined below.

• Lemma 4.3.13 states that when removing an unconstrained binding from the input, the bindings of the output may have to be reordered.

As mentioned above, given a prefix Q and a type t, the algorithm may return different results due to different choices of fresh variables. This is captured by saying that renamings preserve the translation.

Lemma 4.3.5 (Stability by renaming)

If (Q) t : (Q ′ , α) holds, then (φ(Q)) φ(t) : (φ(Q ′ ), φ(α)
) holds for any renaming φ.

Conversely, the choice of fresh variables is the only source of non-determinism, so that outputs for a single input are always equal up to renaming. Additionally, the renaming can be chosen to be invariant on any "fresh" set of variables I.

Lemma 4.3.6 (Determinism up to α-conversion) If (Q) t : (Q 1 , α 1 ) and (Q) t : (Q ′ 1 , α ′ 1 ), then for all finite set I disjoint from dom(Q 1 ) ∪ dom(Q ′ 1 ), there exists a renaming φ such that dom(φ) # dom(Q) ∪ ftv(t) ∪ I φ(Q 1 ) = Q ′ 1 φ(α 1 ) = α ′ 1 As a consequence, ∀(Q 1 ) α 1 is equal to ∀(Q ′ 1 ) α ′ 1 by α-conversion.
The translation is also stable by iteration: translating a type under a prefix already containing the bindings of the translation returns the same prefix.

Lemma 4.3.7 (Idempotence) If (∅) t : (Q, α), then (QQ ′ ) t : (QQ ′ , α) for any Q ′ such that QQ ′ is well-formed. (Proof p. 60)
The insertion of a type σ in a prefix Q (that is, Q σ) is defined so as to maximize sharing. The result depends on the initial prefix Q. Therefore, the translation of a type t under Q (that is, (Q) t ) also depends on Q. We wish to show that the translation of a single type under different initial prefixes yields comparable prefixes, up to some equivalence relation that we define now.

The equivalence relation on shared prefixes ≡ I is the smallest equivalence (reflexive, symmetric, and transitive) relation also satisfying the two following rules:

eSha-Free α / ∈ I ∪ dom(Q) ∪ ftv(Q) σ / ∈ bnds(Q) Q ≡ I (Q, α ⇒ σ) eSha-Comm α 1 / ∈ ftv(σ 2 ) α 2 / ∈ ftv(σ 1 ) (Q, α 1 ⇒ σ 1 , α 2 ⇒ σ 2 , Q ′ ) ≡ I (Q, α 2 ⇒ σ 2 , α 1 ⇒ σ 1 , Q ′ )
The superscript I is a finite set of type variables called the interface. Bindings of variables in I are "exposed" to equivalence. Rule eSha-Free allows the insertion (or removal) of bindings not in the interface I. Side conditions ensure that the prefix is kept well-formed and shared. Rule eSha-Comm allows the commutation of independent binders. Unsurprisingly, two types built with equivalent prefixes are equivalent.

Lemma 4.3.8 If Q 1 ≡ I Q 2 and ftv(σ) ⊆ I, then (Q) ∀(Q 1 ) σ ≡ ∀(Q 2 ) σ holds under any suitable Q.
(Q) Q 1 ----> φ Q 2 (Q) ∀(Q 1 ) τ ----> ∀(Q 2 ) φ(τ ) eTsh-Empty (Q) ∅ ----> id ∅ eTsh-Flex (Qα) Q 1 ----> φ Q 2 (Q) αQ 1 ----> φ αQ 2 eTsh-Subst (Q) σ ----> σ ′ (α ′ ⇒ σ ′ ) ∈ Q (Q) Q 1 [α ′ /α] ----> φ Q 2 (Q) (α ⇒ σ, Q 1 ) ----> φ•[α ′ /α] Q 2 eTsh-Context (Q) σ ----> σ ′ σ ′ / ∈ bnds(Q) (Q, α ⇒ σ ′ ) Q 1 ----> φ Q 2 (Q) (α ⇒ σ, Q 1 ) ----> φ (α ⇒ σ ′ , Q 2 )
Equivalent prefixes also yield equivalent translations. Informally, this may be illustrated by the commutative diagram below. The translation of t under two equivalent prefixes Q 1 and Q 2 , yields equivalent prefixes

Q ′ 1 and Q ′ 2 . Q 1 Q 2 Q ′ 1 Q ′ 2 (Q 2 ) t ≡ (Q 1 ) t ≡ Lemma 4.3.9 (Equiv) Let I be ftv(t). We assume that Q 1 is rigid and Q 1 ≡ I Q 2 holds. If (Q 1 ) t : (Q ′ 1 , α 1 ) and (Q 2 ) t : (Q ′ 2 , α 2
) hold, then there exist a set J and a renaming φ such that:

dom(φ) # I I ∪ {α 1 } ⊆ J Q ′ 1 ≡ J φ(Q ′ 2 ) φ(α 2 ) = α 1 (Proof p. 61)
Corollary 4.3.10 If σ 1 , σ 2 ∈ t , then (Q) σ 1 ≡ σ 2 under any suitable Q.

(Proof p. 64)

We now consider the effect of type instance on the translation. More precisely, substituting α by t ′ in a type t has an effect on sharing, in the sense that the translation of t[t ′ /α] is not only a substitution of the translation of t. For example, consider the type t equal to (σ id → α) → (σ id → σ id ). A valid translation of t under an empty prefix is (after harmless simplification)

∀(α 1 ⇒ σ id , α 2 ⇒ α 1 → α, α 3 ⇒ α 1 → α 1 ) α 2 → α 3 (1). Substituting α by σ id in t, we get t[σ id /α], that is, (σ id → σ id ) → (σ id → σ id ). A valid translation of the latter is ∀(α 1 ⇒ σ id , α 2 ⇒ α 1 → α 1 ) α 2 → α 2 (2).
We see that α 2 and α 3 have been merged. In order to transform (1) into (2), the substitution [α 1 /α] must be applied first, then similar bindings must be shared again (namely, α 2 and α 3 ).

To this end, we define an algorithm ----> φ that shares prefixes as much as possible. The subscript φ is a substitution that keeps track of sharing that has already been performed. In the example above, φ would be [α 2 /α 3 ]. The algorithm ----> is recursively defined as a set of (deterministic) inference rules given in Figure 14. The algorithm is written (Q) σ 1 ----> σ 2 for types, where Q and σ 1 are inputs and σ 2 in an output (Rule eTsh-

Types). It is written (Q) Q 1 ----> φ Q 2 for
prefixes, where Q and Q 1 are inputs and φ and Q 2 are outputs. As usual, the prefix Q may be omitted in

(Q) Q 1 ----> φ Q 2 or (Q) σ 1 ----> σ 2
when it is empty. Rules eTsh-Empty, eTsh-Flex, and eTsh-Context are context rules that do not perform any sharing. On the contrary, Rule eTsh-Subst detects and shares two similar bindings.

The next lemma describes properties of this algorithm.

Lemma 4.3.11 i) If (Q) Q 1 ----> φ Q 2 , then dom(φ) = dom = (Q 1 ) -dom(Q 2 ) and dom(Q 1 ) = dom(Q 2 ) ∪ dom(φ). ii) If (Q) Q 1 ----> φ Q 2 holds, then for any type σ closed under QQ 1 , we have (Q) ∀(Q 1 ) σ ⊏ -∀(Q 2 ) φ(σ).
Item i) is a technical invariant: the domain of Q 1 is the disjoint sum of the domain of Q 2 and the domain of φ. More precisely, the domain of φ is included in the rigid domain of Q 1 (which means that only rigid bindings are INRIA shared). Item ii) asserts that the sharing performed by the algorithm corresponds to abstraction at the type level.

(Proof p. 64)

The following lemma, composed of three properties, specifies the effect of a substitution ψ of the form [α/β] over a translation t . Property P-i is used in the proof of the following commutative diagram (Property P-ii):

Q 1 Q 2 Q ′ 1 Q ′ 2 ψ(t) ψ(Q ′ 1 ) ----> t ψ(Q 1 ) ---->
Moreover, the effect of ψ on the translation is equivalent to the substitution [t ′ /β], provided (Q ′ , α) is a translation of t ′ (Property P-iii).

Lemma 4.3.12 Let ψ be the substitution

[α/β]. We assume that the α is bound in Q. We say that Q is α-rigid if Q is rigid or of the form Q ′ , α ⋄ σ, Q ′′ with Q ′ rigid.
The following implications hold:

P-i ψ(Q) ----> φ Q ′ β = α ′ Q is α-rigid β / ∈ dom(Q) Q α ′ σ is defined φ • ψ(σ) ----> σ ′ ∃φ ′ such that ψ(Q α ′ σ) ----> φ ′ •φ Q ′ φ ′ •φ(α ′ ) σ ′ dom(φ ′ ) ⊆ {α ′ } P-ii Q 1 shared Q 1 is α 1 -rigid β / ∈ dom(Q ′ 1 ) ftv(t) # dom = (Q ′ 1 ) (Q 1 ) t : (Q ′ 1 , α 1 ) ψ(Q 1 ) ----> φ Q 2 ∃Q ′ 2 , α 2 , φ ′ s.t. (Q 2 ) ψ(t) : (Q ′ 2 , α 2 ) ψ(Q ′ 1 ) ----> φ ′ •φ Q ′ 2 φ ′ • φ • ψ(α 1 ) = α 2 P-iii (∅) t ′ : (Q ′ , α) (Q ′ ) ψ(t) : (Q ′ 2 , α 2 ) (Q ′ ) t[t ′ /β] : (Q ′ 2 , α 2 ) (Proof p. 64)
In the following lemma, we show that an unconstrained binding (here β) may be removed from the input prefix of the translation and only requires some reordering of binders in the output. To this end, we define the relation ≈ as the smallest equivalence relation on prefixes satisfying eSha-Comm. Noticeably,

Q ≈ Q ′ implies Q ≡ I Q ′ for any I.
Lemma 4.3.13 Let Q 1 and Q 2 be rigid prefixes. Let P and P ′ be two prefixes, each of which is either empty or starts with an unconstrained binding. Then, the following implication holds:

(Q 1 βQ 2 P ) t : (Q ′ 1 βQ ′ 2 P ′ , α) Q 1 Q 2 ≈ Q 3 ∃Q ′ 3 (Q 3 P ) t : (Q ′ 3 P ′ , α) ∧ Q ′ 1 Q ′ 2 ≈ Q ′ 3 (Proof p. 65)
We are finally equipped to show the correctness of the translation from System F into ML F . We shall use the two following derivable rules as short-cuts in the proof.

Lemma 4.3.14 The following rules are derivable:

Shift ⋆ Q ′ rigid (QQ ′ ) ∀(Q ′ ) σ ⊏ -σ Share ⋆ (QQ ′ ) ∀(Q ′ ) τ ⊑ τ
Theorem 5 If F :: Γ ′ ⊢ a : t holds, then there exists an expression a ′ with type erasure a and such that eML F :: (Q) Γ ⊢ a ′ : σ holds for any Γ ∈ Γ ′ , σ ∈ t and suitable prefix Q.

(Proof p. 66)

The main result follows as a corollary.

Theorem 6 Any term typable in implicit System F is typable in ML F by adding some type annotations on function arguments.

Noticing that type annotations on function arguments depend only on the type of the argument, and not on the rest of the typing derivation, a more precise statement is the following: Theorem 7 Any term typable in explicit System F is typable in ML F by dropping type abstractions and type applications and by translating type annotations.

Remarkably, all the System-F terms that differ only in their type abstractions and type applications are translated towards the same eML F program. Since every eML F program admits a principal type (this result is not shown in this paper, but has been shown for Full ML F as well as a small variant of eML F by Le Botlan ( 2004)), this type captures all the possible type abstractions and type applications of the term.

While the encoding of System F terms into eML F uses an annotation on every λ-abstraction, these annotations could in fact be omitted when the argument is not used polymorphically, as shown below by the embedding of ML into eML F .

Embedding ML into eML F

We show that eML F is a conservative extension to ML. That is, we consider ML raw terms. i.e. eML F terms that do not use type annotations, and show that well-typedness in ML implies well-typedness in eML F . Conversely, closed ML raw terms that are well-typed in eML F are also well-typed in ML.

ML types are a subset of F-types where quantification is allowed only at the outermost level.

The instance relation for ≤ ML has been defined in the introduction ( §2.1, page 12). We recall that it is composed of exactly all pairs of the form ∀(ᾱ) σ ≤ ML ∀( β) σ[τ / ᾱ]) with β # ftv(∀(ᾱ) σ). Notice that variables ᾱ may only be substituted by monotypes τ . The following chain of relations in eML F shows that ≤ ML is a subrelation of ⊑.

∀(ᾱ) σ = ∀(α 1 , .., α n ) σ by notation = ∀(α 1 ≥ ⊥, .., α n ≥ ⊥) σ by notation ≡ ∀( β) ∀(α 1 ≥ ⊥, .., α n ≥ ⊥) σ by eEqu-Free ⊑ ∀( β) ∀(α 1 ≥ τ 1 , .., α n ≥ τ n ) σ by eIns-Bot and context rule ⊑ ∀( β) ∀(α 1 ⇒ τ 1 , .., α n ⇒ τ n ) σ by eIns-Rigid ≡ ∀( β) σ[τ 1 /α 1 ]..[τ n /α n ] by eEqu-Mono = ∀( β) σ[τ / ᾱ]
by notation ML terms are in eML F . The typing rules of ML are exactly those of eML F , namely Var, Fun, App, Inst, Gen, Let without Annot, and of course, modulo the restriction to ML types and prefixes and the use of ≤ ML instead of ⊑ in rule Inst. Consequently, any typing derivation in ML is also a typing derivation in eML F (which is not a derivation of the most principal type in eML F , in general).

Theorem 8 Any term typable in ML is also typable in eML F .

Conversely, terms that are typable in eML F are not necessarily typable in ML. Indeed, eML F contains the full power of System F, but ML does not. However, given an unannotated term of eML F , it does also typecheck in ML.

Unannotated eML F terms are in ML We prove this by translating eML F typing derivations of unannotated terms into ML typing derivations in two steps. First, rigid bindings are removed from the initial derivation by "flexifying" the derivation (Definition 4.4.1). The result which contains only flexible types, is still a valid derivation (Lemma 4.4.3). Last, all quantifiers are extruded to the outermost level. The final derivation is still correct and it is a derivation in ML (Lemma 4.4.7).

Definition 4.4.1 eML F types that do not contain rigid bindings are said to be flexible. We say that a derivation is flexible if it does not contain any rigid binding in any type nor in any prefix appearing in the derivation. A judgment is flexible if it has a flexible derivation.

Let flex be the function defined on eML F types and prefixes that transforms every rigid binding into a flexible binding. For instance, flex

(∀(α ⇒ σ 1 , β ≥ σ 2 ) σ) is ∀(α ≥ flex (σ 1 ), β ≥ flex (σ 2 )) flex (σ).
The following lemma shows that flexifying an instance relation is indeed correct.

INRIA Lemma 4.4.2 i) If (Q) σ 1 ≡ σ 2 , then (flex (Q)) flex (σ 1 ) ≡ flex (σ 2 ) is flexible. ii) If (Q) σ 1 ⊏ -σ 2 , then (flex (Q)) flex (σ 1 ) ⊑ flex (σ 2 ) is flexible. iii) If (Q) σ 1 ⊑ σ 2 , then (flex (Q)) flex (σ 1 ) ⊑ flex (σ 2 ) is flexible. (Proof p. 67)
We lift the function flex to typing environments and to typing judgments in the natural way. This operation preserves typing judgments.

Lemma 4.4.3 For any unannotated term a, if (Q) Γ ⊢ a : σ holds in eML F , then so does flex ((Q) Γ ⊢ a : σ).

(Proof p. 67)

We recall a standard result of ML.

Lemma 4.4.4 If we have ∀(ᾱ) τ 1 ≤ ML ∀( β) τ 2 , then for any σ such that ftv(σ) # ᾱ ∪ β, we have

∀(ᾱ) σ[τ 1 /γ] ≤ ML ∀( β) σ[τ 2 /γ]
We now show how a flexible eML F type is transformed into an ML type by extrusion of quantifiers. We first transform prefixes. A flexible prefix is transformed into the pair of a set of quantifiers and a monotype substitution.

Definition 4.4.5 The ML approximation of a flexible prefix Q, written Q , and the ML approximation of a flexible type σ, written σ , are defined recursively as follows (we overload the notation used for System F, which should not raise any ambiguity):

∅ = (∅, id) Q = (ᾱ, θ) σ = ∀( β) τ ᾱ # β Q, α ≥ σ = (ᾱ β, θ • [τ /α]) ⊥ = ∀(α) α Q = (ᾱ, θ) ∀(Q) τ = ∀(ᾱ) θ(τ )
Notice that the ML approximation of a prefix Q is a pair (ᾱ, θ) that may be renamed. For example, the approximation of (α

≥ σ id ) is (β, [β → β/α]) which is considered equivalent to the pair (γ, [γ → γ/α]).
As a consequence, we may always assume freshness conditions on the new variables introduced by the approximation. We omit the details.

Lemma 4.4.6 i) For any σ and any monotype substitution θ, we have θ(σ) = θ( σ ).

ii) If (Q) σ 1 ⊑ σ 2 is flexible, and Q = (ᾱ, θ), then θ( σ 1 ) ≤ ML θ( σ 2 ) holds.

(Proof p. 67)

We lift • to typing environments in the obvious way.

Lemma 4.4.7 If there exists a flexible derivation of (Q) Γ ⊢ a : σ in eML F then there exists a derivation of (ᾱ) θ( Γ ) ⊢ a : θ( σ ) in ML where (ᾱ, θ) is Q .

(Proof p. 68)

Theorem 9 Any unannotated term typable in eML F under a flexible typing environment Γ (including an empty one) is typable in ML under Γ .

(Proof p. 68)

This shows why terms that are insufficiently annotated are rejected. For example, ω is not typable in eML F , as we claimed earlier. By contrast, the annotated version ω † is, as explained on page 35. Thus, although the full power of System F is available in eML F , it must be gently introduced by means of explicit type annotations. Few type annotations are needed (the encoding of System F is already concise and still sometimes redundant), but some are mandatory: annotations on function arguments that are used polymorphically. This provides a clear intuition to the programmer with respect to when to put type annotations.

Rather than a weakness, it is the strength of eML F to enforce such annotations. Since such a clear difference can be made between implicit and explicit polymorphism and programs rejected accordingly, type inference never has to guess polymorphism and, as a result, is decidable (and tractable).

Although our guideline to put annotations on function arguments that are used polymorphically is intuitive and accurate, based on our experience, it lacks a formal definition. Unfortunately, it is difficult to find an exact characterization that does not paraphrase the typing rules of eML F , since typechecking an expression λ(x) a may combine all the expressive features of ML F while typechecking its body a.

Interestingly, there are approximations of this criteria based on the translation of System F into iML F and thus restricted to programs that are typable in System F. Of course, such criteria are only meaningful if we restrict to type annotations on parameters of abstractions, that is, if we replace rules Fun and Annot by Fun ⋆ . Unsurprisingly, if λ(x : t) a is typable in System F and t is a monotype, then λ(x) a is typable in ML F without an annotation on x. This implies, for example, that (λ(x) x) ω † needs no annotation on x.

This simple criterion is weak, but can be combined with type preserving transformations in ML F to show that more involved programs, such as λ(x) choose ω † x, need no annotation either-without explicitly referring to the typing rules of ML F , but to those of System-F.

Type-preserving program transformations

In a type-inference system, it is important that type inference does not interfere with the programming style. Therefore, programs must be stable under some small local transformations, such as the permutation of the order of arguments, the introduction of auxiliary bindings, etc. Such common transformations should therefore be type preserving. We list a few useful type-preserving transformations below and use them to better explain how functions can require some of their parameters to be polymorphic but still use them parametrically, in which case an annotation is not required in eML F .

We write a ⊆ a ′ to mean that all typings of a are typings of a ′ , that is, for all prefix Q, for all typing context Γ and all type τ , the judgment (Q) Γ ⊢ a : τ implies (Q) Γ ⊢ a ′ : τ .

Invariance of typings by let-conversion. The invariance of typings by let-conversion is a particular case of subject reduction-for a liberal reduction strategy that allows reduction of non-evaluated expressions. We have

let x = a 1 in a 2 ⊆ a 2 [a 1 /x].
The proof of this property in ML F is the same as in ML.

The converse property, a 2 [a 1 /x] ⊆ let x = a 1 in a 2 also holds in ML F , whenever x appears free in a 2 . In eML F , this result easily follows from the existence of principal types, which is however not shown in this paper. Principal types allow to factor out the types of the different occurrences of a 1 in a 2 [a 1 /x] as several instantiations of the principal type of a 1 . This property also holds in ML and in church-style System F, both of which have principal types-by design in church-style System F since typing derivations are unique. However, this property does not hold in all systems with principal types [START_REF] Leijen | Flexible types: robust type inference for first-class polymorphism[END_REF][START_REF] Daan | HMF: Simple type inference for first-class polymorphism[END_REF][START_REF] Vytiniotis | FPH: First-class Polymorphism for Haskell[END_REF].

Preservation of typings by β-reduction. Although, we do not prove subject reduction for eML F in this paper, it has been proved in the case of Full eML F in [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF], provided new type annotations may be introduced during reduction-but only to replace existing type annotations. For instance, no propagation of annotations is necessary for applications of unannotated abstractions, and we have (λ(x) a) a ′ ⊆ a[a ′ /x]11 . In particular, if (λ(x ′ ) λ(x) a) a ′ needs no annotations on x and x ′ , then λ(x) (a[a ′ /x ′ ]) needs no annotation on x.

Invariance of typings by abstraction of applications. Typing of applications is "first class" in eML F , in the sense that the primitive application of a 1 a 2 can be redefined as the application of apply to arguments a 1 and a 2 , where apply is the abstraction of the application λ(x) λ(y) x y. Formally, we have a 1 a 2 ⊆ apply a 1 a 2 , and conversely, apply a 1 a 2 ⊆ a 1 a 2 .

Proof: The inverse inclusion follows from the preservation of typings by β-reduction. We thus only need to check the direct inclusion. Assume (Q) Γ ⊢ a1 a2 : τ , a derivation of this judgment will end with a sequence (1) of rules Inst and Gen eventually preceded by a rule App of the form:

App (QQ ′ ) Γ ⊢ a1 : τ2 → τ1 (2) (QQ ′ ) Γ ⊢ a2 : τ2 (3) (QQ ′ ) Γ ⊢ a1 a2 : τ1
We can build the following derivation (where anchors must be replaced by the premises introduced above):

App App (QQ ′ ) Γ ⊢ apply : (τ2 → τ1) → τ2 → τ1 (2) (QQ ′ ) Γ ⊢ apply a1 : τ2 → τ1 (3)
(QQ ′ ) Γ ⊢ apply a1 a2 : τ1 which, when followed by the sequence (1), ends with (Q) Γ ⊢ apply a1 a2 : τ .

As the order of arguments is insignificant in eML F , we also have a 1 a 2 ⊆ revapply a 1 a 2 , and conversely, where revapply stands for the application receiving its argument in reverse order λ(x) λ(y) y x.

Preservation of typings by η-expansion. Of course, this may only hold for functional expressions. Formally, if (Q) Γ ⊢ a : ∀(Q ′ ) τ → τ ′ and x is not free in a, then (Q) Γ ⊢ λ(x) a x : ∀(Q ′ ) τ → τ ′ .

Proof: We may first show the lemma for monotypes, i.e. when Q ′ is empty. Assume (Q) Γ ⊢ a : τ → τ ′ and x is not free in a. By weakening (a standard property that could be shown by induction on the height of the derivation), we have (Q) Γ, x : τ ⊢ a : τ → τ ′ (1). We thus have the following typing derivation:

Fun (1) (Q) Γ, x : τ ⊢ x : τ App (Q) Γ, x : τ ⊢ a x : τ ′ (Q) Γ ⊢ λ(x) a x : τ → τ ′
The general case reduces to the monotype case, by applying a sequence of rules UnGen ⋆ beforehand and a sequence of rules Gen afterward.

Parametric uses of polymorphism. Our guideline for eML F annotate only parameters of functions that are used polymorphically can also be explained by its corollary: parameters of functions that are used monomorphically need not be annotated. These include parameters of function that are monomorphic, as we have seen above with, for example, x in (λ(x) x) ω † , but also parameters with polymorphic types that are used parametrically in the body of the function, such as x in expressions λ(x) x ω † , λ(x) ω † x, or λ(x) choose ω † x. Any typing in System F of these expressions will require a polymorphic type for x.

Still, we can show that x is used parametrically by exhibiting in each case a type preserving transformations in which x can be typed monomorphically.

For example, λ(x) choose ω † x is the reduct of (λ(y) λ(x) choose y x) ω † where both x and y are monomorphic-as can easily be seen on a typing derivation in System F-and thus needs no annotation. Thus, by the subject reduction property, x needs no annotation in the original term.

Similarly, λ(x) x ω † is the reduct of (λ(y) λ(x) x y) ω † , where again x may be assigned a monomorphic type in System F. For λ(x) ω † x, one need not even refer to the typing in System F, as it is also the η-expansion of ω † and is thus typable in eML F , since ω † is.

By contrast λ(x) x x cannot be typed without an annotation on x. Indeed, all types of this expression in System F must assign x a type of the form ∀(α) t where α occurs on the leftmost part of t. In this example, x is explicitly used at two incompatible types. However, x may also be indirectly required to be polymorphic, as in λ(x) let y = x in y y. This programs becomes λ(x) (λ(y) y y) x after let-expansion, which, as we already know, need an annotation, e.g. σ id on y in ML F . This annotation is transferred during β-reduction to the annotation σ id on x in the resulting term. So it is unsurprising that the original program λ(x) let y = x in y y also need an annotation, e.g. σ id , on its parameter x.

We have identified some typical parametric uses of polymorphic parameters for which no annotations are required and, conversely, some polymorphic uses of parameters that require type annotations. Interestingly, we could easily classify these examples without directly referring to the typing rules of eML F .

There are also examples that combine several features of ML F in sequence, for which typechecking is harderbut still possible-to predict. Consider the expression λ(x) let y = ω † x in y y (1). We may abstract ω † away in (λ(z) λ(x) let y = z x in y y) ω † . The expression (λ(z) λ(x) let y = z x in y y) is not typable in ML and thus z or x need a type annotation, but we cannot tell whether both of them need one. It happens that a single annotation ∃ (α) α → σ id on z that specifies the codomain of z is sufficient. Then, x needs not an annotation. We can explain this on the original form as follows: in the type of ω † the domain and the codomain share no type variable, hence the type of ω † x does not depend on the type of x (as long as ω † x is typable), and can therefore be generalized in y and instantiated independently for the two occurrences of y in y y. Thus, the expression (1) is typable in ML F .

Related works

Our work continues a long line of research efforts concerned with type inference with first-class polymorphism. Unsurprisingly, this problem has been tackled from two opposite directions, either performing (partial) type inference for (variants of) System F and attempting to reach most of ML programs ( §5.1), or encapsulating first-class polymorphic values within first-order ML types ( §5.2) in more and more transparent ways.

Type inference for System F

Several interesting works on type inference for System-F-like type systems had already been carried out before it was proved to be undecidable for System F [START_REF] Wells | Typability and type checking in System F are equivalent and undecidable[END_REF] and for some of its variants.

Type containment. In the late 80's, Mitchell noticed that System F might not be the "right" system for studying type inference [START_REF] John | Polymorphic type inference and containment[END_REF]. He introduced the closure of System F by η-conversion, known as F η , and showed that well-typedness in F η could be obtained by replacing the instance relation ≤ F by a larger relation ≤ η , called type containment (see §2.1). He also showed that uses of type-containment were equivalent to the applications of retyping functions-functions whose type-erasure η-reduces to the identity-in System F. Type inference for System F modulo η-expansion is now known to be also undecidable [START_REF] Wells | Type Inference for System F with and without the Eta Rule[END_REF].

Our treatment of type annotations as type-revealing primitives resembles the use of retyping functions. Moreover, ≤ η and our type instance relation ≤ have a few interesting cases in common. However, they also differ significantly. Type containment is implicit, automatically driven by the type structure, and propagated according to polarities of occurrences (e.g. contravariantly on the left-hand side of arrows and covariantly anywhere else). By contrast, our form of type instantiation is always explicitly specified via flexibly bound variables, and may be used at occurrences of arbitrary polarities and in particular, it can be applied simultaneously at occurrences of opposite polarities, so that the weaker the argument, the weaker the result. Of course, typing rules only allow type instantiation at some occurrences and prevent it via rigid bindings anywhere else. As a result, the two relations are incomparable. The resemblance between type containment and ML F is only superficial.

Polymorphic Subtyping. System F <: is another extension of System F with a richer instance relation <:

(see its definition in §2.1). In F <: as in ML F , each type variable is also given a bound. However, it is an upper bound in F <: while it is a lower bound in ML F . As for type-containment, the subtyping relation <: is structural, which makes a huge difference with our instance relation. Type inference for F <: is undecidable. Even type checking is undecidable for some variants of the subtyping relation <: [START_REF] Benjamin | Bounded quantification is undecidable[END_REF].

Type inference based on second-order unification. Second-order unification, although known to be undecidable, has been used to explore the practical effectiveness of type inference for System F by [START_REF] Frank | Partial polymorphic type inference and higher-order unification[END_REF]. Despite our opposite choice, that is not to support second-order unification, there are at least two comparisons to be made. Firstly, Pfenning's work does not cover the language ML per se, but only the λ-calculus, since let-bindings are expanded prior to type inference. Indeed, ML is not the simply-typed λ-calculus and type inference in ML cannot, in practice, be reduced to type inference in the simply-typed λ-calculus after expansion of let-bindings. Secondly, one proposal seems to require annotations exactly where the other can skip them: Pfenning's system requires place holders (without type information) for type abstractions and type applications but never need type information on arguments of functions. Conversely, ML F requires type information on some arguments of functions, but no information for type abstractions or applications. While Pfenning's system relies on second-order unification to really infer polymorphic types, we strictly keep a first-order unification mechanism and never infer polymorphic types-we just propagate them. It might be interesting to see whether our form of unification could be understood as a particular case of second-order unification. For instance, using a constraint-based presentation of second-order unification (Dowek et al., 1996), could flexible bounds help capture certain multi-sets of unification constraints in a more principal manner, and so reduce the amount of backtracking?

Another restriction of second-order unification is unification under a mixed prefix [START_REF] Miller | Unification under a mixed prefix[END_REF]. However, our notion of prefix and its role in abstracting polytypes is quite different. In particular, mixed prefixes mention universal and existential quantification, whereas ML F prefixes are universally quantified. Besides, ML F prefixes associate a bound to each variable, whereas mixed prefixes are always unconstrained.

Partial type inference in System F. Several people have considered partial type inference for System F (Boehm, 1985;[START_REF] Pfenning | On the undecidability of partial polymorphic type reconstruction[END_REF]Schubert, 1998) and stated undecidability results for some particular variants. For instance, Boehm (Boehm, 1985) and Pfenning [START_REF] Pfenning | On the undecidability of partial polymorphic type reconstruction[END_REF] considered programs of System F where λabstractions can be unannotated, and only the locations of type applications were given, not the actual type argument. They both showed that type reconstruction then becomes undecidable as it can encode second-order unification problems. The encoding introduces an unannotated λ-abstraction the parameter of which is used INRIA polymorphically. This is precisely what we avoid in ML F : all polymorphic λ-abstraction must be annotated, whereas type abstractions and type applications are inferred.

As another example, Schubert (Schubert, 1998) considers sequent decision problems for System F in both Curry style and Church style. They, in fact, correspond to type inference problems in System F, as already studied by Wells [START_REF] Wells | Typability and type checking in System F are equivalent and undecidable[END_REF], and are known to be undecidable. An inverse typing problem in Church-style System F consists in finding the typing environment Γ that makes a fully annotated program M typable. Schubert proves that this problem is undecidable in general by encoding a restricted form of second-order unification, which is then proved equivalent to the problem of termination for two-counter automatons. We see, that although the program is fully annotated, the knowledge of the typing environment is necessary to typecheck it in a decidable way. It is then unsurprising that systems with intersection types, and more generally systems aiming at principal typings, which have to infer both the type and the typing environment, are undecidable.

On the contrary, the typing context is always known in the approach followed in ML F --as in ML.

Decidable fragments of System F. Several approaches have considered fragments of System F, for which complete type reconstruction may be performed: Rank-2 polymorphic types [START_REF] Kfoury | A direct algorithm for type inference in the rank-2 fragment of the second-order λ-calculus[END_REF], called Λ 2 , and rank-2 intersection types [START_REF] Trevor | Rank-2 type systems and recursive definitions[END_REF], called I 2 actually type the same programs. They have been generalized to even-rank polymorphic types and odd-rank intersection types [START_REF] Trevor | A polar type system[END_REF]. However, none of these system is compositional, because of the rank limitation: one may not abstract over arbitrary values of the language. Since first-class polymorphism is precisely needed to introduce a higher level of abstraction, we think this is a fundamental limitation that is not acceptable in practice. Besides, their type inference algorithm in Λ 2 requires rewriting programs according to some non-intuitive set of reduction rules. Hence, no simple intuitive specification of well-typedness is provided to the user. Worse, type inference can only be performed on full programs: it is thus not possible to split a program into several modules and typecheck them independently. Noticeably, I 2 has better properties than Λ 2 , such as principal typings. However, the equivalence between I 2 and Λ 2 is shown by means of rewriting techniques; thus, although a typing in I 2 can be inferred in a modular way, it does not give a modular typing in Λ 2 .

Intersection types and System E. Wells and Carlier have proposed a type system, called System E, that generalizes intersection types with expansion variables (Carlier et al., 2004). Although their work is quite different in nature, as type inference is undecidable and only a semi-algorithm is given, there are interesting connections to be made. In particular, both works attempt to share several derivations of a same term, using implicit sharing via expansion variables in the case of System E or more explicit sharing via auxiliary quantifiers in the case of ML F .

Local type inference. Local type inference (Cardelli, 1993;[START_REF] Pierce | Local type inference[END_REF] uses typing constraints between adjacent nodes to propagate type information locally, as opposed to the global propagation that is performed by unification as used in ML F (or ML). This technique is quite successful at leaving implicit many (but not all) eliminations of both subtyping and universal polymorphism. However, it usually performs poorly for their introduction forms, which remain mandatory in most cases. The technique has been tested in practice and ambiguous results were reported: While many dummy type annotations can be removed, a few of them remained necessary and sometimes in rather unpredictable ways. One difficulty arises from anonymous functions as well as so-called hard-to-synthesize arguments [START_REF] Hosoya | How good is local type inference?[END_REF]. The technique is actually fragile and does not resist to simple program transformations. As an example, the application app f x may be untypable with local type inference when f is polymorphic12 . Principal types are ensured by finding a "best argument" each time a polymorphic type is instantiated. If no best argument can be found, the typechecker signals an error. Such errors do not exist in ML nor ML F , where every typable expression has a principal type.

It should be noticed that finding a "best argument", and thus inferring principal types in local type systems is sometimes made more difficult because of the presence of subtyping, which ML F does not consider. In particular, to our knowledge, local type inference and its refinement described in the next paragraph are still the only partial type inference techniques that deal with both second-order polymorphism and subtyping. The extension of ML F with subtyping has not been explored at all.

Colored local type inference [START_REF] Odersky | Colored local type inference[END_REF] is considered as an improvement over local type inference, although some terms typable in the latter are not typable in the former. It enriches local type inference by allowing only partial type information to be propagated.

Stratified type inference.

Beyond its treatment of subtyping, local type inference also brings the idea that explicit type annotations can be propagated up and down the source tree according to fixed well-defined rules. This can sometimes be viewed as a preprocessing pass on the source term, which we then called stratified type inference. When the preprocessing step is simple and intuitive it need not be defined through logical typing rules, but may instead be defined algorithmically. Such a mechanism was already used in the first prototype of ML F to move annotations of toplevel definitions to annotations of their respective parameters [START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]. Here, stratified type inference is used as a secondary tool that helps writing annotations at different places rather than removing them. The use of stratified type inference as the main tool for performing type inference for System F has been shown unsatisfactory, even for its rather limited predicative fragment [START_REF] Didier | Simple, partial type-inference for System F based on type-containment[END_REF]. Stratified type inference has been applied more successfully for performing type inference in ML in the presence of Guarded Abstract Data Types (GADT) [START_REF] Pottier | Stratified type inference for generalized algebraic data types[END_REF].

Embedding first-class polymorphism in ML

ML programmers did not wait for solutions to the problem of type inference with first-class polymorphic types to introduce them in existing languages. Boxing polymorphism is a backup solution that consists in embedding polymorphic values into first-class ML values. Initially introduced for existential types it was quickly applied to universal types and later turned into more and more sophisticated proposals, some of which have now been in use in OCaml or Haskell for several years.

First-class polymorphism in FX The language FX (O 'Toole Jr. and Gifford, 1989) seems to be a precursor of all extensions of ML with first-class polymorphism. Although its expressiveness is somewhat limited-it approximately fits between boxed polymorphism and Poly-ML described below-FX already contained several of the ideas reused in some later works. Roughly, FX allows ML implicit topmost quantifiers as in ML type schemes and explicit first-class quantifiers as in System F, plus constructions to coerce between the two. By definition, it supersedes both ML and System F, hence its expressiveness. However, expressiveness is achieved by relying more on explicit than on implicit polymorphism. In particular, an important restriction of FX, which makes its inference mechanism less expressive than the one of Poly-ML, is that implicit type instantiation remains predicative. That is, implicit quantifiers can only be instantiated by simple types-types that do not contain any quantifier. To recover impredicativity, implicit polymorphism may (and often need to) be converted to explicit polymorphism. Moreover, the type system specification requires typing derivations to be principal, disallowing any form of weakening, whenever first-class polymorphism is being used. Furthermore, implicit quantifiers do not commute and are instead inserted in some fixed left-to-right order so that they can later be unambiguously converted to explicit quantifiers the order of which matters. As a result, although the user need not always write quantifiers explicitly, he must still usually think in terms of explicit polymorphism.

Boxed polymorphism refers to the encapsulation of first-class polymorphic values into monomorphic ones via injection and projection functions. In their most basic version, injections and projections are explicit, even though, in practice, they can be attached to datatype constructors [START_REF] Läufer | Polymorphic type inference and abstract data types[END_REF][START_REF] Didier | Programming objects with ML-ART: An extension to ML with abstract and record types[END_REF]. Typically, preliminary type definitions are made for all polymorphic types that appear in the program. For instance, the following program defines three versions of ω and applies them to id:

type sid = Sid of ∀(α) α → α let id = Sid (λ(x) x) : sid let ω 1 = λ(x) let Sid z = x in z z : ∀(β) sid → (β → β) let ω 2 = λ(x) let Sid z = x in z x : sid → sid let ω 3 = λ(x) ω 2 x : sid → sid (ω 1 id, ω 2 id, ω 3 id) : ∀(β) (β → β) × sid × sid
The symbol Sid is both used as a constructor in the creation of the polymorphic value id (second line) and as a destructor when it appears on the left-hand side of let-bindings (third and fourth lines)-or in place of parameters as in λ(Sid x) x x, which could be an alternative definition of ω 1 . Notice the difference between ω 1

INRIA

and ω 2 : the former returns the unboxed identity while the latter returns the boxed identity. Here, the coercion between the two forms must be explicit. This may be quite annoying in practice, as already suggested by the involved encoding of System F into boxed polymorphism [START_REF] Odersky | Putting type annotations to work[END_REF]. The fifth line shows that an η-expansion need no type annotation even when the argument is polymorphic.

Poly-ML (Garrigue and Rémy, 1999) is an improvement over this mechanism that replaces the projection from monotypes to polytypes by a simple place holder • , indicating the need for a projection but eluding the projection itself. It also introduces a notation [• : σ] for embedding polymorphic values into monomorphic ones, which alleviates the need for prior type definitions. The previous example may be rewritten as follows (where σ id is a meta-level abbreviation for ∀(α) α → α, and boxed polymorphism is represented inside square brackets):

let id = [λ(x) x : σ id ] : [σ id ] let ω 1 = λ(x : [σ id ]) x x : ∀(β) [σ id ] → (β → β) let ω 2 = λ(x : [σ id ]) x x : [σ id ] → [σ id ] let ω 3 = λ(x) ω 2 x : [σ id ] → [σ id ] (ω 1 id, ω 2 id, ω 3 id) : ∀(β) (β → β) × [σ id ] × [σ id ] id : ∀(β) (β → β)
Explicit type information is still required when creating a polymorphic value (first line). Abstracting over an (unknown) polymorphic value also requires explicit type information (second and third lines). However, type information may be omitted when using a known polymorphic value (last line). In fact, polymorphism must always be known in order to be used. For instance, λ(x) x would be rejected. Notice that, we could also have written ω 1 as λ(x : [σ id ]) let z = x in z z, so as to avoid repeating the projection, much as for the treatment of type annotations in eML F . (But this is unsurprising, since eML F was much inspired by Poly-ML.) The fourth line shows that η-expansion need no type annotation even when the argument is polymorphic. The progress made between boxed polymorphism and Poly-ML is significant, which can already be seen on the encoding of System F into Poly-ML-much simpler than the encoding into boxed polymorphism. Yet, Poly-ML is not quite satisfactory. In particular, each polymorphic value must still be embedded and so requires an explicit type annotation at its creation (first line). The explicit type information necessary to build a polymorphic value is utterly redundant: can a programmer accept to write down a type that is already inferred by the typechecker? Moreover, this information may be much larger than what one would need to write in System F. For example, Λα. λ(x : α → α) x must be encoded as

[λ(x) x : ∀(α) (α → α) → (α → α)].
Still, when using core Poly-ML to typecheck objects, every polymorphic-method invocation must be explicitly marked as an instantiation site. To avoid this burden, an extension that has been proposed (and now in use in OCaml) considers that every method invocation is implicitly a possible instantiation site. However, this extension requires typing derivations to be principal so as to be non ambiguous-and thus well-defined-in a pathological case. A similar restriction was already used in FX, but in a more crucial way for the main cases.

Boxy types [START_REF] Vytiniotis | Boxy types: inference for higher-rank types and impredicativity[END_REF] go one step-further than Poly-ML by removing the "coercion box" of Poly-ML from the level of expressions-retaining it only at the level of types. In Poly-ML one could define the ordinary polymorphic identity function λ(x) x with (toplevel) type scheme ∀(α) α → α or the boxed first-class polymorphic value [λ(x) x : ∀(α) α → α] with polytype [∀(α) α → α]. With boxy types, there is no syntax to express this difference and instead, it is left to the typechecker to infer which form is meant. While there is an obvious competition between these two forms, the typing rules are presented in an algorithmic fashion, i.e. as an algorithm, that (silently) resolves competing cases in favor of one or the other view. The type system has principal types, but with respect to its algorithmic specification. Unfortunately, it is unknown whether there is a logic specification of the type system equivalent to the algorithmic presentation. Actually, this is unlikely, as the logic rules would somehow have to encode the left-to-right evaluation order followed by the algorithmic rules.

Because boxy types have an algorithmic specification it is difficult to compare them with ML F , precisely. As they (arbitrarily) privilege propagation of type information from the function type to the argument type, they can type examples where ML F would require an annotation and thus fail. Conversely, there are many examples that ML F can type and that boxy types cannot-for some much deeper reason. In particular, if a 1 a 2 is typable, then app a 1 a 2 is not necessarily typable with boxy types-a severe problem. More generally, boxy types are not conservative with respect to small program transformations, as seen earlier ( §4.5).

As boxy types, ML F also removes the "coercion boxes" of Poly-ML, but does so in a more symmetric way, without arbitrary choices, by enriching the types of System F just as little as needed to represent all possible choices in derivations within (unique, principal) types.

Rigid ML F is a restriction of eML F that restricts the typechecking of let-bindings to use only rigid type schemes for bound expressions (Leijen, 2007). Interestingly, Rigid ML F can only type programs of System F, as Simple ML F . In the absence of let-bindings, it does not perform better than ML F . However, it also allows implicit generalization at let-bindings, as ML F , but remaining within System F, as Simple ML F . Hence, Rigid ML F can use System F as an intermediate explicitly typed language, which ML F still lacks. Having an intermediate explicitly typed language is useful for compilers, such as the Haskell compiler, that simultaneously perform aggressive program transformations and maintain precise type information during compilation. As a corollary, Rigid ML F can be used as a front end to Haskell.

Unfortunately, Rigid ML F looses principal types in the usual sense-technically it recovers principal types by using an ad hoc, non logical side condition in typing rules to rule out some otherwise correct typing derivationsmuch as in FX. As a result, Rigid ML F is fragile to some minor, but useful program transformations; It also requires more type annotations than ML F -and the additional type annotations are often annoying.

(Partial) Type inference for the predicative fragment. Odersky and Läufer have also extended boxed polymorphism to implicit predicative instantiation of rank-2 polymorphism [START_REF] Odersky | Putting type annotations to work[END_REF], which was later improved to arbitrary-rank types by Peyton Jones and Shields (Jones and Shields, 2004b;[START_REF] Simon | Practical type inference for arbitrary-rank types[END_REF]. Technically, this approach mixes local type inference with ML-style, unification-based type inference. However, this approach has two serious problems. Inherited from local type inference, and as boxy types it makes algorithmically specified, arbitrary choices. Moreover, the restriction to predicative polymorphism is far too drastic (see [START_REF] Didier | Simple, partial type-inference for System F based on type-containment[END_REF] for detailed arguments). As a result, this approach is not sufficiently powerful and can only be used in combination with the more basic form of boxed polymorphism to recover the full power of System F. This results in a rather complicated language with several not well-integrated idioms to accomplish similar goals. In fact, this proposal seems to have been dropped in favor of boxy types by the common authors of both works.

Summary. The different proposals for embedding first-class polymorphism within first-class values are schematically summarized below. Unnanotated arrows mean is weaker than; annotated arrows are only approximations that applies to the main aspects of the systems but some particular programs may typecheck in the source and not in the target, with the following meaning for annotations: (1) up to small details; (2) the target is not stable by η-conversion while the source is; (3) except when relying on the left-to-right bias in the order of arguments in the source. Double lines are used for type systems enjoying principal types. Oval nodes are used for all restriction variants of ML F .

Boxy types FPH

Poly-ML FX HMF HML

Boxed Polymorphism Rigid ML F ML F Pred. Frag. of F (1) (1)
(2)

(3) (2) (3)
The languages FPH, HMF, and HML that have been proposed more recently are discussed in § 5.4.

Comparison with (other presentations of) ML F

We have restricted our investigation to (Shallow) ML F , because it is based on a semantics of types as sets of System-F types. The original presentation [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF], instead focuses on the more expressive Full ML F system and introduces Shallow ML F as a restriction of Full ML F . We first compare INRIA (Shallow) ML F , with the original, Full and Shallow versions, successively. We then discuss the more recent graphical presentation of ML F (Rémy andYakobowski, 2007, 2008a).

Comparison with Full ML F . Although the original presentation was about Full eML F , and the comparison should a priori be made with eML F , there is little to say about type inference, but more about expressiveness. We thus consider the simpler, implicitly typed version Full iML F and compare it with iML F .

Types of iML F are stratified: they distinguish between types, which are isomorphic to System-F types, and can be used to form arrow types, from type schemes, which can only be used as such or in the bound of variables to form other type schemes. By contrast, types are not stratified in Full iML F and instead are identified with type schemes, as follows:

τ, σ ∈ T Full ::= α | τ → τ | ∀(α ≥ τ ) τ | ⊥
In particular, Full iML F allows proper flexible types σ, e.g. ∀(α≥σ ′ ) τ to appear in positions where polymorphism is required, as in σ → ∀(α) α, which is a type of Full iML F but not of iML F . For this reason, our semantics for iML F does not easily extend to Full iML F .

The problem may be illustrated by considering the semantics of the simpler type σ → int. In iML F , σ is restricted to be a type τ of System F, i.e. whose semantics is a singleton {t}. Hence, the semantics of σ → int could be simply defined as the singleton {t → int}. In Full iML F , σ may be a proper flexible type, i.e. one whose semantics is not a singleton type. What should be the semantics of σ → int in this case? Certainly not {t → int | t ∈ { {σ} }}, as this is the semantics of ∀(α ≥ σ) α → int, which is quite different from σ → int. Intuitively, { {σ → int} } should describe the type of functions that require their argument to have all types in { {σ} }. A temptation is to write "{ {σ} } → int", but this is ill-formed since { {σ} } is a set of types, not a type.

It is actually instructive to draw an analogy with intersection types (which can be used to model finite sets of types) where the intersection ∧ distributes on the right-hand side of arrow types, but not on its left-hand side. (τ 1 ∧ τ 2 ) → τ is not equivalent to (τ 1 → τ ) ∧ (τ 2 → τ ). Hence, intersection types of the form (τ 1 ∧ τ 2 ) → τ , which are not intersection of System-F types, are essential. This suggests that extending the semantics of iML F to Full iML F would have to go beyond sets of System-F types, and perhaps, introduce a form of infinitary intersection types. However, these would have to be studied on their own first, which is likely to be more difficult than studying Full iML F types alone! Comparison with the Original. There remain a few differences between ML F we presented here and the original Shallow ML F (Le Botlan and Rémy, 2003) that are not just a matter of presentation. For the sake of comparison and by contrast with above, we here consider the explicitly typed versions.

The abstraction relation ⊏in this version of eML F is larger than the original one so that eML F coincides exactly with iML F . This is an improvement, as it follows from the semantics of iML F and its canonical definition of type-instance by interpretation of types as sets of System-F types.

This difference in the definition of abstraction is unimportant in practice, even though we may easily build an example in eML F that is not in the original version. For instance, consider the types σ 1 and σ 2 , respectively defined as

∀(α ≥ ∀(β ⇒ σ id ) β → β) α → α and ∀(β ⇒ σ id ) (β → β) → β → β. We have σ 1 ⊏ -σ 2 and σ 2 ⊐ -σ 1 , hence σ 1 ⊏ -⊐ -σ 2 .
That is, types σ 1 and σ 2 can be (explicitly) converted to one another. However, in the original version we do not have σ 1 ⊏o σ 2 but only σ 1 ⊑ o σ 2 (subscript o stands for the original version). Therefore, only σ 1 is (implicitly) convertible to σ 2 by type instance but σ 2 is not convertible to σ 1 in the original version. More precisely, the program λ(x : σ 2 ) (x : σ 1 ) is in our version of ML F but not in the original one.

This improvement in the definition of the abstraction relation was first suggested by François Pottier. However, its naive formalization in the original version would not be correct, because of pathological contexts in which uses of unprotected abstraction would break type soundness, as explained in §4.1 (page 31). In order to prevents these misuses of abstraction, we introduced the auxiliary relation ⊏ -♯ in the definition of ⊏ -. Quite interestingly, this change, which appears to be a small complication in the syntactic presentation of abstraction is actually a simplification when we view types as graphs (Rémy and Yakobowski, 2007), as described below.

There are other minor differences with the original presentation. For instance, the encoding of System F into eML F we have presented is different from the original one, as explained page 37. More precisely, the abstraction relation defines a lattice over types, as shown in [START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF]. A given type of System F corresponds to several types in the lattice, any of which could be chosen as its default encoding. In [START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF], we chose the meet of all candidates, which is easier to build. In this paper, we chose their join, favoring the shortness of the proof.

Comparison with the graphical presentation. A graphic presentation of ML F types and type-instance has recently been proposed [START_REF] Didier | A graphical presentation of MLF types with a linear-time unification algorithm[END_REF] and their application to graphical typing constraints is ongoing work. These works are complementary, as both bring different enlightenment on ML F and its instance relation. In this work the instance relation is derived from a more canonical definition as sets of System-F types. In the graphic presentation, it is derived from type instance on first-order types and natural, simple operations on the binding tree. While, the semantics definition of type instance does not easily generalize to Full ML F , the graphic presentation is in fact directly defined in Full ML F . The graphic presentation is also targeted at performing efficient type inference, which we did not address in this work.

Ongoing works around ML F

Although eML F requires very few type annotations, and has a simple criterion for where and when to provide them, two criticisms have been made, namely the lack of an internal explicitly typed language and the introduction of "unfamiliar" types. These have motivated ongoing works on finding restrictions of ML F that would circumvent these issues. Unsurprisingly, any limitation come at some price, increasing the number of required type annotations and losing robustness to program transformations and other interesting properties of ML F -such as preservation of typing by reduction.

An internal, explicitly typed language for ML F . An argument against the use ML F has been that programs cannot be elaborated into terms of System F. The system F let is certainly not meant to be a replacement for System F as an internal language because the translation from ML F to F let does not preserve the modularity properties of ML F .

The problem with finding an internal language for eML F is that source terms contain type annotations that must be transformed during reduction, as shown in the original work [START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF].

Fortunately, an internal language, called x ML F , has just been proposed for ML F (Rémy and Yakobowski, 2008b). This language generalizes type abstraction of System F by introducing flexible bounds on type variables and replaces type applications by instantiations-a small sub-language describing exactly how types are instantiated. Type annotations of ML F are translated by type instantiations in x ML F , which can then be transformed during reduction so as to maintain well-typedness.

This improves over the only previously known alternative that is to insert coercion functions so as to remain within System F [START_REF] Daan | Qualified types for MLF[END_REF]. Indeed, those coercions are retained at runtime with an unnecessary runtime cost, in particular due to duplication of data structures. Furthermore, it has never been proved that the insertion of these coercion functions actually preserves the semantics of programs.

Strange looking types. Types of eML F may look unfamiliar because they use two new forms of quantification: flexible and rigid bindings. It has been argued that this might hinder the adoption of ML F . We agree that types of ML F are sometimes harder to print and read because they are richer. However, the introduction of both flexible and rigid quantification has been driven by properties and program transformations that should hold in a reasonable type inference system.

Flexible types are used to factor into a principal typing derivation of ML F , correct but incomparable derivations of System F. As a side effect, they also increase expressiveness, although this was not their first purpose. Flexible types now have some simple semantic explanation, which may help them look more familiar.

Rigid types do not increase expressiveness, but introduce extra information that partially remembers the way types have been derived, and in particular, distinguishes polymorphism that has been requested from polymorphism that has been provided. Even though rigid types may not be justified by semantic arguments, they mainly mimic flexible types in the way they keep track of sharing. Hopefully, they will look more familiar once flexible types will be well-understood and used.

Eliminating the need for rigid bindings. Leijen has identified a quite interesting restriction of ML F , called HML, that does not use rigid bindings at all, but still permits type inference [START_REF] Leijen | Flexible types: robust type inference for first-class polymorphism[END_REF]. His proposal, inspired by iML F , could have been described as a stable subset of eML F , which we explain below.

Leijen's restriction proposal can be summarized as disallowing the use of rigid bindings in the prefix of typing judgments. As a result, all other rigid bindings, i.e. appearing in the typing environment or the result type INRIA become local and can be locally maximally shared. Below, we call restricted typing judgments of eML F that do not use rigid binding in prefixes and where all other types are maximally shared. When rigid bindings are maximally shared in types, they may be printed inlined and look as iML F types.

In order to allow all judgments to be restricted, we use derived rules App ⋆ and Fun ⋆⋆ instead of App and Annot in derivations, which we call restricted derivations. The rule Fun ⋆⋆ is the following variant of Fun ⋆ :

Fun ⋆⋆ (Q) Γ, x : ρ ⊢ a : ∀(Q ′ ) τ ᾱ ⊆ dom(Q) (Q) Γ ⊢ λ(x : ∃ (ᾱ) ρ) a : ∀(Q ′ , β ⇒ ρ) β → τ
That avoids the need for putting rigid bindings in the prefix Q. We still allow rigid bindings to appear in derivations of instantiation and abstraction judgments (although we could also introduce derived rules instead).

Interestingly, under restricted prefixes, ⊐ -; ⊑ steps may always be turned into ⊑; ⊐steps-a result that does not hold in general. This implies that under restricted prefixes, imposing maximal sharing in τ and Γ does not restrict typability. Formally, if Q is a restricted prefix and (Q) Γ ⊢ a : σ and Γ ⊏ -Γ ′ (when ⊏is extended to type environments pointwise), then there exists σ ′ such that (Q) Γ ′ ⊢ a : σ ′ and σ ⊏σ ′ . This enables to transform any restricted derivation of a judgment in restricted form into one where all intermediate judgments are also in restricted form. In such derivations, revelation needs never be used. By forcing maximal sharing in Γ, we may be forced to do more sharing in σ ′ as well; however, this is harmless, as this sharing could always-but never need to-be recovered a posteriori by a single final revelation.

The cost of bridling ML F to restricted derivations is that all polymorphic arguments must be annotated regardless of whether they are treated parametrically or used polymorphically. Consequently, typing judgments are not themselves stable by arbitrary substitutions (but only by monotype ones). In particular, preservation of typings by β-reduction is lost. In practice, this also means that polymorphic types are not quite first class citizens. For instance, replacing a ground datatype by its Church encoding, e.g. replacing int by nat where nat is an abbreviation for ∀(α) (α → α) → α → α, does not preserve typability. This also means that data structures with inner but passive polymorphism (that is just stored in data-structures or passed around to functions) cannot be used as conveniently as similar data structures where polymorphism has been abstracted away as a new ground or simple type.

In addition, this version requires additional type annotations, which may sometimes be surprising and unpleasant. For example, (λ(x) λ(y) x y) ω † (1) is typable but its reduct λ(y) ω † y is not. That is, extratype annotations need to be inserted during reduction. The drawback is that the user may be tempted to write programs with extra, obfuscating abstractions that also have a runtime cost, just to avoid extra type annotations. The example above also illustrate the lost of stability by both η-expansion and β-reduction. Consequently, although HML type inference engine is in essence more powerful and more practical than that of Poly-ML, it is not strictly speaking an extension of Poly-ML.

Nevertheless, this remains an interesting variant of ML F as it preserves principal types and the logical flavor of typing rules, as well as interesting program transformation such as abstraction of application, as shown in (1), or let-conversion. Moreover, the use of simpler types that moreover coincide with those of iML F is unquestionably a clear gain.

Depriving ML F from flexible bindings has also been proposed by Leijen (Leijen, 2007) and called HMF. However, this is a drastic restriction that does not interact well with type inference. In particular, the two typings of choose id cannot be captured by a principal type without flexible typings. Hence, principal types per se are lost. They may be recovered by an ad hoc non logical side condition that disallows one of the two typings-in fact, the choice is always made in favor of more external polymorphism, so as to remain compatible with ML. Unsurprisingly, the robustness of the type system to program transformation is really lost. For example, one may no longer always abstract over type applications or share common subexpressions in let-bindings.

Back to System F-types. The two restrictions of ML F to HMF or HML are independent of one another and can be combined together [START_REF] Leijen | Flexible types: robust type inference for first-class polymorphism[END_REF]. The result is attractive because types then look just as regular System-F types. Unfortunately, the drawbacks accumulate and are so important that the author of the proposal does not himself recommend dropping flexible bindings [START_REF] Leijen | Flexible types: robust type inference for first-class polymorphism[END_REF].

Yet, another proposal by Vytiniotis et al [START_REF] Vytiniotis | FPH: First-class Polymorphism for Haskell[END_REF], called FPH, which looks quite different in presentation, using boxes to keep track of impredicative type instantiations, is of comparable expressive power, and interestingly, can also be explained using the ML F framework.

As for HMF, rigid types are disallowed in the prefix and therefore they can always be maximally shared. Alternatively, types may be considered up to abstraction, as in iML F . This may actually be made explicit by introducing an additional bound "=" that stands for equivalence and behaves as "⇒" except for the two following differences: firstly, under a prefix containing α = σ, we have α ≡ σ, i.e. both σ ⊏α and α ⊏σ; secondly, turning a rigid binding into an equivalence binding is part of revelation but not of equivalence-except for monotype bounds which can always be inlined. The second fact is the key to FPH that requires explicit type annotations to confirm impredicative type instantiations, and so disambiguate between predicative and impredicative type instantiations.

Interestingly, FPH can now be explained by restricting typing judgments Q, Γ ⊢ a : σ of ML F so that Q is always the empty prefix, flexible bindings are never used in Γ nor in σ, and rigid bindings are only used at the toplevel of σ. Equivalence bounds can be printed inlined in FPH. Rigid bindings represent boxed types. As they can always be maximally shared, as in HMF, they can also be printed inlined.

While FPH has a modular type inference algorithm, in the sense that typechecking of let-bound expressions need not be delayed, it does not enjoy principal types, because flexible bindings may only be used internally, for type inference, but may not appear in the result of type inference. For this reason, choose id does not have a principal type.

Of course, despite the benefit that the user need not (in principle) be exposed to boxed types but only to System-F types, this proposal loses many modularity properties of ML F , much as the combination of HML and HMF. Moreover, rigid types (i.e., boxes) cannot be really hidden from the user when displaying type errors. In fact, even flexible types, which are used internally, would help explaining type errors. The absence of principal types in FPH also implies that interfaces of compilation units must always be given explicitly.

Viewing FPH in the framework of ML F has some advantages. It first shows, even though we did not make all the details explicit, that FPH is a subset of ML F , as already noticed by its authors. It also emphasizes the strong relations between FPH and HML, originally remarked by Leijen. Additionally, it suggests a simpler presentation of FPH where the subtyping relation allows extra boxing so that equality-up-to-unboxing side conditions on the application and annotation typing rules can be removed, leading to a more traditional presentation of FPH in the style of our generic type system.

Despite their drawbacks and limitations when compared with ML F , both FPH and HML (with or without flexible bindings), may be interesting in several ways: they show that rigid bindings are not necessary for the sole purpose of type inference, but only for getting more type inference and more robustness to program transformations. They may also allow a faster migration of existing languages based on Hindley-Milner type systems to type systems with first class-polymorphism, in particular in the case of Haskell which uses System F as an internal language.

ML F with graphical types is a parallel work where a graph-based representation of types and of the type instance relation is used to simplify their definitions and explore the different variants more systematically. Hopefully, graphic types provide better intuitions on both flexible and rigid bindings and will help for their acceptance. Simple notational conventions can also be used to display eML F as System-F types in many cases (Rémy and Yakobowski, 2008a).

The graph representation has already enabled a new, efficient unification algorithm for ML F types. It is currently used to revisit, improve and modularize type inference for ML F . As mentioned earlier ( §2.3, page 19), this work validates a posteriori the design choices made in the definition of the instance relation of eML F .

Graphs have also helped find an internal language x ML F (Rémy and Yakobowski, 2008b). Finally, graphs bring syntactic and semantic types closer. Interestingly, the graph representation applies indifferently to the shallow or full versions, and might be a means to also give a semantics to Full ML F .

Future works

ML F types are strictly-but only slightly-more expressive than System-F types. One may wonder whether they could be subsumed by higher-order types. We think that the two mechanisms are complementary and equally desired. We already see two solutions to higher-order polymorphism.

A limited form of higher-order polymorphism can be obtained with the use of higher-order kinds, which treats type operators as first-order type variables. This allows abstraction and instantiation of type operators, but not any reduction at the level of types. Technically, a type application F (τ ) where F is a type operator is treated as an application @(F, τ ) where @ is an application operator and F can be treated as an ordinary type, but of a higher-order kind. This extension is minor and only differs in the introduction of kinds, which are easy to INRIA keep track of. Interestingly, instantiation of type operators can then be inferred as all other type-instantiations in ML F .

Another solution that would better integrate higher-order types and reach all of F ω is to use a distinct universal quantifier at higher kinds with type introduction and type elimination constructs that would always be explicit at higher kinds.

Although, inferring instantiation of type operators at higher-order kinds seems possible in some interesting cases, type-level computation resulting from instantiation of higher-order types seems to be conflicting with the precise sharing between polymorphic types that has to be maintained in ML F . Studying this interaction remains an interesting research direction.

Extending ML F with recursive types is another interesting investigation to pursue. In the presence of type inference, one would expect implicit equi-recursive types to be used, as in ML. While we anticipate no difficulty with monomorphic recursion, the problem seems much harder when recursion crosses polymorphic boundaries. A solution might have to combine implicit monomorphic equi and explicit polymorphic iso recursive types, altogether.

Extensions of ML F -types with subtyping, type constraints, assertions, etc. are of course also worth exploring.

Conclusions

In our quest for better integration of first-class polymorphism within ML, we have come up with ML F -a new type system for second-order polymorphism that is actually two-fold. The Curry-style version iML F just extends second-order types with flexible bindings so as to capture instances of a given type as a single type scheme. This is written ∀(α ≥ σ) σ ′ , meaning that α may be replaced by any instance of σ in σ ′ . Types schemes are interpreted by sets of System-F types. The instance relation on types is defined as set inclusion of their semantics. The language iML F is a subset of F let , an extension of System F with a very restricted form of intersection types that contains exactly all let-expansions of System-F expressions.

We have also proposed a Church-style version eML F that permits type inference. Expressions of eML F , given with some explicit type annotations, always have principal types13 . Technically, eML F introduces rigid bindings written ∀(α ⇒ σ) σ ′ to mediate between explicit type information σ and its implicit view α within σ ′ . Interestingly, eML F is a conservative extension of ML as fully unannotated programs are typable in eML F if and only if they are typable in ML. Moreover, all System F programs can be turned into eML F programs by simply dropping type abstractions and type applications and by a simple translation of type annotations. Besides, only function arguments that are used polymorphically need a type annotation in eML F . This provides a clear specification of when and how to annotate type parameters.

We believe that ML F is a user-friendly extension of ML with first-class polymorphism. Additionally, without significantly departing from System F, programs in iML F have more-expressive types (and more principal types) than in System F and are therefore more modular and more robust to program transformations.

Although there are still a few options in the design space, eML F seems to be a local optimal, where any restriction looses some of its interesting properties and any extension in expressiveness would very likely require a form of higher-order unification. The restriction of ML F to flexible-only bindings [START_REF] Leijen | Flexible types: robust type inference for first-class polymorphism[END_REF] is another interesting point in the design space that might be another alternative, a less expressive but simpler surface language for iML F .

Proof of Lemma 3.6.2

By induction on the derivation of (Q ∋ θ) Γ ⊢ a : σ ∋ t ⇒ ∆. We show a stronger result, that is, F let :: θ({ {Γ} }), ∆ ∧ ∆ ′ ⊢ a : θ(t) holds for any context ∆ ′ such that dom(∆ ′ ) # dom({ {Γ} }) (1). All cases are straightforward, except iF-Gen, which can be shown as follows. We reuse the notations of rule iF-Gen. By definition, we must have θ(∀( β) t ′ [t/α]) in θ({ {∀(α ≥ σ) σ ′ } }). As the last rule of the derivation is iF-Gen, we must have (Q, α ≥ σ ∋ θ • [t/α]) Γ ⊢ a : σ ′ ∋ t ′ ⇒ ∆ (2), α / ∈ ftv(Γ) (3), and β # dom(Q) (4) hold. By induction hypothesis applied to (2), we get F let :: θ • [t/α]({ {Γ} }), ∆ ∧ ∆ ′ ⊢ a : θ(t ′ [t/α]) (5) for any ∆ ′ satisfying the hypothesis (1). From (3), we have θ • [t/α]({ {Γ} }) = θ({ {Γ} }). Thus, from (5), we have F let :: θ({ {Γ} }), ∆ ∧ ∆ ′ ⊢ a : θ(t ′ [t/α]) (6). From (4), we have β # ftv({ {Γ} }) ∪ ftv(∆). By α-conversion, we may also assume β # ftv(∆ ′ ), w.l.o.g. We may thus conclude with rule Gen applied to (6).

Proof of Theorem 2

This is an immediate consequence of Lemmas 3.6.1 and 3.6.2. 9). Then, we conclude by Lemma 3.3.11.ii (page 23). Otherwise, σ a / ∈ V. We conclude by (9), iCon-AllLeft, iCon-AllRight, and iEqu-Inert, using Lemma 4.1.7.

• Case eEqu-Comm: This rule commutes two binders. Each one is either flexible or rigid. Because of symmetry, we only have to consider three subcases: either both bindings are rigid, or both are flexible, or one is flexible and one is rigid. The first subcase is shown by commutation of the two substitutions. The second subcase is shown by Rule iEqu-Comm. The last subcase is by reflexivity.

• Case eEqu-Var: We distinguish two subcases, depending on the binding being flexible or rigid. If it is flexible, we use iEqu-Var. Otherwise, we use reflexivity.

• Case eEqu-Free: Similarly, we use iEqu-Free if the binding is flexible. Otherwise, we use reflexivity.

• Case eEqu-Mono: We use iEqu-Inert if the binding is flexible. Otherwise, we use reflexivity.

As for the abstraction relation (statement ii), we show the property for both relations ⊏and ⊏ -♯ , simultaneously by induction on the derivation. That is, if (Q) σ 1 ⊏σ 2 or (Q) σ 1 ⊏ -♯ σ 2 , then (Q) ′ θ σ 1 ⊏ -⊐θ σ 2 . Transitivity is by induction hypothesis. Rule eAbs-SharpLeft : shown as above, like for equivalence. Rule eAbs-Equiv : by consequence of property i. Rule eAbs-Hyp : by reflexivity. Rule eAbs-SharpDrop : by induction hypothesis.

• Case eAbs-Left : σ 1 is of the form ∀(α ≥ σ ′ 1 ) σ ′ and σ 2 is ∀(α ≥ σ ′ 2 ) σ ′ . By hypothesis, (Q) σ ′ 1 ⊏ -♯ σ ′ 2 (10) holds. If σ ′ 1 or σ ′ 2 is in V, then (Q) σ ′ 1 ≡ σ ′ 2 holds by Lemma 4.1.5, so we get (Q) σ 1 ≡ σ 2 by congruence, and

INRIA

  . . . . . . . . . . . . . . . . . . . . . . . . . . 10 2.2 iML F : Curry-style ML F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.3 eML F : Church-style ML F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15 i ML F , Curry-style ML F 19 3.1 Types and prefixes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 3.2 Interpretation of types and prefixes . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20 3.3 Syntactic versions of instance and equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 3.4 Typing rules . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24 3.5 System F as a subset of (Simple) iML F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.6 Type soundness, by viewing iML F as a subset of F let . . . . . . . . . . . . . . . . . . . . . . . . . 25 3.7 Expressiveness and modularity . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 eML F , Church-style ML F 30 4.1 Types, prefixes, and type relations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 4.2 Terms, typing rules, and type soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34 4.3 Translating System F into eML F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 4.4 Embedding ML into eML F . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 42 4.5 Type-preserving program transformations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 44

Figure 1 :

 1 Figure 1: Expressiveness of variants of ML F .

Figure 2 :

 2 Figure 2: The small hierarchy of ML F variants.

Figure

  Figure 3: Encodings

INRIA

Figure 4 :

 4 Figure 4: Typing rules for G(T , S, Q, ).

Var

Figure

  Figure 6: Syntactic type equivalence ⊏ -⊐in iML F .

(

  Proof p. 56) Definition 3.3.10 (Syntactic type instance) The syntactic instance relation is the smallest transitive and ≥-congruent relation on closed judgments satisfying rules of Figure 7.

Figure

  Figure 8: Translating iML F to F let .

Figure 9 :

 9 Figure 9: Type Congruence in eML F .

  eCon

  Definition 4.1.1 (Congruence) A relation R is ≥-congruent if it satisfies both eCon-FlexLeft and eCon-AllRight (Figure 9). It is congruent if it satisfies both eCon-AllLeft and eCon-AllRight. Definition 4.1.2 (Equivalence) The equivalence relation, written ≡, is the smallest congruent equivalence relation satisfying the rules of Figure 10.

Figure 11 :

 11 Figure 11: Type Abstraction in eML F .

  eAbs

  Definition 4.1.4 (Abstraction) The abstraction relation ⊏and the protected abstraction relation ⊏ -♯ are the smallest transitive relations satisfying the rules of Figure 11 and Rule eCon-AllRight.

  Definition 4.1.6 (Instance) The instance relation, written ⊑, is the smallest transitive and ≥-congruent relation satisfying the rules of Figure 12. Notice the inclusions (≡) ⊆ (⊏ -♯ ) ⊆ (⊏ -) ⊆ (⊑).

  Definition 4.3.3 The translation relation is the smallest relation on quadruples of the form (Q) t : (Q ′ , α)

Figure 14 :

 14 Figure 14: Translation of types and prefixes

  Proof of Lemma 4.1.11 Each statement is shown separately, by induction on the given derivation.Let us consider the equivalence relation first (statement i). Reflexivity is immediate. Transitivity and symmetry are by induction hypothesis. As for congruence (rules eCon-AllLeft and eCon-AllRight), we consider two cases:• Case ⇒-congruence: By hypothesis, σ 1 is ∀(α⇒σ a ) σ ′ a and σ 2 is ∀(α⇒σ b ) σ ′ b . The premises are (Q) σ a ≡ σ b and (Q, α ⇒ σ b ) σ ′ a ≡ σ ′ b . We have to show (Q ′ ) θ( σ ′ a [ σ a /α]) ⊏ -⊐θ( σ ′ b [ σ b /α]). By induction hypothesis, we have (Q ′ ) θ σ a ⊏ -⊐θ( σ b ) (1) and (Q ′ ) θ( σ ′ a [ σ b /α]) ⊏ -⊐θ( σ ′ b [ σ b /α]) (2). By Lemma 3.3.11.ii (page 23) and (1), we have(Q ′ ) θ( σ ′ a )[θ( σ a )/α] ⊏ -⊐θ( σ ′ a )[θ( σ b )/α], that is, (Q ′ ) θ( σ ′ a [ σ a /α]) ⊏ -⊐θ( σ ′ a [ σ b /α]).We conclude by transitivity and (2).• Case ≥-congruence: By hypothesis, σ 1 is ∀(α ≥ σ a ) σ ′ a and σ 2 is ∀(α ≥ σ b ) σ ′ b . The premises are (Q) σ a ≡ σ b and (Q, α ≥ σ b ) σ ′ a ≡ σ ′ b .By induction hypothesis, the former gives (Q ′ ) θ σ a ⊏ -⊐θ σ b (3). We consider two subcases:Subcase σ b / ∈ V: Then, we get by induction hypothesis(Q ′ , α ≥ θ( σ b )) θ σ ′ a ⊏ -⊐θ σ ′ b . By iCon-AllLeft, iCon-AllRight and (3), we get (Q ′ ) ∀(α ≥ θ( σ a )) θ σ ′ a ⊏ -⊐ -∀(α ≥ θ( σ b )) θ σ ′ b (4). If σ a /∈ V, this is the expected result. Otherwise, σ a ≡ β, which implies (Q) σ b ≡ β, and then by Lemma 4.1.7, σ b ≡ τ ′ (5) for some type τ ′ . Since σ b / ∈ V, this implies τ ′ / ∈ V (6). By iCon-AllLeft, (4) and (5), we have(Q ′ ) ∀(α≥ θ( σ a )) θ σ ′ a ⊏ -⊐ -∀(α≥ θ(τ ′ )) θ σ ′ a(7). By (6), we have θ(τ ′ ) ∈ I i . Hence, by iEqu-Inert applied to (5), we have (Q′ ) ∀(α ≥ θ(τ ′ )) θ σ ′ a ⊏ -⊐ -(θ( σ ′ a )[θ(τ ′ )/α], i.e. (Q ′ ) ∀(α ≥ θ(τ ′ )) θ σ ′ a ⊏ -⊐θ( σ ′ a [τ ′ /α])(8). We conclude by (8), (7), (4) and transitivity. Subcase σ b ∈ V: we assume σ b ≡ β. By induction hypothesis, we have (Q ′ ) θ( σ ′ a )[θ(β)/α] ⊏ -⊐θ( σ ′ b )[θ(β)/α]. From (3), we have (Q ′ ) θ σ a ⊏ -⊐θ(β) (9). If σ a ≡ γ, then (Q ′ ) θ σ a ⊏ -⊐θ(γ), and we get (Q ′ ) θ(γ) ≡ θ(β) from (

RR n°6228

Principal types should not be confused with principal typings(Wells,

2002).INRIA

The i stands for implicit.

Simple ML F was called Restricted ML F in (Le Botlan and Rémy, 2003;[START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF].

The e stands for explicit.

In the case where σ is a monotype τ , as in ML, α can be equivalently replaced by τ in x : α (indeed, monotypes can be inferred).INRIA

We use "≤" rather than ≤ F here, as we are about to extend the set of types and enlarge the type-instance relation accordingly.INRIA

Arguably, eML F could be considered half way between Curry style and Church style since some type reconstruction based on first-order unification is still needed for parameters of functions that are left unannotated.RR n°6228

Formally, this is only true if we restrict local bindings let x = a in a ′ to cases where x appears at least once in a ′ , or if we define the closure more precisely, as done for the language F let below.RR n°6228

The presentation of[START_REF] Pierce | Programming with Intersection Types and Bounded Polymorphism[END_REF] is in Church style, but this is irrelevant here.INRIA

Formally, this result has only been shown in Full eML F for closed expressions. INRIA

The problem disappears in the uncurrified form, but uncurrifying is not always possible, or it may amount to introducing anonymous functions with an explicit type annotation.RR n°6228

This has only been shown formally for a small variant of eML F (Le[START_REF] Didier | MLF: Raising ML to the power of System-F[END_REF][START_REF] Didier | MLF : Une extension de ML avec polymorphisme de second ordre et instanciation implicite[END_REF].RR n°6228

Acknowledgments

The authors are grateful to Boris Yakobowski for many technical discussions and his expertise on the graphic presentation of ML F . We express our gratitude to Daan Leijen and Dimitrios Vytiniotis whose interesting insight on ML F helped us improve the technical content of this article. We thank the anonymous referees for their precious comments.

Proofs of main results

Proof of Lemma 3.3.8 By structural induction on σ.

• Case α: Obviously, α is exposed in σ, therefore t must be inert. To conclude, observe that both { {⌊θ⌋(σ)} } and θ({ {σ} }) are equal to {t}.

• Case β with β = α: Then, both { {⌊θ⌋(σ)} } and θ({ {σ} }) are equal to {β}.

• Case τ 1 → τ 2 : Then, both { {⌊θ⌋(σ)} } and θ({ {σ} }) are equal to {θ(τ 1 ) → θ(τ 2 )}.

• Case ⊥: Let t ′ be in { {θ(⊥)} }, that is { {⊥} }, with α / ∈ ftv(t ′ ). Then θ(t ′ ) = t ′ , which we may also write t ′ ∈ θ({t ′ }). Thus, t ′ ∈ θ({ {⊥} }) holds.

• Case ∀(β ≥ σ 1 ) σ 2 : Let t ′ be in { {⌊θ⌋(σ)} } with α / ∈ ftv(t ′ ) (1). We may assume β # dom(θ) ∪ codom(θ) w.l.o.g. Then, ⌊θ⌋(σ) is equal to ∀(β ≥ ⌊θ⌋(σ 1 )) ⌊θ⌋(σ 2 ). By Definition 3.2.1, t ′ is of the form ∀(γ) t 2 [t 1 /β] with γ # ftv(⌊θ⌋(σ)), t 1 ∈ { {⌊θ⌋(σ 1 )} } and t 2 ∈ { {⌊θ⌋(σ 2 )} } (2). We may assume α / ∈ γ, w.l.o.g. If α is not exposed in σ, it must also be not exposed in σ 1 and in σ 2 by Definition 3.3.6. Moreover, (1) implies both α / ∈ ftv(t 2 ) and α / ∈ ftv(t 1 ). By induction hypothesis applied to (2), we get t 2 ∈ θ({ {σ 2 } }) and t 1 ∈ θ({ {σ 1 } }). That is, t 1 and t 2 are of the form θ(t ′ 1 ) and θ(t ′ 2 ) with t ′ 1 ∈ { {σ 1 } } and t ′ 2 ∈ { {σ 2 } }. Therefore, t ′ is equal to ∀(γ) θ(t ′ 2 )[θ(t ′ 1 )/β], which implies that t ′ is also equal to θ(∀(γ) t ′ 2 [t ′ 1 /β]). By definition 3.2.1, we have t ′ ∈ θ({ {σ} }), as expected.

Proof of Lemma 3.3.9

Each rule is considered separately.

• Case iEqu-Comm: Let σ a be ∀(α 1 ≥σ 1 ) ∀(α 2 ≥σ 2 ) σ and σ b be ∀(α 2 ≥σ 2 ) ∀(α 1 ≥σ 1 ) σ, with α 1 / ∈ ftv(σ 2 ) (1) and α 2 / ∈ ftv(σ 1 ) (2). Our goal is to show { {σ a } } = { {σ b } }, which implies the expected result θ({ {σ a } }) = θ({ {σ b } }) for all θ ∈ { {Q} }. By symmetry, it suffices to show { {σ a } } ⊆ { {σ b } }. Let t a be an F-type in { {σ a } }. We show that t a is also in { {σ b } } (3). By Definition 3.2.1, t a is of the form ∀( β) t ′ [t 1 /α 1 ] (4) with β # ftv(σ a ), t ′ ∈ { {∀(α 2 ≥σ 2 ) σ} }, and t 1 ∈ { {σ 1 } }. By Definition 3.2.1, t ′ is in turn of the form ∀( β′ ) t[t 2 /α 2 ] (5) with β′ # ftv(∀(α 2 ≥ σ 2 ) σ), t ∈ { {σ} }, and t 2 ∈ { {σ 2 } } (6). By α-conversion, we may assume, w.l.o.g., α 2 / ∈ ftv(t 1 ) ∪ {α 1 } (7) and β′ # ftv(t 1 ) ∪ {α 1 } ∪ ftv(σ 1 ). By inlining (5) in ( 4), it appears that t a is equal to ∀( β β′ ) t[t 2 /α 2 ][t 1 /α 1 ]. By (7), we may commute the two substitutions in t a and obtain ∀(

, which is included in { {σ 2 [t 1 /α 1 ]} } by Lemma 3.3.5. The latter equals { {σ 2 } }, given (1). In summary, t a is equal to ∀( β β′ ) t[t 1 /α 1 ][t ′ 2 /α 2 ] with t ′ 2 ∈ { {σ 2 } } and β β′ # ftv(σ b ), which implies (3) by Definition 3.2.1.

• Case iEqu-Free: Let σ with α / ∈ ftv(σ). We show { {σ} } = { {∀(α ≥ σ ′ ) σ} } by considering both inclusions separately. Assume t ∈ { {σ} }. We may as well assume α / ∈ ftv(t), w.l.o.g. Then, t is trivially of the form t[t ′ /α], by choosing some arbitrary t ′ in { {σ ′ } }, which implies t ∈ { {∀(α ≥ σ ′ ) σ} }. Conversely, assume t ∈ { {∀(α ≥ σ ′ ) σ} }. By Definition 3.2.1, it is of the form ∀( β) t ′′ [t ′ /α] with t ′′ ∈ { {σ} } and t ′ ∈ { {σ ′ } }. Thus, t ∈ ∀( β) { {σ} }[t ′ /α]. By Lemma 3.3.5, this implies t ∈ ∀( β) { {σ[⌊t ′ ⌋/α]} }, that is, t ∈ { {σ} } by Lemma 3.3.4.

• Case iEqu-Var is by definition and Lemma 3.3.4.

• Case iEqu-Inert: by hypothesis, (α ≥ σ ′ ) ∈ Q. Thus, Q is of the form (Q 1 , α ≥ σ ′ , Q 2 ) for some Q 1 and Q 2 . Let θ be in { {Q} }. By definition, a canonical decomposition of θ is of the form

, where τ is an inert type, this implies t a = ⌈τ ⌉ (9) by induction hypothesis. By Lemma 3.2.6, θ is equal to θ

Proof of Property 3.3.11

The proof of (i) holds by structural induction on the derivation. The proof of (ii) is by structural induction on σ.

INRIA

Proof of Lemma 3.3.12 Each rule is considered separately. Rule iIns-Equiv is by Lemma 3.3.9. Rule iIns-Bot is by definition. For Rule iIns-Subst, it suffices to show { {σ

Proof of Lemma 3.5.1

some variable α with α ∈ ᾱ, then ⌊t⌋ is equivalent to ⊥ by iEqu-Var, and we conclude directly by iIns-Bot. From now on, we assume t is not a variable α in ᾱ. As a consequence, all α's in ᾱ are not exposed in ⌊t⌋ (1). We have

We conclude by transitivity of ≤.

Proof of Theorem 1

By induction on the derivation of F :: Γ ⊢ a : t. Let Q be a prefix binding the free variables of Γ and t.

• Case Var: By hypothesis, we have x : t ∈ Γ. By definition of ⌊Γ⌋, we have x : ⌊t⌋ ∈ ⌊Γ⌋, and ⌊Γ⌋ is closed under Q. Hence, (Q) ⌊Γ⌋ ⊢ x : ⌊t⌋ holds by Var.

• Case App: Then, a is of the form a 1 a 2 and the premises are F :: Γ ⊢ a 1 : t 2 → t 1 and F :: Γ ⊢ a 2 : t 2 . Let Q ′ be an unconstrained prefix binding ftv(t 2 ) \ dom(Q). This implies dom(Q ′ ) # ftv(⌊A⌋) (1) and dom(Q ′ ) # ftv(t 1 ) (2). By induction hypothesis, we have both (QQ ′ ) ⌊Γ⌋ ⊢ a 1 : ⌊t 2 → t 1 ⌋ (3) and (QQ ′ ) ⌊Γ⌋ ⊢ a 2 : ⌊t 2 ⌋ (4). By definition, ⌊t 2 → t 1 ⌋ is ⌊t 2 ⌋ → ⌊t 1 ⌋. Hence, (3) becomes (QQ ′ ) ⌊Γ⌋ ⊢ a 1 : ⌊t 2 ⌋ → ⌊t 1 ⌋. By App, we get (QQ ′ ) ⌊Γ⌋ ⊢ a 1 a 2 : ⌊t 1 ⌋. By Gen and (1), we get (Q) ⌊Γ⌋ ⊢ a 1 a 2 : ∀(Q ′ ) ⌊t 1 ⌋. By equivalence (Inst and iEqu-Free with (2)), we obtain the expect result (Q) ⌊Γ⌋ ⊢ a 1 a 2 : ⌊t 1 ⌋.

• Case Inst: The premises are F :: Γ ⊢ a : t ′ and t ′ ≤ F t (5). By induction hypothesis, we have (Q) ⌊Γ⌋ ⊢ a : ⌊t ′ ⌋ (6). By Lemma 3.5.1 and (5), we have (Q) ⌊t ′ ⌋ ≤ ⌊t⌋. We conclude by Inst.

• Case Fun: The premise is F :: Γ, x : t 1 ⊢ a : t 2 . By induction, we have (Q) ⌊Γ⌋, x : ⌊t 1 ⌋ ⊢ a : ⌊t 2 ⌋. By Rule Fun, we get the expected result (Q) ⌊Γ⌋ ⊢ λ(x) a : ⌊t 1 ⌋ → ⌊t 2 ⌋.

• Case Gen: The premise is F :: Γ ⊢ a : t ′ and α / ∈ ftv(Γ) (7). By induction, we have (Q, α) ⌊Γ⌋ ⊢ a : ⌊t ′ ⌋. Besides, (7) implies α / ∈ ftv(⌊Γ⌋). By Rule Gen, we get (Q) ⌊Γ⌋ ⊢ a :

Proof of Lemma 3.6.1

By induction on the derivation of (Q) Γ ⊢ a : σ. We simultaneously show that for any x : ∧(t i ) i∈I in ∆, we have x : σ in Γ such that (θ(t i ) ∈ θ({ {σ} })) i∈I . All cases are straightforward, except iF-Inst, which relies on Lemma 3.3.12.

we conclude by property i. We assume now that neither σ ′ 1 nor σ ′ 2 are in V. Then, σ 1 is ∀(α ≥ σ 1 ) σ ′ and σ 2 is ∀(α ≥ σ 2 ) σ ′ . We conclude by induction hypothesis and (10).

• Case eEqu-Inert : σ 1 is ∀(α ≥ σ) σ ′ and σ 2 is ∀(α ⇒ σ) σ ′ . By hypothesis, σ is inert in eML F . As a consequence, σ is inert in iML F (this is an easy consequence of the definition). Hence, we get the expected result by iEqu-Inert.

The instance relation (statement iii) is shown similarly. Transitivity is by induction hypothesis. Flexiblecongruence is shown as above (see the equivalence case), using iIns-Subst if the right-hand side is in V. eIns-Abstract is a consequence of ii and iIns-Equiv. eIns-Bot is shown with iIns-Bot. eIns-Hyp is shown with iIns-Hyp. Finally, eIns-Rigid is shown with iIns-Subst, using Lemma 4.1.9 (page 33).

Proof of Lemma 4.1.12 By structural induction on σ. Both cases ⊥ and β (with β = α) are immediate. We remind that ≡ is a subrelation of ⊏ -♯ .

•

. By eAbs-Hyp, we get ( Q ) α ⊐σ ′ . We conclude by (1).

• Case σ = τ 1 → τ 2 is by induction hypothesis and eAbs-SharpLeft.

• Case σ = ∀(α ≥ σ 1 ) σ 2 is by induction hypothesis and eAbs-Left.

Proof of Lemma 4.1.14 i) is shown by induction on the derivation of (Q) σ 1 ⊏ -⊐σ 2 . Reflexivity, transitivity, and symmetry are immediate by definition of (⊏ -♯ ∪ ⊐ -♯ ) * .

• Case iEqu-Comm: by Rule eEqu-Comm.

• Case iEqu-Free: by Rule eEqu-Free.

• Case iEqu-Inert: by Lemma 4.1.12 and induction hypothesis.

• Case iEqu-Var: by Rule eEqu-Var.

Congruence of ⊏ -⊐is defined by rules iCon-AllLeft, iCon-AllRight, and iCon-Arrow: • Case iCon-AllLeft: by induction hypothesis and Rule eAbs-Left.

, where the binding of α is rigid if σ is equivalent to an inert type τ , and flexible otherwise. By Rule eCon-AllRight, we get

). If σ is not equivalent to a monotype, this is the expected result. Otherwise, (∅) σ ⊏ -⊐τ holds and we derive (

hold by eEqu-Inert. We conclude by doing the same derivation for the right-hand side of (1) and transitivity.

hold, and so by induction hypothesis, we get both (

• Case iIns-Equiv: by property i), and rules eAbs-SharpDrop and eIns-Abstract.

• Case iIns-Bot: by eIns-Bot • Case iIns-Hyp: by eIns-Hyp, eAbs-Hyp and eAbs-SharpLeft.

• Case iIns-Subst: by eIns-Rigid and Lemma 4.1.13.

The ≥-congruence of ≤ is defined by the rules iCon-AllLeft and iCon-AllRight. • Case iCon-AllLeft: by induction hypothesis and Rule eCon-FlexLeft.

• Case iCon-AllRight: similar to case iCon-AllRight above.

Proof of Theorem 3

By a simple induction on the typing derivation of (Q) Γ ⊢ a : σ. The interesting cases are Annot and Inst, which immediately follow from properties 4. 1.11.ii (page 34) and 4.1.11.iii (page 34).

Proof of Theorem 4

The proof is constructive as it explicitly builds the translated term a ′ . Thus, an algorithm that returns a ′ given a derivation of a could extracted from the proof. By induction on the derivation of iML F :: (Q) Γ ⊢ a : σ.

• Case Var: necessarily, a is a variable x such that x : σ belongs to Γ, and so x : σ belongs to Γ . We conclude by Rule Var, taking a ′ = x.

• Case Fun: a is of the form λ(x) b, σ is τ → τ ′ , and the premise is iML F :: (Q) Γ, x : τ ⊢ b : τ ′ . By induction hypothesis, there exists b ′ (with type erasure b) such that eML F ::

We get (5) by equivalence from (4) (Rule Inst and Rule eEqu-Var). We obtain ( 6) by Rule UnGen ⋆ , and ( 7) by Rule Fun ⋆ . By Rule Gen, we get (8), which is equal to the expected result (9).

• Case App: a is a 1 a 2 , and the premises are iML

where τ 1 is σ. By induction hypothesis, there exist both a ′ 1 and a ′ 2 (with respective type erasures a 1 and a 2 ) such that eML F :: 14). By induction hypothesis, there exists a 0 such that eML F :: ( Q ) Γ ⊢ a 0 : σ ′ . By Lemma 4.1.14.ii and ( 14

We show by induction on i, for i n, that there exists a i with type erasure a, such that ( Q ) Γ ⊢ a i : σ i (15). Then, the expected result ( Q ) Γ ⊢ a ′ : σ is obtained with i = n -1 and a ′ = a n-1 . The judgment (15) holds for i = 0, as shown above. By induction hypothesis, we assume it holds for some i < n. If i is even, we get judgment (15) for i + 1 using Rule Inst. If i is odd, we get judgment (15) for i + 1 using Rule Annot, taking a i+1 = (a i : σ i+1 ). In fact, the sequence of instance and annot could be rearranged into a single instance followed by a single annotation, as

However, a proof of this commutation lemma, which has been done in the graphical presentation, would be very tedious, syntactically.

• Case Gen: The premise is iML F :: (Q, α≥σ 1 ) Γ ⊢ a : σ 2 , with α / ∈ ftv(Γ), and σ is ∀(α≥σ 1 ) σ 2 . By induction hypothesis, there exists a ′′ such that eML F :: ( Q, α≥σ 1 ) Γ ⊢ a ′′ : σ 2 (16). Let ∀(Q 1 ) σ ′ 1 be σ 1 , with Q 1 rigid and as large as possible. Then ( 16

We notice that the domain of Q 1 can be chosen disjoint from ftv(Γ). By repeated uses of Rule Gen, we get (

σ 2 holds by eCon-AllRight, eAbs-Left, and repeated uses of eAbs-Hyp, we conclude by Rule Annot, taking a ′ = (a ′′ : σ ).

• Case Let: by induction hypothesis and Rule Let.

Proof of Lemma 4.3.7

This is a particular case of the following result, taking P , P ′ , and P ′′ empty. In the following, P ′ may be an empty prefix or a prefix starting with an unconstrained binding. Similarly for P ′′ . Also, P and Q must be rigid (Q is indeed rigid in the Lemma, since it is returned under an empty input prefix).

(P P ′ ) t : (P QP ′′ , α) P QQ ′ P ′′ well-formed (P QQ ′ P ′ ) t : (P QQ ′ P ′′ , α) This is shown by structural induction on t.

INRIA

Proof of Lemma 4.3.9

To lighten the notation in this proof and subsequent ones, we let Q mean dom(Q) and α mean {α} when a set of variables is non-ambiguously expected from context. For example, given a set of variables J, a variable α, and a prefix Q, we may write

This lemma is a simplification of the invariant stated further, making also use of the following result, which is shown by structural induction on t (we omit its proof)

Lemma 4.3.9 is not strong enough to be proved directly. Instead, we consider the following huge much stronger invariant, (we recover the Lemma by taking P , P ′ 1 , P ′ 2 empty, I = ftv(t) and using the previous short result to introduce the unconstrained binding (α) in prefixes).

Assume, moreover, that one of the following set of condition holds:

Then, there exists a set J and a renaming φ such that

We show the result for each of the two sets of conditions separately. The first result is shown by induction on

The second result is shown by structural induction on t.

First result: Instead of showing ftv(P ′ 1 ) ⊆ J ∪ α (last predicate), we show ftv(P ′ 1 ) ⊆ I ∪ α, which is stronger. Also, the hypothesis dom(

, we take φ = id. Otherwise, let φ be the renaming of domain {α 1 , α 2 } that swaps α 1 and α 2 . The binding (α

) by reflexivity. Also, ftv(P ′ 1 ) ⊆ ftv(P ) ∪ ftv(σ)dom(P ) which implies ftv(P ′ 1 ) ⊆ I ∪ α. • Case Transitivity: To ease readability (with respect to indices), we assume

hold and we show the conclusion where the index 2 is replaced by 3. We take α 2 such that Q 2 αP α2 σ is defined (it always exists). By renaming, we may also freely assume α 2 / ∈ dom(Q 2 P 2 ) =⇒ α 2 / ∈ I. The hypotheses are

By induction hypothesis and (1), there exist J 1 and φ 1 such that

Note that ( 7), (3), and (4) imply φ 1 (P ) = P and φ 1 (σ) = σ. From (2), we get φ 1 (Q 2 ) ≡ I φ 1 (Q 3 ). From ( 5) and ( 6), we get the following:

By ( 10) and ( 11), the former gives

By induction hypothesis, there exist J 2 and φ 2 such that

Let φ be φ 2 • φ 1 and J be J 1 ∩ J 2 . We have to show the following:

We have ( 18) as a consequence of of ( 7) and ( 13). From ( 8) and ( 14), we have 9). The latter implies α 1 ∈ J 2 from ( 14). Consequently, if

This implies ( 19). We get (20) from ( 9) and ( 15). Also, ( 21) is ( 16), ( 22) is ( 17), and ( 23) is ( 12). This concludes the case.

• Case Symmetry: by induction hypothesis and by taking φ -1 (J) for J and φ -1 for φ.

• Case eSha-Comm: Similar to reflexivity.

If α 1 = β, then we take φ = id and J = I ∪ α 1 . Otherwise, φ is the renaming of domain {α 1 , β} swapping α 1 and β. In both cases,

Second result (by structural induction on t):

• Case β:

We get the expected result by taking J = I and φ = id.

• Case t 1 → t 2 : By hypothesis, we have ftv(t) ⊆ I ∪ αP (24) as well as

By induction hypothesis, ( 25) and ( 26), there exist a set J 1 and a renaming φ 1 such that

Note that (31) and ( 24) imply φ 1 (t) = t. By Lemma 4.3.5 (page 39) and (28), we get

INRIA By induction hypothesis (taking J 1 for I), (32) and ( 27), there exist a set J 2 and a renaming φ 2 such that

The results above can be rewritten like this:

By applying φ ′ to (30), we get

Then, by using the first result of the Lemma, there exists a set J and a renaming ψ such that

• Case ∀(β) t 0 : By hypothesis, we have

By induction hypothesis, there exist a set J ′ and a renaming φ ′ such that

Note that (37) implies both φ ′ (P a 2 ) = P a 1 and φ ′ (P b 2 ) = P b 1 . Additionally, (38) implies both ftv(P a 1 ) ⊆ J ′ ∪ α and ftv(P b 1 ) ⊆ J ′ ∪ αβP a 1 . From (36), we have

By using the first result of the lemma, there exists a set J and a renaming ψ such that

Let φ be ψ • φ ′ . We have

This is the expected result.

Proof of Corollary 4.3.10

In order to lighten the presentation, we use the notations defined in the proof of Lemma 4.3.9. Let (Q ′ , α ′ ) be the translation of t under an empty prefix (formally, (∅) t : (Q ′ , α ′ ) (1) holds). We show below that, for any σ in t , we have (Q) σ ≡ ∀(Q ′ ) α ′ (2) under any suitable Q. Indeed, we then have ∀(Q) σ i ≡ ∀(Q ′ ) α ′ for i in {1, 2} and the result follows by symmetry and transitivity of ≡.

Let us show (2). Let I be ftv(t) and σ in t . By hypothesis, there exist shared rigid prefixes Q 1 and Q ′ 1 such that:

Using ( 5) and eSha-Free repeatedly, one may derive ∅ ≡ I Q 1 . By Lemma 4.3.9 (page 40), there exist a set J and a renaming φ such that

From ( 8), ( 7), and Lemma 4.3.8 (page 39), we get (Q) 6). Therefore, ( 9) can be written

Proof of Property 4.3.11

Both properties are shown by induction on

Proof of Lemma 4.3.12 Each property is shown separately. P-i: By hypothesis, Q α ′ σ is defined and ψ(Q) ----> φ Q ′ (1) holds. Also, φ • ψ(σ) ----> σ ′ (2) holds. There are two subcases:

Let i be the index corresponding to the insertion of (α ′ ⇒σ). Then,

We distinguish two other subcases: either (γ ⇒ σ ′ ) ∈ Q ′ for some γ or not. In the latter case,

We now consider the last remaining case, when (γ

By induction hypothesis and (3), there exist Q a 2 , α a 2 and φ a such that

By induction hypothesis and ( 4), there exist

2 holds. Thus, Property P-i and ( 7), imply that there exists φ c such that dom(φ c ) ⊆ {α 1 } (8) and 5) and ( 6), we have 10). This is the expected result.

Subcase ∀(γ) t ′ : By hypothesis, (Q

Thus, by induction hypothesis, there exist

We note that (12) implies that there exist φ b and φ c such that 13) and ( 15), we may use Property P-i with ( 14) which provides 11) and ( 17)), and 16) and noting that ψ(α 1 ) = α 1 ). P-iii: Let θ be the substitution [t ′ /β]. Property P-iii is a particular case of the following rule, taking P = ∅:

The proof is by structural induction on t.

• Case t = γ with γ = β: Then, P ′ = P and α ′ = γ. The result is immediate.

• Case t = β: Then, ψ(t) is α and so P ′ is P and α ′ is α. Using Lemma 4.3.7 (page 39), we have (Q ′ P ) t ′ : (Q ′ P, α), which is the expected result.

• Case t 1 → t 2 : by induction hypothesis.

• Case ∀(γ) t 1 : by induction hypothesis.

Proof of Lemma 4.3.13

By structural induction on t. We assume (Q 1 βQ 2 P ) t : (Q ′ 1 βQ ′ 2 P ′ , α) holds (1). • Case t is γ: In order for (1) to hold, α must be γ and Q 1 βQ 2 P must be Q ′ 1 βQ ′ 2 P ′ (exactly in the same order). Hence

By induction hypothesis applied to (2) and (3), we get (

, or P b , and as left as possible. If α was inserted in 6) By induction hypothesis applied to (6), we get (Q 3 P γ) t a :

RR n°6228

This follows by a case analysis as in the previous case.

Proof of Theorem 5

By induction on F :: Γ ′ ⊢ a : t (1). Let Γ be in Γ ′ . Thanks to Corollary 4.3.10 (page 40) and Inst, it suffices to show eML F :: (Q) Γ ⊢ a ′ : σ for one σ in t instead of all of them. By default, we let typing judgment be in eML F .

• Case Var: a is x and (1) implies x : t ∈ Γ ′ . Hence, x : σ ∈ Γ with σ ∈ t . By Var, we have (Q) Γ ⊢ x : σ, which is the expected result.

• Case App: a is a 1 a 2 and (1) implies F :: Γ ′ ⊢ a 1 : t 2 → t (2) and F :: Γ ′ ⊢ a 2 : t 2 (3). Let ∀(Q ′ ) α be in t 2 → t . By definition, there exists a prefix Q 0 such that (Q 0 ) t 2 → t : (Q ′ , α) holds. The premises of this judgment are (Q 0 ) t 2 : (Q 1 , α 1 ) and (Q

By induction hypothesis and (2), there exists a ′ 1 such that (Q) Γ ⊢ a ′ 1 : ∀(Q ′ ) α. We note from ( 5) that (Q) ∀(Q ′ ) α ≡ ∀(Q 2 ) α 1 → α 2 holds by eEqu-Var. Thus, by Inst and eEqu-Var, we have

By induction hypothesis and (3), there exists

holds by Inst. From App ⋆ (page 24), ( 6) and ( 7), we get

We conclude by taking a ′ = a ′ 1 a ′ 2 and noting that ∀(Q 2 ) α 2 ∈ t holds from (4).

• Case Fun: a is λ(x) a 1 , and (1) implies that t is t 1 → t 2 and F :: Γ ′ , x :

By induction hypothesis and ( 8), there exists a ′ 1 such that (QQ 2 ) Γ, x : 10) holds by eEqu-Free. Then, the following holds:

from (9) Thus, by Inst, we get (Q) Γ ⊢ a ′ : ∀(Q ′ ) α. This is the expected result.

• Case Gen: (1) implies that τ is of the form ∀(α) t ′ with α / ∈ ftv(Γ ′ ) and F :: Γ ′ ⊢ a : t ′ (11). Let Q ′ and α ′ be such that (∅) ∀(α) t ′ : (Q ′ , α ′ ). The premise is (α) t ′ : (Q 1 αQ 2 , β) (12) and Q ′ is Q 1 α ′ ∀(αQ 2 ) β (13). By Lemma 4.3.13 (page 41) and ( 12), there exists 14). Thus, by induction hypothesis and (11), there exists a ′ such that (Qα) Γ ⊢ a ′ : ∀(Q 3 ) β holds. From ( 14), we get (Qα)

By eEqu-Comm and Inst, we get (Q) Γ ⊢ a ′ : ∀(Q 1 αQ 2 ) β. We get the expected result by noting that (Q) ∀(Q ′ ) α ′ ≡ ∀(Q 1 αQ 2 ) β holds from (13).

• Case Inst: (1) implies that t is of the form t 0 [t ′ /β] and F :: Γ ′ ⊢ a : ∀(β) t 0 (15). Let (Q ′ , α) be such that (∅) t ′ : (Q ′ , α) (16) and ftv(t) # dom(Q ′ ) (17) hold. We may freely assume that β /

By induction hypothesis and ( 15), there exists a ′ such that (Q) Γ ⊢ a ′ : ∀(Q 0 ) α 0 holds. From ( 19) and Inst,

Let ψ be [α/β]. From (18), we have β / ∈ dom(Q 1 ) ∪ ftv(Q 1 ). Therefore, ψ(Q 1 ) = Q 1 . Then, we derive the following:

(

From ( 18) and Lemma 4.3.13, there exists

Then, by Property P-ii and ( 17), there exist Q ′ 2 , α 2 and φ ′ such that

From ( 21), ( 22), and Inst, we get (Q) Γ ⊢ a ′ : ∀(ψ(Q 3 )) ψ(γ) (26). From ( 24) and Lemma 4.3.11.ii (page 40), we have

2 ) α 2 (27) by Inst and (26). From ( 23) and P-iii, we get (Q ′ ) t : (Q ′ 2 , α 2 ), which implies ∀(Q ′ 2 ) α 2 ∈ t and so ( 27) is the expected result.

Proof of Property 4.4.2

Each property is proved by induction on the derivation. Properties i and iii are easy. As for ii, the case eAbs-Hyp is replaced by eIns-Hyp and congruence is replaced by flexible congruence. Finally, eIns-Rigid is replaced by reflexivity (that is, by the equivalence relation).

Property ii): As a preliminary result, we show the same property for equivalence, that is, if (Q) σ 1 ≡ σ 2 holds, then θ( σ 1 ) and θ( σ 2 ) are equivalent in ML. The proof is by induction on the derivation of (Q) σ 1 ≡ σ 2 . Transitivity is by induction hypothesis. Reflexivity and symmetry are immediate: the ML equivalence relation is reflexive and symmetric. For congruence, the proof is similar to the one for the instance relation (see below). It remains to consider the following cases:

• Case eEqu-Free: We may as well add or remove useless binders in an ML type scheme.

• Case eEqu-Comm: We may as well commute binders in an ML type scheme.

• Case eEqu-Var: By definition, ∀(α ≥ σ) α and σ are identical.

• Case eEqu-Mono: Then σ 2 is of the form σ 1 [τ /α] and the premise is

• θ 2 with θ 1 and θ 2 being the substitutions associated with Q 1 and Q 2 respectively. By well-formedness, ftv(τ ) # dom(θ 2 ) and α / ∈ dom(θ 2 ). As a consequence, we also have

. This implies the expected result by reflexivity of ≤ ML . The ends the proof for the case of equivalence.

The proof for the general case is by induction on the derivation of (Q) σ 1 ⊑ σ 2 . Transitivity is by induction hypothesis and transitivity of the ≤ ML . Rule eIns-Rigid cannot occur since it mentions a rigid binding, whereas the derivation is assumed to be flexible.

• Case eIns-Bot: ∀(α) α ≤ ML σ holds for any ML type σ.

• Case eIns-Hyp: We have (α≥ σ 1 ) ∈ Q and σ 2 is α. Let ∀( β) τ 1 be σ 1 and (ᾱ, θ) be Q . By definition of Q , θ(α) = θ(τ 1 ) (1). Besides, θ(∀( β) τ 1 ) is ∀( β) θ(τ 1 ) (2), and ∀( β) θ(τ 1 ) ≤ ML θ(τ 1 ) (3) holds. By combining (2), (3), and (1), we have θ(∀( β) τ 1 ) ≤ ML θ(α), as expected.

• Case eIns-Abstract: The premise is (Q) σ 1 ⊏σ 2 . Necessarily, we have (Q) σ 1 ≡ σ 2 (Rule eAbs-Equiv), because other possible rules for abstraction mention rigid bindings. Then, we conclude using the preliminary result.

• Case Flexible Congruence: We recall the congruence rule:

Keeping the notations of this rule, we have to show θ( ∀(α ≥ σ 1 ) σ ′ 1 ) ≤ ML θ( ∀(α ≥ σ 2 ) σ ′ 2 ) (6). Let ∀( ᾱ1 ) τ 1 be σ 1 and ∀( ᾱ2 ) τ 2 be σ 2 . By induction hypothesis and (5), we have θ(∀( ᾱ1 ) τ 1 ) ≤ ML θ(∀( ᾱ2 ) τ 2 ) (7) Using the definition of • , we may rewrite (6) as follows:

We show this result in two steps, as follows:

The first step ( 8) is a consequence of Lemma 4.4.4 (page 43) and ( 7). The second step ( 9) is by induction hypothesis applied to (4).

Proof of Lemma 4.4.7

By induction on the derivation. Case Var is immediate. Cases Fun, App, and Let are by induction hypothesis.

Case Inst is a direct consequence of Property 4.4.6.ii (page 43). Case Gen: The premise is (Q, α≥σ 1 ) Γ ⊢ a : σ 2 . Let ∀( β) τ 1 be σ 1 (1), and θ 1 be [τ 1 /α] (2). We choose β such that β # ftv(Γ) (3). By definition, we have (Q, α ≥ σ 1 ) = (ᾱ β, θ • θ 1 ). By induction hypothesis, we have θ • θ 1 ( Γ ) ⊢ a : θ • θ 1 ( σ 2 ) in ML. Since α / ∈ ftv(Γ), we have θ 1 ( Γ ) = Γ . Hence, θ( Γ ) ⊢ a : θ • θ 1 ( σ 2 ) holds. From (3), we get by Rule Gen of ML, θ( Γ ) ⊢ a : ∀( β) θ • θ 1 ( σ 2 ). Notice that ∀( β) θ • θ 1 ( σ 2 ) is equal to θ(∀( β) θ 1 ( σ 2 )), which, by definition of • , (1), and ( 2) is also θ( ∀(α ≥ σ 1 ) σ 2 ). We thus have θ( Γ ) ⊢ a : θ( ∀(α ≥ σ 1 ) σ 2 ), as expected.

Proof of Theorem 9

Direct consequence of Lemmas 4.4.7 and 4.4.3.

Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, revised edition, 1984. ISBN 0-444-86748-1. ⊲ Gilles Dowek, Thérèse Hardin, Claude Kirchner, and Frank Pfenning. Higher-order unification via explicit substitutions: the case of higher-order patterns. In M. Maher, editor, Joint international conference and symposium on logic programming, pages 259-273, 1996.

⊲ Jacques Garrigue and Didier Rémy. Extending ML with Semi-Explicit higher-order polymorphism. Journal of Functional Programming, vol 155, pages pages 134-169, 1999. A preliminary version appeared in TACS'97.

INRIA