From Classes to Objects via Subtyping^{⋆}

Didier Rémy

INRIA-Rocquencourt^{⋆⋆}

Abstract

We extend the Abadi-Cardelli calculus of primitive objects with object extension. We enrich object types with a more precise, uniform, and flexible type structure. This enables to type object extension under both width and depth subtyping. Objects may also have extend-only or virtual contra-variant methods and read-only co-variant methods. The resulting subtyping relation is richer, and types of objects can be weaken progressively from a class level to a more traditional object level along the subtype relationship.

1 Introduction

Object extension has long been considered unsound when combined with subtyping. The problem may be explained as follows: in an object built with two methods ℓ_{1} and ℓ_{2} of types τ_{1} and τ_{2}, the method ℓ_{1} may require ℓ_{2} to be of type τ_{2}. Forgetting the method ℓ_{2} by subtyping would result in the possible redefinition of method ℓ_{2} with another, incompatible type τ_{3}. Then, the invocation of ℓ_{1} may fail.

Indeed, the first strongly-typed object-based languages that have been proposed provided either subtyping [1] or object extension [21] to circumvent the problem described above. However, each proposal was missing an important feature supported by the other one.

Both of them were improved later following the same principle: At an earlier stage, object components were assembled in prototypes [20] or classes [2], relying on some extension mechanism to provide inheritance. Objects were formed in a second, atomic step, immediately losing their extension capabilities for ever, to the benefit of subtyping.

In contrast to the previous work, we allow both extension and subtyping at the level of objects, avoiding stratification. Our solution is based on the enrichment of the structure of object types. Thus, our type-system rejects the above counter-example while keeping many other useful programs. In our proposal, an object and its class are unified and can be considered as two different perspectives on the same value: the type of an object is a supertype of the type of its class. Fine grain subtyping allows type information to be lost gradually, both width-wise and depth-wise, slowly fading classes into objects. As is well-known, when more type information is exposed, more operations can be performed (class perspective). On the contrary, hiding a sufficient amount of type information allows for more object interchangeability, but permits fewer operations (object perspective).

We add object extension to the object calculus of Abadi and Cardelli [3]. We adapt their typing rules to our enriched object types. In particular, we force methods to be parametric in self, that is, polymorphic over all possible extensions of the respective object. In this sense, our proposal is not a strict extension of theirs.

In addition to object extension, the enriched type structure has other benefits. We can allow virtual methods in objects (i.e. methods that are required by some other method but that have not been defined yet) since we are able to described them in types. Using co-variant subtyping forbids further re-definition of the corresponding method, as in [3]. Since classes are objects, such methods are in fact final methods. Final methods can only be accessed but no more redefined (except, indirectly, by the invocation of a previously defined method).

⋆A preliminary version appeared in [26]

⋆⋆BP 105, 78153 Le Chesnay Cedex, France. Email: Didier.Remy@inria.fr

Virtual methods are useful because they allow objects to be built progressively, component by component, rather than all at once. They also improve security, since they sometime avoid the artificial use of dangerous default methods. While final methods are co-variant, virtual methods, are naturally contra-variant.

The rest of the paper is organized as follows. In the next section, we describe our solution informally. The following section is dedicated to the formal presentation. In section 4, we show some properties of the type system, in particular the type soundness property. Section 5 illustrates the gain in security and flexibility of our proposal by running a few examples. To a large extend, these examples can be understood intuitively and may also be read simultaneously with or immediately after the informal presentation. In section 6 we discuss possible extensions and variations of our proposal, as well as further meta-theoretical developments. A brief comparison with other works is done in section 7 before concluding.

2 Informal presentation

Technically, our first goal is to provide method extension, while preserving some form of subtyping. The counter-example given above does not imply that both method extension and width subtyping are in contradiction. It only shows that combining two existing typing rules would allow to write unsafe programs. Thus, if ever possible, a type system with both method extension and subtyping should clearly impose restrictions when combining them. Our solution is to enrich types so that subtyping becomes traceable, and so that extension can be limited to those fields whose exact type is known.

We first recall record types with symmetric type information. Using a similar structure for object types, some safe uses of subtyping and object extension can be typed, while the counterexample given in the introduction is rejected.

Record types

Record values are partial functions with finite domains that map labels to values. Traditionally, the types of records are also partial functions with finite domains that map labels to types. They are represented as records of types, that is, {ℓ_{i} : τ_{i} ^{i∈I}}. This type says that fields ℓ_{i}’s are defined with values of type τ_{i}’s. However, it does not imply anything about other fields.

Another richer, more symmetric structure has also been used for record types, originally to allow type inference for records in ML [23, 24]. There, record types are treated as total functions mapping labels to field types, with the restriction that all but a finite number of labels have isomorphic images (i.e. are equal modulo renaming). Thus, record types can still be represented finitely by listing all significant labels with their corresponding field types and then adding an extra field-type acting as a template for all other labels.

In their simplest form, field types are either P τ (read present with type τ) or A (read absent). For instance, a record with two fields ℓ_{1} of type τ_{1} and ℓ_{2} of type τ_{2} is given type ⟨ℓ_{1}: P τ_{1} ; ℓ_{2}: P τ_{2} ; A⟩. It could also, equivalently, be given type ⟨ℓ_{1}: P τ_{1} ; ℓ_{2}: P τ_{2} ; ℓ: A ; A⟩ where ℓ is distinct from ℓ_{1} and ℓ_{2}.

In the absence of subtyping, standard types for records {ℓ_{i} : τ_{i} ^{i∈I}} can indeed be seen as a special case of record types, where field variables are disallowed; their standard subtyping relation then corresponds to the one generated by the axiom P τ <:A (and obvious structural rules). The type {ℓ_{1} : τ_{1}; ..ℓ_{n} : τ_{n}} becomes an abbreviation for ⟨ℓ_{1}: P τ_{1} ; ..ℓ_{n}: P τ_{n} ; A⟩. However, record types are much more flexible. For instance, they inherently and symmetrically express negative information. Before we added subtyping, a field ℓ of type A was known to be absent in the corresponding record. This is quite different from the absence of information about field ℓ. Such precise information is sometimes essential; a well-known example is record concatenation [16]. Instead of breaking the symmetry with the subtyping axiom P τ <: A, we might have introduced a new field U (read unknown), with two axioms P τ <: U and A <: U. This would preserve the property that a field of type A is known to be absent, still allowing present and absent field to be interchanged but at their common supertype U.

Field variables and row variables also increase the expressiveness of record types. However, for simplicity, we do not take this direction here. Below, we use meta-variables for rows. This is just a notational convenience. It does not add any power.

Object types

In their simplest form, objects are just records, thus object types mimic record types. We write object types with [ρ] instead of ⟨ρ⟩ to avoid confusion. An object with type [ℓ_{1}: P τ_{1} ; ℓ_{2}: P τ_{2} ; A] possesses two methods ℓ_{1} and ℓ_{2} of respective types τ_{1} and τ_{2}. Intuitively, an object [ℓ_{1} = a_{i} ^{i∈I}] can be given type [ℓ_{i}: P τ_{i} ^{i∈I} ; A] provided methods a_{i}’s have type τ_{i}’s.

However, objects soon differ from records by their ability to send messages to themselves, or to return themselves in response to a method call. More generally, objects are of the form [ℓ_{i} = ς(x_{i})a_{i}]. Here, x_{i} is a variable that is bound to the object itself when the method ℓ_{i} is invoked. Consistently, the expression a_{i} must be typed in a context where x_{i} is assumed of the so-called “mytype”, represented by some type variable χ equal to the object type τ. The following typing rule is a variant of the one used in [3].

\frac{τ ≡ ζ(χ)[ℓ_{i}: P τ_{i} ^{i∈I} ; A] A, χ = τ, x_{i} : χ ⊢ a_{i} : τ_{i}}{A ⊢ ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}] : τ}

(The type annotation (χ, τ) in the object expression binds the name of mytype locally and specifies the type of the object.)

An extendible object v may also be used to build a new object v′ with more methods than v and thus of a different type, say τ′. The type τ′ of self in v′ is different from the type τ of self in v. In order to remain well-typed in v′, the methods of v, should have been typed in a context where the type of self could have been τ′ as well as τ. This applies to any possible extension v′ of v. In other words, methods of an object of type τ should be parametric in all possible types of all possible successive extensions of an object of type τ. This condition can actually be expressed with subtyping by χ <: # τ, where # τ is called the extension type of τ (also called the internal type of the object). That is, the least upper bound of all exact^{1} types of complete extensions (extensions in which no virtual method remains) of objects of external type τ.

