Classes = Objects + Data Abstraction

Kathleen Fisher^{∗} and John C. Mitchell^{†} Computer Science Department, Stanford University, Stanford, CA 94305

                       {kfisher,mitchell}@cs.stanford.edu

January 11, 1996

Abstract

We describe a type-theoretic foundation for object systems that include “interface types” and “implementation types,” in the process accounting for access controls such as C++ private, protected and public levels of visibility. Our approach begins with a basic object calculus that provides a notion of object, method lookup, and object extension (an object-based form of inheritance). In this calculus, the type of an object gives an interface, as a set of methods (public member functions) and their types, but does not imply any implementation properties such as the presence or layout of any hidden internal data. We extend the core object calculus with a higher-order form of data abstraction mechanism that allows us to declare supertypes of an abstract type and a list of methods guaranteed not to be present. This results in a flexible framework for studying and improving practical programming languages where the type of an object gives certain implementation guarantees, such as would be needed to statically determine the offset of a function in a method lookup table or safely implement binary operations without exposing the internal representation of objects. We prove type soundness for the entire language using operational semantics and an analysis of typing derivations. Two insights that are immediate consequences of our analysis are the identification of an anomaly associated with C++ private virtual functions and a principled, type-theoretic explanation (for the first time, as far as we know) of the link between subtyping and inheritance in C++, Eiffel and related languages.

1 Introduction

In theoretical studies of object systems, such as [AC94b, Bru93, FHM94, PT94] and the earlier papers appearing in [GM94], types are viewed as interfaces to objects. This means that the type of an object lists the operations on the object, generally as method names and return types, but does not restrict its implementation. As a result, objects of the same type may have arbitrarily different internal representations. In contrast, the type of an object in common practical objectoriented languages such as Eiffel [Mey92] and C^{+}^{+} [Str86, ES90] may impose some implementation constraints. In particular, although the “private” internal data of an object is not accessible outside the member functions of the class, all objects of the same class must have all of the private internal data listed in the class declaration. In this paper, we present a type-theoretic framework that incorporates both forms of type. We explain the basic principles by extending a core object calculus with a standard higher-order data abstraction mechanism as in [MP88, CW85]. We also discuss a special-purpose syntax that is closer to common practice and that eliminates a few minor syntactic inconveniences in our specific use of standard abstract data type declarations.

∗Supported in part by a Fannie and John Hertz Foundation Fellowship and NSF Grant CCR-9303099.

†Supported in part by NSF Grant CCR-9303099 and the TRW Foundation.

From a programming point of view, “interface” types are often more flexible than types that constrain the implementation of objects. With this form of type, we could define a single type of matrix objects, for example, then represent dense matrices with one form of object and sparse matrices with another. If the type only gives the interface of an object, then both matrix representations could have the same type and therefore be used interchangeably in any program. This kind of flexibility is particularly useful when we write library operations on matrices without assuming any particular implementation. Such library functions may be written using a standard interface type, without concern for how matrices might be implemented in later (or earlier) development of a software system.

Types that restrict the implementations of objects are also important. If we know that all point objects inherit a specific representation of x and y coordinates, for example, then a program may be optimized to take advantage of this static guarantee. The usual implementations of C^{+}^{+}, for example, use type information to statically calculate the offset of member data relative to the starting address of the object. (A similar calculation is used to find the offset of virtual member functions in the v-table at compile time; see [ES90, Section 10.7c].) Such optimizations are not possible in an untyped language such as Smalltalk [GR83] and would not be possible in a typed language where objects of a single type could have arbitrarily dissimilar implementations.

A second, more methodological reason that programmers may be interested in implementation types is that there are greater guarantees of behavioral similarity across subtype hierarchies. More specifically, traditional type systems generally give useful information about the signature (or domain and range) of operations. This is a very weak form of specification and, in many programming situations, it is desirable to have more detailed guarantees. While behavioral specifications are difficult to manipulate effectively, we have a crude but useful approximation when types fix part of the implementation of an object. To return to points, for example, if we know that all subtypes of point share a common implementation of a basic function like move, then the type system, in effect, guarantees a behavioral property of points. (This may be achieved in our framework if move is private or if we add the straightforward capability of restricting redefinition of protected or public methods.)

A more subtle reason to use types that restrict the implementations of objects has to do with the implementation of binary operations. In an object-oriented context, a binary operation on type A is realized as a member function that requires another A object as a parameter. In a language where all objects of type A share some common representation, it is possible for an A member function to safely access part of the private internal representation of another A object. A simple example of this arises with set objects that have only a membership test and a union operation in their public interfaces. With interface types, some objects of type set might be represented internally using bit-vectors, while others might use linked lists. In this case, there is no type-safe way to implement union, since no single operation will access both a bit-vector and a linked list correctly. With only interface types, it is necessary to extend the public interface of both kinds of sets to make this operation possible. In contrast, if the type of an object conveys implementation information, then a less flexible but type-safe implementation of set union is possible. In this case, all set objects would have one representation and a union operation could be implemented by taking advantage of this uniformity.

This paper presents a provably sound type system, based on accepted type-theoretic principles, that allows us to write both “interface types” and “implementation types”. The system is relatively simple in outline, since it may be viewed as a straightforward combination of basic constructs that have been studied previously. However, there are a number of details involving subtype assertions about abstract types, extensions to abstract types, covariance and contravariance of methods, and the absence of methods that make the exact details of the system relatively subtle. In summary, the paper has three main points: (i) the general view that classes correspond to abstract data types, (ii) a precise formulation of a higher-order abstract type mechanism and a flexible underlying object calculus that together make it possible to establish a correspondence between C^{+}^{+}-style classes and abstract data types whose representations are objects, (iii) a proof of type soundness for the type system that arises from this analysis. While there is a folkloric belief that C^{+}^{+} and Eiffel classes provide a form of data abstraction, we believe that this is the first technical account suggesting a precise correspondence between class constructs and a standard non-object-oriented form of data abstraction.

Our presentation of classes as abstract data types requires a number of operations on objects. Specifically, the underlying object calculus without data abstraction must provide a basic form of object that allow us to invoke methods of an object, extend objects with new methods, and replace existing methods. Moreover, in order to capture the form of subtyping present in typed objectoriented languages, we must have at least the usual form of subtyping between object types. This much was already provided by our previous object calculus, presented in [FHM94, FM95]; similar primitives are also provided in alternative approaches such as [AC94b, AC94a].

In adding a data abstraction mechanism, we must incorporate subtype specifications, negative information (absence of methods), and variance information in abstract type declarations. This is so that abstract types are extensible in essentially the same way as their underlying representations. Therefore, we extend our basic calculus from [FHM94, FM95] with more detailed static information about type variables and (since most operations are done on functions from types to so-called rows) row variables. While the intuitive decomposition of classes into data abstraction and object primitives is essentially straightforward, the need to maintain detailed information about subtyping properties and extensibility of abstract types leads to certain technical complications and subtleties that had to be overcome in developing this analysis.

A detail for readers of [FHM94] is that the “class” types of that paper were interface types, not classes in the sense of a form of object type that includes implementation information. We therefore renamed them “pro” (for prototype) types in [FM95] and continue that terminology here.

2 Overview by Example

2.1 Protection levels

Each class in an object-oriented program has two kinds of external clients: sections of the program that use objects created from the class and classes that derive new classes from the original. Since the methods of a class may refer to each other, the class also has an internal “client,” namely itself. We therefore associate three interfaces with each class. Using C^{+}^{+} terminology, these may be distinguished as follows:

Private methods are only accessible within the implementation of the class,

Protected methods are only accessible in the implementation of the class and derived classes,

Public methods may be accessible, through objects of the class, in any module of the program.

One goal of this paper is to show how we can associate a different type with each interface and use essentially standard type-theoretic constructs to restrict visibility in each part of a program appropriately. In doing so, we pay particular attention to the fact that although the private or protected methods may not be accessible in certain contexts, it is important for the type system to guarantee their existence.

