[Prev][Next][Index][Thread]

"A Theory of Primitive Objects"; paper available by ftp.


The following paper is now available; see instructions at the bottom.
Comments are welcome.

-----------------------------------------------------------------

                 A Theory of Primitive Objects

                Martin Abadi and Luca Cardelli

    All common object-oriented languages support some combination 
of object subsumption and method override, and most handle these 
features properly. However, type correctness is achieved via rather 
subtle conditions, if at all. We hope to illuminate the origin of 
some of these conditions, and illustrate the pitfalls that they avoid. 

    In semantics and type-theory, where one aims for simplicity and 
generality, the combination of subsumption and override has proven 
difficult to model. We provide basic object calculi that support 
those features. Our approach is to axiomatize the typing and equational 
properties of objects, rather than to define objects in terms of 
other constructs. The soundness of our rules is guaranteed by a denotational 
semantics, and by a syntactic translation inspired by the semantics. 

    We begin our paper with a challenge: finding an adequate type 
system for an untyped object calculus. This calculus is patently 
object-oriented: it has built-in objects, methods with self, and 
the characteristic semantics of method invocation and override. The 
calculus is also very simple, with just four syntactic forms, but 
expressive enough to encode the lambda-calculus and to formulate 
object-flavored examples in a direct way. 

    After describing the untyped calculus, we define type systems, 
equational theories, and denotational semantics. We account for subsumption, 
field update, method override, and the so-called Self type, in addition 
to standard bounded polymorphism and data abstraction. Classes, inheritance, 
and method combination can be layered on top of our basic framework. 
Our final formal system is obtained as a conventional second-order 
extension of a rather elementary first-order theory of objects. 

--------------------------------------------------

Ftp instructions:

    ftp gatekeeper.pa.dec.com
    anonymous
    <your email address>
    cd pub/DEC/SRC/personal/luca
    binary
    get PrimObj.ps.Z
    quit

    uncompress PrimObj.ps.Z

Print PrimObj.ps on Apple or HP postscript printers, for best results.