A field of type A can be overridden with methods of arbitrary types. Thus, the best type for that field in the self parameter is U, i.e. we choose #A to be U. Symmetrically, we choose #(P τ) to be U. This makes methods of type P τ internally unaccessible. Fields of type P τ are known to be present externally, but are not assumed to be so internally. Thus, fields of type P τ can be overridden with methods of arbitrary types, such as fields of type A. To recover the ability to send messages to self, we introduce a new type field R τ (read required of type τ). A field of type R τ is defined with a method of type τ, and is required to remain of at least type τ, internally. Such a field can only be overridden with a method of type τ. Therefore, self can also view it as a field that is, and will remain, of type τ. In math, #R τ is R τ. A field of type P τ, can safely be considered as a field of type R τ. Thus, we assume P τ <: R τ. We also assume R τ to be a subtype of U. As an example, # ζ(χ)[ℓ_{1}: R τ_{1} ; ℓ_{2}: P τ_{2} ; ℓ_{3}: U ; A] is ζ(χ)[ℓ_{1}: R τ_{1} ; ℓ_{2}: U ; ℓ_{3}: U ; U], or shortly ζ(χ)[ℓ_{1}: R τ ; U].

1The exact type of an object is the type with which the methods can initially be typed. The external type of an object may be a supertype of the exact type.

The extension of a field with a method of type τ requires that field to be either of type A or R τ in the original record (the field may also be of type P τ, which is a subtype of R τ.) It is possible to factor the two cases by introducing a new field type M τ (read maybe of type τ), and the axioms R τ <: M τ, A <: M τ, and M τ <: U. Intuitively, M τ is the union type R τ ∪ A. This allows, in a first step, to ignore the presence of a method while retaining its type, and, in a second step, to forget the type itself. The type of object extension becomes more uniform. Roughly, if the original object has type [ℓ_{1}: M τ_{1} ; τ_{2}] and the new method ℓ_{1} has type τ_{1} then the resulting object has type [ℓ_{1}: R τ_{1} ; τ_{2}].

A field of type M τ may later be defined or redefined with some method of type τ, becoming of type R τ, which is a subtype of M τ. It may also be left unchanged and thus remain of type M τ. Thus, a field of type M τ will always remain of a subtype of M τ. That is, #(M τ) is M τ.

Deep subtyping

Subtyping rules described so far allow for width subtyping but not for depth subtyping, since all constructors have been left invariant. The only constructor that could be made covariant without breaking type-soundness is P. Making R co-variant would be unsafe. However, we can safely introduce a new field type R^{+} τ to tell that a method is defined and required to be of a subtype of τ, provided that a field of type R^{+} τ is never overridden. On the other hand, a method ℓ_{1} can safely be invoked on any object of type [ℓ_{1}: R^{+} τ_{1} ; U], which returns an expression of type τ_{1}. Of course, we also add R τ <: R^{+} τ to just forget the fact that we are revealing the exact type information.

Symmetrically, a field ℓ of type M τ cannot be accessed, but it can be redefined with a method of a subtype of τ. Still, it would be unsound to make M τ contra-variant. By contradiction, consider an object p of type ζ(χ)[ℓ: R τ ; ℓ′: P χ ; A] where calling method ℓ′ overrides ℓ in self with a new method of type τ. By subtyping p_{0} could be given type ζ(χ)[ℓ: M τ_{0} ; ℓ′: P χ ; A] where τ_{0} is a subtype of τ. Then let p_{2} of type ζ(χ)[ℓ: M τ_{0} ; ℓ′: P χ ; ℓ′′: Punit ; A] be the extension of p_{1} with a new method ℓ′′ that requires ℓ of type τ_{0}. Calling method ℓ′ of p_{2} restore field ℓ of p_{2} to some method of type τ and returns an object p_{3}. However, calling method ℓ′′ of p_{3} expects a method ℓ of type τ_{0} but finds one of type τ.

We can still introduce a contra-variant symbol M^{−} with the axiom M τ <: M^{−} τ. Then, a method M^{−} τ can be redefined, but the method in the resulting object remains of type M^{−} τ and is thus unaccessible. This is still useful in situations where contra-variance is mandatory or to enforce protection against accidental access (see sections 5.6, 5.2 and [3].)

Virtual methods

A method ℓ is virtual with type τ (which we write V τ) if other methods have assumed ℓ to be of type R τ, while the method itself might not have been defined yet. When an object has a virtual method, no other method of that object can be invoked. Thus, V τ should not be a subtype of U. A method of type V τ can be extended as a method of type R τ. Virtual methods may also be contra-variant. We use another symbol V^{−} τ to indicate that deep subtyping has been used. A contra-variant virtual method can be extended, but it must remain contra-variant after its extension, i.e. of type M^{−} τ, and thus inaccessible. This may be surprising at first. The intuition if that #(V^{−} τ) should be R^{−} τ. However, a method of field-type R^{−} τ would be inaccessible, since its best type is unknown. Thus R^{−} τ has been identified with M^{−} τ.

For convenience, we also introduce a new constant F that is a top type for fields. That is, we assume V^{−} τ <: F and U <: F (all other relations hold by transitivity).

         P τ A           R τ M τ V τ  M^{−} τ V^{−} τ  R^{+} τ U F

Static Dynamic Allowed
φ # φ Pre Type .ℓ ↼ ↽
P τ U   √ <:τ τ ∀
A    U       <:τ ⊥ ∀
R τ φ √ <:τ τ τ
R^{+} τ φ √ <:τ τ ⊥
M τ φ  <:τ ⊥ τ
M^{−} τ φ  ∀ ⊥ τ
U φ  ∀ ⊥ ⊥
V τ R τ  <:τ ⊥ τ
V^{−} τ M^{−} τ  ∀ ⊥ τ

Figure 1: Structure of field types

The final structure of field types and subtyping axioms are summarized in figure 1. Thick arrows represent the function #. Thick nodes are used instead of reflexive thick arrows, that is, thick nodes are left invariant by #. Thin arrows represent subtyping. We added a redundant but useful distinction between continuous and dashed thin arrows. They are respectively covariant and contra-variant by type-extension: when a continuous arrow connects τ_{1} and τ_{2}, then # τ_{1} is also a subtype of # τ_{2}; the inverse applies to dashed arrows.

Although it is easy to give intuitions for parts of the hierarchy taken alone (variances, virtual methods, idempotent field-types), we are not able to propose a good intuition for the whole hierarchy. The different components are modular technically, but their intuitive, thus approximative descriptions, cannot be composed here. We think that the field-type hierarchy should be understood locally, and then considered as such.

The table on the right is a summary of field types and their properties. The entry φ in the first column indicates the static external type. The second column # φ is its extension type, i.e. the static internal type. The two following columns tell whether the field is guaranteed to be present (√ sign) and its type if present. The reason for having <:τ instead of τ is the covariance of P. The symbol ∀ means any possible type. The last two columns describe access and overriding capabilities (⊥ means disallowed).

3 Formal developments

3.1 Types

We assume given a denumerable collection of type variables, written α, β, or χ. Type expressions, written with letter τ, are type variables, object types, or the top type T. An object type ζ(χ)[ℓ_{i}: φ_{i} ^{i∈I} ; φ] is composed of a finite sequence of fields ℓ_{i} : φ_{i}, without repetition, and a template φ for fields that are not explicitly mentioned. Variable χ is bound in the object type, and should only appear positively in φ_{i}’s as in φ.

τ ::= α | ζ(α)[ℓ_{i}: φ_{i} ^{i∈I} ; φ] | T
φ ::= A | P τ | R τ | M τ | V τ | R^{+} τ | M^{−} τ | V^{−} τ | U | F

The variance of an occurrence is defined in the usual way: it is the parity of the number of times a variable crosses a contra-variant position (i.e., the number of symbols V^{−} or M^{−}) on that path from the root to that occurrence. The set of free variables of τ is fv(τ). We write fv^{−}(τ) the subset of those variables that occurs negatively at least once.

Object types are considered equal modulo reordering of fields. They are also equal modulo expansion, that is, by extracting a field from the template:

ζ(χ)[ℓ_{i}: φ_{i} ^{i∈I} ; φ] = ζ(χ)[ℓ_{i}: φ_{i} ^{i∈I} ; ℓ: φ ; φ]  ℓ ≠ ℓ_{i}, ∀i ∈ I

Rules for the formation of types will be defined jointly with subtyping rules in figure 2 and are described below.

Notation For convenience and brevity of notation, we use meta-variables ρ for rows of fields, that is, syntactic expressions of the form (ℓ_{i}: φ_{i} ^{i∈I} ; φ_{0}), where φ_{i}’s and I are left implicit. We write ρ(ℓ) the value of ρ in ℓ, that is, φ_{i} if ℓ is one of the ℓ_{i}’s, or φ_{0} otherwise. We write ρ \ ℓ for (ℓ_{i}: φ_{i} ^{i∈I,ℓ_{i}≠ℓ} ; φ_{0}). and ℓ : φ; ρ for (ℓ: φ ; ℓ_{i}: φ_{i} ^{i∈I,ℓ_{i}≠ℓ} ; φ_{0}). If R is a relation, we write ρ R ρ′ for ∀ℓ, ρ(ℓ) R ρ′(ℓ).

This is just a meta-notation that is not part of the language of types. It can always be expanded unambiguously into the more explicit notation (ℓ_{i}: φ_{i} ^{i∈I} ; φ).

3.2 Type extension

