Skip to main content
SpringerLink
Log in

Subtyping with union types, intersection types and recursive types

  • Conference paper
  • First Online:
Theoretical Aspects of Computer Software (TACS 1994)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 789))

Included in the following conference series:

Abstract

Union, intersection and recursive types are type constructions which make it possible to formulate very precise types. However, because of type checking difficulties related to the simultaneous use of these constructions, they have only found little use in programming languages. One of the problems is subtyping. We show how the subtype decision problem may be solved by an encoding into regular tree expressions, and prove soundness and completeness with respect to the classical ideal model for types [MPS86].

As a part of the work we show how the structure of values may be described by trees, and how the metric space of ideals may be related to a metric space of sets of trees. The proof techniques applied here may be of independent interest.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Roberto M. Amadio and Luca Cardelli. Subtyping recursive types. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL'91), pages 104–118, ACM Press, 1991. Extended abstract. Full version in [AC92].

    Google Scholar 

  2. Roberto M. Amadio and Luca Cardelli. Subtyping Recursive Types. Technical Report 133, INRIA, Institut National de Recherche en Informatique et en Automatique, Lorraine, February 1992.

    Google Scholar 

  3. Alexander Aiken and Brian M. Murphy. Implementing regular tree expressions. In J. Hughes, editor, Proceedings of the 5th A CM Conference on Functional Programming Languages and Computer Architecture (FPCA '91), Cambridge, MA, USA, August 1991, volume 523 of Lecture Notes in Computer Science, pages 427–447, Springer-Verlag, 1991.

    Google Scholar 

  4. Alexander Aiken and Brian M. Murphy. Static type inference in a dynamically typed language. In Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages (POPL '91), pages 279–290, ACM Press, 1991.

    Google Scholar 

  5. Alexander Aiken and Edward L. Wimmers. Solving systems of set constraints (extended abstract). In Proceedings of the Seventh Annual IEEE Symposium on Logic in Computer Science (LICS'92), Santa Cruz, California, June 1992, pages 329–340, IEEE Computer Society, IEEE Computer Society Press, 1992.

    Google Scholar 

  6. Alexander Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Proceedings of the 6th ACM Conference on Functional Programming Languages and Computer Architecture (FPCA '93), Copenhagen, Denmark, June 1993, pages 31–41, ACM Press, 1993.

    Google Scholar 

  7. Robert Cartwright and Mike Fagan. Soft typing. In Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI'91), pages 278–292, ACM Press, 1991.

    Google Scholar 

  8. Luca Cardelli and Peter Wegner. On understanding types, data abstraction, and polymorphism. Computing Surveys, 17(4):471–522, 1985.

    Google Scholar 

  9. Flemming M. Damm. Subtyping with Union Types, Intersection Types and Recursive Types. Technical Report, Department of Computer Science, The Technical University of Denmark, 1994. Forthcoming.

    Google Scholar 

  10. Tim Freeman and Frank Pfenning. Refinement types for ML. In Proceedings of the ACM SIGPLAN'91 Conference on Programming Language Design and Implementation (PLDI'91), pages 268–277, ACM Press, 1991.

    Google Scholar 

  11. Ferenc Gécseg and Magnus Steinby. Tree Automata. Akadémiai Kiadó, Budapest, 1984.

    Google Scholar 

  12. R. Gilleron, S. Tison, and M. Tommasi. Solving systems of set constraints with negated subset relationships. In Proceedings of the 34th Annuel Symposium on Foundations of Computer Science (FOCS'93), pages 372–380, IEEE Computer Society, IEEE Computer Society Press, 1993.

    Google Scholar 

  13. David MacQueen, Gordon Plotkin, and Ravi Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95–130, 1986.

    Google Scholar 

  14. Prateek Mishra and Uday S. Reddy. Declaration-free type checking. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages (POPL'85), pages 7–21, 1985.

    Google Scholar 

  15. Benjamin C. Pierce. Programming with Intersection Types, Union Types and Polymorphism. Technical Report CMU-CS-91-106, Carnegie Mellon University, 1991.

    Google Scholar 

  16. W.A. Sutherland. Introduction to metric and topological spaces. Oxford University Press, 1975.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, The Technical University of Denmark, 2800, Lyngby, Denmark

    Flemming M. Damm

Authors
  1. Flemming M. Damm
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Masami Hagiya John C. Mitchell

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Damm, F.M. (1994). Subtyping with union types, intersection types and recursive types. In: Hagiya, M., Mitchell, J.C. (eds) Theoretical Aspects of Computer Software. TACS 1994. Lecture Notes in Computer Science, vol 789. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-57887-0_121

Download citation

  • DOI: https://doi.org/10.1007/3-540-57887-0_121

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-57887-1

  • Online ISBN: 978-3-540-48383-0

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation