Nothing Special   »   [go: up one dir, main page]

skip to main content
10.1145/141471.141537acmconferencesArticle/Chapter ViewAbstractPublication PageslfpConference Proceedingsconference-collections
Article
Free access

A calculus for overloaded functions with subtyping

Published: 01 January 1992 Publication History

Abstract

We present a simple extension of typed λ-claculus where functions can be overloaded by adding different “pieces of code”. In short, the code of an overloaded function is formed by several branches of code; the branch to execute is chosen, when the function is applied, according to a particular selection rule which depends on the type of the argument. The crucial feature of the present approach is that a subtyping relation is defied among types, such that the type of a term generally decreases during computation, and this fact induces a distinction between the “compile-time” type and the “run-time”type of a term. We study the case of overloaded functions where the branch selection depends on the run-time type of the argument, so that overloading cannot be eliminated by a static analysis of code, but is an essential feature to be dealt with during computation. We prove Confluence and Strong Normalization for this calculus as well as a generalized Subject-Reduction theorem (but proofs are ommitted in this abstract.
The definition of this calculus is driven by the understanding of object-oriented features and the connections between our calculus and object-orientedness are extensively stressed. We show that this calculus provides a foundation for typed object-oriented languages which solves some of the problems of the standard record-based approach. It also provides a type-discipline for a relevant fragment of the “core framework” of CLOS.

References

[1]
R. Amadio and L. Cardelli. $ubiyping Recursive Types. Technical Report, Digital System Research Center, August 1990.
[2]
A. Asperti and G. Longo. Categories, Types and Structures: An Introduction to Category Theory for the Working Computer Scientist. MIT-Press, 1991.
[3]
K.B. Bruce and G. Longo. A modest model of records, inheritance and bounded quantification. Information and Computation, 87(1/2):196-240, 1990. A first version can be found in 3rd Ann. Syrup. on Logic in Uomputer Science, 1988.
[4]
Luca Cardelli. A semantics of multiple inheritance. Information and Computation, 76:138-164, 1988. A first version can be found in Semantics of Data Types, LNCS 173, 51-67, Springer-Verlag, 1984.
[5]
M. Coppo, M. Denzani-Ciancaglini, and B. Venneri. Functional characters of solvable terms. Zeit. Maih. Logik, 27:45-58, 1981.
[6]
P.L. Curien and G. Ghelli. Coherence of subsumption. Mathematical Structures in Computer Science, 2(1), 1992.
[7]
G. Castagna, G. Ghelli, and G. Longo. A calculus for overloaded functions with subtyping. Technical Report 92-4, Laboratoire d'Informatique, Ecole Normale Supdrieure- Paris, February 1992.
[8]
W.R. Cook, W.L. Hill, and P.S. Canning. Inheritance is not subtyping. 17th Ann. A UM Syrup. on Principles of Programruing Languages, January 1990.
[9]
L. Cardelli and G. Longo. A semantic basis for Quest. Technical Report, Digital System Research Center, February 1990. LISP and FP, Nice, July 1990; Journal of Functional Programming, 1(4):417-458 (to appear).
[10]
G. Castagna and G. Longo. From inheritance to Quest's type theory, in Ecole Jeunes Chercheurs du GRECO de Programmation, Sophia-Antipolis (Nice), April 1991.
[11]
L. Cardelli and J.C. Mitchell. Operations on records. Mathematical Structures in Computer Science, 1(1):3-48, 1991.
[12]
L. Cardelli and P. Wegner. On understanding types, data abstraction and polymorphism. Computing Surveys, 17(4):471-522, December 1985.
[13]
L.G. DcMichiel and R.P. Gabriel. Common lisp object system overview, ill Proc. of ECOOP '87 European Conference on Object Oriented Programming, 1987.
[14]
G. Ghelli. A static type system for message passing. In Proc. of OOPSLA '91, 1991.
[15]
S.K. Keene. Object Oriented Programming in COMMON LISP: A Programming Guide to CLO$. Addison-Wesley, 1989.
[16]
J.C. Mitchell. A type inference approach to reduction properties and semantics of polymorphic expressions. In A CM Conference on LISP and Functional Programming (~FP), pages 308-319, 1986.
[17]
J.C. Mitchell. Toward a typed foundation for method specialization and inheritance. 17th Ann. A CM Syrup. on Principles of Programming Languages, January 1990.
[18]
N. Marti-Oliet and J. Meseguer. Inclusions and Subtypes. Technical Report, SRI International, Computer Science Laboratory, December 1990.
[19]
B. Pierce. Intersection and Union Types. Technical Report, Carnegie Mellon University, 1990.
[20]
F. Rouaix. ALCOOL-90, Typage de la surcharge dans un langage fonctionnel. PhD thesis, Universit~ PARIS VII, December 1990.
[21]
Mitchell Wand. Complete type inference for simple objects. In 2nd Ann. Syrup. on Logic in Computer Science, 1987.
[22]
Mitchell Wand. Type inference for record concatenation and multiple inheritance, in Jth Ann. Syrup. on Logic in Computer Science, 1989.
[23]
Philip Wadler and Stephen Blott. How to make "ad-hoc" polymorphism less "adhoe". In 16th Ann. ACM Syrup. on Principles of Programming Languages, pages 60- 76, 1989.

Cited By

View all
  • (2022)Formalizing ϕ-Calculus: A Purely Object-Oriented Calculus of Decorated ObjectsProceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3611096.3611103(29-36)Online publication date: 7-Jun-2022
  • (2019)Decidable tag-based semantic subtyping for nominal types, tuples, and unionsProceedings of the 21st Workshop on Formal Techniques for Java-like Programs10.1145/3340672.3341115(1-11)Online publication date: 15-Jul-2019
  • (2019)Polymorphic symmetric multiple dispatch with varianceProceedings of the ACM on Programming Languages10.1145/32903243:POPL(1-28)Online publication date: 2-Jan-2019
  • Show More Cited By

Recommendations

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences
LFP '92: Proceedings of the 1992 ACM conference on LISP and functional programming
January 1992
365 pages
ISBN:0897914813
DOI:10.1145/141471
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 January 1992

Permissions

Request permissions for this article.

Check for updates

Qualifiers

  • Article

Conference

LFP92
LFP92: ACM Conference on Lisp and Functional Programming
June 22 - 24, 1992
California, San Francisco, USA

Acceptance Rates

Overall Acceptance Rate 30 of 109 submissions, 28%

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)90
  • Downloads (Last 6 weeks)26
