Skip to main content
SpringerLink
Log in

F ≤ & : integrating parametric and “ad hoc” second order polymorphism

Extended abstract

  • Conference paper
Database Programming Languages (DBPL-4)

Part of the book series: Workshops in Computing ((WORKSHOPS COMP.))

Abstract

In the last years several object-oriented database systems have come to life. However among them there is a lack of statically strongly typed languages. This is a very important deficiency especially for languages, as the database programming languages, which are designed for complex applications of large size and that evolve in time.

The absence of such a type discipline is justified by the complexity of the problem and of the structures it has to be applied to. Therefore we think that only a fundamental study, which were able to capture the essential features of the system, would lead to a typeful object-oriented programming. Thus we define an extension of F ≤ [CG92] to which we add functions that dispatch on different terms according to the type they receive as argument. In other words, we enrich the explicit parametric polymorphism of by F ≤ an explicit “ad hoc” polymorphism (according to the classification of [Str67]). We prove that the calculus we obtain, called F ≤ & , enjoys the properties of Church-Rosser and Subject Reduction.

This extension constitutes our paradigmatic language for the foundation of object-oriented programming: the connections between F ≤ & and object-oriented languages are widely stressed, and the modeling by F ≤ & of some features of the object-oriented style is described.

The author was supported by the grant n. 203.01.56 of the Consiglio Nazionale delle Ricerche — Comitato Nazionale delle Scienze Matematiche

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. A. Albano, G. Ghelli, M.E. Occhiuto, and R. Orsini. Galileo reference Manual Version 2.0. Servizio editoriale universitario di Pisa, Febbraio 1988.

    Google Scholar 

  2. Apple Computer Inc., Eastern Research and Technology. Dylan: an object-oriented dynamic language, April 1992.

    Google Scholar 

  3. F. Bancilhon, C. Delobel, and P. Kanellakis (eds.). Implementing an Object-Oriented database system: The story of 02. Morgan Kaufmann, 1992.

    Google Scholar 

  4. K.B. Bruce. A paradigmatic object-oriented programming language: Design, static typing and semantics. Technical Report CS-92–01, Williams College, Williamstown, MA 01267, January 1992.

    Google Scholar 

  5. V. Breazu-Tannen, T. Coquand, C. Gunter, and A. Scedrov. Inheritance as implicit coercion. Information and Computation, 93 (1): 172–221, July 1991.

    Article  MathSciNet  MATH  Google Scholar 

  6. Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138–164, 1988. A previous version can be found in Semantics of Data Types, LNCS 173, 51–67, Springer-Verlag, 1984.

    Google Scholar 

  7. Luca Cardelli. Extensible records in a pure calculus of subtyping. Research report 81, DEC Systems Research Center, January 1992. To appear in [GM93].

    Google Scholar 

  8. G. Castagna. A meta-language for typed object-oriented languages. In R.K. Shyamasundar, editor, 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, LNCS, Bombay, India, December 1993. Springer-Verlag.

    Google Scholar 

  9. P.S. Canning, W.R. Cook, W.L. Hill, J. Mitchell, and W.G. Orthoff. F-bounded quantification for object-oriented programming. In ACM Conference on Functional Programming and Computer Architecture, September 1989.

    Google Scholar 

  10. P. L. Curien and G. Ghelli. Coherence of subsumption, minimum typing and the type checking in Mathematical Structures in Computer Science, 2 (1), 1992.

    Google Scholar 

  11. G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping, 1992. To appear in Information and Computation. An extended abstract has appeared in the proceedings of the ACM Conference on LISP and Functional Programming, pp.182–192; San Francisco, June 1992.

    Google Scholar 

  12. CGL93] G. Castagna, G. Ghelli, and G. Longo. A semantics for early: a calculus with overloading and early binding. In M. Bezem and J.F. Groote, editors, International Conference on Typed Lambda Calculi and Applications,number 664 in LNCS, pages 107–123, Utrecht, The Netherlands, March 1993. Springer-Verlag. TLCA’93.

    Google Scholar 

  13. W.R. Cook, W.L. Hill, and P.S. Canning. Inheritance is not sub-typing. 17th Ann. ACM Symp. on Principles of Programming Languages, January 1990.

    Google Scholar 

  14. L. Cardelli and G. Longo. A semantic basis for Quest. Journal of Functional Programming, 1 (4): 417–458, 1991.

    Article  MathSciNet  MATH  Google Scholar 

  15. L. Cardelli, S. Martini, J.C. Mitchell, and A. Scedrov. An extension of system F with subtyping. In T. Ito and A.R. Meyer, editors, Theoretical Aspects of Computer Software,pages 750–771. Springer-Verlag, September 1991. LNCS 526 (preliminary version). To appear in Information and Computation.

    Google Scholar 

  16. L. Cardelli and P. Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17 (4): 471–522, December 1985.

    Article  Google Scholar 

  17. L.G. DeMichiel and R.P. Gabriel. Common lisp object system overview. In Bézivin, Hullot, Cointe, and Lieberman, editors, Proc. of ECOOP ’87 European Conference on Object-Oriented Programming, number 276 in LNCS, pages 151–170, Paris, France, June 1987. Springer-Verlag.

    Chapter  Google Scholar 

  18. G. Ghelli. Proof Theoretic Studies about a Minimal Type System Integrating Inclusion and Parametric Polymorphism. PhD thesis, Dipartimento di Informatica, Università di Pisa, March 1990. Tech. Rep. TD-6/90.

    Google Scholar 

  19. G. Ghelli. A static type system for message passing. In Proc. Of OOPSLA ‘81, 1991.

    Google Scholar 

  20. Carl A. Gunter and John C. Mitchell. Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design. The MIT Press, 1993. To appear.

    Google Scholar 

  21. R. Hindley. The Church-Rosser property and a result of combinatory logic. Dissertation, 1964. University of Newcastle-upon-Tyne.

    Google Scholar 

  22. Bertrand Meyer. Object-Oriented Software Construction. Prentice-Hall International Series, 1988.

    Google Scholar 

  23. M.H.A. Newman. On theories with a combinatorial definition of “equivalence”. Annals of Math., 43 (2): 223–243, 1942.

    Article  MATH  Google Scholar 

  24. NeXT Computer Inc. NeXTstep-concepts. Chapter 3: Object-Oriented Programming and Objective-C,2.0 edition, 1991.

    Google Scholar 

  25. Ontologic Inc., 47 Manning Rd., Billerica, MA 01821. Vbase+:object database for C++.

    Google Scholar 

  26. B.C. Pierce. Bounded quantification is undecidable. In 20th Ann. ACM Symp. on Principles of Programming Languages. ACM-Press, 1993.

    Google Scholar 

  27. B.C. Pierce and D.N. Turner. Simple type-theoretic foundations for object-oriented programming. Journal of Functional Programming,1993. To appear; a preliminary version appeared in Principles of Programming Languages, 1993, and as University of Edinburgh technical report ECS-LFCS-92–225, under the title “Object-Oriented Programming Without Recursive Types”.

    Google Scholar 

  28. B. K. Rosen. Tree manipulation systems and Church-Rosser theorems. Journal of ACM, 20: 160–187, 1973.

    Article  MATH  Google Scholar 

  29. C. Strachey. Fundamental concepts in programming languages. Lecture notes for International Summer School in Computer Programming, Copenhagen, August 1967.

    Google Scholar 

  30. Mitchell Wand. Complete type inference for simple objects. In 2nd Ann. Symp. on Logic in Computer Science, 1987.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIENS(CNRS)-DMI, 45 rue d’Ulm, 75005, Paris, France

    Giuseppe Castagna

Authors
  1. Giuseppe Castagna
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Institute of Computer Science, The Hebrew University of Jerusalem, 91904, Givat-Ram, Jerusalem, Israel

    Catriel Beeri PhD

  2. Research Institute for Mathematical Sciences, Kyoto University, Kitashirakawa, Sakyo-ku, 606-01, Kyoto, Japan

    Atsushi Ohori PhD

  3. Department of Computer Science, Courant Institute of Mathematical Sciences, New York University, 251 Mercer Street, 10012-1185, New York, NY, USA

    Dennis E. Shasha PhD

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Castagna, G. (1994). F ≤ & : integrating parametric and “ad hoc” second order polymorphism. In: Beeri, C., Ohori, A., Shasha, D.E. (eds) Database Programming Languages (DBPL-4). Workshops in Computing. Springer, London. https://doi.org/10.1007/978-1-4471-3564-7_19

Download citation

  • DOI: https://doi.org/10.1007/978-1-4471-3564-7_19

  • Publisher Name: Springer, London

  • Print ISBN: 978-3-540-19853-6

  • Online ISBN: 978-1-4471-3564-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation