Luca Cardelli

Xavier Leroy

Abstract types and the dot notation

Introduction

Type abstraction has emerged as one of the most important techniques for specifying and building large software systems [START_REF] Liskov | Abstraction and Specification in Program Development[END_REF][START_REF] Guttag | The Larch Family of Specification Languages[END_REF], since it provides fundamental typing support for modularization [START_REF] Parnas | On the criteria to be used in decomposing systems into modules[END_REF].

Abstract types (sometimes called opaque types) are therefore one of the necessary features of modern programming languages. However, for a long time their standing has been rather mysterious, and their type rules have been explained in ad-hoc and operational ways, making formal reasoning about abstract types difficult. For example, it is still commonly said that an opaque type is "different from any other type in the system when seen from outside the abstraction", or that a new abstract type is "created" whenever its description is evaluated. Such statements are both informal and arbitrary; clearly, a formal background is needed to define precisely what type abstraction means, derive sensible typechecking rules, and reason about programs using abstract types.

In an attempt to fill this need, Mitchell and Plotkin [START_REF] Mitchell | Abstract types have existential type[END_REF] made an important connection between type abstraction and the second-order existential quantifiers of logic. They proposed that an abstraction-that is, an abstract type A, together with operations f, g, . . . whose types F, G, . . . normally involve A-should be viewed as an "existential" statement. That is, there should exist a concrete type representation of A and an implementation of the operations f, g, . . . such that f, g, . . . have the types F, G, . . ., respectively 1 . For instance, a package implementing complex numbers could be specified by the existential type shown in figure 1; two different implementations meeting this specification are shown in figure 2. An abstraction is therefore an assertion that adequate implementations exist; it provides a partial specification of such implementations. These existential statements might be false, in which case the specification of the abstract type should be seen as inconsistent.

The approach of Mitchell and Plotkin showed for the first time that the type rules for abstract types could be described non-operationally, by looking at the well-known rules of constructive logic from the standpoint of programming. It also provided the necessary formal framework for proving fundamental properties of abstract types, such as representation independence [START_REF] Reynolds | Towards a theory of type structure[END_REF][START_REF] Mitchell | Representation independence and data abstraction (preliminary version)[END_REF].

The connection between this approach to type abstraction and the notion of type abstraction found in several modern programming languages is however not complete. These languages use a dot notation, such as a.f , to refer to an operation f provided by an abstraction a, or in other words, to the field named f of module a. The type theory approach provides an elimination construct that looks totally different, for the same purpose . We set out in this paper to investigate this difference in notation, explore type Complex = ∃C. make : let square = λx : complex .C. (complex .mul x x) in complex .re(square(complex .make 2 3))

Real → Real → C re : C → Real im : C → Real mul : C → C → C . . .
Figure 4: Using a package with the dot notation also whether there is a difference in expressive power, and try to relate both notations, in the hope of filling one of the remaining gaps between the theory and the practice of type abstraction.

The "logical" notation for abstraction uses a construct, which we call open here, corresponding to the logical rule for existential elimination. Namely, given a package p implementing an abstraction A, f, g, . . ., we can open the package p, bind its components to variables A , f , g , . . ., and use such variables in a usage scope (following in):

p : ∃A. f, g, . . . open p as A , f , g , . . . in . . . A . . . f . . . g . . .
The result of this expression is the result of the subexpression following in. Figure 3 shows how the complex arithmetic package above can be used with this notation. Additional examples using this notation can be found in Cardelli and Wegner [START_REF] Cardelli | On Understanding Types, Data Abstraction, and Polymorphism[END_REF].

It is easy to see why abstraction is enforced. Although A may be implemented in p as, say, Int, A is a formal variable and cannot match any type except itself. This corresponds to the informal idea that abstract types are "different from any other type". There is also a crucial restriction that the type variable A should not escape its scope: it must not appear free in the type of the result of open or in the types of global variables.

Existential types provide a fully satisfactory theoretical solution to the problem of modelling abstract types. However, the open notation is very clumsy for programming purposes; if a package is opened twice, the two abstract type variables thus introduced will not match. Hence one must find a sufficiently large usage scope around which to place the open construct without violating the typing rules; MacQueen [START_REF] Macqueen | Using Dependent Types to Express Modular Structure[END_REF] points out that the required usage scope may be so large that most benefits of abstraction are lost.

This difficulty motivated MacQueen to take a different approach to abstraction, using dependent types and general sums [START_REF] Macqueen | Using Dependent Types to Express Modular Structure[END_REF]. His approach is adequate for modules (when they are not first-class values, as in Standard ML [START_REF] Macqueen | Modules for Standard ML[END_REF]), but not for abstract types, since packages must now necessarily stop being first-class values to preserve typing decidability [START_REF] Mitchell | The Essence of ML[END_REF]. In addition, general sums do not ensure abstraction by themselves; hence, Standard ML provides a separate abstraction construct. Independently, programming languages providing facilities for type abstraction were developed, and most of them use a different notation. This programming notation uses a dot operator to select the components of a package, including selecting the abstract type when it is in a type context: p : ∃A. f, g, . . . . . . p.A . . . p.f . . . p.g . . .

See figure 4 for a reformulation of the example above using this notation.

This dot notation has proved very convenient for actual programming, especially for programming in the large. However, it does not lend itself to formalization as readily as the open notation.

One difficulty with the dot notation is that the name A is bound and can be renamed: ∃A.B = ∃A .B{A←A }. Hence what does p.A really mean? Similarly, how are the names f, g, . . . handled? Programming languages seem to avoid this problem by rejecting αconversion of existential variables. Here we circumvent the problem by using positions instead of names: p.Fst refers to the type component of an abstraction, and p.snd to the operation-set component.

Apart from this difficulty, the main problem is that we no longer have a precise notion of the usage scope of a package. If p.A always matches (another occurrence of) p.A, why should it not match Int, or some other type? Moreover, p.A (or p.Fst) is now a type; hence we have introduced value expressions as subexpressions of type expressions. Should p.A match p .A only if p = p ? Or if p and p have the same normal form? Clearly some restriction should be imposed here to preserve typing decidability.