2.2 Point and color point classes

Using C^{+}^{+}-like syntax, we might declare classes of points and colored points as shown below. For simplicity, we use only one-dimensional points.

 class Point
  private      x  : int;
  protected  setX : int -> Point;
  public     getX : int;
               mv : int -> Point;
         newPoint : int -> Point;
  end;
class ColorPoint : Point
  private       c : color;
  protected  setC : color -> ColorPoint;
  public     getC : color;
    newColorPoint : color -> int -> ColorPoint
 end;

Intuitively, the set methods are used to assign to private x-coordinate or color data, and get methods are used to read the values of the data. The move method mv changes the x-coordinate of a point or colored point. These classes reflect a common idiom of C^{+}^{+} programming, where the basic data fields are kept private so that the class implementor may change the internal representation without invalidating client code. Protected methods make it possible for derived classes to change the values of private data, without providing the same capability outside of derived classes.

In C^{+}^{+} and in the pseudo-code above, each class contains a special function called a constructor for the class. Here the constructor is distinguished by the syntactic form newClassname. Since all objects of a class are created by calling a class constructor, it is important to be able to call the constructor function before any objects have been created. Therefore, unlike the other functions listed in the class declarations, the class constructor is not a method; it does not belong to objects of the class. Constructors are included in class declarations primarily as a syntactic convenience.

2.3 Interface type expressions

In translating the pseudo-code above into a more precise form, we write a type expression for each interface of each class, resulting in six distinct but related types. In hopes that this practice will provide useful mnemonics, we follow a systematic naming convention where, for class A, we call the type expressions for the public, protected, and private interfaces A_{pub}, A_{prot} , and A_{priv} , respectively.

Although each interface is essentially a list of methods names and their types, it is necessary to use a type function instead of a type for each interface. The reason is that the type associated with the objects instantiated from a given class is recursively defined; this type is a fixed-point of a type function. Point-wise subtyping between such type functions is the critical relation between interfaces for type-checking inheritance.

For Point, this methodology gives us the following type functions, using the form ⟨⟨ … ⟩⟩ for object interface types:

          Point_{pub}   =^{def} λ t ⟨⟨getX : int, mv : int → t⟩⟩
          Point_{prot}  =^{def} λ t ⟨⟨setX : int → t, getX : int, mv : int → t⟩⟩
          Point_{priv}  =^{def} λ t ⟨⟨x : int, setX : int → t, getX : int, mv : int → t⟩⟩

These interface functions are formed from the class declaration for Point by replacing occurrences of Point by a type variable t and lambda-abstracting to obtain a type function. We will use row variables to range over such type functions, (which map types to finite lists of method/type pairs).

The analogous interfaces for ColorPoint are written using a free row variable p, which will be bound to the abstract type-function for points in the scope where the ColorPoint interfaces will appear:

         ColorPoint_{pub}   =^{def} λ t ⟨⟨pt | getC : Color⟩⟩
         ColorPoint_{prot}  =^{def} λ t ⟨⟨pt | setC : Color → t, getC : Color⟩⟩
         ColorPoint_{priv}  =^{def} λ t ⟨⟨pt | c : Color, setC : Color → t, getC : Color⟩⟩

Since the supertyping bounds on identifier p will give all of the relevant (protected or public) Point methods, there is no need to list the methods inherited from Point. Consequently these ColorPoint interfaces list exactly the same methods as our pseudo-code ColorPoint class. Since the variable p will be “existentially bound” in an abstract data type declaration, the occurrence of p in each expression will guarantee that all the private methods of Point objects are present in every ColorPoint object, without exposing any other information about private Point methods. So-called “kind” information in the declaration of p will guarantee that methods named c, setC, and getC are not present, making it type-safe to extend p objects with these new methods.

2.4 Implementations

A class implementation specifies an object layout and set of method bodies (code for the methods of the objects). In our approach, the object layout will be given by a type expression and the method bodies will be part of the constructor function. Following general principles of data abstraction, the method bodies may rely on aspects of the representation that are hidden from other parts of the program.

We use a subtype-bounded form of data abstraction based on existential types [MP88, CW85]. Using this formalism, the implementation of points will be given by a pair with subtype-bounded existential type of the form

{|p <: (…) :: κ = P_{priv}, ConsImp_{p}|}

consisting of the private interface P_{priv} for points and a constructor function ConsImp_{p} that might use an initial value for the x-coordinate, for example, to return a new point object. (Our framework allows any number of constructor functions, or other “non-virtual” operations to be provided here. However, for simplicity, we discuss only the special case of one constructor per class.) For the moment, we leave the supertype bound, indicated by the ellipsis (…) above, unspecified since we later discuss two separate approaches, a minimal one in which we give the protected interface here (later restricting the program view to the public interface) and a more special-purpose approach in which both the protected and public interfaces are specified in the class implementation. The “kind”

 Abstype  p <:_{w} P_{prot} :: T^{+} → ({c, getC, setC}; ∅)
    with  newPoint : Int → pro u pu
      is {|p <:_{w} P_{prot} :: (T^{+} → ({c, getC, setC}; ∅)) = P_{priv}, Imp_{p}|}

      in

          Abstype  cp <:_{w} CP_{prot} :: T^{+} → (∅; ∅)
             with  newColorPoint : Int → Color → pro u cpu
               is {|cp <:_{w} CP_{prot} :: (T^{+} → (∅; ∅)) = CP_{priv}, Imp_{cp}|}

               in

                   Abstype  p <:_{w} P_{pub} :: T^{+} → (∅; ∅)
                      with  newPoint : Int → obj t pt

is {|p <:_{w} P_{pub} :: (T^{+} → (∅; ∅)) = p, newPoint|}

                        in

                            Abstype  cp <:_{w} CP_{pub} :: T^{+} → (∅; ∅)
                               with  newColorPoint : Int → Color → obj t cpt
                                 is {|cp <:_{w} P_{pub} :: (T^{+} → (∅; ∅)) = cp, newColorPoint|}

                                 in

                                     ⟨Program⟩

Figure 1: Nested abstract data types for points and colored point classes.

κ will indicate that we are declaring an abstract type function, list methods that are guaranteed not to be present in the implementation of points, and describe the variance of point objects. The variance information is needed to infer subtyping relationships for object types that contain row variable p.

The implementation of ColorPoint similarly has the form

                        {|cp <: (. . .) :: κ′ = CP_{priv}, ConsImp_{cp}|}

where the constructor ConsImp_{cp} , first invokes the Point class constructor newPoint, then extends the resulting prototype with the new methods c, setc, and getc. Definitions of the Point and ColorPoint class constructors are given in Section 3.4.

2.5 Class hierarchies as nested abstract types

Our basic view of classes and implementation types is that the class-based pseudo-code in Section 2.2 may be regarded as sugar for the sequence of nested abstract data type (Abstype) declarations given in Figure 1. Since it is syntactically awkward to use two declarations per class, one giving the protected interface and the other the public interface, we discuss alternate syntactic presentations in Section 3.5.

In order, the four abstract type declarations give the protected view of Point, the protected view of ColorPoint, the public view of Point, and the public view of ColorPoint. The nesting structure allows the implementation of ColorPoint to refer to the protected view of Point and allows the program to refer to public views of both classes.

The two inner declarations hide the protected view of a class by redeclaring the same type name and constructor and exposing the public view (with a different type, as discussed below). Since the implementation of the public view, in each case, is exactly the same as the implementation of the protected view, hiding the protected methods is the only function of the two inner declarations. We admit that reusing bound variables is a bit of a “hack,” but this is a relatively minor issue that can be solved by departing from the simple block-structured scoping mechanism we use here.

