Foundations of Object-Oriented Languages

FOOL 3

*Abstract:*
The past five years have seen an explosion of foundational models for
statically typed object-oriented programming. Many have been
presented as translations from high-level object notations to typed
lambda-calculi with subtyping, differing in technical details but
sharing underlying intuitions. This tutorial develops a uniform
notational framework -- a typed lambda-calculus with subtyping,
higher-order polymorphism, existential types, and recursive types --
and uses it to compare and contrast four previously studied models.

[Joint work with Kim Bruce and Luca Cardelli.]

Permissive Types,

*Abstract:*:
Component override is a powerful and common technique in object oriented
programming; strongly typed systems need to impose restrictions on the types of
the components involved. Usually, the type of the overriding component must be
a subtype of the overridden component. For methods, this results into the sound
contravariant rule, which requires the argument types of the overriding method
to be supertypes of the argument types of the overridden method. For ST&T, a
type system for Smalltalk we adopted a 'permissive' approach, which allows
covariant override for instance variables and any override for method. All
subclasses are treated as subtypes, and message expressions are type checked by
considering the types of methods in the receiver and all its subtypes. Our
approach aims to consider type correct as many expressions as possible, and
does not require data flow analysis. Thus it should be suitable for type
checking legacy software, and should provide an appropriate alternative to the
current suggestions for type checking Eiffel. However, it operates under the
closed world assumption, ie. subclasses defined in separately compiled modules
would invalidate any previously type checked modules importing the superclass.
ST&T, a static type system for Smalltalk was developed, and implemented as a
browser extension for Smalltalk. In this paper we prove the soundness of our
approach. We introduce $\lambda^{\&,S}$, a syntax based on $\lambda^{\&}$,
which reflects the essentials of the language Smalltalk. We define the
operational semantics and type rules for $\lambda^{\&,S}$. We demonstrate the
soundness of the approach by proving the subject reduction theorem.

Further work includes developing parameterized types to describe container classes and possible extensions to higher order.

Currying multi-methods in a merge calculus,

*Abstract:*:
We present a calculus based on the view that it should be possible to
define a subclass method by specifying only the way in which it
differs from the superclass methods of the same name. The calculus is
a polymorphic extension of the merge calculus in which late binding
can be expressed. We show that multi-methods can be represented
naturally from this viewpoint; multi-methods and single-methods can
both be expressed as generic functions with one argument by Currying,
and a generic function behaves like a multi-method or a single-method
depending on the covariance or contravariance of the component
functions.

Primitive subtyping /\ implicit polymorphism |= object-orientation,

*Abstract:*:
We present a new predicative and decidable type system, called ML<, suitable
for object-oriented languages with implicit polymorphism in the tradition of
ML. Instead of using extensible records as a foundation for object-oriented
extensions of functional languages, we propose to reinterpret classical
datatype declarations as abstract and concrete class declarations, and to
replace pattern-matching on run-time values by dynamic dispatch on run-time
types. ML< is based on universally quantified polymorphic constrained types,
where constraints are conjunctions of inequalities between monotypes built
from extensible and partially ordered classes of type constructors. We show
how this type system can be used to design programming languages retaining
much of the ML spirit while integrating in a seamless fashion higher-order and
object-oriented programming, dynamic dispatch on several arguments, and
parametric polymorphism. We give type-checking rules for a small, explicitly
typed functional language with methods, and show that the resulting system has
decidable minimal typing. We discuss type inference for this language. We show
how abstraction and encapsulation can be achieved by proper use of a module
system. We give a type-checking algorithm and discuss its complexity. We
conclude by a comparison with related type systems in the literature.

*Abstract:*
This talk presents 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. The 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.

This is joint work with John Mitchell.

Related work available from
Kathleen Fisher's home page.

Objective ML: A simple object-oriented extension to ML,

*Abstract:*
Objective ML is a small practical extension of ML with objects and toplevel
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. This demonstrates that objects can be added to
strongly typed languages based on ML polymorphism.

Full paper (postscript) test

Full paper (dvi)

Classes in Object ML via Modules,

*Abstract:*
We describe a simple encoding of classes in Object ML
(OML) using the Standard ML (SML) module system. We show how to
mimic class-based implementation inheritance using an extension of
Abadi and Cardelli's "pre-methods". We also show how to encode
other various class-based features, such as static members,
protected members, and multiple inheritance. Our thesis is that
the rich scoping discipline provided by SML has enough power to
encode various aspects of the class systems of C++ and other
languages.

Object Type Constructors,

*Abstract:*
Adding container objects (such as list objects) to polymorphic languages,
particularly languages with type inference such as ML, faces serious technical
obstacles. One problem is the fact that polymorphic functions are
second-class in languages with type inference, otherwise type inference is
undecidable. Another problem is that type-checking of container objects with
recursive interfaces remains an open problem, even for explicitly typed
languages.

A type system is presented that overcomes all of these problems. The type system provides first-class objects with polymorphic methods, subtyping, recursive object types, method override and method type specialization. At the heart of the approach is the use of primitive method types, higher-order polymorphism and object type constructors. The object calculus can be considered as a class-based version of the object system of Abadi & Cardelli, with self types. The type system motivates the addition of primitive objects to polymorphic languages with type inference: objects with polymorphic methods are not possible with approaches that encode objects using records, datatypes or universal types.

