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
letrecx1 = a1andx2 = a2ina as letx = fix
(l (x1,x2). (a1, a2)) ina. 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.