We define the extension of field type φ, written # φ by the two first columns of the table 1. Type extension is lifted to object types homomorphically, i.e., # ζ(χ)[ρ] is ζ(χ)[# ρ]. The extension is not defined for type variables, nor for F. Note that the extension is idempotent, that is #(# τ) is always equal to # τ.

Well-formation of environments

(Env ∅) ; \overline{∅ ⊢ ⋄}  (Env x) ; \frac{E ⊢ τ <: T  x ∉ dom (E)}{E, x : τ ⊢ ⋄}  (Env α) ; \frac{E ⊢ τ <: T  α ∉ dom (E)}{E, α <: τ ⊢ ⋄}

General subtyping

(Sub Var) ; \frac{E, α <: τ, E′ ⊢ ⋄}{E, α <: τ, E′ ⊢ α <: τ} (Sub Ref F)

\frac{E ⊢ φ <: F}{E ⊢ φ <: φ}

(Sub Ref T)

\frac{E ⊢ τ <: T}{E ⊢ τ <: τ}

(Sub Trans T)

\frac{E ⊢ τ_{1} <: τ_{2} E ⊢ τ_{2} <: τ_{3}}{E ⊢ τ_{1} <: τ_{3}}

(Sub Trans F)

\frac{E ⊢ φ_{1} <: φ_{2} E ⊢ φ_{2} <: φ_{3}}{E ⊢ φ_{1} <: φ_{3}}

Field subtyping (assuming E ⊢ τ <: T)

{(Sub PA) \atop E ⊢ P τ <: A}    {(Sub PR) \atop E ⊢ P τ <: R τ}  {(Sub AM) \atop E ⊢ A <: M τ}  {(Sub UF) \atop E ⊢ U <: F}    {(Sub RR^{+}) \atop E ⊢ R τ <: R^{+} τ}  {(Sub RM) \atop E ⊢ R τ <: M τ}
{(Sub R^{+}U) \atop E ⊢ R^{+} τ <: U}      {(Sub MV) \atop E ⊢ M τ <: V τ}  {(Sub MM^{−}) \atop E ⊢ M τ <: M^{−} τ}  {(Sub M^{−}U) \atop E ⊢ M τ <: U}      {(Sub VV^{−}) \atop E ⊢ V τ <: V^{−} τ}

{(Sub V^{−}F) \atop E ⊢ V^{−} τ <: F}

(Sub PP) ; \frac{E ⊢ τ <: τ′}{E ⊢ P τ <: P τ′}  (Sub R^{+}R^{+}) ; \frac{E ⊢ τ <: τ′}{E ⊢ R^{+} τ <: R^{+} τ′}  (Sub M^{−}M^{−}) ; \frac{E ⊢ τ <: τ′}{E ⊢ M^{−} τ′ <: M^{−} τ}  (Sub V^{−}V^{−}) ; \frac{E ⊢ τ <: τ′}{E ⊢ V^{−} τ′ <: V^{−} τ}

Object subtyping

(Sub TT) ; \frac{E ⊢ ⋄}{E ⊢ T <: T}

(Sub Obj OK)

\frac{E, χ <: T ⊢ ρ <: F χ ∉ fv^{−}(ρ)}{E ⊢ ζ(χ)[ρ] <: T}

(Sub Obj Invariant) (τ ≡ ζ(χ)[ρ], τ′ ≡ ζ(χ)[ρ′])

\frac{E ⊢ τ <: T  E ⊢ τ′ <: T  E, χ <: T ⊢ ρ <: ρ′}{E ⊢ τ <: τ′}

Figure 2: Types and Subtypes

3.3 Expressions

Expressions are variables, objects, method invocation, and method overriding.

a ::= x | ζ(χ, τ)[ℓ_{i}: ς(x_{i})a_{i}] | a.ℓ | a.ℓ ↼ ↽ ζ(χ, τ)ς(x)a

The expression a.ℓ ↼ ↽ ζ(χ, τ)ς(x)a_{ℓ} is the extension of a on field ℓ with a method ς(x)a_{ℓ}. The expression (χ, τ) binds χ to the type of self in a_{ℓ} and indicates that the resulting type of the extension should be τ. This information is important so that types do not have to be inferred but only checked. Field update is just a special case of object extension. This is more general, since the selection between update and extension is resolved dynamically.

3.4 Well formation of types and subtyping

Typing environments are sequences of bindings written with letter E. There are free kinds of judgments (the second and third ones are similar):

E ::= ∅ | α <: τ | x : τ  Typing environments
E ⊢ ⋄  Environment E is well-formed
E ⊢ τ <: τ′  Regular type τ is a subtype of τ′ in E
E ⊢ φ <: φ′  Field type φ is a subtype of φ′ in E
E ⊢ a : τ  Expression a has type τ in E

The subtyping judgment E ⊢ τ <: T is used to mean that τ is a well-formed regular type in E, while E ⊢ φ <: F means that φ is a well-formed field-type in E. Thus, T and F also play a role of kinds. For sake of simplicity, we do not allow field variables α <: F in environments. We have used different meta-variables τ and φ for regular types and field-types for sake of readability, although this is redundant with the constraint enforced by the well-formation rules. The formation of environments is recursively defined with rules for the formation of types and subtyping rules given in figure 2.

The subtyping rules are quite standard. Most of the rules are dedicated to field subtyping; they formally described the relation that was drawn in figure 1. A few facts are worth noticing. First we cannot derive E ⊢ F <: F. Thus F is only used in E ⊢ φ <: F to tell that φ is a well-formed field type. It prevents using F in object types. The typing rule Sub PA is also worth consideration. By transitivity with other rules, it allows P τ to be a subtype of M τ′, even if types τ and τ′ are incompatible. However, it remains true, and this is essential, that P τ is a subtype of R τ′ if and only if τ is a subtype of τ′.

The rule Sub Obj Invariant describes subtyping for object types. As explained above, row variables are just a meta-notation; thus, the judgment E ⊢ ρ <: ρ′ is just a short hand for E ⊢ ρ(ℓ) <: ρ′(ℓ) for any label ℓ, which only involves a finite number of them. This rule is restrictive and prevents (positive) occurrences of self to be replaced by # τ where τ is the current type of the object. In particular, object types cannot be unfolded (see section 6.2).

3.5 Typing rules

Typing rules are given in figure 3. The rules for subsumption, variables, and method invocation are quite standard.

Rule Expr Object has been discussed earlier. The last premise says that the fields ℓ_{i} may actually be super-types of P τ_{i} in ρ and other fields may also be super types of A. One cannot simply require that ρ be (ℓ_{i} : P τ_{i} ^{i∈I}; A) and later use subsumption, since the assumption made on the type of x_{i} while typing a_{i} could then be too weak.

Rule Expr Update is similar to the overriding rule in [3]. This rule is important since it permits both internal and external updates: the result type of the object is exactly the same as the one before the update.

On the contrary, rule Expr Extend is intended to add new methods that were not necessarily defined before, and thus change the type of the object. There are three different sub-cases in rule Expr Extend; the one that applies is uniquely determined by the given type τ. Then the type of field ℓ in the argument is deduced from the small table.

(Expr Subsumption)

\frac{E ⊢ a : τ E ⊢ τ <: τ′}{E ⊢ a : τ′}

(Expr Var) ; \frac{E, x : τ, E′ ⊢ ⋄}{E, x : τ, E′ ⊢ x : τ}

(Expr Object) (τ ≡ ζ(χ)[ρ])