Finally, are packages first-class values? In Modula-2 for instance, modules are not firstclass values. In this paper, we wish to avoid this additional stratification, and assume that the p in p.A is a first-class value, so we can handle general abstract types and not just modules. Alternatively, we are assuming that our modules are first-class values and that multiple implementations of an interface can coexist [START_REF] Cardelli | Typeful Programming[END_REF]. But should we require p in p.A to be a simple identifier x, as in most programming languages, or a sequence x.y.z . . . ? Or can we allow p to be an arbitrarily complex expression, provided that it has no side-effect, and that equality of two such expressions is decidable?

If we had a translation between some flavor of dot notation and the open notation, we could avoid answering directly all such hard questions about the dot notation. We should not be afraid of losing expressiveness in the translation, since we believe existential types characterize the correct notion of abstraction.

The main question then that this paper addresses is under which circumstances is the dot notation equivalent to the open notation? First, in section 2, we introduce a simple calculus with the open notation, intended to serve as a reference point. We give typechecking rules, denotational semantics, and show the soundness of the type system. In section 3, the open elimination construct is replaced by a simplified dot notation, consisting of two projections, .Fst and .snd, that are syntactically restricted to apply to simple variables only. Then we prove that the calculus thus obtained is equivalent to the former one by translating one calculus into the other. The translations are reasonably faithful, since they preserve both typing and semantics. Finally, in section 4, we lift the restriction on .Fst and .snd, and allow them to operate on any term; it seems that not all terms of this calculus with generalized dot notation have equivalents in the original calculus with open; however, we characterize a large class of terms that can be encoded in the open notation, while retaining typing and semantics.

A simple calculus with abstract types

The calculus in this section is based upon the usual simply typed λ-calculus, extended with constants and primitive operations as needed (such as integers, booleans and pairs, though we shall axiomatize only integers for simplicity.) To model type abstraction, we add existential quantification on types, and two term constructors: second-order dependent pairs and the open construct. These term constructors correspond to the introduction and elimination rules for existential quantification in constructive logic.

Syntax

In the following, X and Y range over a given countable set of type variable identifiers, A and B range over the class of types, similarly, x and y range over the set of term variable identifiers, and a, b, c range over the class of terms.

A ::= X | A → B | ∃X. A a ::= x | λx : A. b | b(a) | X = A, b : B | open a as X, y : B in b
The construct X = A, b : B builds a second-order dependent pair. This is basically a pair of a type A and a term b of type B; however, b and B may depend on the binding X = A; that is, X may appear in b or in B, and is considered to be bound to A there. This binding is not visible outside of the pair; in particular, the type of the pair is simply ∃X. B, without any mention of A.

The elimination construct open a as X, y : B in b evaluates a to a pair, binds X to its internal type and y to its value, and returns the value of b in this new environment. The variable X gets bound in B and b; y is bound in b.

For some purposes, we also consider the calculus above extended with integer constants:

A ::= . . . | Int a ::= . . . | 0 | succ(a) | case a of 0: b, succ(x): c
The pattern-matching construct case a of 0: b, succ(x): c subsumes test for zero, the predecessor function, and the usual if . . . then . . . else construct; x is considered bound (to the predecessor of a) in c.

As usual, expressions are identified up to a renaming of bound variables.

Typechecking

We specify the typing of terms of this calculus by a system of inference rules. The rules define the judgment "term a has type A under the assumptions E", written E o a : A.

The assumptions are either "variable x has type A" or "identifier X is a valid type variable", hence the syntax of typing environments E is as follows:

E ::= ∅ | E, X | E, x : A.
We write Dom(E) for the set of variables introduced in E, that is:

Dom(∅) = ∅ Dom(E, X) = Dom(E) ∪ {X} Dom(E, x : A) = Dom(E) ∪ {x}
However, we must put additional constraints on the environments, to ensure that type variables are introduced in the environment before being used in types. So we have to define two more judgments: "typing environment E is well-formed", written o E env; and "type A is valid in environment E", written E o A type, as follows.

o ∅ env o E env X / ∈ Dom(E) o E, X env E o A type x / ∈ Dom(E) o E, x : A env o E env E o Int type o E, X, E env E, X, E o X type E o A type E o B type E o A → B type E, X o A type E o ∃X. A type
We can now give the typechecking rules for terms. The first rules are exactly those of the simply typed λ-calculus:

o E, x : A, E env E, x : A, E o x : A E o A type E, x : A o b : B E o λx : A. b : A → B E o b : A → B E o a : A E o b(a) : B
Typing rules for integers are straightforward:

o E env E o 0 : Int E o a : Int E o succ(a) : Int E o a : Int E o b : A E, x : Int o c : A E o case
E o A type E o b{X←A} : B{X←A} E o X = A, b : B : ∃X. B
If a has an existential type ∃X. B, then an open a as X, y : B in c construction has the same type as c. The term c is considered in an environment where the type variable X is defined and the term variable y has type B. Inside c, the type X is a formal variable, which cannot match any type except itself. To ensure that X does not escape the scope of the open expression, we require that X is not free in the type C of the body c. This is ensured by requiring that C is a valid type in the original environment E, in which X is unbound.

E o a : ∃X. B E o C type E, X, y : B o c : C E o open a as X, y : B in c : C It is easy to see that E o a : A implies E o A type, which implies o E env in turn.
This fact is used implicitly in the rules above.

Evaluation

The usual approach to evaluation would be to define reduction rules on the typed terms; following Mitchell and Plotkin [START_REF] Mitchell | Abstract types have existential type[END_REF], we could take, for instance:

(λx : A. b)(a) → b{x←a} open X = A, b : B as X, y : B in c → c{y←b}{X←A}
plus some rules for constants. However, these rules do not identify terms that intuitively have exactly the same meaning, for instance

