Objective ML is a small practical extension to ML with objects and top level classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ML polymorphism.
We present a generalization of the ideal model for recursive polymorphic types. Types are defined as sets of terms instead of sets of elements of a semantic domain. Our proof of the existence of types as a solution of a fixpoint does not rely on metric spaces properties, but instead uses the fact that the identity is the limit of projection terms. This establishes a connection with the work of Pitts on relational properties of domains. We suggest that the right generalization of ideals are closed sets of terms defined by orthogonality with respect to a set of contexts.
We present an object-oriented calculus which allows arbitrary hiding of methods in prototypes, even in the presence of binary methods and friend functions. This combination of features permits complete control of the interface a class exposes to the remainder of a program (which is of key importance for program readibility, security and ease of maintenance), while still allowing complex interactions with other classes belonging to a same module or software component.
We propose regular expression types as a foundation for statically typed XML processing languages. Regular expression types capture and generalize regular expression notations such as repetition, alternation, etc., that are commonly found in schema languages for XML, and support a powerful notion of subtyping. We argue that the flexibility provided by this form of subtyping is useful in supporting smooth evolution of XML-based systems.
Subtyping can be fairly complex for union types, due to interactions with other types, such as function types. Furthermore, these interactions turn out to depend on the calculus considered: for instance, a call-by-value calculus and a call-by-name calculus will have different possible subtyping rules. In order to abstract ourselves away from this dependence, we consider a fairly large class of calculi. We define types in a semantic fashion, as sets of terms. Then, a type can be a subtype of another type if its denotation is included in the denotation of the other type. We first consider a simple type system with union, function, pair and constant types. Using inference rules, we specify a subtyping relation which is both sound and complete with respect to the class of calculi. We then extend this result to a richer type system with ML-style polymorphism and type constructors. We expect this framework to allow the study of subtyping relations that only hold for some calculi by restricting the class considered, and to allow the study of subtyping relations for richer type systems by enriching the class.
We construct a realizability model of recursive polymorphic types, starting from an untyped language of terms and contexts. An orthogonality relation e⊥π indicates when a term e and a context π may be safely combined in the language. Types are interpreted as sets of terms closed by biorthogonality. Our main result states that recursive types are approximated by converging sequences of interval types. Our proof is based on a “type-directed” approximation technique, which departs from the “language-directed” approximation technique developed by MacQueen, Plotkin and Sethi in the ideal model. We thus keep the language elementary (a call-by-name λ-calculus) and unstratified (no typecase, no reduction labels). We also include a short account of parametricity, based on an orthogonality relation between quadruples of terms and contexts.
A file synchronizer is a tool that reconciles disconnected modifications to a replicated directory structure. Trustworthy synchronizers are difficult to build, since they must deal correctly with both the semantic complexities of file systems and the unpredictable failure modes arising from distributed operation. On the other hand, synchronizers are often packaged as stand-alone, user-level utilities, whose intended behavior is relatively easy to isolate from the other functions of the system. This combination of subtlety and isolability makes file synchronizers attractive candidates for precise mathematical specification. We present here a detailed specification of a particular file synchronizer called Unison.
We show, mostly through detailed examples, that programming patterns known to involve the notion of virtual types can be implemented in a real object-oriented language—Ocaml—in a direct way by taking advantage of parametric classes and a flexible treatment of object types via the use of row variables.
We show how classes can be combined with a ML-like module system, so that the same constructions be used for both classes and modules. For that, we are brought to slightly extend the module system with implicit type quantification of module types.