One distinction between the protected and public views is that the constructors for the protected view return an object with a pro type while the public view constructors return objects with obj types. These two types from our underlying object calculus allow different sets of operations on objects. Specifically, new methods may be added to an object with a pro type and existing methods can be overridden. If an object has an obj type, on the other hand, the only operation is to invoke a method of the object. Since we have different sets of operations, there are different subtyping rules: the subtyping relation is relatively rich between obj types, while the only supertypes of a pro type are object types. Intuitively, this means that the methods of an object may be modified or extended when it is used as a prototype, but not once it is “promoted” to a member of an obj type. While the distinction between these two kinds of types is convenient for our purposes here, it was originally devised as a mechanism for obtaining nontrivial subtyping in the presence of object inheritance primitives (object extension and method redefinition).

3 Object calculus and type system

3.1 The calculus

The expressions of our core calculus are untyped lambda terms, including variable x, application e_{1}e_{2} and lambda abstraction λx. e, extended with four object forms:

⟨⟩  the empty prototype or object
e ⇐ m  send message m to prototype or object e
⟨e_{1} ←+ m=e_{2}⟩ extend prototype e_{1} with new method m having body e_{2}
⟨e_{1} ← m=e_{2}⟩ replace prototype e_{1}’s method body for m by e_{2}

These expressions are the same as in [FHM94, FM95]. However, the type system used in the present paper is more detailed. We extend this core calculus with two encapsulation primitives:

                     Abstype r <:_{w} R : : κ with x : τ is e_{1} in e_{2}

{|r <:_{w} R : : κ = R′, e|}

The first is used to provide limited access to implementation e_{1} in client e_{2} . Type expression r <:_{w} R : : κ and assumption x : τ provide the interface for this access. The type system will require expression e_{1} to have the form {|r <:_{w} R : : κ = R′, e|}, which is the implementation of the abstraction. The components of these expressions will be explained in more detail after we introduce the type system.

3.2 Operational semantics

The operational semantics include β -reduction for evaluating function applications and a (⇐) rule for evaluating message sends:

⟨e_{1} ←∘ m=e_{2}⟩ ⇐ m ⟶^{eval} e_{2} ⟨e_{1} ←∘ m=e_{2}⟩

where ←∘ may be either ←+ or ←. We also need various bookkeeping rules to access methods defined within e_{1} . These bookkeeping rules appear in Appendix A; they are explained in full in [FHM94]. The reduction rule (Abstype) for abstract data type declarations is:

   Abstype r <:_{w} R : : κ with x : τ is {|r <:_{w} R : : κ = R′, e_{1}|} in e_{2}  ⟶^{eval} [R′/r, e_{1}/x]e_{2}

3.3 Static Type System

The type expressions, given in Appendix B, include type variables, function types, pro types, obj types, and existential types. To reduce the complexity of the type system, these types are divided into two categories. The unquantified, monotypes are indicated using metavariables τ, τ′, τ_{1}, . . .. The quantified types, indicated using metavariables σ, σ′, σ_{1}, …, may contain existential quantifiers.

A row is a finite list of method name, type pairs. Row expressions appear as subexpressions of type expressions, with rows and types distinguished by kinds. Intuitively, the elements of kind ({m⃗}; V) are the rows that do not include the method names in {m⃗} and whose the free type variables appear with variance indicated in variance set V . We keep track of the absence of methods in order to guarantee that methods are not multiply defined. The variance information, which tells whether a variable appears monotonically, antimonotonically, or neither, is necessary for subtyping judgements involving types of the form pro t R or obj t R since R may contain row variables. Type functions, which arise as row expressions with kind T^{a} → ({m⃗}; V), are used to infer a form of higher-order polymorphism for method bodies and to provide type interfaces to encapsulated implementations. The annotation a indicates the variance of the abstracted variable.

To avoid unnecessary repetition in our presentation, we use the meta-variable probj for either obj or pro. Intuitively, the elements of type probj t ⟨⟨m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩ are objects e such that for 1 ≤ i ≤ k, the result of e ⇐ m_{i} is a value of type τ_{i}. However, since the bound type variable t may appear free in τ_{i}, the type of e ⇐ m_{i} is actually the result of replacing each free occurrence of t in τ_{i} by probj t ⟨⟨m_{1} : τ_{1}, …, m_{k} : τ_{k}⟩⟩. Because of this substitution, probj t ⟨⟨…⟩⟩ is effectively a special form of recursively-defined type.

The typing rule for sending a message to an object is

(probj ⇐)  \frac{\begin{matrix}Γ ⊢ e : probj t R \\ Γ, t: \{t^{+}\} & ⊢ & R <:_{w} ⟨⟨m: τ⟩⟩ \end{matrix}}{Γ ⊢ e ⇐ m : [probj t R/t]τ}

where the substitution for t in τ reflects the recursive nature of pro and obj types. This rule differs from the ones given in [FHM94, FM95] by requiring only that we may derive Γ, t: {t^{+}} ⊢ R <:_{w} ⟨⟨m: τ⟩⟩ instead of the more stringent requirement that R ≡ ⟨⟨R′|m : τ⟩⟩. This relaxation permits us to type message sends to objects whose types may be partially abstract (i.e., types containing row variables). Another thing to notice about this rule is the subscript w on the subtyping judgment. This symbol indicates that only width subtyping was used to reach this conclusion. Our system supports both width and depth subtyping on object types; however, for soundness of certain operations, it is essential to keep track of exactly where depth subtyping occurs.

The rule for method override is as follows:

(pro over)  \frac{Γ ⊢ e_{1} : pro u R Γ, u: \{u^{+}\} ⊢ R <:_{w} ⟨⟨m: τ⟩⟩ Γ, I_{r} ⊢ e_{2} : [pro u ru/t](t → τ)}{Γ ⊢ ⟨e_{1} ← m=e_{2}⟩ : pro u R}

where I_{r} = r <:_{w} λt. R : : T^{0} → (∅; Invar(V_{Γ})).

The primary difference between this rule and the one given in [FHM94, FM95] is again the relaxation of the requirement that R be of the form ⟨⟨R′ | m : τ⟩⟩, which permits us to override methods in objects with partially abstract types.

The distinction between pro and obj types is that the former allows redefinition or extension of methods, while the latter gives subtyping instead. An inessential artifact of our calculus is that we may use the same untyped terms for prototypes and objects. We might like to use this coincidence to advantage by using the following rule (along with subsumption) to convert prototypes to objects:

(seal-unsound)  \frac{Γ ⊢ obj u R : T}{Γ ⊢ pro u R <: obj u R}

where the hypothesis Γ ⊢ obj u R : T ensures that obj u R is well formed. Unfortunately, this rule is problematic when the variable u appears contravariantly in R. Hence we need a more complicated rule that we combine with the rule for obj subtyping since they both have the same form:

(<: obj)  \frac{\begin{aligned}Γ, t : \{t^{+}\} & ⊢ & R_{1} <:_{B} R_{2} \\ Γ, t : \{t^{+}\} & ⊢ & R_{2} : : (M; V) \\ V ar(t, V) ∈ \{?, +\} \end{aligned}}{Γ ⊢ probj t R_{1} <: obj t R_{2}}

Because R_{1} and R_{2} in this rule might contain row variables, we cannot use their syntactic form to determine whether the critical type variable appears covariantly (monotonically). Therefore, we appeal to the kind of R_{2} , which contains so-called variance (monotonicity or antimonotonicity) information. The auxiliary function V ar(t, V) gives the variance of type variable of t in variance set V . If V ar(t, V) is ?, then t does not appear in R_{2} , and hence is vacuously covariant. If V ar(t, V) is +, then t appears covariantly. In either case, the consequent of the rule follows from the premises. Since the subscript B on the subtype relation is unconstrained, this rule gives us subtyping in both width and depth for obj types . This rule also has the somewhat unfortunate property that we cannot convert prototypes to obj type if there are methods that are contravariant in the bound type variable. However, this appears to be a fundamental trade-off and limitation.