\frac{E, χ <: # τ, x_{i} : χ ⊢ a_{i} : τ_{i}, i ∈ I E, χ <: # τ ⊢ (P τ_{i} ^{i∈I}; A) <: ρ}{E ⊢ ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}] : τ}

(Expr Select)

\frac{E ⊢ a : τ E ⊢ τ <: ζ(χ)[ℓ: R^{+} τ_{ℓ} ; U]}{E ⊢ a.ℓ : τ_{ℓ}\{τ/χ\}}

(Expr Update)

\frac{E ⊢ a : τ  E ⊢ τ <: ζ(χ)[ℓ: R τ_{ℓ} ; ρ_{0}]  E, χ <: # τ, x : χ ⊢ a_{ℓ} : τ_{ℓ}}{E ⊢ a.ℓ ↼ ↽ ζ(χ, τ)ς(x)a_{ℓ} : τ}

(Expr Extend) (τ ≡ ζ(χ)[ρ])

\frac{\begin{matrix}(φ_{0}, ρ(ℓ)) ∈ \{(A, P τ_{ℓ}), (V τ_{ℓ}, R τ_{ℓ}), (V^{−} τ_{ℓ}, M^{−} τ_{ℓ})\} \\ E ⊢ a : ζ(χ)[ℓ: φ_{0} ; ρ \ ℓ] E, χ <: # τ, x : χ ⊢ a_{ℓ} : τ_{ℓ} \end{matrix}}{E ⊢ a.ℓ ↼ ↽ ζ(χ, τ)ς(x)a_{ℓ} : τ}

Figure 3: Typing rules

Rules Expr Extend and Expr Update both apply only when τ is of the form ζ(χ)[ℓ: P τ_{ℓ} ; ρ] or ζ(χ)[ℓ: R τ_{ℓ} ; ρ]. Then, the requirements on the type of a are the same (letting the premise of Sub Extend be preceded by a subsumption rule). Thus, different derivations lead to the same judgment. It would also be possible to syntactically distinguish between object extension and method update, as well as to separate the extension between three different primitive corresponding to each of the three typing cases.

3.6 Operational semantics

We give a reduction semantics for a call-by-value strategy. Values are reduced to objects. A leftmost outermost evaluation strategy is enforced by the evaluation contexts C.

v ::= ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}] C ::= {} | C.ℓ | C.ℓ ↼ ↽ ζ(τ, χ)ς(x)a

The reduction rules are given in figure 4. Since programs are explicitly typed, the reduction must also manipulate types in order to maintain programs both well-formed and well-typed, even though it is not type-driven. In fact, the reduction uses an auxiliary binary operation on types φ ↼ ↽ φ′, to recompute the witness type of object values during object extension. It is defined in figure 5. The partial φ ↼ ↽ φ′ is extended to object types homomorphically, i.e., ζ(χ)[ρ] ↼ ↽ ζ(χ)[ρ′] is ζ(χ)[ρ ↼ ↽ ρ′]. Type extension is defined so as it validates lemma 4. When there is some flexibility, we sought for more uniformnity. Type extension is undefined when the cell is left empty in the figure. Those are cases that will never meet the hypotheses of lemma 4.

Let ℓ and ℓ_{i} ^{i∈I} be distinct labels, j in I,

and v be of the form ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}].

v.ℓ_{j} ⟶ a_{j}{τ/χ}{v/x} (Select) v.ℓ_{j} ↼ ↽ ζ(χ, τ′)ς(x)a ⟶ ζ(χ, τ ↼ ↽ τ′)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I−j}, ℓ_{j} = ς(x)a] (Update) v.ℓ ↼ ↽ ζ(χ, τ′)ς(x_{0})a_{0} ⟶ ζ(χ, τ ↼ ↽ τ′)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}, ℓ = ς(x)a] (Extend) if a_{1} ⟶ a_{2} then C{a_{1}} ⟶ C{a_{2}} (Context)

Figure 4: Reduction rules

↼ ↽ φ′ # φ
P τ′, A   U   R τ′, R^{+} τ′ M τ′ M^{−} τ′ V τ′ V^{−} τ′
P τ, A  φ′  U
R τ, R^{+} τ, U, M^{−} τ  .  φ  φ
φ  M τ  . .  R τ  φ  V τ  φ  φ
V τ  . .  R τ  φ  R τ
V^{−} τ  …  .  M^{−} τ  .  φ  M^{−} τ
# φ′  U  φ′  R τ′ M^{−} τ′

Figure 5: Type reduction φ ↼ ↽ φ′

4 Soundness of the typing rules

The soundness of the typing rules results from a combination of subject reduction and canonical forms. The proof of subject reduction is standard (see [3] for instance). A few classical lemmas help simplifying the main proof. Lemma 1 (Bound weakening) If E ⊢ τ <: τ′ and E, α <: τ′, E′ ⊢ J, then E, α <: τ, E′ ⊢ J. \underline{Proof}: By induction on the size of the proof of the derivation of the second. Lemma 2 (Substitution)

1. If E, α <: τ, E′ ⊢ J and E ⊢ τ′ <: τ, then E, E′{τ′/α} ⊢ J {τ′/α}.

2. If E, x : τ, E′ ⊢ J and E ⊢ a : τ, then E, E′ ⊢ J {a/x}. Lemma 3 (Structural subtyping)

1. If τ ≡ ζ(χ)[ρ] and E ⊢ τ <:τ′, then τ′ is either T or of the form ζ(χ)[ρ′] and E, χ<:T ⊢ ρ<:ρ′.

2. If E ⊢ φ <: R τ_{ℓ}, then φ is either R τ_{l} or P τ_{0} where E ⊢ τ_{0} <: τ_{ℓ}.

3. If E ⊢ φ <: R^{+} τ_{ℓ}, then φ is either P τ_{0}, R τ_{0}, or R^{+} τ_{0} where E ⊢ τ_{0} <: φ_{ℓ}.

4. If E ⊢ φ <: P τ_{ℓ}, then φ is P τ_{0} where E ⊢ τ_{0} <: τ_{ℓ}.

Etc.

\underline{Proof}: By induction on the size of subtyping derivations. Should use the fact that transitivity rules can be pushed to the leaves.

The proof of subject reduction also uses an essential lemma that relates computation on types to subtyping. Actually, the proof does not depend on the particular definition of #, but only on the following lemma.

Lemma 4 (Type computation) Let τ and τ′ be two object types ζ(χ)[ρ] and ζ(χ)[ρ′]. Assume that there exists a row ρ′′ such that E, χ <: T ⊢ ρ <: ρ′′ and for each label ℓ, the pair (ρ′′(ℓ), ρ′(ℓ)) is one of the four forms (A, P τ_{ℓ}), (V τ_{ℓ}, R τ_{ℓ}), (V^{−} τ_{ℓ}, M^{−} τ_{ℓ}), or (φ, φ). Let τ̂ be τ ↼ ↽ τ′ and ρ̂ be ρ ↼ ↽ ρ′. Then,

E ⊢ τ̂ <: τ′  E ⊢ # τ̂ <: # τ  E ⊢ # τ̂ <: # τ′

Moreover, in the three first cases, if E, χ <: T ⊢ ρ(ℓ) <: ρ′(ℓ), then E, χ <: T ⊢ ρ(ℓ) <: ρ̂(ℓ); otherwise E, χ <: T ⊢ P τ_{ℓ} <: ρ̂(ℓ).

Lemma 5 (Virtual methods) If E ⊢ τ <: ζ(χ)[U], then E ⊢ τ <: # τ.

\underline{Proof}: This is obviously true field by field: the only field that does not satisfy E ⊢ τ <: # τ are virtual fields, which are excluded if E ⊢ τ <: U. The property easily follows for object types.

Theorem 1 (Subject Reduction) Typings are preserved by reduction. If E ⊢ a : τ_{a} and a ⟶ a′ then E ⊢ a′ : τ_{a}.

Theorem 2 (Canonical Forms) Well-typed expressions that cannot be reduced are values. If ∅ ⊢ a : τ and there exists no a′ such that a ⟶ a′, then a is a value.

\underline{Proof}: If a value v has type ζ(χ)[ℓ: P τ ; U], then v must have a field ℓ. The theorem is then a trivial induction on the size of a, assuming that a cannot be reduced.

5 Examples

For simplicity, we assume that the core calculus has been extended with abstraction and application. This extension could either be primitive or derived from the encoding given in section 5.6. For brievity, we write a.ℓ ↼ ↽ a′ instead of a.ℓ ↼ ↽ ζ(χ, τ)ς(z)a′ when a′ does not depend on the self parameter z. In practice, other abbreviations could be made, but we avoid them here to reduce confusion.

We consider the simple example of points and colored points. These objects can of course already be written in [3]. The expressiveness of our calculus is not so much its capability to write new forms of complete objects but to provide new means of defining them. This provides more flexibility, increases security in several ways , and removes the complexity of the encoding of classes into objects.

5.1 Objects

A point object p_{0} can be defined as follows:

ζ(χ, point)[x = 0 ; mv = ς(z)λy.(z.x ↼ ↽ y) ; print = ς(z)print int z.x]

where point is ζ(χ)[x: Rint ; mv: Pint → χ ; print: Punit ; A]. As in [3], new points can be created using method update as in p_{0}.x ↼ ↽ ζ(χ, point)ς(z)1. Moreover, colored points can be defined inheriting from points:

cpoint =^{△} ζ(χ)[x: Rint ; c: Rbool ; mv: Pint → χ ; print: Punit ; A]

cp =^{△} (p_{0}.c ↼ ↽ ζ(χ, cpoint)ς(z)true).print ↼ ↽ ζ(χ, cpoint)ς(z)if z.c then print int z.x

When two values of different types have a common super-type τ, they can be interchanged at type τ. Here, cpoint is not a subtype of point, since both types carry too precise type information. However, they admit the common super-type ζ(χ)[x: Rint ; c: U ; mv: Pint → χ ; print: Punit ; A]..

5.2 Abstraction via subtyping

Subtyping can also be used to enforce security. For instance, field x may be hidden by weakening its type to U. Similarly, method mv may be protected against further redefinition by weakening its type to R^{+} τ. That is, by giving p_{0} the type ζ(χ)[mv: R^{+}int → χ ; print: Runit ; U]. While method mv can no longer be directly redefined, there is still a possibility for indirect redefinition. For instance, method print could have been written so that it overrides method mv before printing. To ensure that a method can never be redefined, directly or indirectly, it must be given type R^{+} τ at its creation.

5.3 Virtual methods