open x as Y, z : Int in succ(z) and succ(open x as Y, z : Int in z).
Though the open a as . . . construct performs very little computation, it is not allowed to disappear until a is reduced to an explicit pair, which may never occur. This prevents a number of desirable reductions: (open x as Y, z : Y in λu : Int. u)(0) is in normal form, while the corresponding untyped term (λz. λu. u)(x)(0) may be reduced. This turns out to be a major problem when trying to relate other calculi with this one, as we shall do later on, since the various typed reductions do not match, while the untyped reductions are the same. We could add other reduction rules to perform the desired identifications, but it is unclear whether the Church-Rosser and strong normalization properties would still hold.

Instead, we choose to reduce the underlying untyped λ-terms, obtained by erasing all type annotations. Pairs of a type and a term are identified with the term itself, hence the pairing operation simply disappears, and open becomes a simple binding of a term to a variable, similar to the let construct of ML. For simplicity, we express it by mere substitution of the variable by the term.

Erase o (x) = x Erase o (λx : A. b) = λx. Erase o (b) Erase o (b(a)) = Erase o (b)(Erase o (a)) Erase o ( X = A, b : B ) = Erase o (b) Erase o (open a as X, y : A in b) = Erase o (b){y←Erase o (a)} Erase o (0) = 0 Erase o (succ(a)) = succ(Erase o (a)) Erase o (case a of 0: b, succ(x): c) = case Erase o (a) of 0: Erase o (b), succ(x): Erase o (c)
After the erasing is performed, the untyped λ-term thus obtained is reduced in the usual way [START_REF] Barendregt | The Lambda Calculus, its Syntax and Semantics[END_REF]. However, when we add constants to this calculus, there is a possibility of a run-time type error during reduction; for instance, an integer could be applied as if it were a function. It remains to show that this cannot occur if the initial term is well-typed.

To be more precise, we shall use a denotational semantics for the untyped λ-calculus. Following MacQueen, Plotkin and Sethi [START_REF] Macqueen | An Ideal Model for Recursive Polymorphic Types[END_REF], we choose a domain V isomorphic to N ⊥ + (V → V) + {wrong} ⊥ . Then to each untyped term m, considered in an environment ρ, we associate a meaning that is a value [[m]] ρ of the "universe" V; meaningless terms, that is terms whose evaluation leads to a type error, are mapped to wrong. The environment ρ is a partial mapping from term variables to values of V.

[[x]] ρ = ρ(x) if defined, wrong otherwise [[λx.m]] ρ = v → [[m]] ρ[x←v] [[m(n)]] ρ = if [[m]] ρ is in V → V then ([[m]] ρ )([[n]] ρ ) else wrong [[0]] ρ = 0 [[succ(m)]] ρ = if [[m]] ρ ∈ N ⊥ then [[m]] ρ + 1 else wrong [[case m of 0: n, succ(x): p]] ρ = if [[m]] ρ = 0 then [[n]] ρ if [[m]] ρ = i + 1 then [[p]] ρ[x←i]
else wrong

We can now state the soundness of the typing rules:

Proposition 1 For all terms a and types

A, if ∅ o a : A, then Erase o (a) does not denote wrong, that is [[Erase o (a)]] ∅ = wrong.
To prove this proposition, we shall first give a meaning to type expressions as well. Following the ideal model of types [START_REF] Macqueen | An Ideal Model for Recursive Polymorphic Types[END_REF], we interpret type expressions as ideals of V, as follows:

[[Int]] ρ = N ⊥ [[X]] ρ = ρ(X) if defined, ∅ otherwise [[A → B]] ρ = {f ∈ V → V | ∀v ∈ [[A]] ρ , f (v) ∈ [[B]] ρ } [[∃X. A]] ρ = W ideal wrong/ ∈W [[A]] ρ[X←W ]
where in addition ρ maps type variables to ideals of V. Notice that if wrong is not in ρ(X) for any X, then wrong / ∈ [[A]] ρ for all types A. The soundness of typing then follows easily from the following claim, which is proved in [START_REF] Macqueen | An Ideal Model for Recursive Polymorphic Types[END_REF]: Proposition 2 Assume E o a : A. Let ρ be a mapping compatible with E; that is, for all type variables X ∈ Dom(E), the ideal ρ(X) does not contain wrong, and for all term variables x ∈ Dom(E), the denotation ρ(x) belongs to

[[E(x)]] ρ . Then [[Erase o (a)]] ρ ∈ [[A]] ρ .
Apart from confirming that the type rules are sensible, this soundness result is a clue that indeed data abstraction is ensured in this calculus. Data abstraction is usually characterized by representation independence properties. These properties formalize the intuition that two "equivalent" implementations of an abstract type are not distinguishable; that is, the observed behavior of a program using one or the other is the same. Soundness of typing is a (weak) representation independence property, where two terms are equivalent when they have the same type, and observed behavior is the absence of run-time type errors. Stronger representation independence properties hold for this calculus; for instance, Mitchell [START_REF] Mitchell | Representation independence and data abstraction (preliminary version)[END_REF] shows (for a superset of the calculus in this section) that if two implementations of an abstraction are related by a logical relation, then one can be substituted for the other in any closed term without modifying its meaning.

A calculus with the dot notation

We now formalize a calculus based on the dot notation. This is a λ-calculus with secondorder dependent products, differing from the one in the previous section only in the way of splitting existentials: instead of a single open construct, it provides two constructs: one for accessing the value part of the pair, written x.snd; and one to get a witness of the abstracted type, written x.Fst. As this is intended to model the "qualified identifiers" of Modula-2 [START_REF] Wirth | Programming in Modula-2[END_REF] and the "abstract tuples" of Quest [START_REF] Cardelli | Typeful Programming[END_REF], we shall in this section restrict .Fst and .snd to operate on term variables only.

Syntax

We keep the same notational conventions: X and Y are type variables, A and B are types, x and y are term variables, and a and b are terms.

A ::= X | A → B | ∃X. A | x.Fst a ::= x | λx : A. b | b(a) | X = A, b : B | x.snd
As previously, we can extend this dot calculus with integer constants:

Typechecking

As in the previous section, we have to define the judgment E d a : A, as well as two auxiliary judgments d E env and E d A type.

Type environments have exactly the same structure, and are well-formed under the same conditions :