The rule for forming a class implementation: is the standard rule for existential introduction, extended to address kinding and supertyping constraints.

(∃ <: intro)  \frac{\begin{matrix}Γ ⊢ R_{1} : : κ \\ Γ ⊢ R_{1} <:_{w} R \\ Γ ⊢ e : [R_{1}/r]τ \end{matrix}}{Γ ⊢ \{|r <:_{w} R : : κ = R_{1}, e|\} : ∃(r <:_{w} R : : κ)τ}

The rule for existential types is standard as well. The full type system appears in Appendix C.

3.4 Examples

The Point class constructor Imp_{p} from Section 2.4 may be written as follows:

            λ initX ⟨  x = λ self initX,
                     setX = λ self λ newX ⟨self ← x = λ self′ newX⟩,
                     getX = λ self (self ⇐ x),
                       mv = λ self λ dx (self ⇐ setX(dx + self ⇐ getX))⟩

The ColorPoint constructor Imp_{cp} first invokes the Point class constructor newPoint, (which is implemented by the above Imp_{p} function) then extends the resulting prototype with the new methods c, setc, and getc:

   λ iX λ iC ⟨⟨⟨⟨newPoint(iX) ←+ c  = λ self iC⟩
                             ←+ getC = λ self (self ⇐ c)⟩
                             ←+ setC = λ self λ newC ⟨self ← c = λ self′ newC⟩⟩⟩

By first calling the constructor for the Point class, the ColorPoint class permits the parent Point class to build the parts of the ColorPoint objects inherited from Point, including the private components that the ColorPoint class cannot access.

3.5 An explicit class construct

Although the pattern of nested abstract data type declarations discussed in Section 2.5 gives us some useful insight into classes, this is an “encoding” of a relatively complex construct into a pattern of use of two simpler ones; it not a class construct that could be used as the basis for programming language design. In this brief section, we discuss an alternate “foundational object calculus” with classes taken as basic instead of derived from abstract data type declarations. While additional redesign is possible, we confine ourselves to replacing patterns of abstype by a single class construct; we do not consider modifications of the underlying core object calculus. As a simplifying syntactic assumption, we continue to work with block-structured syntax, instead of a more complicated module formalism with visibility controlled by explicit uses declarations.

A simple construct that may be used in place of standard abstype is a class declaration of the form

    Class   p <: P_prot <: P_pub :: kind_p with newP(pars_p) is <P_priv, Imp_p>
    and     q <: Q_prot <: Q_pub :: kind_q with newQ(pars_q) is <Q_priv, Imp_q>
    and     ...
    and     r <: R_prot <: R_pub :: kind_r with newR(pars_r) is <R_priv, Imp_r>
    in
        Program
    end

We can derive direct typing rules for this construct using the translation into nested abstype’s.

The idea is that classes q … r may declare subtypes of p. Therefore, this declaration binds p and newP in the subsequent class declaration clauses and in Program. However, the subtyping information about p and type of newP will be different in the two scopes. Specifically, the clauses giving possible subtypes of p are type-checked using the assumptions p <: P prot :: kind p and newP : pars p → pro u pu, while the program is type-checked using the assumptions p <: P pub :: kind p and newP : pars p → obj u pu. This makes it possible for the implementation of derived classes q … r to access the protected methods of p and extend the implementation of p objects by adding new methods or redefining existing ones. Each of the subsequent class declaration clauses are treated similarly so that, for example, the declaration of r has analogous access to the protected methods of q. As in the pattern of abstype declarations given in Section 2.5, the client program does not have these capabilities.

Although we have explained this construct under the assumption that q … r are subtypes of p, they are more properly viewed as derived classes that may or may not result in subtypes. In particular, since there is no restriction on the syntactic form of Q pub, for example, this could be an expression giving obj u qu <: obj u pu, or it might not. If it is not, then we have the analog of C^{+}^{+} private base classes where inheritance does not produce a subtype.

4 Overview of soundness proof

The soundness proof, using the operational semantics discussed in Section 3.2, has two parts. The first shows that evaluation preserves type; this property is traditionally called subject reduction. The second part established that no typable expression evaluates to error. In the second part, we use a specific evaluation strategy, described in [FHM94], to carry out the argument. The two parts together guarantee that we never obtain a “message-not-understood” errors from any typable expression.

While the details are different, the proof follows the same outline as [FHM94, FM95]. A sketch of the proof appears in Appendix D.

Theorem 4.1 (Subject Reduction) If Γ ⊢ e : τ is derivable, and e ⟶^{eval} e′, then Γ ⊢ e′ : τ is also derivable.

Theorem 4.2 (Type Soundness) If the judgement ϵ ⊢ e : τ is derivable, then eval(e) ≠ error, where the function eval is as in [FHM94], extended with rules for (Class) reduction.

5 Analysis

Here we briefly note several implications of our approach.

5.1 Representation independence for classes

One advantage of our decomposition of classes into object operations and standard data abstraction is that a number of properties developed in the analysis of traditional data abstraction without objects may be applied to object-oriented languages. For example, the results in [Rey83, MM85, Mit86, Mit91] give various sufficient conditions on interchangeability of implementations. Put briefly, we may replace one implementation of a class with another, in any program, as long as the protect and public interfaces of the new implementation conform to the old ones and the observable behaviors correspond.

5.2 Subtyping and inheritance

A basic issue in the literature on object-oriented programming is the relation between subtyping and inheritance. An early and influential paper, [Sny86], argues that the way these two ideas are often linked (as in Eiffel and C^{+}^{+}) is inconvenient and unfounded. We believe that the arguments in [Sny86, Coo92] and related papers are essentially correct for interface types: subtyping between interface types has nothing to do with the way objects are implemented. However, the analysis in the present paper shows that for implementation types, inheritance may be necessary (although not always sufficient) to produce a subtype. In short, if a type t is abstract, in the sense that all or part of its implementation is hidden, then the only safe way to define a subtype of t is by extending the hidden implementation.

5.3 “Private virtual” functions

There are some interesting problems associated with C^{+}^{+} private virtual functions. In our representation of classes, these show up immediately in the need to include “negative information” in the interface of an abstract type. This is necessary if if we want to be able to extend the representation, since otherwise we might try to add a new method that replaces an existing method, invalidating another method that depends on the presence of the one that is replaced. (See [FM94], for example, for further discussion.) However, this form of negative information is not used in C^{+}^{+} class interfaces or header files. Therefore, we have an anomalous situation in which private virtual functions, which are not supposed to be visible to derived classes, can be unintentionally overridden because in addition to being “private,” they are also declared “virtual,” which means they are allowed to be redefined in derived classes.

6 Conclusion

In this paper, we describe a type-theoretic model of various levels of encapsulation and visibility in object-oriented systems. More specifically, we show that classes, of the form found in C^{+}^{+}, Eiffel and related languages, may be regarded as the combination of two orthogonal language features: a form of objects without encapsulation and a standard form of data abstraction mechanism (albeit higher-order and including subtype constraints). This intuitive view explains the correlation between subtyping and inheritance and answers some of the criticism found in papers such as [Sny86, Coo92]; other advantages of our approach are outlined in Section 5.

Several other features of C^{+}^{+}-like object systems can be modeled in our framework. In particular, we can account for friend functions, non-virtual functions and inheritance with private base classes (i.e., inheritance that does not result in a subtype) using the concepts presented here.

There are a number of promising directions for further work. One direction is to examine further features of C^{+}^{+}, with the goal of identifying anomalies or simplifying the language. An interesting topic in this vein is the incorporation of “abstract” classes. An issue related to both improving C^{+}^{+}-like systems and the general problem of name spaces for method names might be to develop a binding mechanism so that method names remain local to their intended scope. This could resolve the problem with C^{+}^{+} private virtual functions and also simplify our type system by eliminating the need for negative kind information in abstract type declarations. With an eye toward future language design, we also hope to refine the special syntax described briefly in Section 3.5 and consider the reformulation of our block-structured constructs using modules and dot notation [CL90, HL94]