The creation of new points by updating the field of an already existing point is not quite satisfactory since it requires the use of default methods to represent the undefined state, which are often arbitrary and may be a source of errors. Indeed, a class of points can be seen as a virtual point lacking its field components.

POINT =^{△} ζ(χ)[x: Vint ; mv: Pint → χ ; print: Punit ; A]

P =^{△} ζ(χ, POINT)[mv = ς(z)λy.(z.x ↼ ↽ y) ; print = ς(z)print int z.x]

New points are then created by filling in the missing fields:

new point=^{△} λy.(P.x ↼ ↽ ζ(χ, point)ς(z)y) p_{1} =^{△} new point 0

5.4 Traditional class-based perspective

To keep closer to the traditional approach, we may by default choose to hide both fields corresponding to instance variables and the extendible capabilities of the remaining methods. For instance, treating x as an instance variable, and mv and print as “regular” methods, we choose ζ(χ)[mv: R^{+}int → χ ; print: R^{+}unit ; U] for point. Intuitively, the object-type point hides all information that is not necessary to increase security. Conversely, the class-type POINT remains as precise as possible, to keep expressiveness. Indeed, a class of points is still an object. However, as opposed to the previous section, we adopt some uniform, more structured style, treating “real” objects differently from those representing classes.

In colored points, we may choose to leave field c readable and overridable, as if we defined two methods set c and get c.

cpoint =^{△} ζ(χ)[c: Rbool ; mv: R^{+}int → χ ; print: R^{+}unit ; U]

Single inheritance is obtained by class extension:

CPOINT =^{△} ζ(χ)[x: Vint ; c: Vbool ; mv: Pint → χ ; print: Punit ; A]

CP =^{△} (P.print ↼ ↽ ζ(χ, CPOINT)ς(z)if z.c then print int z.x)

new cpoint=^{△} λy.λw.(CP.x ↼ ↽ ζ(χ, cpoint)ς(z)y).c ↼ ↽ ζ(χ, cpoint)ς(z)w

While CPOINT is not a subtype of POINT at the class level, we recover the usual relationship that cpoint is a subtype of point at the object level. Moreover, at the object level, types are invariant by #. Thus, we also recover the subtyping relation of [3]. In particular, object types can be unfolded.

5.5 An advanced example

A colorable point p′ is a point prepared to be colored without actually being colored. It can be obtained by adding to the point p_{0} an extra method paint that when called with an argument y returns the colored point obtained by adding the color field c with value y and by updating the print method of p_{0}.

p′ =^{△} p_{0}.paint ↼ ↽ ς(z, point′)λy.

((z.c ↼ ↽ y).print ↼ ↽ ζ(χ, cpoint)ς(z)if z.c then print int z.x)

where point′ is

ζ(χ)[x: Rint ; ...print: Runit ; paint: Pbool → cpoint ; c: Mbool ; U]

This example may be seen as the installation (method paint) of a new behavior (method print) that interacts with the existing state x and adds some new state c. The above solution becomes more interesting if each installation involves many methods, and especially if several installation are either different fields of the same objects or the same field of different objects. Then, the installation procedure can be selected dynamically by message invocation instead of manually by applying an external function to the object.

5.6 Encoding of the lambda-calculus

This part improves the encoding proposed in [3]. It also illustrates the use of virtual methods and variances. The untyped encoding of the lambda-calculus into objects in [3] is the following^{2}:

⟨⟨x⟩⟩ =^{△} x.arg ⟨⟨λx.M⟩⟩ =^{△} [arg = ς(x)x.arg ; val = ς(x).⟨⟨M⟩⟩]

⟨⟨M M′⟩⟩ =^{△} (⟨⟨M⟩⟩.arg ↼ ↽ ς(x)⟨⟨M′⟩⟩).val

2If both functions and objects co-exist, one should actually mark variables introduced by the encoding of functions so as to leave the other variables unchanged.

A function is encoded as an object with a diverging method arg. The encoding of an application overrides the method arg of the encoding of the function with the encoding of the argument and invokes the method val of the resulting object. Programs obtained by the translation of functional programs will never call val before loading the argument. However, if the encoding is used as a programming style, the type system will not provide as much safety as a type system with primitive function types would. The method val could also be called, accidently, before the field arg has been overridden. In general, this will, in turn, call the method arg and diverge. The use of default diverging methods is a hack that palliates the absence of virtual methods. It can be assimilated to a “method not understood” type error and one could argue that the encoding of [3] is not strongly typed.

The encoding can be improved using object extension to treat a function λx.M as an object [val = ς(x).⟨⟨M⟩⟩] with a virtual method arg (remember that x.arg may appear in ⟨⟨M⟩⟩). The type-system will then prevent the method val to be called before the argument has been loaded. More precisely, let us consider the simply typed lambda-calculus:

t ::= α | t → t  M ::= x | λx : t.M | M M

Functional types are encoded as follows:

⟨⟨α⟩⟩ =^{△} α ⟨⟨t → t′⟩⟩ =^{△} ζ(χ)[arg: V^{−}⟨⟨t⟩⟩ ; val: R^{+}⟨⟨t′⟩⟩ ; U]

This naturally induces a subtyping relation between function types that is contra-variant on the domain and covariant on the co-domain. The typed encoding is given by the following inference rules:

\frac{x : t ∈ A}{A ⊢ x : t ⇒ x.arg}        \frac{A, x : t ⊢ M : t′ ⇒ a  x ∉ dom (A)}{A ⊢ λx : t.M : t → t′ ⇒ ζ(χ, ⟨⟨t → t′⟩⟩)[val = ς(x).a]}