d ∅ env d E env X / ∈ Dom(E) d E, X env E d A type x / ∈ Dom(E)
d E, x : A env For type validity, we have to add one rule for the new construction x.Fst, stating that it is a valid type whenever x is shown to have an existential type.

d E, X, E env E, X, E d X type E, X d A type E d ∃X. A type E d A type E d B type E d A → B type E d x : ∃X. A E d x.Fst type
For typechecking of terms, we drop the open rule and keep the other four rules. As term variables may now appear in a type expression, they must be prevented from escaping their scope. Hence, the rule for functions λx : A. b states that x is not free in the type B of the body b. As in section 2.2, this is ensured by requiring that B is a valid type in the original environment E, which does not define x.

d E, x : A, E env E, x : A, E d x : A E d A type E d B type E, x : A d b : B E d λx : A. b : A → B E d b : A → B E d a : A E d b(a) : B E d A type E d b{X←A} : B{X←A} E d X = A, b : B : ∃X. B
The new construct x.snd is well-typed provided that x has an existential type ∃X. A; its type is A, where the abstracted type X is substituted by its witness x.Fst.

E d x : ∃X. A E d x.snd : A{X←x.Fst}

Evaluation

As in section 2.3, we do not reduce typed terms directly, but rather strip all type information first and then evaluate the untyped λ-term thus obtained. This stripping is defined on terms with dot in the same vein as in section 2.3, with the additional case:

Erase d (x.snd) = x
Instead of directly investigating this calculus -proving the soundness of the type system, for instance -we shall first try to relate it to the open calculus. Indeed, we are going to provide translations from terms of one calculus into the other calculus. The translations are reasonably faithful in that they preserve typing and semantics. Most interesting properties of the open calculus can then be effortlessly shown to hold in the dot calculus as well. For instance, this would allow the following translation:

Encoding the dot calculus in the open calculus

λx : ∃X. X × X → Int. (second(x.snd))(first(x.snd)) -→ λx : ∃X. X × X → Int. (open x as Y, z : Y × Y → Int in second(z)) (open x as Y, z : Y × Y → Int in first(z))
and this is obviously wrong, since the scoping constraint of open is not respected. (Y appears free in the types of the results.) So, this scheme must be restricted to the cases where x.Fst does not appear in the type of b[x.Fst, x.snd]. Presumably, this may be achieved by taking a subexpression b large enough to enclose all uses of x.Fst and x.snd;

ComplexWRT (X) abbreviates (Real → Real → X) × (X → Real) × (X → Real) × (X → X → X)
In the dot calculus: λx : ∃X. ComplexWRT (X). second(x.snd) (λz :

x.Fst. fourth(x.snd)(z)(z))(first(x.snd)(3)(2))
In the open calculus:

λx : ∃X. ComplexWRT (X). open x as X, y : ComplexWRT (X) in second(y) (λz : X. fourth(y)(z)(z))(first(y)(3)(2))
Figure 5: Translation from the dot calculus to the open calculus indeed, the body of the λ-abstraction binding x will do, since the typing rule for λ prevents x (and, hence, x.Fst) from being free in the type of the body. Therefore, the following translation scheme seems sensible:

λx : ∃X. A. b -→ λx : ∃X. A. open x as X, y : A in b{x.Fst←X}{x.snd←y}
For instance, if we express the complex arithmetic example (figures 3 and 4) in the open calculus and in the dot calculus (see figure 5), the translation outlined above actually transforms the first program into the second one. This scheme works for closed terms, but we shall soon describe a translation for open terms as well. Now, we would like to show that a well-typed term translates to a well-typed term. To allow for easy induction on derivations, we need to translate not only terms, but also whole judgments. Hence, we first reformulate the translation in a more general (and more controlled) way.

Formal definition of the translation

Let a 0 be a closed, well-typed term of the dot calculus. To avoid name clashes, we rename the identifiers appearing in a 0 so that none gets bound more than once.

Let P be the set of term variables x such that x.Fst or x.snd appear in a 0 . Given the typechecking rules for projections, each x ∈ P has an existential type; we write it as ∃T x . A x , after renaming if necessary 2 .

2 Due to the typing rule for pairs, this type may differ from the type declared for x by the abstraction binding it, as in X = ∃Y. Int, λx : X. x.snd : X → Int . The type ∃T x . A x we associate with x is the "true" type of x; that is, the type given to it in the derivation of a 0 : A 0 (this derivation is unique, given the typing rules), or alternatively the type declared for x, where all bindings such as X = ∃Y. Int above have been performed.

To each x ∈ P, we associate a term variable v x that does not appear in a 0 . For each subterm a of a 0 , we define its translation a as follows:

x = x x.snd = v x λx : A. b = λx : A . open x as T x , v x : A x in b if x ∈ P λx : A. b = λx : A . b if x / ∈ P b(a) = b ( a ) X = A, b : B = X = A , b : B
This is basically the transformation outlined above, with substitutions delayed, and performed only when necessary: we insert an open x as . . . only when x ∈ P; that is, when x.Fst or x.snd are actually used.

In the same vein, types translate as follows:

X = X x.Fst = T x A → B = A → B ∃X. A = ∃X. A
To translate environments, the only case that needs special treatment is the introduction of a variable x belonging to P. In the derivation, this case corresponds to the typechecking of the body b of a function λx : A. b. After translation, b will be preceded by an open x as T x , v x : A x in . . ., so we must typecheck the translation of b in an environment where T x and v x are defined. Hence the translation of E, x : A introduces T x and v x : A x in addition to x : A .

∅ = ∅ E, X = E , X E, x : A = E , x : A , T x , v x : A x if x ∈ P E, x : A = E , x : A if x / ∈ P

Preservation of typing

We are now able to translate any judgment componentwise, and in particular ∅ d a 0 : A 0 .

To prove that the translation preserves typing, it remains to show that its translation ∅ o a 0 : A 0 can be derived in the open calculus.

Proposition 3 Let a 0 be a closed, well-typed term of the dot calculus. Let be the associated translation function. Let D be the derivation of ∅ o a 0 : A 0 .

• If d E env is proved in D, then o E env. • If E d A type is proved in D, then E o A type. • If E d a : A is proved in D, then E o a : A .
Proof: By induction on the three derivations, starting with the one of E d a : A.