References

[AC94a] M. Abadi and L. Cardelli. A theory of primitive objects: second-order systems. In Proc. European Symposium on Programming, pages 1–24. Springer-Verlag, 1994.

[AC94b] M. Abadi and L. Cardelli. A theory of primitive objects: untyped and first-order systems. In Proc. Theor. Aspects of Computer Software, pages 296–320. Springer-Verlag LNCS 789, 1994.

[Bru93] K. Bruce. Safe type checking in a statically-typed object-oriented programming language. In Proc 20th ACM Symp. Principles of Programming Languages, pages 285–298, 1993.

[CL90] Luca Cardelli and Xavier Leroy. Abstract types and the dot notation. Technical Report 56, DEC Systems Research Center, Palo Alto, CA, March 1990.

[Coo92] W.R. Cook. Interfaces and specifications for the Smalltalk-80 collection classes. In ACM Conf. Object-oriented Programming: Systems, Languages and Applications, pages 1–15, 1992.

[CW85] L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

[ES90] M. Ellis and B. Stroustrop. The Annotated C^{++} Reference Manual. Addison-Wesley, 1990.

[FHM94] K. Fisher, F. Honsell, and J.C. Mitchell. A lambda calculus of objects and method specialization. Nordic J. Computing (formerly BIT), 1:3–37, 1994. Preliminary version appeared in Proc. IEEE Symp. on Logic in Computer Science, 1993, 26–38.

[FM94] K. Fisher and J.C. Mitchell. Notes on typed object-oriented programming. In Proc. Theoretical Aspects of Computer Software, pages 844–885. Springer LNCS 789, 1994.

[FM95] K. Fisher and J. Mitchell. A delegation-based object calculus with subtyping. In Fundamentals of Computation Theory (FCT’95). Springer LNCS, 1995. To appear.

[GM94] C.A. Gunter and J.C. Mitchell, editors. Theoretical aspects of object-oriented programming. MIT Press, Cambridge, MA, 1994.

[GR83] A. Goldberg and D. Robson. Smalltalk–80: The language and its implementation. Addison Wesley, 1983.

[HL94] Robert Harper and Mark Lillibridge. A type-theoretic approach to higher-order modules with sharing. In Proc. 21-st ACM Symp. on Principles of Programming Languages, 1994.

[Mey92] B. Meyer. Eiffel: The Language. Prentice-Hall, 1992.

[Mit86] J.C. Mitchell. Representation independence and data abstraction. In Proc. 13th ACM Symp. on Principles of Programming Languages, pages 263–276, January 1986.

[Mit91] J.C. Mitchell. On the equivalence of data representations. In V. Lifschitz, editor, Artificial Intelligence and Mathematical Theory of Computation: Papers in Honor of John McCarthy, pages 305–330. Academic Press, 1991.

[MM85] J.C. Mitchell and A.R. Meyer. Second-order logical relations. In Logics of Programs, pages 225–236, Berlin, June 1985. Springer-Verlag LNCS 193.

[MP88] J.C. Mitchell and G.D. Plotkin. Abstract types have existential types. ACM Trans. on Programming Languages and Systems, 10(3):470–502, 1988. Preliminary version appeared in Proc. 12th ACM Symp. on Principles of Programming Languages, 1985.

[PT94] Benjamin C. Pierce and David N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming, 4(2):207–248, 1994.

[Rey83] J.C. Reynolds. Types, abstraction, and parametric polymorphism. In Information Processing ’83, pages 513–523. North-Holland, Amsterdam, 1983.

[Sny86] A. Snyder. Encapsulation and inheritance in object-oriented programming languages. In Proc. ACM Symp. on Object-Oriented Programming Systems, Languages, and Applications, pages 38–46, October 1986.

[Str86] B. Stroustrop. The C^{++} Programming Language. Addison-Wesley, 1986.

A Syntax and operational semantics of expressions

Expressions e : : = x | c | λx. e | e_{1}e_{2} | ⟨⟩ | e ⇐ m | ⟨e_{1} ← m = e_{2}⟩ | ⟨e_{1} ←+ m = e_{2}⟩ | {|r <:_{w} R_{1} : :κ = R_{2}, e|} | Abstype r <:_{w} R : : κ with x : ρ is e_{1} in e_{2}

Operational Semantics:

(switch ext ov)  ⟨⟨e_{1} ← m_{2}=e_{2}⟩ ←+ m_{3}=e_{3}⟩  ⟶^{book} ⟨⟨e_{1} ←+ m_{3}=e_{3}⟩ ← m_{2}=e_{2}⟩
(perm ov ov)  ⟨⟨e_{1} ← m_{2}=e_{2}⟩ ← m_{3}=e_{3}⟩  ⟶^{book} ⟨⟨e_{1} ← m_{3}=e_{3}⟩ ← m_{2}=e_{2}⟩
(add ov)  ⟨e_{1} ←+ m_{2}=e_{2}⟩  ⟶^{book} ⟨⟨e_{1} ←+ m_{2}=e_{2}⟩ ← m_{2}=e_{2}⟩
(cancel ov ov)  ⟨⟨e_{1} ← m_{3}=e_{2}⟩ ← m_{3}=e_{3}⟩  ⟶^{book} ⟨e_{1} ← m_{3}=e_{3}⟩
(β)  (λx. e_{1})e_{2}  ⟶^{eval} [e_{2}/x]e_{1}
(⇐)  ⟨e_{1} ←∘ m=e_{2}⟩ ⇐ m  ⟶^{eval} e_{2}⟨e_{1} ←∘ m=e_{2}⟩

where ←∘ may either ←+ or ←.

(Abstype)  Abstype r <:_{w} R : : κ with x: τ ⟶^{eval} [R′/r, e_{1}/x]e_{2}
is {|r <:_{w} R : : κ = R′, e_{1}|} in e_{2}

B Type System

Types σ : : = τ | ∃(r <:_{w} R : : κ)τ τ : : = t | τ_{1} → τ_{2} | pro t R | obj t R

Rows

R : : = r | ⟨⟨⟩⟩ | ⟨⟨R | m: τ⟩⟩ | λt. R | Rτ

Kinds kind : : = V | κ

V : : = {t⃗^{b}},  b : : = + | − | o
κ : : = T^{a} → ν | ν,  a : : = b |?

ν : : = (M; V) M : : = {m⃗}

Contexts

Γ : : = ϵ | Γ , x: τ | Γ , t: V | Γ , r <:_{w} R : :κ

The judgement forms are:

Γ ⊢ ∗  well-formed context
Γ ⊢ e: τ  term has type
Γ ⊢ σ : V  well-formed type with variance V
Γ ⊢ R_{1} <:_{B} R_{2}  row R_{1} subtype of R_{2}

B gives width vs. depth

Γ ⊢ τ_{1} <: τ_{2}  type τ_{1} subtype of τ_{2}
Γ ⊢ R: :κ  row has kind

The subtyping annotations are:

Width vs. Depth B : : = w | d | w, d |B_{1} + B_{2} Indicate record subtyping forms.

“+” is the union of B_{1} and B_{2} .

Operations on Variance Sets:

