article

Open access

Subtyping recursive types

Editor: Andrew W. Appel Authors:

Roberto M. Amadio,

Luca CardelliAuthors Info & Claims

ACM Transactions on Programming Languages and Systems (TOPLAS), Volume 15, Issue 4

Pages 575 - 631

https://doi.org/10.1145/155183.155231

Published: 01 September 1993 Publication History

Abstract

We investigate the interactions of subtyping and recursive types, in a simply typed λ-calculus. The two fundamental questions here are whether two (recursive)types are in the subtype relation and whether a term has a type. To address the first question, we relate various definitions of type equivalence and subtyping that are induced by a model, an ordering on infinite trees, an algorithm, and a set of type rules. We show soundness and completeness among the rules, the algorithm, and the tree semantics. We also prove soundness and a restricted form of completeness for the model. To address the second question, we show that to every pair of types in the subtype relation we can associate a term whose denotation is the uniquely determined coercion map between the two types. Moreover, we derive an algorithm that, when given a term with implicit coercions, can infer its least type whenever possible.

References

[1]

AMADiO, R. Formal theones of inheritance for typed funct~onal languages. Tech. Rep. TR 28/89, Dip. dl Informatica, Univ. dl Fisa, Pisa, Italy, 1989.

[2]

AMAD~O, R. Typed equivalence, type assignment and type contamment. In Proceedings of Condttional and Typed Rewr~ting Systeras 90. Lecture Notes in Computer Science, 516. Spr}nger~Verlag, New York, 1990.

[3]

AMADIO, R. Recursion over realizability structures, lnf. Comput. 91, 1 (1991), 55-85.

[4]

ARNOLD, A., AND NIVAT, M. The metric space of infinite trees. Algebraic and topological properties. Fundamenta Inf. III. (1980), 445 476.

[5]

BREAZU-TANNEN, V., COQUAND, T., GUNTER, C., AND SCEDROV, A. Inheritance as implicit coercion. Inf. Comput. 93, (1991), 172-221.

[6]

REAZU-TANNEN, V., GUNTER, C., AND SCEDROV, A. Denotational semantics for subtyping between recursive types. Rep. MS-CIS 89 63, Logic of Computation 12, Dept. of Computer and Information Science, Univ. of Pennsylvania, Philadelphia, 1989.

[7]

BRUCE, K., AND LONGO, G. A modest model of records, inheritance and bounded quantification. Inf. Comput. 87, 1/2 (1990), 196 240.

[8]

CANNING, P., COOK, W., HILL, W., OLTHOFF, W., AND MITCHELL, J.C. F-bounded polymorphism for object-oriented programming. In Proceedings of Functional Programming and Computer Architecture 89. ACM Press, New York, 1989.

[9]

CARDELLI, L. A semantics of multiple inheritance, lnf Comput. 76, (1988), 138 164.

[10]

CARDELLI, L. Amber, combinators and functiona} programming }anguages. In Proceedings of the 13th Summer School of the LITP, Le Val D'Ajol (Vosges, France, May 1985). Lecture Notes m Computer Science, 242. Springer-Verlag, New York, 1985.

[11]

CARDELLI, L. Typeful programming. In Formal Descrtption of Programming Concepts, E. J. Neuhold and M. Paul, Eds. Springer-Verlag, New York, 1991, 431 507.

[12]

CARDELLI, L., AND LONaO, G. A semantic basis for Quest. J. Functional Program. 1, 4 (Oct. 1991), 417-458.

[13]

CARDELLI, L., AND WEGNER, P. On understanding types, data abstraction and polymorphism. ACM Comput. Surv. 17, 4 (Dec. 1985), 471-522.

[14]

CARDONE, F., AND CoPPO, M. Type inference with recursive types: Syntax and semantics. Inf. Comput. 92, 1, 48-80.

[15]

COOK, W. A denotational semantics of inheritance. Ph.D. dissertation, Brown Univ., Providence, R.I., 1989.

[16]

COURCELLE, B. Fundamental properties of infinite trees. Theor. Comput. Sci. 25, (1983), 95-169.

[17]

COURCELLE, B. Equivalence and transformation of regular systems--Applications to recursive program schemes and gTammars. Theor. Comput. Sci. 42, (1986), I 122.

[18]

CURIEN, P.-L., AND GHELLI, G. Coherence of subsumption, minimum typing and type checking in F<. Math. Struc. Comput. Sci. 2, (1992), 55 91.

[19]

H~ANo, M. A small complete category. Ann. Pure Appl. Logic 40, 2, (1989), 135 165.

[20]

MACQUEEN, D., PLOTKIN, G., AND SETHI, R. An ideal model for recursive polymorphic types. Inf. Comput. 71, (1986), 1-2.

[21]

MmNER, R. A complete inference system for a class of regular behaviors. J. Comput. Syst. Sci. 28 (1984), 439-466.

[22]

NELSON, G., ED. Systems Programming with Modula-3. Prentice-Hall, Englewood Cliffs, N.J., 1991.

[23]

PARI~, D. M.R. Concurrency and automata on infinite sequences. In Proceedings ofthe 5th GI conference. Lecture Notes ~n Computer Science, 104. Springer-Verlag, New York, 1981, 167 183.