• For value variables: we have the following derivation . . . • For value access in a pair: from the original derivation . . .

d E 1 , x : A, E 2 env E 1 , x : A, E
d E 1 , x : ∃T x . A x , E 2 env E 1 , x : ∃T x . A x , E 2 d x : ∃T x . A x E 1 , x : ∃T x . A x ,
E o A type E, x : A o b : B that is E , x : A o b : B hence E o λx : A . b : A → B
which is the desired result.

If x ∈ P, then A = ∃T x . A x , and the same steps lead to:

E o ∃T x . A x type E o B type E , x : ∃T x . A x , T x , v x : A x o b : B
so we have the following derivation:

E , x : ∃T x . A x o x : ∃T x . A x E o B type E , x : ∃T x . A x , T x , v x : A x o b : B E , x : ∃T x . A x o open x as T x , v x : A x in b : B E o ∃T x . A x type E o λx : ∃T x . A x . open x as T x , v x : A x in b : ∃T x . A x → B
that leads to the desired result:

E o λx : A. b : A → B
• For application: obvious by induction hypothesis.

• For pair construction: from

E d A type E d b{X←A} : B{X←A} E d X = A, b : B : ∃X. B
we get by induction hypothesis proofs of

E o A type E o b{X←A} : B{X←A} To conclude that E o X = A , b : B : ∃X. B , it suffices to show that b{X←A} = b {X← A } B{X←A} = B {X← A }
The proof is by induction on b and B. We give the non-trivial case: b = λx : C. d with x ∈ P.

b{X←A} = λx : C{X←A} . open x as T x , v x : A x in d{X←A} = λx : C {X← A }. open x as T x , v x : A x in d {X← A }
by induction hypothesis. The type variable X is not free in A x (indeed, by definition of T x and A x , the type ∃T x .A x is C where some type variables have been substituted, and especially X has been substituted by A). Therefore X is not free in A x either. Hence the desired result:

b{X←A} = (λx : C . open x as T x , v x : A x in d ){X← A } = b {X← A }
We turn now to the E d A type judgment. All cases are straightforward, except maybe the one for x.Fst; but then the original derivation is: . . .

d E 1 , x : ∃T x . A x , E 2 env E 1 , x : ∃T x . A x , E 2 d x : ∃T x . A x E 1 , x : ∃T x . A x , E 2 d x.Fst type
The translation of E 1 , x : ∃T x . A x , E 2 introduces the type variable T x , and it is a wellformed environment, so E 1 , x : ∃T x . A x , E 2 o T x type holds, which is the desired result since x.Fst = T x .

Similarly, for the d E env judgment, the only interesting case is the introduction of an x belonging to P. By definition of T x and A x , the type given to x must be ∃T x . A x . . . .

E, T x

d A x type E d ∃T x . A x type x / ∈ Dom(E) d E, x : ∃T x . A x env
By induction, we have a proof of E , T x o A x type, hence the following derivation:

E , T x o A x type E o ∃T x . A x type x / ∈ Dom( E ) o E , x : ∃T x . A x env T x / ∈ Dom( E , x : ∃T x . A x ) o E , x : ∃T x . A x , T x env
We can substitute this for the proof of o E , T x env in the derivation of E , T x o A x type, thereby obtaining a proof of E , x : ∃T x . A x , T x o A x type. Hence: Hence Erase o ( a 0 ) = Erase d (a 0 ).

E , x : ∃T x . A x , T x o A x type v x / ∈ Dom( E , x : ∃T x . A x , T x ) o E , x : ∃T x . A x , T x , v x : A x env 2
Proof: By induction on a. We give the main cases: The remaining cases are obvious.

• if a = x.

2

Using the last two propositions, we can show the soundness of the type system of the dot calculus, extended with integer constants as mentioned in section 3.1. (The translation function is extended to the integer constructs in the trivial way, by translating their components recursively; it is easy to see that propositions 3 and 4 still hold.)

Corollary 1 If ∅ d a 0 : A 0 ,

Encoding the open calculus in the dot calculus

The reverse translation is much less informative, but would confirm the intuition that the dot calculus is no less powerful than the open calculus, so we shall sketch it quickly. The basic idea is to replace every open a as X, y : A in b by (λz : ∃X. A. b{X←z.Fst, y←z.snd})(a)

for some unused term variable z. In contrast with the previous translation, any type of the open calculus is also a type of the dot calculus, and this also holds for wellformed environments. Hence we just have to provide a translation for terms, which is straightforward:

x = x λx : A. b = λx : A. b b(a) = b ( a ) X = A, b : B = X = A, b : B open a as X, y : A in b = (λz : (∃X. A). b {X←z.Fst, y←z.snd})( a )
where z is not free in open a as X, y : A in b

We must check that, in the last rule, the substitution of y by z.snd can be performed, since in x.Fst or x.snd, x cannot be substituted by any term but another variable without producing a syntactically incorrect term such as a(b).Fst. Happily, by definition of the translation, if y.Fst or y.snd appears in b , then y is bound by a λ, and hence will not have to be substituted.

As , the function preserves typing and semantics:

Proposition 5 If E o a : A, then E d a : A.
Proof: by induction on the original derivation. The only interesting case is the translation of an open construct: Proof: similar to the proof of proposition 4. 2