V_{1} − V_{2}  = set difference
\overline{\{t_{1}^{a_{1}}, …, t_{n}^{a_{n}}\}}  = \{t\overline{a_{1}} ; 1, …, t\overline{a_{n}} ; n\}, where \overline{a_{i}} inverts the sign of a_{i}.
D(V_{1}, …, V_{n})  = {t | t^{a} ∈ V_{i} for some a,i}
V ar(t, V)  = \{ \begin{matrix}a & if t^{a} ∈ V \\ ? & otherwise \end{matrix}
V \t  = V − {t^{V ar(t,V)}}
GV ar(t, V_{1}, …, V_{n}) = lub{V ar(t, V_{1}), …, V ar(t, V_{n})}
Merge(V_{1}, …, V_{n}) = {t^{GV ar(t,V_{1},...,V_{n})} | t ∈ D(V_{1}, …, V_{n})}
Invar(V)  = {t^{o} | t ∈ D(V)}
V_{Γ}  = {t^{a} | t^{a} ∈ dom(Γ)}

where lub is taken with respect to the ordering: + ≤ o, − ≤ o, ? ≤ −, ? ≤ +. Variance Substitutions

[V_{2}/t]V_{1} = \{ \begin{matrix}Merge(V′_{1}, V_{2}) & if V_{1} = V′_{1}, t^{+} \\ Merge(V′_{1}, \overline{V_{2}}) & if V_{1} = V′_{1}, t^{−} \\ Merge(V′_{1}, Invar(V_{2})) & if V_{1} = V′_{1}, t^{o} \\ V_{1} & if t ∉ D(V_{1}) \end{matrix}

Ordering on kinds:

V_{1} ≤ V_{2} iff ∀t, V ar(t, V_{2}) ≤ V ar(t, V_{1})
(M_{1}; V_{1}) ≤ (M_{2}; V_{2}) iff M_{1} ⊆ M_{2} and V_{1} ≤ V_{2}
T^{a} → ν_{1} ≤ T^{b} → ν_{2} iff b ≤ a and ν_{1} ≤ ν_{2}

C Typing rules

C.1 Context Rules

(start)  \overline{ϵ ⊢ ∗}

(type var)  \frac{\begin{matrix}Γ ⊢ ∗ \\ t ∉ dom(Γ) \end{matrix}}{Γ, t : \{t^{+}\} ⊢ ∗}

(row var)  \frac{\begin{matrix}Γ ⊢ R_{1} : : S_{1} → (M_{1}; V_{1}) \\ S_{0} → (M_{0}; V_{0}) ≤ S_{1} → (M_{1}; V_{1}) \\ D(V_{0}) ⊆ dom(Γ) \\ r ∉ dom(Γ) \end{matrix}}{Γ, (r <:_{w} R_{1} : : S_{0} → (M_{0}; V_{0})) ⊢ ∗}

(exp var)  \frac{\begin{matrix}Γ ⊢ τ : V \\ x ∉ dom(Γ) \end{matrix}}{Γ, x: τ ⊢ ∗}

(weakening)  \frac{\begin{matrix}Γ_{1}, Γ_{2} ⊢ A \\ Γ_{1}, a, Γ_{2} & ⊢ & ∗ \end{matrix}}{Γ_{1}, a, Γ_{2} ⊢ A}

where a: : = x: τ | t: V | r <:_{w} R : : κ

C.2 Rules for type expressions

(type proj)  \frac{\begin{matrix}Γ ⊢ ∗ \\ t : \{t^{+}\} ∈ Γ \end{matrix}}{Γ ⊢ t : \{t^{+}\}}

(type arrow)  \frac{\begin{matrix}Γ ⊢ τ_{1} : V_{1} \\ Γ ⊢ τ_{2} : V_{2} \end{matrix}}{Γ ⊢ τ_{1} → τ_{2} : Merge(\overline{V_{1}}, V_{2})}

(pro)  \frac{Γ, t: \{t^{+}\} ⊢ R : : (M; V)}{Γ ⊢ pro t R : Invar(V \ t)}

(cov object)  \frac{\begin{matrix}Γ, t: \{t^{+}\} & ⊢ & R : : (M; V) \\ V ar(t, V) ∈ \{+,?\} \end{matrix}}{Γ ⊢ obj t R : V \ t}

(non cov object)  \frac{\begin{matrix}Γ, t: \{t^{+}\} & ⊢ & R : : (M; V) \\ V ar(t, V) ∈ \{o, −\} \end{matrix}}{Γ ⊢ obj t R : Invar(V \ t)}

(exist)  \frac{\begin{matrix}Γ, r <:_{w} R : : κ & ⊢ & τ : V_{1} \\ κ = S → (M; V_{2}) \end{matrix}}{Γ ⊢ ∃(r <:_{w} R : : κ)τ : Merge(V_{1}, V_{2})}

C.3 Rules for rows

(row proj)  \frac{\begin{matrix}Γ ⊢ ∗ \\ r <:_{w} R : : κ ∈ dom(Γ) \end{matrix}}{Γ ⊢ r : : κ}

(empty row)  \frac{Γ ⊢ ∗}{Γ ⊢ ⟨⟨⟩⟩ : : (M; ∅)}

(row label)  \frac{\begin{matrix}Γ ⊢ R : : S^{i} → (M; V) \\ N ⊆ M  i ∈ \{0, 1\} \end{matrix}}{Γ ⊢ R : : S^{i} → (N; V)}

(row fn abs)  \frac{Γ, t: \{t^{+}\} ⊢ R : : (M; V)}{Γ ⊢ λt. R : : T^{V ar(t,V)} → (M; V \t)}

(row fn app cov)  \frac{\begin{matrix}Γ ⊢ R : : T^{+} → (M; V_{1}) \\ Γ ⊢ τ : V_{2} \end{matrix}}{Γ ⊢ Rτ : : (M; Merge(V_{1}, V_{2}))}

(row fn app contra)  \frac{\begin{matrix}Γ ⊢ R : : T^{−} → (M; V_{1}) \\ Γ ⊢ τ : V_{2} \end{matrix}}{Γ ⊢ Rτ : : (M; Merge(V_{1}, \overline{V_{2}}))}

(row fn app inv)  \frac{\begin{matrix}Γ ⊢ R : : T^{o} → (M; V_{1}) \\ Γ ⊢ τ : V_{2} \end{matrix}}{Γ ⊢ Rτ : : (M; Merge(V_{1}, Invar(V_{2})))}

(row fn app vac)  \frac{\begin{matrix}Γ ⊢ R : : T^{?} → (M; V_{1}) \\ Γ ⊢ τ : V_{2} \end{matrix}}{Γ ⊢ Rτ : : (M; V_{1})}

(row ext)  \frac{\begin{matrix}Γ ⊢ R : : (\{m⃗, m\}, V_{1}) \\ Γ ⊢ τ : V_{2} \end{matrix}}{Γ ⊢ ⟨⟨R | m: τ⟩⟩ : : (\{m⃗\}; Merge(V_{1}, V_{2}))}

C.4 Subtyping rules for types

(<: type refl)  \frac{Γ ⊢ τ : V}{Γ ⊢ τ <: τ}

(<:→)  \frac{\begin{matrix}Γ ⊢ τ′_{1} <: τ_{1} \\ Γ ⊢ τ_{2} <: τ′_{2} \end{matrix}}{Γ ⊢ τ_{1} → τ_{2} <: τ′_{1} → τ′_{2}}

(<: obj)  \frac{\begin{aligned}Γ, t : \{t^{+}\} & ⊢ & R_{1} <:_{B} R_{2} \\ Γ, t : \{t^{+}\} & ⊢ & R_{2} : : (M; V) \\ V ar(t, V) ∈ \{?, +\} \end{aligned}}{Γ ⊢ probj t R_{1} <: obj t R_{2}}

(<: trans)  \frac{\begin{matrix}Γ ⊢ τ_{1} <: τ_{2} \\ Γ ⊢ τ_{2} <: τ_{3} \end{matrix}}{Γ ⊢ τ_{1} <: τ_{3}}

C.5 Subtyping Rules for rows

(<: row refl)  \frac{Γ ⊢ R : : κ}{Γ ⊢ R <:_{B} R}

(row proj bound)  \frac{\begin{matrix}Γ ⊢ ∗ \\ r <:_{w} R : : κ ∈ Γ \end{matrix}}{Γ ⊢ r <:_{w} R}

(<: λ)  \frac{\begin{aligned}Γ, t : \{t^{+}\} & ⊢ & R_{1} <:_{B} R_{2} \\ Γ, t : \{t^{+}\} & ⊢ & R_{2} : : ν \end{aligned}}{Γ ⊢ λt. R_{1} <:_{B} λt. R_{2}}

(<: app cong)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ R_{2} : : T^{a} → ν \\ Γ ⊢ τ : V \end{matrix}}{Γ ⊢ R_{1}τ <:_{B} R_{2}τ}

(<: app cov)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ R_{2} : : T^{+} → ν \\ Γ ⊢ τ_{1} <: τ_{2} \end{matrix}}{Γ ⊢ R_{1}τ_{1} <:_{B+d} R_{2}τ_{2}}