*Abstract:*
This tutorial will review attempts to ascribe semantics to concurrent
object-based languages using both operational (SOS) and translational
(to process algebras) approaches. The two semantic approaches will be
compared as to their usefulness for gaining an intuitive understanding
of the COOL in question. Thus far there is nothing very novel but
the light shed on issues such as granularity will be considered and a
tentative link with Benjamin Pierce's tutorial will be a comment on
some novel properties which might be captured with type inference.
Furthermore the question of proving the soundness of some equivalences
will be shown to be a non-trivial challenge using either semantics.

Formalising and prototyping a concurrent object-oriented language,

*Abstract:*
The piece of work reported here originates from the design of a real
concurrent and distributed object-oriented design language developed
within Ericsson. Originally constructs for distribution and
concurrency were missing from the language, making it necessary to
call on operating system services to implement distributed
applications. The goal of the project was to include support for
these aspects in the language itself thereby enabling implementations
on different operating system platforms. In this paper we concentrate
on the formal definition of a small core fraction of the design
language, which we name Erken, and on some simulation and prototyping
activities based on the formal definition.

In our opinion the first and foremost motive to formally define the semantics of a programming language is to enable language proposals to be stated precisely at an early design phase. This facilitates discussions about language design by reducing the potential for confusion due to unclear ideas and specifications.

In this paper we describe the Erken semantics which is defined via a translation of language constructs into the pi-calculus. The translation has been implemented as a compiler from Erken to the pi-calculus. To enable experimentation with the semantics a compiler from the variant of the pi-calculus used in the translation to the concurrent functional programming language Facile was also implemented. Defining the compiler in two steps has the advantage that a change in the semantics, that is, in the translation function to the pi-calculus, only results in a change in the Erken to pi-calculus compiler, which is an easy task due to the fact the the compiler is a straightforward implementation of the translation.

Formal reasoning about Actor Programs using temporal logic,

*Abstract:*
We present an approach to reasoning about actor programs on the base
of temporal logic. Temporal logic is particularly appropriate for the
specification of concurrent programs, but most known temporal logic
proof systems for concurrent computations rely on imperative language
constructs and static process topologies, ignoring, e.g., the creation
of processes and the dynamic configuration of communication channels,
which are crucial for actor systems or other concurrent
object-oriented programming languages.
After sketching the actor model and introducing a simple syntax for
actor programs we describe a general temporal logic system and then
adjust it to the describtion of actor computations.

Inheritance of Proofs,

*Abstract:*
The Curry--Howard isomorphism, a fundamental property shared by many type
theories, establishes a direct correspondence between programs and
proofs. This suggests that the same structuring principles that ease
programming be used to simplify proving as well.

To exploit object-oriented structuring mechanisms for verification, we extend the object-model of Pierce and Turner, based on the higher order typed lambda-calculus Fomegasub, with a proof component. By enriching the (functional) signature of objects with a specification, the methods and their correctness proofs are packed together in the objects. The uniform treatment of methods and proofs gives rise in a natural way to object-oriented proving principles | including inheritance of proofs, late binding of proofs, and encapsulation of proofs | as analogues to object-oriented programming principles.

We have used LEGO, a type-theoretic proof checker, to explore the feasibility of this approach. In particular, we have verified a small hierarchy of classes.

*Abstract:*
The pi-calculus (Milner, Parrow and Walker, 1989) has gained a
lot of attention over the past few years as a process algebra for
mobile processes. Central to the pi-calculus is the notion of
*name*. Two processes with acquaintance of a given name can use it to
interact with each other. In the interaction, names may be exchanged
and, in this way, a process can acquire the ability to communicate
with other processes. A major strength of the pi-calculus is the
rich algebraic theory. Type systems for the pi-calculus have been
recently put forward (Pierce and Sangiorgi 1993, Honda and Vasconcelos
1993, Turner 1995, etc..), as developments of Milner's *sorting
discipline*.

The notions of name and of mobility are also central in Object-Oriented programming: Objects refer to each other using names and, during computation, object acquaintances may change and new objects may be created.

In my talk I will report on some experiments with the pi-calculus as a metalanguage for the semantics of typed Object-Oriented languages. Another motivation for this work is testing the usefulness of pi-calculus type systems, and investigating their relationship to familiar types of programming languages.

I will present an interpretation of Abadi and Cardelli's first-order functional *Object Calculus* (OC) into a first-order typed pi-calculus. The interpretation validates the subtyping relation and the typing judgements of OC, and is computationally adequate. Types are necessary to justify certain algebraic laws for the pi-calculus which are important in the proof of computational adequacy of the translation.

If there is time, I will discuss modifications/extensions of this interpretation to handle the imperative OC and the second-order OC.

Formal Objects in type theory using very dependent types,

*Abstract:*
We present an extension to basic type theory to allow a uniform
construction of abstract data types (ADTs) having many of the
properties of objects, including abstraction, subtyping, and
inheritance. The extension relies on allowing type dependencies for
function types to range over a well-founded domain. Using the
propositions-as-types correspondence, abstract data types can be
identified with logical theories, and proofs of the theories are the
objects that inhabit the corresponding ADT.

A type system for record concatenation and subtyping,

*Abstract:*
We define an extension of a second-order type system with records, subtyping
and record concatenation. This system can model the most important concepts
of object-oriented languages. The novelty in our approach is that
concatenation is only permitted if the types on common fields agree.
We give examples of how object-oriented concepts can be modeled and show how
the system can be translated to a type system without subtyping.

Return to the FOOL home page.