E o a : ∃X. A E o B type E, X, y : A o b : B E o open
E d ∃X. A type E d B type E, z : ∃X. A d b {X←z.

A more powerful calculus with dot

In this section, we simply lift the restriction that only a value variable may be the argument of a .Fst or .snd construction, and allow instead any term, provided it has an existential type.

Regarding the formalism, this is a very natural generalization of the previous dot calculus, reminiscent of the second-order general sums (also called strong sums) of type theory [START_REF] Martin-Löf | Constructive mathematics and computer programming[END_REF][START_REF] Howard | The formulae-as-types notion of construction[END_REF].

From the point of view of programming languages, this extension, in its full generality, does not seem to model any real situation, especially since .Fst now embeds the whole class of values into the class of types; this means that the dividing line between types and values begins to blur dangerously.

However, we may feel the need for a calculus less restrictive than the dot calculus of the previous section. For instance, to deal with nested modules, it seems natural to have not only one-level access in modules, such as module.Type, but also access through paths of arbitrary length, such as module.submodule.data. To formalize this, the argument of a .Fst or .snd must be allowed to be a path, where a path is a term variable followed by an arbitrary number of .snd.

We could study this first extension of the dot calculus in the same way as for the dot calculus, by finding a translation to the open calculus and proving that it is faithful. However, other similar extensions may come to mind, and the same work would have to be done for each. Therefore, it seems easier to study the most general extension of all, where any term can appear to the left of a .Fst or .snd construct.

Typing

The typing rules are exactly those of the simple dot calculus, with the obvious generalization for the projections:

E s a : ∃X. A E s a.Fst type E s a : ∃X. A E s a.snd : A{X←a.Fst}
It may be tempting to identify certain type expressions of this calculus, for instance X = A, b : B .Fst and A, and to use this notion of type equivalence for typechecking, instead of for strict equality. This amounts to adding the following rule:

E s a : A A ↔ B E s a : B
At first, we choose to disallow the latter rule and require syntactic equality for two types to be compatible; we shall come back to this issue later on.

Evaluation

As usual, we strip all type information before reducing. The .snd operation becomes identity on λ-terms:

Erase s (a.snd) = Erase s (a)

As for the simple calculus with dot, we shall not investigate this calculus directly, but try to relate it to the open calculus first. and that b must not bind any of the free variables of a. However, the previous example shows that sometimes both constraints cannot be satisfied, especially when type variables are free in a.

Relation to the open calculus

If a has no free type variables, the transformation might work: let b be the body of the smallest abstraction λx : A. b enclosing all uses of a.Fst and a.snd. Either a.Fst does not appear in the type B of b, in which case it is possible to insert an open a as . . . there, or a.Fst is part of B. But in the latter case, x / ∈ F V (B), hence x is not free in a. Therefore, we can "lift" a out of b, consider the next enclosing λ, and iterate.

We are now going to formalize this argument in the same way as in the previous section by providing translations for terms, types, and environments.

A translation function

Let a 0 be a closed, well-typed term, renamed so that each variable gets bound once at most, and let D be the derivation of ∅ s a 0 : A 0 . We write P for the set of subterms a of a 0 such that a.Fst or a.snd appears in D.

From now on, we shall suppose that the following condition holds:

(C) For all a ∈ P, there are no type variables free in a.

For instance, it was not the case in the previous example, where P = { Y = X, a : Y }.

For each a ∈ P, the term a has no free type variables, therefore D derives a type for a 3 ; this type is an existential type (given the typechecking rules for .Fst and .snd), and we write ∃T a . A a for it (after renaming of variables if necessary). Furthermore, we associate with a a value variable v a unused in a 0 . Now we have to decide, for all a ∈ P, where to insert an open a as . . . Let a ∈ P. We consider the smallest subexpression b of a 0 binding all free variables of a. Since no variables are bound twice, such a b exists, and it contains all occurences of a.Fst and a.snd. If a is closed, it is a 0 . Otherwise, as there are no type variables free in a, it is the body of a λ-abstraction λx : A. b. We shall consider only the latter case, since we can assume without loss of generality that a 0 itself is a λ-abstraction. We say that the variable x bound by this abstraction is the first free variable of a.

For all term variables x, we write F(x) for the sequence of all a ∈ P such that x is the first free variable of a. The translation of terms consists mainly in inserting, before the body b of any function λx : A. b, an open a as T a , v a : A a in . . . for each a ∈ F (x). However, we must take care of the order of insertion, to avoid using a T a or v a before it is defined. More precisely, if a and a belong to F(x) and a is a subexpression of a , then open a as . . . must precede open a as . . . Therefore, we enumerate the sequence

F(x) = a 1 , . . . , a n in topological order, that is if a i is a subexpression of a j , then i ≤ j. x = x a.snd = v a λx : A. b = λx : A . open a 1 as T a 1 , v a 1 : A a 1 in . . . open a n as T a n , v a n : A a n in b if F(x) = a 1 , . . .
∅ = ∅ E, X = E , X E, x : A = E , x : A , T a 1 , v a 1 : A a 1 , . . . , T a n , v a n : A a n if F(x) = a 1 , . . . , a n
Condition (C) ensures that all a ∈ P are translated, and that no T a or v a is free in a 0 , since the open a as T a , v a : A a in . . . encloses all uses of T a and v a . Proof: the proof is a straightforward generalization of the proof given for proposition 3. We proceed by induction on the derivation of the judgment. Here are the interesting cases:

Preservation of typing

• For value access in a pair: the original derivation is . . . E s a : ∃T a . A a E s a.snd : A a {T a ←a.Fst} so a ∈ P and E binds all free variables of a, including its first free variable. Hence, E introduces v a with the type A a . By induction, we get a proof of E o a : ∃T a . A a , from which we can extract a proof of o E env. Hence, E o v a : A a , which is the expected result, since a.snd = v a and obviously,

A a {T a ←a.Fst} = A a • For λ-abstraction: . . . E s A type . . . E s B type . . . E, x : A s b : B E s λx : A. b : A → B
Let a 1 , . . . , a n be F(x). For all i, since a i is a subterm of b and since there are no type variables free in a i , the derivation of E, x : A s b : B contains a derivation of E a i s a i : ∃T a i . A a i for some environment E a i . So, by induction, we get proofs of

E o A type E o B type Σ n o b : B E a i o a i : ∃T a i . A a i where Σ j = E , x : A , T a 1 , v a 1 : A a 1 , . . . , T a j , v a j : A a j for all 0 ≤ j ≤ n.
As a i is a subexpression of b, it is easy to see that Σ n and E a i bind the free variables of a i to the same types. Furthermore, as F(x) is enumerated in topological order, for all j ≥ i, the terms a j .Fst and a j .snd do not appear in a i , therefore T a j and v a j are not free in a i . Hence, Σ i-1 and E a i bind the free variables of a i to the same types. So, from the derivation of

E a i o a i : ∃T a i . A a i we can build a proof of Σ i-1 o a i : ∃T a i . A a i
Since Σ i is an extension of E , from the proof of E o B type, we get a proof of Σ i o B type. Hence the desired result: The remaining cases are easy. Hence Erase o ( a 0 ) = Erase s (a 0 ).

Σ n o b : B Σ n-1 o B type Σ n-1 o a n : ∃T a n . A a n Σ n-1 o open a n as T an , v an : A an in b : B Σ n-2 o B type Σ n-2 o a n-1 : ∃T a n-
Proof: Same proof as for proposition 4. 2

As a consequence of propositions 7 and 8, no closed term for which condition (C) holds can evaluate to wrong. Indeed, this is true even if condition (C) does not hold, since the type system of the generalized dot notation is sound, as can be proved directly along the lines of section 2.3. However, it is not clear whether the generalized dot notation ensures as strong an abstraction as the original open construct. Informally, we may fear that it is not the case, since, for instance, implementations of abstractions can be fully visible in types: X = Int, 0 : X .snd : X = Int, 0 : X .Fst thus publicizing that X = Int.

Type equivalence modulo reduction

As mentioned previously, we may add the following rule:

E s a : A A ↔ B E s a : B ( 1
)
where the equivalence relation ↔ is the congruence generated by the axioms: Even if rule 1 uses only equivalence between types, we need to define also equivalence between terms, because a.Fst is equivalent to b.Fst if a is equivalent to b. This rule leads to a weaker notion of abstraction, where succ( X = Int, 0 : X .snd) typechecks, for instance. MacQueen [START_REF] Macqueen | Using Dependent Types to Express Modular Structure[END_REF] argues that this additional flexibility is desirable for a programming language, in order to be able to express complex dependencies between modules. However, the DL language he proposes is stratified, and this is not by chance, since an unstratified system like ours equipped with rule 1 is inconsistent, as it is possible to encode a calculus with a type of all types in it [START_REF] Mitchell | The Essence of ML[END_REF].

X = A
Even if we add some stratification, allowing reduction during typechecking, as above, does not seem to modify drastically the previous results. Admittedly, the counterexample we gave to show that some terms have no equivalent in the open calculus, Moreover, the translation above can still be applied to terms in normal form satisfying condition (C), and, in that case, still leads to well-typed terms of the open calculus, since for terms in normal form, type equivalence is again syntactic equality.

Conclusion

We have described two notations for type abstraction, one coming from logic, the other from programming, and investigated their relationships. This work contributes to the to actual programming languages than are calculi based on logical notation, but enjoy all the same interesting properties.

Figure 1 :Figure 2 :Figure 3 :

 123 Figure 1: A specification of a complex arithmetic package

  a of 0: b, succ(x): c : A A pair X = A, b : B has type ∃X. B if the claim b : B holds when considering the binding X = A in b and B. The type A does not appear in the type of the pair; it is therefore hidden outside of the pair.

A

  ::= . . . | Int a ::= . . . | 0 | succ(a) | case a of 0: b, succ(x): c

  The idea behind both translations is that, in the body of an open x as Y, z : A in b expression, Y and z seem to have the same meaning as x.Fst and x.snd, respectively. This remark suggests the following strategy to transform a program with dot into one with open: insert some open x as Y, z : A in . . . for each variable x used in a x.Fst or x.snd construct, and use Y and z instead of x.Fst and x.snd. In other words: b[x.Fst, x.snd] -→ open x as Y, z : A in b[Y, z]

3. 4 . 3 Proposition 4

 434 Preservation of semanticsAs the translation respects the structure of functions and applications, a closed term of the dot calculus and its translation in the open calculus have exactly the same underlying untyped terms. More precisely, we have: For all subterms a of a 0 , Erase o ( a ){v x ←x for all x ∈ P} = Erase d (a).

  snd, Erase d (a) = x and Erase o ( a ) = v x . • if a = λx : A. b and x ∈ P, then Erase o ( a ) = Erase o (λx : A . open x as T x , v x : A x in b ) = λx. (Erase o ( b ){v x ←x}) hence, by induction hypothesis, Erase o ( a ){v y ←y for all y ∈ P} = λx. (Erase o ( b ){v x ←x}{v y ←y for all y ∈ P \ {x}}) = λx. Erase d ( b ) which is the expected result.

  then Erase d (a 0 ) does not denote wrong. Proof: The translation a 0 is a well-typed closed term of the open calculus. Hence, by proposition 1, [[Erase o ( a 0 )]] ∅ = wrong, which is the desired result, since Erase o ( a 0 ) = Erase d (a 0 ). 2

2 Proposition 6

 26 Fst, y←z.snd} : B E d λz : ∃X. A. b {X←z.Fst, y←z.snd} : ∃X. A → B E d a : ∃X. A E d (λz : ∃X. A. b {X←z.Fst, y←z.snd})( a ) : B This is the expected result. For any term a of the open calculus, Erase d ( a ) β-reduces to Erase o (a).

  When we try to encode this calculus into the open calculus, we find terms which apparently have no equivalents in the open calculus. For instance, assume a : A and consider the following term:X = A, Y = X, a : Y .snd : Y = X, a : Y .FstTo express it in the open calculus, we have to insert an open Y = X, a : Y as . . . at some point, and since X is free in the pair, the only literal translation is:X = A, open Y = X, a : Y as Z, z : Z in z : Z but then Z escapes the scope of the open construct. (See later for a similar term but with no trivial redexes.) To try to find an equivalent term in the open calculus, the general strategy is the same as in section 3.4: replace subterms such as b[a.Fst, a.snd] by open a as X, y : A in b[X, y], with the additional constraints that a.Fst should not appear in the type of b[a.Fst, a.snd],

  , a n b(a) = b ( a ) X = A, b : B = X = A , b : B Notice that the third rule remains valid if F(x) = ∅, and means λx : A. b = λx : A . b in this case. The translation of types is the same as for the original dot calculus:X = X a.Fst = T a A → B = A → B ∃X. A = ∃X. AAs for the original dot calculus, we must synchronize the translation of environments with the translation of terms. Adding x : A to E means that we are about to typecheck the body b of λx : A. b. After translation, b will be preceded by open a as T a , v a : A a in . . . for each a ∈ F(x). So, the translation of E, x : A must define T a and v a : A a for each a ∈ F(x).