(<: app contra)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ R_{2} : : T^{−} → ν \\ Γ ⊢ τ_{2} <: τ_{1} \end{matrix}}{Γ ⊢ R_{1}τ_{1} <:_{B+d} R_{2}τ_{2}}

(<: app vac)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ R_{2} : : T^{?} → ν \\ Γ ⊢ τ_{1} : V_{1}  Γ ⊢ τ_{2} : V_{2} \end{matrix}}{Γ ⊢ R_{1}τ_{1} <:_{B} R_{2}τ_{2}}

(<: cong)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2}  Γ ⊢ τ : V \\ Γ ⊢ ⟨⟨R_{i} | m: τ⟩⟩ : : ν_{i}  i ∈ \{1, 2\} \end{matrix}}{Γ ⊢ ⟨⟨R_{1} | m: τ⟩⟩ <:_{B} ⟨⟨R_{2} | m: τ⟩⟩}

(<: d)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2}  Γ ⊢ τ_{1} <: τ_{2} \\ Γ ⊢ ⟨⟨R_{i} | m: τ_{i}⟩⟩ : : ν_{i}  i ∈ \{1, 2\} \end{matrix}}{Γ ⊢ ⟨⟨R_{1} | m: τ_{1}⟩⟩ <:_{B+d} ⟨⟨R_{2} | m: τ_{2}⟩⟩}

(<: w)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ ⟨⟨R_{1} | m: τ⟩⟩ : : ν \end{matrix}}{Γ ⊢ ⟨⟨R_{1} | m: τ⟩⟩ <:_{B+w} R_{2}}

(<: trans)  \frac{\begin{matrix}Γ ⊢ R_{1} <:_{B} R_{2} \\ Γ ⊢ R_{2} <:_{B′} R_{3} \end{matrix}}{Γ ⊢ R_{1} <:_{B+B′} R_{3}}

Type and Row Equality Type or row expressions that differ only in names of bound variables are considered identical. Additional equations between types and rows arise as a result of β -reduction, written →_{β}, or β -conversion, written ↔_{β}.

(row β)  \frac{Γ ⊢ R : : κ, R →_{β} R′}{Γ ⊢ R′ : : κ}

(type β)  \frac{Γ ⊢ τ : V , τ →_{β} τ′}{Γ ⊢ τ′ : V}

(type eq)  \frac{Γ ⊢ e : τ, τ ↔_{β} τ′, Γ ⊢ τ′ : V}{Γ ⊢ e : τ′}

(<: β right)  \frac{Γ ⊢ R_{1} <:_{B} (λt. R_{2})τ_{2}}{Γ ⊢ R_{1} <:_{B} [τ_{2}/t]R_{2}}

(<: β left)  \frac{Γ ⊢ (λt. R_{1})τ_{1} <:_{B} R_{2}}{Γ ⊢ [τ/t]R_{1} <:_{B} R_{2}}

C.6 Rules for assigning types to terms

(exp proj)  \frac{\begin{matrix}Γ ⊢ ∗ \\ x : τ ∈ Γ \end{matrix}}{Γ ⊢ x : τ}

(subsumption)  \frac{Γ ⊢ e : τ_{1}, Γ ⊢ τ_{1} <: τ_{2}}{Γ ⊢ e : τ_{2}}

(exp abs)  \frac{Γ , x: τ_{1} ⊢ e : τ_{2}}{Γ ⊢ λx. e : τ_{1} → τ_{2}}

(exp app)  \frac{Γ ⊢ e_{1} : τ_{1} → τ_{2} Γ ⊢ e_{2} : τ_{1}}{Γ ⊢ e_{1} e_{2} : τ_{2}}

(empty pro)  \frac{Γ ⊢ ∗}{Γ ⊢ ⟨⟩ : pro t ⟨⟨⟩⟩}

(pro ext)  \frac{Γ ⊢ e_{1} : pro t R Γ, t: \{t^{+}\} ⊢ R : : (\{m\}; V) Γ, I_{r} ⊢ e_{2} : [pro t rt/t](t → τ)  r ∉ V (τ)}{Γ ⊢ ⟨e_{1} ←+ m=e_{2}⟩ : pro t ⟨⟨R | m: τ⟩⟩}

where I_{r} = r <:_{w} λt.⟨⟨R | m : τ⟩⟩ : : T^{0} → (∅; Invar(V_{Γ})).

(pro over)  \frac{Γ ⊢ e_{1} : pro t R Γ, t: \{t^{+}\} ⊢ R <:_{w} ⟨⟨m: τ⟩⟩ Γ, I_{r} ⊢ e_{2} : [pro t rt/t](t → τ)}{Γ ⊢ ⟨e_{1} ← m=e_{2}⟩ : pro t R}
where I_{r} = r <:_{w} λt. R : : T^{0} → (∅; Invar(V_{Γ})).

(probj ⇐)  \frac{\begin{matrix}Γ ⊢ e : probj t R \\ Γ, t: \{t^{+}\} & ⊢ & R <:_{w} ⟨⟨m: τ⟩⟩ \end{matrix}}{Γ ⊢ e ⇐ m : [probj t R/t]τ}

(∃ <: intro)  \frac{\begin{matrix}Γ ⊢ R_{1} : : κ \\ Γ ⊢ R_{1} <:_{w} R \\ Γ ⊢ e : [R_{1}/r]τ \end{matrix}}{Γ ⊢ \{|r <:_{w} R : : κ = R_{1}, e|\} : ∃(r <:_{w} R : : κ)τ}

(∃ <: elim)  \frac{\begin{matrix}Γ ⊢ e_{1} : ∃(r <:_{w} R : : κ)τ \\ Γ, r <:_{w} R : : κ, x: τ & ⊢ & e_{2} : σ \\ Γ ⊢ σ : V \end{matrix}}{Γ ⊢ Abstype r <:_{w} R : : κ with x : τ is e_{1} in e_{2} : σ}

D Overview of soundness proof

We prove the soundness of our type system with respect to the operational semantics given in Section 3.2. We first prove that evaluation preserves type; this property is traditionally called subject reduction. We then show that no typable expression evaluates to error using the evaluation rules given in [FHM94], extended in a straightforward manner to account for the new encapsulation primitives. This fact guarantees that we have no message-not-understood errors for expressions with pro types.

The proof begins with two lemmas about substitution for row and type variables. We then prove a normal form lemma that allows us to restrict our attention to derivations of a certain form, simplifying later proofs. Lemmas D.5 and D.6 give us subject reduction for the bookkeeping rules and β -reduction, respectively. Lemmas D.7, D.8, and D.9 imply subject reduction for (⇐)-reduction, while Lemmas D.1 and D.6 give us subject reduction for (Class)-reduction.

In the remainder of this section, we use meta-variable U to refer to either a row or type expression, meta-variable γ to refer to arbitrary kinds, and meta-judgement Γ ⊢ U : −γ to indicate either “row has kind γ ” or “type is well-formed.”

The first two lemmas are substitution lemmas that are used to specialize pro types to contain additional methods and to prove (Class) reduction sound.

Lemma D.1 (Row Substitution)