\frac{A ⊢ M : t′ → t ⇒ a A ⊢ M′ : t′ ⇒ a′}{A ⊢ M M′ : t ⇒ (a.arg ↼ ↽ ζ(χ, #⟨⟨t → t′⟩⟩)ς(x)a′).val}

It is easy to see that the translation transforms well-typed judgments ∅ ⊢ M : t into well-typed judgments ∅ ⊢ ⟨⟨M⟩⟩ : ⟨⟨t⟩⟩.

As in [3], the translation provides a call-by-name operational semantics for the lambda-calculus. The encoding of [3] also provides an equational theory for the object calculus and, thefore, for the lambda calculus, via translation, which we do not.

6 Discussion

6.1 Variations

Several variations can be made by consistently modifying field-types, their subtyping relationship, and the typing rule for object extension. The easiest is to drop some subtyping asumption (such as Sub PP, or Sub PA) or drop the field-type P τ altogether. This weakens the type system (some examples are not typable any longer), but it retains the essential features. More significant simplifications can be made at the price of a higher restriction of expressiveness. For instance, virtual field-types could be removed.

Some extensions or modifications to the type hierarchy are also possible. For instance, one could introduce fields of type †P τ that do no depend on any other method. These methods would be dual of those of type P τ on which no other method depend; somehow they would behave as record fields in the sense they could always be called even if the object is virtual. This extends to field-types †R τ and † R^{+} τ similarly.

6.2 Better subtyping for object types

The subtyping rule Sub-Obj-Invariant does not allow unfolding of object types. It is thus weaker that the Abadi-Cardelli:

(Sub Obj Deep) (τ ≡ ζ(χ)[ρ], τ′ ≡ ζ(χ)[ρ′])
\frac{E ⊢ τ <: T  E ⊢ τ′ <: T  E, χ <: τ ⊢ ρ <: ρ′}{E ⊢ τ <: τ′}

This rule would not be correct, since it would not be transitive. Indeed transitivity would require that A ⊢ τ <: τ′ implies A ⊢ # τ <: # τ′ which is not true.

Just replacing the bound T of χ in Sub Obj Deep by # τ would actually not behave well with respect to transitivity. In a preliminary version of this work [26], we added another premise to recover transitivity. However, this simultaneously weakens the subtyping relationship, and some useful examples become untypable.

It should be possible to define a subtyping rule that allows unfolding of self types only when objects have no more extension capabilities. It seems however, that the subtyping structure of fields should either be simplified (e.g. eliminating the arrow from M τ to V τ) or almost equivalently enriched to avoid M τ <: V τ but only once in a certain definite state.

6.3 Extensions

Imperative update is an orthogonal issue to the one studied here, and it could be added without any problem. Object extension should, of course, remain functional.

Equational theory We see no difficulty in adding an equational theory to our calculus, but this remains to be investigated. Treating object extension as a commutative operator would allow to reduce object construction to a sequence of object extensions of the empty object (virtual methods would be crucial here).

Higher-order types As shown above, our objects are sufficiently powerful to represent classes. As opposed to [3], this does not necessitate higher-order polymorphism because methods are already required to be parametric in all possible extensions of self.

The addition of higher-order polymorphism might still be useful, in particular to enable parametric classes. We believe that there is no problem in constraining type abstraction by some supertype bound, written α <: τ as in F_{<:}. However, it would also be useful to introduce #-bounds of the form α <: # τ. This might require more investigation.

Row variables and binary methods We have used row variables only as a meta-notation for simplifying the presentation. It would be interesting to really allow row variables in types. This would probably augment the expressiveness of the language, since it should provide some form of matching that revealed quite useful, especially for binary methods [11, 9, 27].

Actually, it remains to investigate how the presented calculus could be extended to cope with binary methods. Row variables might not be sufficient to express matching, and some new form of matching might have to be found. It is unclear whether the known solutions [10] could be adapted to our calculus.

7 Comparison with other works

Our proposal is built on the calculus of objects of Abadi and Cardelli [3], which is invoked throughout this paper. Our use of variance annotations is in principle similar to theirs. By attaching variance annotations to field-types rather than to fields themselves, we eliminate some useless types such as M^{+} τ. Indeed, such a field could not be overriden, nor accessed, and thus it could be just given type U. (Our use of variances also eliminate the ability to specify the type of a field without specifying its variance, which may cause problem with type inference [22].) An essential imported tool is the structure of record-types of [23], which was originally designed for type inference in ML [24]. The use of a richer structure of record types has previously been proposed for type checking records [15, 16, 13, 12]. To our knowledge, the benefits of symmetric information were first transfered from record types to object types in [25]. There, first-order typing rules for objects with extension and both deep and width subtyping were roughly drafted without any formal treatment.

A similar approach has also been independently proposed by Bono, Liquori and others. Their first related work [6] has later lead to many closely related proposals [8, 7, 4, 18, 17, 19]. Most of these are extensions of the Fisher-Honsel calculus of objects [20]. The differences between their approach and the one of [3] (which is also ours) are not always significant but they make a close comparisson more difficult. Only two of these works [19, 18] are extensions of the Abadi-Cardelli calculus of objects [3] and are thus more connected to our proposal. The first-order version [19], is subsumed by both [25] (which also covers deep subtyping) and [18] (which also addresses self types.) Our proposal extends both [25] and [18].

The most interesting comparison can be made with [18]. The main motivation and the key idea behind both proposals are similar: they integrate object subtyping and object extension, using a richer type structure to preserve type soundness. Saturated vs diamond types correspond to our object-types with a field template U vs A, respectively. Our treatment seems more uniform. We only have one kind of object types. We distinguish between the “saturation” and “diamond” properties in fields instead of objects. As a result, we can write an object type that is saturated, except for a few particular fields. Our proposal also includes several additional features: it addresses deep subtyping and virtual methods; it also allows methods to extend self. Moreover, in our proposal, the subtyping relationship is structural for object types. Additionally, subtyping axioms are only given at the level of fields, each one of them treating a different important subtyping capability. As a result, object types have a more regular structure, and can easily be adapted to further extensions. We think this is easier to understand, to modify, and to manipulate.

An alternative to virtual methods has also been studied in [4], using a quite different approach, which consists in annotating each method with the list of all other methods they depend on. Thus, each method has a different view of self. Their approach to incomplete objects is, in principle, more powerful that ours; in particular, they can type programs that even traditional class-based languages would reject. We found their types of objects too detailed, and thus their proposal less practical than ours. (Tracing dependencies is closer to some form of program analysis than to standard type systems.) In fact, we intendedly restricted our type system so that methods have a uniform view of self. In practice, our solution is sufficient to capture common forms of inheritance.

In [20], pre-objects have pro-types and can be turned into objects with obj-types by subtyping. Pro-types and obj-types are similar to our object types ζ(χ)[ℓ_{i}: R τ_{i} ^{i∈I} ; A] and ζ(χ)[ℓ_{i}: R^{+} τ_{i} ^{i∈I} ; U]. One difference is that, in our case, subtyping is defined and permitted field by field rather than all at once. Fisher and Mitchell also studied the relationship between objects and classes in [14]. They use bounded existential quantification to hide some of the structure of the object in the public interface. This still allows public methods to be called, while private methods become innaccessible. In our calculus, the richer structure of objects permits to use subtyping instead of bounded existential quantification to provide a similar abstraction. This is not suprising, theoretically, since subtyping, as existential quantification, is a lost of type information. However, this is practically a significant difference, since subtyping allows more explicit type information but is less expressive. Another difference is that using the standard record types they had to introduce record sorts to express negative type information. As pointed out in a more recent paper [5], the design of the language of kinds becomes important for modularity. In particular, [5] improves over [14] by changing default kinds from unknown (U in our setting) to absent (A). Instead, our record types express positive and negative information symmetrically and are viewed as total functions from fields to types, which avoids the somehow ad hoc language of sorts.

In a recent paper, Riecke and Stone have circumvented the problem of merging extension with deep and width subtyping by changing the semantics of objects [28]. In fact, their semantics remain in correspondance with the standard semantics of objects in the general case, but the semantics of extension is changed so that the counter example becomes sound in the new semantics. They distinguish between method update and object extension. Then, a field that is already defined is automatically renamed by extension into an anonymous field that becomes externally inaccessible.

With their semantics, some of our enriched type information would become obsolete for ensuring type soundness, but it might remain useful for compile-time optimizations. Other pieces of information, e.g. virtual types, would remain quite pertinent.

8 Conclusion

We have proposed a uniform and flexible method for enriching type systems of object calculi by refining the field structure of object types, so that they carry more precise type information.

Applying our approach to the object calculus of Abadi and Cardelli, we have integrated object extension and depth and width subtyping, with covariant final methods and contra-variant virtual methods, in a type-safe calculus. When sufficient type information is revealed, objects may represent classes. Type information may also be hidden progressively, until objects can be used and interchanged in a traditional fashion.

An important gain is to avoid the encoding of classes as records of pre-methods. Instead, we provide a more uniform, direct approach. Another benefit of this integration is to allow mixed formed of classes and objects. The use of richer object types also increases both safety by capturing more dynamic misbehavior as static type errors and security by allowing more privacy via subtyping. Moreover, our approach subsumes several other unrelated proposals, and it might provide a unified framework for studying or comparing new proposals. Some extensions and variations are clearly possible, provided the operations on objects, their types and the subtyping hierarchy are changed consistently.

More investigation still remains to be done. Adding an equational theory to the calculus, would simplify our primitives, since objects could always be built field by field using object extension only. This might also be a first step towards a better integration of record-based and delegation-based object calculi. In the future, we would also like to study the potential increase of expressiveness that field and row variables could provide. Of course, investigating binary methods remains one of the most important issues.

Classes can be viewed as objects. We hope that an even richer type structure would finally enable to see objects for what they really are —records of functions— in the (yet untyped) selfapplication interpretation.

References

[1] Martín Abadi and Luca Cardelli. A theory of primitive objects: Untyped and first-order systems. In Theoretical Aspects of Computer Software, pages 296–320. Springer-Verlag, April 1994.

[2] Martín Abadi and Luca Cardelli. A theory of primitive objects: Second-order systems. Science of Computer Programming, 25(2-3):81–116, December 1995. Preliminary version appeared in D. Sanella, editor, Proceedings of European Symposium on Programming, pages 1-24. Springer-Verlag, April 1994.

[3] Martín Abadi and Luca Cardelli. A theory of objects. Springer, 1996.

[4] V. Bono, M. Bugliesi, M. Dezani-Ciancaglini, and L. Liquori. Subtyping Constraints for Incomplete Objects. In Proceedings of TAPSOFT-CAAP-97, International Joint Conference on the Theory and Practice of Software Development, Lecture Notes in Computer Science. Springer-Verlag, 1997.

[5] V. Bono and K. Fisher. An imperative, first-order calculus with object extension. In Informal Proceedings of the FOOL 5 workshop on Foundations of Object Oriented Programming, Sans Diego, CA, January 1998. To appear.

[6] V. Bono and L. Liquori. A subtyping for the fisher-honsell-mitchell lambda calculus of object. In Proc. of CSL-94, International Conference of Computer Science Logic, volume 933 of Lecture Notes in Computer Science, pages 16–30. Springer-Verlag, 1995.

[7] Viviana Bono and Michele Bugliesi. A lambda calculus of incomplete objects. In Proceedings of Mathematical Foundations of Computer Science(MFCS), number 1113 in Lecture Notes in Computer Science, pages 218–229, 1996.

[8] Viviana Bono and Michele Bugliesi. Matching constraints for the lambda calculus of objects. In Proceedings of (MFCS), 1997.

[9] Kim B. Bruce. Typing in object-oriented languages: Achieving expressibility and safety. Revised version to appear in Computing Surveys, November 1995.

[10] Kim B. Bruce, Luca Cardelli, Giuseppe Castagna, Valery Trifonov) the Hopkins Objects Group (Jonathan Eifrig, Scott Smith, Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):221–242, 1996.

[11] Kim B. Bruce, Angela Schuett, and Robert van Gent. Polytoil: A type-safe polymorphic object-oriented language. In ECOOP, number 952 in LNCS, pages 27–51. Springer Verlag, 1995.

[12] Luca Cardelli. Extensible records in a pure calculus of subtyping. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design, pages 373–425. MIT Press, 1994.

[13] Luca Cardelli and John C. Mitchell. Operations on records. In Fifth International Conference on Mathematical Foundations of Programming Semantics, 1989.

[14] K. Fisher and J. C. Mitchell. On the relationship between classes, objects and data abstraction. Theoretical And Practice of Objects Systems, To appear, 1998. A preliminary version appeared in the proceedings of the International Summer School on Mathematics of Program Construction, Marktoberdorf, Germany, Springer LNCS, 1997.

[15] Robert W. Harper and Benjamin C. Pierce. Extensible records without subsumption. Technical Report CMU-CS-90-102, Carnegie Mellon University, Pittsburg, Pensylvania, February 1990.

[16] Robert W. Harper and Benjamin C. Pierce. A record calculus based on symmetric concatenation. Technical Report CMU-CS-90-157, Carnegie Mellon University, Pittsburg, Pensylvania, February 1990.

[17] L. Liquori and G. Castagna. A Typed Lambda Calculus of Objects. In Proc. of ASIAN-96, International Asian Computing Science Conference, volume 1212 of Lecture Notes in Computer Science. Springer-Verlag, 1996.

[18] Luigi Liquori. Bounded polymorphism for extensible objects. Technical Report CS-24-96, Dipartimento di Informatica, Universita’ di Torino, 1997.

[19] Luigi Liquori. An Extended Theory of Primitive Objects: First Order System. In Proceedings of ECOOP-97, International European Conference on Object Oriented Programming, Lecture Notes in Computer Science. Springer-Verlag, 1997.

[20] John C. Mitchell and Kathleen Fisher. A delegation-based object calculus with subtyping. In Fundamentals of Computation Theory, number 965 in LNCS, pages 42–61. Springer, 1995.

[21] John C. Mitchell, Furio Honsell, and Kathleen Fisher. A lambda calculus of objects and method specialization. In IEEE Symposium on Logic in Computer Science, pages 26–38, June 1993.

[22] Jens Palsberg and Trevor Jim. Type inference of object types with variances. Private Discussion, 1996.

[23] Didier Rémy. Syntactic theories and the algebra of record terms. Research Report 1869, Institut National de Recherche en Informatique et Automatisme, Rocquencourt, BP 105, 78 153 Le Chesnay Cedex, France, 1993.

[24] Didier Rémy. Type inference for records in a natural extension of ML. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming. Types, Semantics and Language Design. MIT Press, 1993.

[25] Didier Rémy. Better subtypes and row variables for record types. Presented at the workshop on Advances in types for computer science at the Newton Institute, Cambridge, UK, August 1995.

[26] Didier Rémy. From classes to objects via subtyping. In European Symposium On Programming, volume 1381 of Lecture Notes in Computer Science. Springer, March 1998.

[27] Didier Rémy and Jérôme Vouillon. Objective ML: An effective object-oriented extension to ML. Theoretical And Practice of Objects Systems, To appear, 1998. A preliminary version appeared in the proceedings of the 24th ACM Conference on Principles of Programming Languages, 1997.

[28] Jon G. Riecke and Christopher A. Stone. Privacy via subsumption. In Informal Proceedings of the FOOL 5 workshop on Foundations of Object Oriented Programming, Sans Diego, CA, January 1998. To appear.

A Type computation

Lemma 4 (Type computation) Let τ and τ′ be two object types ζ(χ)[ρ] and ζ(χ)[ρ′]. Assume that there exists a row ρ′′ such that E, χ <: T ⊢ ρ <: ρ′′ and for each label ℓ, the pair (ρ′′(ℓ), ρ′(ℓ)) is one of the four forms (A, P τ_{ℓ}), (V τ_{ℓ}, R τ_{ℓ}), (V^{−} τ_{ℓ}, M^{−} τ_{ℓ}), or (φ, φ). Let τ̂ be τ ↼ ↽ τ′ and ρ̂ be ρ ↼ ↽ ρ′. Then,

E ⊢ τ̂ <: τ′  E ⊢ # τ̂ <: # τ  E ⊢ # τ̂ <: # τ′

Moreover, in the three first cases, if E, χ <: T ⊢ ρ(ℓ) <: ρ′(ℓ), then E, χ <: T ⊢ ρ(ℓ) <: ρ̂(ℓ); otherwise E, χ <: T ⊢ P τ_{ℓ} <: ρ̂(ℓ).

\underline{Proof}: Let E′ be E, χ <: T. By rule Sub Obj Invariant it sufficies to check

(1) E′ ⊢ ρ̂ <: ρ′  (2) E′ ⊢ # ρ̂ <: # ρ  (3) E′ ⊢ # ρ̂ <: # ρ′

(4) \{ \begin{matrix}E′ ⊢ ρ <: ρ̂ & if ρ′′ is ρ′, \\ ∃τ′_{ℓ}, E′ ⊢ τ_{ℓ} <: τ′_{ℓ} ∧ E′ ⊢ P τ′_{ℓ} <: τ̂(ℓ) & otherwise. \end{matrix}

independently for each cell of the table 5 and for any of the fourth possible forms (three first forms for (4)).

Case (φ): These cases cannot occur because all hypotheses cannot be met simultaneously.

Case first line: Note that this completely covers the case where (φ′′, φ′) is (A, P τ_{ℓ}). Properties (1) and (3) are immediate since φ̂ is φ′ and (2) is obvious since # φ is U. Since φ̂ is φ′, E′ ⊢ φ <: φ̂ follows from E′ ⊢ φ <: φ′, and E′ ⊢ φ′ <: φ̂ is always true, hence (4).

Case E′ ⊢ φ <: φ′: In particular, this covers the case where (φ′′, φ′) is (φ, φ).

Subcase φ̂ is φ: Then (1), (2) and (4) are obvious. When # φ′ is φ′, it happens that # φ is also φ, thus (3) is true. There are 6 remaining cases in the last two columns:

• In the last column, we must show that E′ ⊢ # φ<:M^{−} τ′. If φ is V^{−} τ or M^{−} τ, then E ⊢ τ′ <:τ, and since # φ is M^{−} τ, then E′ ⊢ # φ <: V^{−} τ′. Otherwise, φ is either R τ or M τ, invariant by # and E′ ⊢ φ <: M^{−} τ.

• In the preceding column, we must show that E′ ⊢ # φ<:R τ′ (5). Here and since E′ ⊢ φ<:φ′, φ is one of the form R τ or V τ, types τ and τ′ are equal, and # φ is R τ. Hence (5).

Other subcases: given that E′ ⊢ φ <: φ′, the only remaining subcase is when φ is M τ and φ′ is V τ′. Then τ and τ′ are equal and thus so are φ̂ and φ′. Hence (1) and (3). Clearly, we also have E′ ⊢ R τ <: M τ (2) and E′ ⊢ M τ <: V τ (4).

Case (φ′′, φ′) is (V τ_{ℓ}, R τ_{ℓ}), first line excluded: Then φ is either M τ or V τ with τ and τ_{l} equal and φ̂ is R τ. Hence (1) and, since φ̂ and φ′ are here invariant by #, we also have (3). Since both E′ ⊢ R τ <: M τ and E′ ⊢ R τ <: V τ, we also have (2). The hypothesis E′ ⊢ φ <: R τ_{ℓ} never holds. However, E′ ⊢ P τ_{l} <: R τ holds since τ and τ_{l} are equal.

Case (φ′′, φ′) is (V^{−} τ_{ℓ}, M^{−} τ_{ℓ}), first line excluded: If φ is either M τ or V τ with τ and τ_{l} equal and we reason as in the previous case. That is τ and τ_{l} are equal and φ̂ is R τ. In particular, (2) is unchanged. Since E′ ⊢ R τ_{l} <: M^{−} τ_{l}, we also have (1), (3) and E′ ⊢ P τ_{l} <: φ̂. The hypothesis E′ ⊢ φ <: M^{−} τ_{ℓ} holds when φ is M τ, and then (4) holds since φ̂ is φ.

Otherwise, φ is either M^{−} τ or V^{−} τ with E′ ⊢ τ_{ℓ} <: τ and φ̂ is M^{−} τ. Since E′ ⊢ M^{−} τ <: M^{−} τ_{ℓ}, i.e. E′ ⊢ φ̂ <: φ′, we have (1). Since M^{−}, i.e. both sides, are invariant by #, we also have (3). Since both # φ is equal to φ̂, which is invariant by #, we also have (2). The inequality E′ ⊢ φ <: φ′ holds when φ is M^{−} τ, i.e. φ̂, and then E′ ⊢ φ <: φ̂ trivially holds. Otherwise, (4) holds taking τ for τ′_{ℓ}.

B Subject reduction

Theorem 1 (Subject Reduction) Typings are preserved by reduction. If E ⊢ a : τ_{a} and a ⟶ a′ then E ⊢ a′ : τ_{a}.

\underline{Proof}: By induction on the size of a and cases on the reduction.

Case Red Select: The expression a is of the form v.ℓ_{j} where v is ζ(χ, τ)[ℓ_{i} = ς(x)a_{i} ^{i∈I}] and j is in I. It reduces to a_{j}{τ/χ}{v/x}. The derivation of E ⊢ a : τ_{a} ends with a subsumption rule preceded by rule Expr Select. Thus, there exists types τ′ and τ′′_{j} such that

E ⊢ v : τ′  E ⊢ τ′ <: ζ(χ)[ℓ_{j}: R^{+} τ′′_{j} ; U] (1)  E ⊢ τ′′_{j}{τ′/χ} <: τ_{a} (2)

The derivation E ⊢ v : τ′ itself ends with a subsumption rule preceded by rule Expr Object. Thus, τ is of the form ζ(χ)[ρ] and there exist τ_{i} ^{i∈I} such that

E, χ <: # τ, x_{i} : χ ⊢ a_{i} : τ_{i}, ∀i ∈ I (3) E, χ <: # τ ⊢ (ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ (4) E ⊢ τ <: τ′ (5)

By transitivity between (5) and (1), we have E ⊢ τ<:ζ(χ)[ℓ_{j}: R^{+} τ′′_{j} ; U] (6). By structural subtyping (lemma 3), and transitivity with (4), we have, in particular, E, χ <: T ⊢ P τ_{j} <: R^{+} τ′′_{j}.

By structural subtyping (lemma 3), E, χ <: T ⊢ τ_{j} <: τ′′_{j}. Thus, by subsumption applied to (3), E, χ <: # τ, x_{i} : χ ⊢ a_{i} : τ′′_{j} (7). The judgment (6) also implies that E ⊢ τ <: ζ(χ)[U], and by lemma 5 we have E ⊢ τ <: # τ. Therefore, applying substitution (lemma 2) to (7), we have E, x_{i} : τ ⊢ a_{i}{τ/χ} : τ′′_{j}{τ/χ}. Since E ⊢ v : τ, by substitution again, we have E ⊢ a_{i}{τ/χ}{v/x} : τ′′_{j}{τ/χ} (8). Since τ′′_{j} is covariant, it follows from (5) that E ⊢ τ′′_{j}{τ/χ} <: τ′′_{j}{τ′/χ} . By transitivity with (2), E ⊢ τ′′_{j}{τ/χ} <: τ_{a} (9). We conclude using subsumption applied to (8) with (9).

Case Red Extend: The expression a is of the form v.ℓ ↼ ↽ ζ(χ, τ′)ς(x_{0})a_{0} where v is ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}] and ℓ is not one of the ℓ_{i}’s. It reduces to ζ(χ, τ̂)[ℓ = ς(x_{0})a_{0} ; ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}] where τ̂ is τ ↼ ↽ τ′.