2

 2

4. 3 . 3 Proposition 8

 338 Preservation of semantics As in the previous section, this translation does not modify the meaning of the program: For all subterms a of a 0 , Erase o ( a ){v b ←Erase o ( b ) for all b ∈ P} = Erase s (a).

  , b : B .Fst ↔ A X = A, b : B .snd ↔ b{X←A} (λx : A. b)(a) ↔ b{x←a}

X

  = A, Y = X, a : Y .snd : Y = X, a : Y .Fst , now fails, since it reduces to X = A, a : X . But we can work out more complicated examples, without any redex, that exhibit the same pathology, for instance: λf : (∃X. A) → (∃Y. B). Z = A, (f X = Z, a : X ).snd : B{Y ←(f X = Z, a : X ).Fst} where a : A, since the open X = Z, a : X as . . . must take place inside the Z = A, . . . : . . . , hence violating the scoping rule for open.

  2 d x : A By induction, we have a derivation of o E 1 , x : A, E 2 env. By definition of the translation, E 1 , x : A, E 2 has clearly the form E 1 , x : A , E 2 . Hence the desired result E 1 , x : A, E 2 o x : A follows.

  E 2 d x.snd : A x {T x ←x.Fst} we get by induction a derivation of o E 1 , x : ∃T x . A x , E 2 env. As x.snd appears in the derivation above, x belongs to P. Therefore, E 1 , x : ∃T x . A x , E 2 introduces the variable v x with type A x . Hence E o v x : A x , which implies the expected result E

	• For abstraction:
	. . .	. . .	. . .
	E d A type	E d B type