If  Γ, r <:_{w} R′ : : κ, Γ′ ⊢ A, Γ ⊢ R <:_{B} R′, and Γ ⊢ R : : κ,
then Γ, [R/r]Γ′ ⊢ A′,

where

• if A ≡ ∗, then A′ ≡ ∗
• if A ≡ U : −γ, then A′ ≡ [R/r]U : −γ
• if A ≡ U_{1} <:_{B} U_{2}, then A′ ≡ [R/r]U_{1} <:_{B} [R/r]U_{2}
• if A ≡ e : σ, then A′ ≡ [R/r]e : [R/r]σ

Lemma D.2 (Type Substitution) If Γ, t : T, Γ′ ⊢ A and Γ ⊢ τ : V then

• if A ≡ ∗, then Γ, [τ : V/t] Γ′ ⊢ ∗
• if A ≡ U : −γ, then Γ, [τ : V/t] Γ′ ⊢ [τ/t]U : −γ
• if A ≡ U_{1} <:_{B} U_{2}, then Γ, [τ : V/t] Γ′ ⊢ [τ/t]U_{1} <:_{B} [τ/t]U_{2}

The type and row equality rules introduce many non-essential judgement derivations, which unnecessarily complicate derivation analysis. We therefore restrict our attention to ⊢_{N} -derivations, which we define as those derivations in which the only appearance of a type or row equality rule is as (β <: right) immediately following an occurrence of a subtyping application rule (<: app ∗) where the left-hand row function expression is a row variable, or as (type eq) immediately before an occurrence of (∃ <: intro). The τnf of a type or row expression is its normal form with respect to β -reduction. The τnf of a term expression e is just e. Since we are only interested in types and rows in τnf, the following lemma shows we can find a ⊢_{N} -derivation for any judgement of interest.

Lemma D.3 (Normal Form for Derivations) If Γ ⊢ A is derivable, then so is τnf(Γ) ⊢_{N} τnf(A).

The proof of this lemma is by induction on the derivation of Γ ⊢ A. Occurrences of equality rules may be eliminated in the ⊢_{N} -derivation because two row or type expressions related via β -reduction must have the same τnf. The cases for the row application rules (row fn app ∗) follows from the somewhat surprising fact that if we may derive that a normal-form row function λt. R′ applied to a normal-form type τ is wellformed, then we may show that [τ/t]R′ is well-formed without using the (row β) typing rule. The cases for (<: app ∗) are similar.

From this point on, we will only concern ourselves with contexts and type or row expressions that are in τnf. This limitation is not severe, since any term that has a type has a type in τnf. Future analyses of derivations will consider only ⊢_{N} -derivations, since its restriction on equality rules greatly simplifies the proofs.

The following lemma is used to show that the (switch ext ov) reduction rule preserves types.

Lemma D.4 If Γ, p <:_{w} λt. R : : T → (M_{p}; V), Γ′ ⊢ A and Γ, r <:_{w} λt.⟨⟨R | m : τ⟩⟩ : : T → (M_{r}; V) ⊢ A are both derivable, r ∉ dom(Γ′) and M_{p} ⊆ M_{r}, then Γ, r <:_{w} λt.⟨⟨R | m : τ⟩⟩ : : T → (M_{r}; V), [r/p]Γ′ ⊢ [r/p]A is also derivable, where A is any judgement not involving strictly σ -types.

The proof of this lemma is very sensitive to the form of the (pro ext) proof rule.

The next four lemmas show that the various components of the ⟶^{eval} relation preserve expression types. Lemma D.5 is the first of these, showing that the (⟶^{book}) relation has the necessary property.

Lemma D.5 If Γ ⊢ e : τ is derivable, and e ⟶^{book} e′, then Γ ⊢ e′ : τ is derivable.

The proof of Lemma D.5 consists of two parts: the first shows that a derivation from Γ ⊢ e : τ can only depend on the form of τ, not on the form of e. More formally, if Γ ⊢ C[e] : τ is derived from Γ′ ⊢ e : σ and Γ′ ⊢ e′ : σ is also derivable, then so is Γ ⊢ C[e′] : τ. This fact is easily seen by an inspection of the typing rules. The second part shows that if Γ ⊢ e : τ is derivable, and e ⟶^{book} e′ by e matching the left-hand side of one of the (⟶^{book}) axioms, then Γ ⊢ e′ : τ is also derivable. This fact follows from a case analysis of the four (⟶^{book}) axioms. Lemma D.4 is essential for the (switch ext ov) case.

The fact that (β)-reduction preserves expression types is an immediate consequence of the following lemma:

Lemma D.6 (Expression Substitution) If Γ, x: τ_{1}, Γ′ ⊢ e_{2} : τ_{2} and Γ ⊢ e_{1} : τ_{1} are both derivable, then so is Γ, Γ′ ⊢ [e_{1}/x]e_{2} : τ_{2} .

Lemma D.6 is proved by induction on the derivation of Γ, x: τ_{1}, Γ′ ⊢ e_{2} : τ_{2} .

The next three lemmas together imply that (⇐)-reduction preserves type. The first is the key lemma in showing subject reduction for messages sent to expressions with pro type. The second, which guarantees that the variance annotations properly track variance, is essentially for showing the soundness of sealing obj types to pro types. The third implies subject reduction for expressions with obj type.

Lemma D.7 (Method Bodies are Type Correct) If Γ ⊢_{N} ⟨e_{1} ←∘ m = e_{2}⟩ : pro t R is derivable in such a way that the last rule in the derivation is not (type eq), then there exists a unique type τ such that Γ, t : {t^{+}} ⊢_{N} R <:_{w} ⟨⟨m : τ⟩⟩ and Γ ⊢_{N} e_{2} : [pro t R/t](t → τ) are both derivable. Furthermore, if ←∘= ← then Γ ⊢_{N} e_{1} : pro t R is also derivable.

Lemma D.8 If Γ, t : {t^{+}}, Γ_{τ} ⊢_{N} U_{1} <:_{B} U_{2} , Γ ⊢_{N} U_{2} : −γ_{2} , Γ ⊢_{N} τ_{1} <: τ_{2} , and Γ ⊢_{N} τ_{i} : V_{i} for i ∈ {1, 2} are all derivable, then

• if V ar(t, γ) =? then
Γ, Γ_{τ} ⊢_{N} [τ_{i}/t]U_{1} <:_{B} [τ_{j}/t]U_{2}
• if V ar(t, γ) = + then
Γ, Γ_{τ} ⊢_{N} [τ_{1}/t]U_{1} <:_{w,d} [τ_{2}/t]U_{2}
• if V ar(t, γ) = − then
Γ, Γ_{τ} ⊢_{N} [τ_{2}/t]U_{1} <:_{w,d} [τ_{1}/t]U_{2}

where Γ_{τ} is a context listing only type variables.

Lemma D.9 (Object Types Come From Pro Types) If Γ ⊢_{N} ⟨e_{1} ←∘ m = e_{2}⟩ : obj t R is derivable, then there exists a type pro t R′ such that

Γ ⊢_{N} ⟨e_{1} ←∘ m = e_{2}⟩ : pro t R′
Γ ⊢_{N} pro t R′ <: obj t R

are both derivable.

Theorem D.10 (Subject Reduction) If Γ ⊢ e : τ is derivable, and e ⟶^{eval} e′, then Γ ⊢ e′ : τ is also derivable.

The proof is similar in outline to that of Lemma D.5; it reduces to showing that each of the basic evaluation steps preserves the type of the expression being reduced. The (⟶^{book}) case follows from Lemma D.5, the (β) case from Lemma D.6, the (⇐) case from Lemmas D.7, D.8, and D.9, and the (Class) case from Lemmas D.1 and D.6.

Theorem D.11 (Type Soundness) If the judgement ϵ ⊢ e : τ is derivable, then eval(e) ≠ error, where the function eval is as in [FHM94], extended with rules for (Class) reduction.