[24]

PIEt~CE, B.C. Bounded quantification is undecidable. In Proceedings of the ACM Symposium on Principles of Programming Languages. ACM, New York, 1992, 305-315.

[25]

SALOMAA, A. Two complete systems for the algebra of regular events. J. ACM 13, I (1966).

[26]

SCOTT, D. Continuous lattices. In Toposes, Algebraic Geometry and Logic. Lecture Notes in Mathematics 274. Springer-Verlag, New York, 1972, 97 136.

[27]

SCOTT, D. Data types as lattices. SIAM J. Comput. 5, (1976), 522-587.

[28]

VAN WIJNGAARDEN ET AL., EDS. Revised Report on the Algorithmlc Language Algo168. Springer-Verlag, New York, 1976, 103 107.

[29]

W,OSWORTH, C. The relation between computational and denotational properties for Scott's D~ models ofthe lambda-calculus. SIAM J. Comput. 5, (1976), 488-521.

Cited By

Udomsrirungruang TYoshida N(2024)Three Subtyping Algorithms for Binary Session Types and their Complexity AnalysesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.5401(49-60)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.5
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Wei GBračevac OJia SBao YRompf T(2024)Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsProceedings of the ACM on Programming Languages10.1145/36328568:POPL(393-424)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632856
Show More Cited By

Recommendations

Subtyping Recursive Types in Kernel Fun - Abstract
LICS '99: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science

The problem of defining and checking a subtype relation between recursive types was studied by Amadio and Cardelli (ACM TOPLAS'93) for a first order type system, but for second order systems, which combine subtyping and parametric polymorphism, only ...
Mutually Iso-Recursive Subtyping

Iso-recursive types are often taken as a type-theoretic model for type recursion as present in many programming languages, e.g., classes in object-oriented languages or algebraic datatypes in functional languages. Their main advantage over an equi-...
Typed compilation of recursive datatypes

Standard ML employs an opaque (or generative) semantics of datatypes, in which every datatype declaration produces a new type that is different from any other type, including other identically defined datatypes. A natural way of accounting for this is ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

Copyright © 1993 ACM.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 01 September 1993

Published in TOPLAS Volume 15, Issue 4

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

344
Total Citations
View Citations
1,265
Total Downloads

Downloads (Last 12 months)188
Downloads (Last 6 weeks)21

Reflects downloads up to 28 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Udomsrirungruang TYoshida N(2024)Three Subtyping Algorithms for Binary Session Types and their Complexity AnalysesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.401.5401(49-60)Online publication date: 6-Apr-2024
https://doi.org/10.4204/EPTCS.401.5
DeYoung HMordido APfenning FDas A(2024)Parametric Subtyping for Structural Parametric PolymorphismProceedings of the ACM on Programming Languages10.1145/36329328:POPL(2700-2730)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632932
Wei GBračevac OJia SBao YRompf T(2024)Polymorphic Reachability Types: Tracking Freshness, Aliasing, and Separation in Higher-Order Generic ProgramsProceedings of the ACM on Programming Languages10.1145/36328568:POPL(393-424)Online publication date: 5-Jan-2024
https://dl.acm.org/doi/10.1145/3632856
Lermusiaux PMontagu B(2024)Detection of Uncaught Exceptions in Functional Programs by Abstract InterpretationProgramming Languages and Systems10.1007/978-3-031-57267-8_15(391-420)Online publication date: 6-Apr-2024
https://dl.acm.org/doi/10.1007/978-3-031-57267-8_15
Rossberg A(2023)Mutually Iso-Recursive SubtypingProceedings of the ACM on Programming Languages10.1145/36228097:OOPSLA2(347-373)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622809
Zhou LZhou YOliveira B(2023)Recursive Subtyping for AllProceedings of the ACM on Programming Languages10.1145/35712417:POPL(1396-1425)Online publication date: 11-Jan-2023
https://dl.acm.org/doi/10.1145/3571241
Cruz RRoss MNightingale RPickering EAllenby MWoodruff MPowell S(2023)An automated parametric ear model to improve frugal 3D scanning methods for the advanced manufacturing of high-quality prosthetic earsComputers in Biology and Medicine10.1016/j.compbiomed.2023.107033162:COnline publication date: 1-Aug-2023
https://dl.acm.org/doi/10.1016/j.compbiomed.2023.107033
Chen ZPfenning F(2023)A Logical Framework with Higher-Order Rational (Circular) TermsFoundations of Software Science and Computation Structures10.1007/978-3-031-30829-1_4(68-88)Online publication date: 21-Apr-2023
https://doi.org/10.1007/978-3-031-30829-1_4
Voigt-Antons JKojic T(2022)Towards an Updated Understanding of Immersive Multimedia ExperiencesACM SIGMultimedia Records10.1145/3578508.357851513:4(1-1)Online publication date: 23-Dec-2022
https://dl.acm.org/doi/10.1145/3578508.3578515
Cimini MFischer BBurgueño LCazzola W(2022)Lang-n-Prove: A DSL for Language ProofsProceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering10.1145/3567512.3567514(16-29)Online publication date: 29-Nov-2022
https://dl.acm.org/doi/10.1145/3567512.3567514
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents