Lecture Notes in Computer Science 788 Edited by G. Goos and J. Hartmanis Advisory Board: W. Brauer D. Gries J. Stoer Donald Sannella (Ed.) Programming Languages and Systems - ESOP '94 5th European Symposium on Programming Edinburgh, U.K., April 11-13, 4991 Proceedings galreV-regnirpS Berlin Heidelberg NewYork London Paris Tokyo Hong Kong Barcelona Budapest Series Editors Gerhard Goos Juris Hartmanis Universit~t Karlsruhe Cornell University Postfach 69 80 Department of Computer Science Vincenz-Priessnitz-Strage 1 4130 Upson Hall D-76131 Karlsrnhe, Germany Ithaca, NY 14853, USA Volume Editor Donald Sannella Department of Computer Science, The University of Edinburgh The King's Buildings, Mayfield Road, Edinburgh EH9 3JZ, U. K. CR Subject Classification (1991): D.3, E3, D.2, E4 ISBN 3-540-57880-3 Springer-Verlag Berlin Heidelberg New York ISBN 0-387-57880-3 Springer-Verlag New York Berlin Heidelberg CIP data applied for This work is subject to copyright. All rights are reserved, whether the whole or part of the material is concerned, specifically the fights of translation, reprinting, re-use of illustrations, recitation, broadcasting, reproduction on microfilms or in any other way, and storage in data banks. Duplication of this publication or parts thereof is permitted only under the provisions of the German Copyright Law of September 9, 1965, in its current version, and permission for use must always be obtained from Springer-Verlag. Violations are liable for prosecution under the German Copyright Law. (cid:14)9 Springer-Verlag Berlin Heidelberg 1994 Printed in Germany Typesetting: Camera-ready by author SPIN: 10132134 45/3140-543210 - Printed on acid-free paper Preface This volume contains the papers selected for presentation at the 5th European Symposium on Programming (ESOP'94), which was held jointly with the 19th Colloquium on Trees in Algebra and Programming (CAAP'94) during 11-13 April in Edinburgh. ESOP is a biennial symposium which has been held previ- ously in Saarbrficken, Nancy, Copenhagen and Rennes. ESOP is devoted to fundamental issues in the specification, design and imple- mentation of programming languages and systems. The emphasis is on research that bridges the gap between theory and practice, for example an implemented system that embodies an important concept or method, or a formal framework for design that usefully addresses issues arising in practical system develop- ment. The scope of the symposium includes work on: software analysis, spe- cification, transformation, development and verification/certification; program- ming paradigms (functional, logic, object-oriented, concurrent, etc.) and their combinations; programming language concepts, implementation techniques and semantics; software design methodologies; typing disciplines and typechecking al- gorithms; and programming support tools. The programme committee received 110 submissions, from which 13 were accepted; invited papers were presented by Luca Cardelli and Robin Milner. Programme Committee R. Back, Turku F. Nielson, Aarhus G. Berry, Sophia-Antipolis D. Sannell~, Edinburgh (chairman) G. Cousineau, Paris A. Sernadas, Lisbon R. De Nicola, Rome A. Tarlecki, Warsaw P. Dybjer, Gothenburg D. Warren, Bristol P. Klint, Amsterdam R. Wilhelm, Saarbrficken B. Krieg-Briickner, Bremen M. Wirsing, Munich A. Myeroft, Cambridge ESOP'94 was organized by the Laboratory for Foundations of Computer Science of the University of Edinburgh. It was held in cooperation with ACM SIGPLAN and was sponsored by Hewlett Packard, LFCS, and the University of Edinburgh. Local Arrangements Committee G. Cleland (chairman) S. Gilmore M. Lekuse D. Sannella I would like to express my sincere gratitude to the members of the pro- gramme committee and their referees (see below) for their care in reviewing and selecting the submitted papers. I am also grateful to the members of the local arrangements committee and to my secretary Tracy Combe for their hard work. Edinburgh, January 1994 Donald Sannella IV Referees for ESOP'94: L. Aceto P. Degano G, Hutton U. Montanari H. Shi .S Agerholm U. de' Liguoro P. Inverardi L. Mounier K. Sieber M. Alt R. de Simone C.B. Jay A. Miick A. Sinclair T. Altenkirch R. DiCosmo M. Jones D. Murphy G. Smolka T. Amtoft .S Diehl N. $r F. Nickl .S Sokotowski L. Augustsson T. Dinesh S. Kahrs X. Nicollin K. Solberg F. Barbanera D. Dranidis K. Karlsson J. Niehren S. Soloviev H. Barendregt H.-D. Ehrich A. Kennedy H.R. Nielson M. Srebrny D. Basin P. Enjalbert N. Klarlund A. Norman R. Stabl M. Bednarczyk J. Exner $. Klop E.-R. Olderog J. Steensgaard- I. Bengelloune F. Fages B. Konikowska C. Palamidessi Madsen .M Benke C. Fecht H.-J. Kreowski F. Parisi Presicce B, Steffen P. Benton C. Ferdinand R. Kubiak C. Paulin J. Stell R. Berghammer G. Ferrari C. Laneve W. Pawtowski B. Stig Hansen J. Berstel G. Frandsen .M Lara de Souza W: Penezek A. Stoughton .M Biatasik T. Franz~n T. Le Sergent H, Peterreins T. Streicher A. Bockmayr L. Fribourg F, Lesske B. Pierce A. Szatas C. BShm H. Ganzinger J. Leszczytowski A. Piperno D. Szczepafiska .M Boreale P. Gardner R. Li K.V.S. Prasad T. Tammet A. Borzyszkowski .S Gastinger L. Liquori C. Priami A. Tasistro G. Boudol B. Gersdorf J. Lloyd R. Pugliese M. Tofte P. Bouillon J. Gibbons G. Longo .Z Qian T.H. Tse F. Boussinot R. Giegerich E, MacKenzie X. Qiwen D, Turner J. Bradfield .S Gilmore E. Madelaine M. Raber P. Urzyczyn K. Bruce .S Gnesi C. Maeder C. Raffalli F. Vaandrager M. Butler M. Gogolla A. Maggiolo- W. Reif .S van Bakel M. Carlsson P. Gouveia Schettini D. R~my A. van Deursen P. Caspi M. Grabowski H. Mairson P. Resende J. van Wamel G. Castagna .S Gregory P. Malacaria B. Reus E. Visser A. Cau G. Grudzirlski K. Malmkj~er M. Rittri B. yon Sydow M.V. Cengarle J. Hannan L. Mandel K. Rose J. von Wright B. Charron-Bost M. Hanus D. Mandrioli B. Ross P, Wadler T.-R. Chuang T. Hardin L. Maranget F. Rouaix L Walukiewicz W. Clocksin J. HIarland F. Maraninchi J. Rutten P. Weis M. Cole R. Harley E. Marchiori M. Ryan J. Winkowski .S Conrad P. Hartel R. Marlet A. Sampaio B. Wolff F. Corradini J. Heering M. Mauny D. Sands D. Wolz V. Costa F. Henglein B. Mayoh D. Sangiorgi J. Wuertz P. Cousot R. Hennicker M. Mehlich O. Schoett R. Yang R. Cousot A. Hense A. Mifsud M. Schwartzbach W. Yi P. Cregut C. Hermida F. Mignard H. Seidl M. Zawadowski R. Crole D. Hofbauer K. Mitchell K. Sere W. Zhang M. Danelutto B. Hoffmann T. Mogensen C. Sernadas .S Zhou O. Danvy C. Holst B. Monsuez K. Shen Contents Invited papers A theory of primitive objects: second-order systems M. Abadi and L. Cardelli Pi-nets: a graphical form of ~r-calculus 26 R. Milner Contributed papers Local type reconstruction by means of symbolic fixed point iteration 43 T. Amtoft An asynchronous process algebra with multiple clocks 58 H.R. Andersen and M. Mendler Foundational issues in implementing constraint logic programming 74 systems J.H. Andrews Programming with behaviors in an ML framework: the syntax and se- 89 mantics of LCS B. Berthomieu and T. Le Sergent Characterizing behavioural semantics and abstractor semantics 105 M. Bidoit, R. Hennicker and M. Wirsing Extending pruning techniques to polymorphic second order )~-calculus 120 L. Boerio h-definition of function(al)s by normal forms 135 .C BShm, A. Piperno and S. Guerrini Simulation of SOS definitions with term rewriting systems 150 K.-H. Buth Strategies in modular system design by interface rewriting 165 S. Cicerone and F. Parisi Presicce Symbolic model checking and constraint logic programming: a cross- 180 fertilization M.-M. Corsini and A. Rauzy A logical denotational semantics for constraint logic programming 195 A. Di Pierro and .C Palamidessi Compilation of head and strong reduction 211 P. Fradet Suffix trees in the functional programming paradigm 225 R. Giegerich and S. Kurtz Viii Type classes in Haskell 142 C. Hall, K. Hammond, S. Peyton Jones and P. Wadler Lazy type inference for the strictness analysis of lists 257 C. Hankin and D. Le Mdtayer Lazy unification with simplification 272 M. Hanus Polymorphic binding-time analysis 287 F. Henglein and .C Mossin Shapely types and shape polymorphism 203 C.B. Jay and J.R.B. Cockett Bottom-up grammar analysis: a functional formulation 317 J. Jeuring and D. Swierstra First-class polymorphism for ML 333 S. Kahrs Dimension types 843 A. Kennedy A synergistic analysis for sharing and groundness which traces linearity 363 A. King A ~r-calculus specification of Prolog 973 B.Z. Li A logical framework for evolution of specifications 394 W. Li A semantics for higher-order functors 409 D.B. MacQueen and M. Tofle The PCKS-machine: an abstract machine for sound evaluation of parallel 424 functional programs with first-class continuations L. Moreau A tiny constraint functional logic language and its continuation semantics 439 A. Miick, T. Streicher and H.C.R. Lock Fully abstract translations and parametric polymorphism 454 P.W. O'Hearn and J.G. Riecke Broadcasting with priority 469 K. V.S. Prasad Towards unifying partial evaluation, deforestation, supercompilation, 485 and GPC M.H. SCrensen, R. Gliick and N.D. Jones Algebraic proofs of properties of objects 105 D. Walker A Theory of Primitive Objects redrO-dnoceS smetsyS Martin Abadi and Luca Cardelli Digital Equipment Corporation, Systems Research Center Abstract eW describe a redro-dnoces calculus of .stcejbo ehT calculus stroppus object -pmusbus tion, method override, dna eht type Self. It si detcurtsnoc sa an extension of System F with ,gnipytbus ,noisrucer dna redro-tsrif tcejbo .sepyt 1. Introduction To its founders and practitioners, object-oriented programming is a new computational paradigm distinct from ordinary procedural programming. Objects and method invocations, in their purest form, are meant to replace procedures and calls, and not simply to complement them. Is there, then, a corresponding "~,-calculus" of objects, based on primitives other than abstraction and application? Such a specialized calculus may seem unnecessary, since untyped objects and methods can be reduced to untyped ~-terms. However, this reduction falters when we take typing and subtyping into account. It becomes even more problematic when we consider the peculiar second-order object-oriented concept of the Self type. This paper is part of an effort to identify object calculi that are as simple and fruitful as -,~ calculi. Towards this goal, we have considered untyped, first-order, and second-order systems, their equational theories, and their semantics. Here we describe, in essence, an object-oriented version of the polymorphic ~,-calcnlus. The starting point for this paper is a first-order calculus of objects and their types, intro- duced in Abadi, Cardelli 1994c. In this calculus, an object is a collection of methods. A method is a function having a special parameter, called self, that denotes the same object the method belongs to. The calculus supports object subsumption and method override. Subsumption is the ability to emulate an object by means of another object that has more refined methods. Override is the operation that modifies the behavior of an object, or class, by replacing one of its methods; the other methods are inherited. We review this calculus in section 2. We add standard second-order constructs to the first-order calculus. The resulting system is an extension of Girard's System F Girard, Lafont, Taylor 1989 with objects, subtyping, and recursion. Only the first-order object constructs are new. However, the interaction of second- order types, recursive types, and objects types is a prolific one. Using all these constructs, we define an interesting new quantifier, ~ (sigma), similar to the g binder of recursive types. This quantifier satisfies desirable subtyping properties that g does not satisfy, and that are important in examples with objects. Using ~ and a covariance condition we formalize the notion of Self, which is the type of the self parameter. We take advantage of Self in some challenging examples. One is a treatment of the tradi- tional geometric points. Another is a calculator that modifies its own methods. A third one is an object-oriented version of Scott numerals, exploiting both Self and polymorphism. Some modern object-oriented languages support Self, subsumption, and override (e.g., Meyer 1988). Correctness is obtained via rather subtle conditions, if at all. We explain Self by deriving its rules from those for more basic constructs. Thus, the problems of consistency are reduced, and hopefully clarified. Our main emphasis is on sound typing rules for objects; because of this emphasis we re- strict ourselves to a stateless computational model. However, our type theories should be largely applicable to imperative and concurrent variants of the model, and our equational theo- ries reveal difficulties that carry over as well. In the next section we review the first-order calculus. Section 3 concerns the second-order constructs, the Self quantifier, and matters of covariance and contravariance. In section 4 we combine the Self quantifier with object types to formalize the type Self, and we present exam- ples. In section 5 we discuss the problem of overriding methods that return values of type Self. We conclude with a comparison with related work. The appendix lists all the typing and equa- tional rules used in the body of the paper. In Abadi, Cardelli 1994a we give a denotational model for these rules. 2. First-Order Calculi In this section we review the typed first-order object calculus introduced in Abadi, Cardelli 1994c. We also recall its limitations, which motivate the second-order systems that are the subject of this paper. 2.1 Informal Syntax and Semantics of Objects We consider a minimal object calculus including object formation, method invocation, and method override. The calculus is very simple, with just four syntactic forms, and even without functions. It is patently object-oriented: it has built-in objects, methods with self, and the char- acteristic semantics of method invocation and override. It can express object-flavored examples in a direct way. Syntax of the first-order ~-calculus A,B ::= li=Bi ir 1( i distinct) types a,b ::= terms x variable li=~(xi:A)b i it n..l 1( i distinct) object 1.a field selection / method invocation a.l~g(x:A)b field update / method override Notation (cid:12)9 We use indexed notation of the form ~i n..lci to denote sequences 1O ..... 0,. (cid:12)9 We use "=~" for "equal by definition", "=" for "syntactically identical", and "=" for "provably equal" when applied to two terms. (cid:12)9 ...1,1':A ... stands for ...I:A, 1,:A.... (cid:12)9 ..., l=b, ... stands for ..., l=~(y:A)b, ..., for an unused y. We call l=b afield. (cid:12)9 o.lj:=b stands for o.lj~-g(y:A)b, for an unused y. We call it an update operation. (cid:12)9 We write b{x} to highlight that x may occur free in b. The substitution of a term c for the free occurrences of x in b is written b{x~c}, or b{c} where x is clear from context. (cid:12)9 We identify q(x:A)b with q(y:A)(b{x<---y}), for any y not occurring free in b. An object is a collection of components li=a i, for distinct labels 1 i and associated methods ai; the order of these components does not matter. The object containing a given method is called the method's host object. The symbol q is used as a binder for the self parameter of a method; q(x:A)b is a method with self parameter x of type A, to be bound to the host object, and body b. Afield is a degenerate method that ignores its self parameter; we talk aboutfield selection and field update. We use the terms selection and invocation and the terms update and override somewhat interchangeably. A method invocation is written o.lj, where lj is a label of o. It equals the result of the substi- tution of the host object for the self parameter in the body of the method named lj. A method override is written o.lje--q(y:A)b. The intent is to replace the method named lj of o with q(y:A)b; this is a single operation that involves a construction binding y in b. A method override equals a copy of the host object where the overridden method has been replaced by the overriding one. The semantics of override is functional; an override on an object produces a modified copy of the object. An object of type li:B iie n..1 can be formed from a collection of n methods whose self pa- rameters have type li:B i iel..n and whose bodies have types B1 ..... Bn. When writing li:B i ie l..n, we always assume that the 1 i are distinct and that permutations do not matter. The type li:Bi iel..n exhibits only the result types B i, and not the types of g-bound variables. The types of all these variables is li:Bi iel..n. When the method named I i is invoked, it produces a result of type B i. A method can be overridden while preserving the type of its host object. Self-substitution is at the core of the semantics. Because of this, it is easy to define non- terminating computations without explicit use of recursion: let o =A l=q(x:)x.1 then o.I = x.l{x<--o} = 1.o .... Using recursive types, it is possible for a method to return or to modify self: let A =~ I-t(X)I:X let o' -~ I= q(x:A)x then o'.1 = x{x+---o'} = o' let o" ~ 1 = q(y:A) (y.le--q(x:A)x) then o".1 = (o".l~q(x:A)x) = o' We place particular emphasis on the ability to modify self. In object-oriented languages, it is very common for a method to modify field components of self. Generalizing, we allow meth- ods to override other methods of self, or even themselves. This feature does not significantly complicate the problems that we address. We do not provide an operation to extract a method from an object as a function; such an operation is incompatible with object subsumption in typed calculi. Methods are inseparable from objects and cannot be recovered as functions; this consideration inspired the use of a spe- cialized g-notation instead of the familiar ~.-notation for parameters. Other choices of primitives are possible; some are discussed in Abadi, Cardelli 1994c. 2,2 Object Typing and Subtyping We now review the typing and subtyping rules for objects. Each rule has a number of an- tecedent judgments above a horizontal line and a single conclusion judgment below the line. Each judgment has the form E -k 5, for an environment E and an assertion ~ depending on the judgment. An antecedent of the form "F.,E i l- i3~ ViE l ..n" is an abbreviation for n antecedents