Previous Up Next
7 Related and future works

The design and implementation of concurrent object-oriented languages, e.g. [2, 33, 1, 6], has recently prompted the investigation of the theoretical foundations of concurrent objects. Several works provide encodings of objects in process calculi [31, 28, 14, 8, 19] or, conversely, supplement objects with concurrent primitives [23, 4, 13, 29]. These works promote a unified framework for reasoning about objects and processes, but they do not address the incremental definition of concurrent objects or its typechecking. (When considered, inheritance is treated as in a sequential language and does not deal with synchronization.) In particular, the TyCO language, developed by Vasconcelos and his collegues, relies on a core calculus which is very close to the objective join calculus in Section 2, with few differences due to name definitions. However the two languages differ when classes are considered. In particular, TyCO [29] only allows simple forms of inheritance, namely extensions of classes with new methods, and updates of old methods with new ones. No mechanism is provided to access methods in the super class and, therefore, to reuse their bodies. As regards the type system, both the languages stick to a predicative polymorphism discipline. However, in our calculus, polymorphism originates from class and obj operations and regards objects and classes as a whole; in TyCO polymorphism originates from a different operator---the let---which allows to define one (polymorphic) function at a time, and regards single methods.

The addition of classes to the join calculus enables a modular definition of synchronization. Different receivers for the same labels can thus be introduced at different syntactic positions in a program. In that respect, we partially recover the ability of the pi calculus to dynamically introduce receivers on channels [21]. However, our layered design confines this modularity to classes, which are resolved at compile time. From a programming-language viewpoint, this strikes a good balance between flexibility and simplicity, and does not preclude type inference or the efficient compilation of synchronization [16].

Odersky independently proposed an object-oriented extension of the join calculus [24, 25]. As in Section 2, they use join patterns to define objects and synchronization between labeled messages. The main difference lies in the encapsulation of methods within objects. In our proposal, a definition binds a single object, with all the labels appearing in the definition, and we rely on types to hide some of those labels as private. In their proposal, a definition may bind any number of objects, and each object explicitly collects some of the declared labels as its methods. As a result, a label that is not collected remains syntactically private. Besides, their synchronization patterns can express matching on the values carried in messages (strings, integers, lists, trees, etc.) rather than matching on just the message labels. For instance, a rule l(h::t) |> P reacts provided l carries a non-empty list. Those design decisions may lead to different implementation strategies. However, they do not deeply affect typing.

As regards polymorphism, our generalization rule Object corresponds to the one currently implemented in JoCaml [15]. It is more expressive than the generalization rule initially proposed in [12] and seems equivalent to the generalization rule of [7]. In [12], non-generalizable type variables were computed altogether for all clauses of a definition, which may be too conservative. In both [15] and [7], non-generalizable type variables are computed one rule at a time, which is more precise. This latter approach is natural in our setting, since recursion is left open till object instantiation. In ML, this amounts to typing let rec x1 = a1 and x2 = a2 in a as let x = fix (l (x1,x2). (a1, a2)) in a. The latter term separates type-checking the body of the recursion from type-checking recursion itself.

Our language supports multiple inheritance of classes, but not mixin inheritance [5], which amounts to parameterize classes by other classes. As in OCaml, we can only combine existing classes, but obtain mixin inheritance indirectly through modules and functors.

In sequential languages, deep method renaming, i.e. rewriting of recursive calls or method hiding, can be expressed using dictionaries [27] or views [30]. In concurrent languages, views offer additional benefits. For example, one can duplicate the synchronization patterns of a superclass by inheriting several copies of the class, independently refine their synchronization, and use different views to access the copies. For instance, one could distinguish internal and external views in the last example of Section 4. The integration of views in the objective join calculus deserves further investigation.

Since classes are just object templates, our typing system allows polymorphic variables in class types, and defer any monomorphic restriction till object instantiation. For type safety, one must check that, in every join pattern of an object, any variable occurring in the type of several labels is monomorphic. To this aim, our class types collect a superset W of these coupled labels, but other approaches are possible. A plain solution is to assume that all labels are coupled. Then, class types don't convey any synchronization information, and generalization is as in [12]. Conversely, the class types could detail the labels of each join pattern. This would allow us to detect refinement errors at compile time. However, the resulting types would be very precise, and we would also need some form of subtyping to get rid of excessive information. This is another promising direction for research.


Previous Up Next