o x.snd : A{X←x.Fst} since, as x.Fst = T x , A{T x ←x.Fst} = A E, x : A d b : B E d λx : A. b : A → B If x / ∈ P, by induction we have proofs of

  By induction, it follows that E d a : ∃X. A and E, X, y : A d b : B. By induction on the proof of the latter, we get a derivation of E, z : ∃X. A d b {X←z.Fst, y←z.snd} : B{X←z.Fst} As X is not free in B, we have B{X←z.Fst} = B. Finally, from the proof of E d a : ∃X. A, we can prove that E d ∃X. A type. Putting all together, we get:

a as X, y : A in b : B

Proposition 7

 7 If one of the judgments s E env, E s A type, or E s a : A is a step of the derivation D, then we can prove o E env, E o A type, or E o a : A respectively.

  1 . A a n-1 . . . E , x : A o open a 1 as T a 1 , v a 1 : A a 1 in . . . b : B E Let a 1 , . . . , a n be F(x). If n = 0, we get by induction a proof of E o A type, hence the desired result o E , x : A env.Otherwise, by the same reasoning as in the case of λ-abstraction, we have a proof of:E , x : A , T a 1 , v a 1 : A a 1 , . . . , T a n-1 , v a n-1 : A a n-1 o a n : ∃T an .A an from which we can extract a derivation of:E , x : A , T a 1 , v a 1 : A a 1 , . . . , T a n-1 , v a n-1 : A a n-1 o ∃T a n . A a n typewhose penultimate step is:E , x : A , T a 1 , v a 1 : A a 1 , . . . , T a n-1 , v a n-1 : A a n-1 , T an o A an typeHence the desired result: A , T a 1 , v a 1 : A a 1 , . . . , T a n , v a n : A a n env

o A type E o λx : A. b : A → B

• For the introduction of a value variable in an environment:

E s A type x / ∈ Dom(A) s E, x : A env o E , x :

This type-theoretical notion of "abstract types", should not be confused with the many-sorted algebra approach. It is both weaker, since it does not involve equations (which can however be added in a typetheoretical logic), and also stronger, because of higher-order functions.

Hypothesis (C) is crucial here, since in general, it is not true that any subterm of a 0 is given a type in D, because of the typing rule for pairs X = A, b : B , which requires that b{X←A} has a type, but not necessarily b itself. For instance, λx : X. succ(x) has no type by itself, though X = Int, λx : X. succ(x) : X → Int is well-typed.

Acknowledgements

We are indebted to Martín Abadi, for having pointed out several flaws in earlier proofs of propositions 3, 5, and 7.

formal foundation of the notion of abstraction found in programming. It also suggests some interesting extensions, as we shall see now.

The grammar of a calculus with the dot notation may ensure that condition (C) always holds. Let p range over the class of terms allowed to appear before a .Fst or a .snd construct: If p cannot contain any type variable at all, then condition (C) will certainly hold. This is the case, of course, for the simple dot calculus of section 2 (p ::= x). This is also the case for the extension to "paths" mentioned at the beginning of the previous section (p ::= x | p.snd). This notion of paths gives a convenient way to deal with nested abstractions, which is much more natural than, for instance, the nested modules of Modula-2 [START_REF] Wirth | Programming in Modula-2[END_REF]. Such a multi-level stratification (as opposed to the usual "flat" structure of programs considered as a set of modules) seems necessary for very large software systems.

Condition (C) even suggests other extensions, for instance:

This would be convenient for dealing with parameterized abstractions. For example, assuming we extend the system with first-order dependent types ∀(x : A)B, we could write:

type Disc(cpx : Complex ) = ∃X. make : cpx .Fst → Real → X, . . .

Here, disc(cpx ) would be a package implementing abstract discs of given origin and radius, depending on a given implementation cpx of Complex . For example, disc(polarcomplex) and disc(cartesian complex ) would provide different implementations of the parametric disc abstraction. Two instances of disc(polar complex ) would be recognized to refer to the same abstraction, according to the translation based on condition (C), and could hence interact freely.

In conclusion, we can define more and more expressive calculi based on the dot notation. The most expressive ones, only sketched in this section, should be able to deal with complex dependencies between first-class parametric abstractions. Our calculi are closer