Reflects downloads up to 16 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2022)Formalizing ϕ-Calculus: A Purely Object-Oriented Calculus of Decorated ObjectsProceedings of the 24th ACM International Workshop on Formal Techniques for Java-like Programs10.1145/3611096.3611103(29-36)Online publication date: 7-Jun-2022
  • (2019)Decidable tag-based semantic subtyping for nominal types, tuples, and unionsProceedings of the 21st Workshop on Formal Techniques for Java-like Programs10.1145/3340672.3341115(1-11)Online publication date: 15-Jul-2019
  • (2019)Polymorphic symmetric multiple dispatch with varianceProceedings of the ACM on Programming Languages10.1145/32903243:POPL(1-28)Online publication date: 2-Jan-2019
  • (2019)Distributive Disjoint Polymorphism for Compositional ProgrammingProgramming Languages and Systems10.1007/978-3-030-17184-1_14(381-409)Online publication date: 6-Apr-2019
  • (2016)Disjoint intersection typesACM SIGPLAN Notices10.1145/3022670.295194551:9(364-377)Online publication date: 4-Sep-2016
  • (2016)Disjoint intersection typesProceedings of the 21st ACM SIGPLAN International Conference on Functional Programming10.1145/2951913.2951945(364-377)Online publication date: 4-Sep-2016
  • (2013)Fine-Grained Function Visibility for Multiple Dispatch with Multiple InheritanceProceedings of the 11th Asian Symposium on Programming Languages and Systems - Volume 830110.1007/978-3-319-03542-0_11(156-171)Online publication date: 9-Dec-2013
  • (2011)Intelligent Service Trading and Brokering for Distributed Network Services in GridSolveHigh Performance Computing for Computational Science – VECPAR 201010.1007/978-3-642-19328-6_32(340-351)Online publication date: 2011
  • (2009)Advanced service trading for scientific computing over the gridThe Journal of Supercomputing10.1007/s11227-008-0234-949:1(64-83)Online publication date: 1-Jul-2009
  • (2008)Baby Modula-3 and a theory of objectsJournal of Functional Programming10.1017/S09567968000010524:2(249-283)Online publication date: 7-Nov-2008
  • Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Login options

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media