Let τ and τ′ be ζ(χ)[ρ] and ζ(χ)[ρ′] (this is not restrictive) and ρ̂ be ρ ↼ ↽ ρ′. A derivation of v.ℓ_{j} ↼ ↽ ζ(χ, τ′)ς(x)a ends with a subsumption rule preceded by rule Expr Extend. Thus, τ′ verifies:

{(φ_{0}, ρ′(ℓ)) ∈ \{(A, P τ_{ℓ}), (V τ_{ℓ}, R τ_{ℓ}), (V^{−} τ_{ℓ}, M^{−} τ_{ℓ})\} (1)  E ⊢ v : ζ(χ)[ℓ: φ_{0} ; ρ′] (2) \atop E, χ <: # τ′, x_{0} : χ ⊢ a_{0} : τ_{ℓ} (3)  E ⊢ τ′ <: τ_{a} (4)}

A derivation of (2) ends with subsumption preceded by rule Expr Object. Thus, τ verifies:

{E, χ <: # τ, x_{i} : χ ⊢ a_{i} : τ_{i}, ∀i ∈ I (5) E, χ <: # τ ⊢ (ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ (6) \atop E ⊢ τ <: ζ(χ)[ℓ: φ_{0} ; ρ′] (7)}

From (7), by structural subtyping, we have E, χ<:T ⊢ ρ<:(ℓ : φ_{0}; ρ′). Thus, E, χ<:T ⊢ ρ\ℓ<:ρ′ \ℓ. This, together with (1) meets the hypotheses of lemma 4. Therefore,

E ⊢ τ̂ <: τ′ (8)  E ⊢ # τ̂ <: # τ (9)  E ⊢ # τ̂ <: # τ′ (10)

Moreover, for some τ′_{ℓ}:

E, χ <: # τ ⊢ ρ \ ℓ <: ρ̂ \ ℓ (11)  E, χ <: # τ ⊢ τ_{ℓ} <: τ̂′_{ℓ} (12)  E, χ <: # τ ⊢ P τ′_{ℓ} <: ρ̂(ℓ) (13)

Combining (6), (11), and (13) we have E, χ <: # τ ⊢ (ℓ : P τ′_{ℓ}; ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ̂. By bound weakening, since (9), we get E, χ <: # τ̂ ⊢ (ℓ : P τ′_{ℓ}; ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ̂ (14). Combining (3) with (12), we have E, χ <: # τ′, x_{0} : χ ⊢ a_{0} : τ′_{ℓ} (15). By substitution lemma applied to (15) and (5), with (9) we have

E, χ <: # τ̂, x_{0} : χ ⊢ a_{0} : τ′_{ℓ} E, χ <: # τ̂, x_{i} : χ ⊢ a_{i} : τ_{i}, ∀i ∈ I

Combining with (14), we have E ⊢ a′ : τ̂. By subsumption applied with (8) and (4), we finally have E ⊢ a′ : τ_{a}.

Case Red Update: We reuse the same notations. The difference is that ℓ is now one the ℓ_{j} for j in I. The expression a is of the form v.ℓ ↼ ↽ ζ(χ, τ′)ς(x)a where v is ζ(χ, τ)[ℓ_{i} = ς(x_{i})a_{i} ^{i∈I}]. It reduces to ζ(χ, τ̂)[ℓ_{j} = ς(x)a ; ℓ_{i} = ς(x_{i})a_{i} ^{i∈I−j}].

We distinguish two subcases according to form of the typing derivation for a.

Subcase Expr Extend: This case is similar to the case for extension. The only differences in the proof if that here, from (6), (9) and (13), we have E, χ <: # τ̂ ⊢ (ℓ : P τ_{ℓ}; ℓ_{i} : P τ_{i} ^{i∈I−j}; A) <: ρ̂ instead of (14).

Subcase Expr Update: A derivation of v.ℓ ↼ ↽ ζ(χ, τ′)ς(x_{0})a_{0} ends with a subsumption rule preceded by rule Expr Update. Thus, τ′ verifies:

E ⊢ v : τ′ (1) E ⊢ τ′ <:ζ(χ)[ℓ: R τ_{ℓ} ; ρ_{0}] (2) E, χ<:# τ′, x_{0} : χ ⊢ a_{0} : τ_{ℓ} (3) E ⊢ τ′ <:τ_{a} (4)

A derivation of (1) ends with subsumption preceded by rule Object. Thus, τ verifies:

E, χ <: # τ, x_{i} : χ ⊢ a_{i} : τ_{i}, ∀i ∈ I (5)  E, χ <: # τ ⊢ (ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ (6)  E ⊢ τ <: τ′ (7)

From (7), by structural subtyping, we have E, χ <: T ⊢ ρ <: ρ′, which enables to apply lemma 4; we get

E ⊢ τ̂ <: τ′ (8)  E ⊢ # τ̂ <: # τ(9)  E ⊢ # τ̂ <: # τ′(10)  E, χ <: # τ ⊢ ρ <: ρ̂ (11)

Combining (11) with (6), we have E, χ<:# τ ⊢ (ℓ_{i} : P τ_{i} ^{i∈I}; A)<:ρ̂. By bound weakening, since (9), we have E, χ <: # τ̂ ⊢ (ℓ_{i} : P τ_{i} ^{i∈I}; A) <: ρ̂ (12). By structural subtyping (lemma 3) applied to (2), we have E, χ<:T ⊢ ρ′(ℓ)<:R τ_{ℓ}. By bound weakening with (10), we have E, χ<:# τ̂ ⊢ ρ′(ℓ)<:R τ_{ℓ}. By transitivity with (8) after applying structural subtyping, we get E, χ <: # τ̂ ⊢ ρ̂(ℓ) <: R τ_{ℓ}. By structural subtyping, we must have E, χ <: # τ̂ ⊢ P τ_{ℓ} <: ρ̂(ℓ). Combining this with (12), we have E, χ <: # τ̂ ⊢ (ℓ : P τ_{ℓ}; ℓ_{i} : P τ_{i} ^{i∈I−j}; A) <: ρ̂ (13).

By substitution lemma applied to (3) and (5), we have

E, χ <: # τ̂, x : χ ⊢ a : τ_{ℓ} E, χ <: # τ̂, x_{i} : χ ⊢ a_{i} : τ_{i}, ∀i ∈ I

Combining with (13), we have E ⊢ a′ : τ̂. By subsumption applied with (8) and (4), we finally have E ⊢ a′ : τ_{a}.

Case Context: Trivial using the induction hypothesis. 23