Skip to main content
SpringerLink
Log in
SpringerLink
Log in

Predicative polymorphic subtyping

  • Contributed Papers
  • Conference paper
  • First Online:
Mathematical Foundations of Computer Science 1998 (MFCS 1998)

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

  • 167 Accesses

Abstract

We consider a version of the Mitchell's polymorphic type containment (aka subsumption). Here, it is not suited for the system F but for the predicative version of it introduced by Leivant. The aim of the approach is to propose a new notion of polymorphic functional subsumption which may be decidable unlike Mitchell's one. We define a system for predicative subsumption in the style of Mitchell and then prove its equivalence with a Gentzen-style definition. Next, we study the notion of bicoercibility. This is followed by a reduction of the typability in the Leivant's system with subsumption to subsumption itself.

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. Marcin Benke. Predicative polymorphic subtyping. Technical Report TR98-02(251), Institute of Informatics, Warsaw University, March 1998. Available from http://zls.mimuw.edu.pl/~ben/Papers/.

    Google Scholar 

  2. Jacek Chrzaszcz. Polimorphic subtyping without distributivity. MFCS'98 (in this volume), 1998.

    Google Scholar 

  3. Luis Damas and Robin Milner. Principal type-schemes for functional programs. In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 207–211, 1982.

    Google Scholar 

  4. J.-Y. Girard. Interprétation fonctionelle et élimination des coupures dans l'arithmetique d'ordre supérieur. PhD thesis, Université Paris VII, 1972.

    Google Scholar 

  5. Trevor Jim. System F plus subsumption reduces to Mitchell's subtyping relation. Manuscript, 1995.

    Google Scholar 

  6. Trevor Jim. What are principal typings and what are they good for? In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 42–53, 1996.

    Google Scholar 

  7. A. J. Kfoury and J. Tiuryn. Type reconstruction in finite-rank fragments of the second-order λ-calculus. Information and Computation, 2(98):228–257, June 1992.

    Article  MATH  MathSciNet  Google Scholar 

  8. Daniel Leivant. Finitely stratified polymorphism. Information and Computation, 93:93–113, 1991.

    Article  MATH  MathSciNet  Google Scholar 

  9. G. Longo, K. Milsted, and S. Soloviev. A logic of subtyping. In Proc. IEEE Symp. on Logic in Computer Science, pages 292–299, 1995.

    Google Scholar 

  10. Konstantin Läufer and Martin Odersky. Polymorphic type inference and abstract data types. ACM Transactions on Programming Languages and Systems, 16(5):1411–1430, September 1994.

    Article  Google Scholar 

  11. Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17(14):348–375, December 1978.

    Article  MATH  MathSciNet  Google Scholar 

  12. John C. Mitchell. Polymorphic type inference and containment. Information and Computation, 76(2/3):211–249, 1988. Reprinted in Logical Foundations of Functional Programming, ed. G. Huet, Addison-Wesley (1990) 153–194.

    Article  MATH  MathSciNet  Google Scholar 

  13. John Mitchell and Gordon Plotkin. Abstract types have existential types. ACM Transactions on Programming Languages and Systems, 10(3):470–502, 1988.

    Article  Google Scholar 

  14. Martin Odersky and Konstantin Läufer. Putting type annotations to work. In Conf. Rec. ACM Symp. Principles of Programming Languages, pages 54–67, 1996.

    Google Scholar 

  15. N. Perry. The Implementation of Practical Functional Programming Languages. PhD thesis, Imperial College of Science, Technology, and Medicine, University of London, 1990.

    Google Scholar 

  16. Didier Rémy. Programming objects with ml-art, and extension to ml with abstract and record types. In Proceedings of Theoretical Aspects of Programming Languages, number 789 in LNCS, pages 321–346. Springer, 1994.

    Google Scholar 

  17. J. C. Reynolds. Mathematical foundations of software development. volume 19 of Lecture Notes in Computer Science, chapter Towards a theory of type structure., pages 408–425. Springer, 1974.

    Google Scholar 

  18. Jerzy Tiuryn. Equational axiomatization of bicoercibility for polymorphic types. In Ed. P.S. Thiagarajan, editor, Proc. 15th Conference Foundations of Software Technology and Theoretical Computer Science, volume 1026 of Lecture Notes in Computer Science, pages 166–179. Springer Verlag, 1995.

    Google Scholar 

  19. Jerzy Tiuryn and Pawel Urzyczyn. The subtyping problem for second-order types is undecidable. In Proceedings of 11th LICS, 1996.

    Google Scholar 

  20. J. Wells. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Proc. 9th Ann. IEEE Symp. Logic in Comput. Sci., pages 176–185, 1994.

    Google Scholar 

  21. J. Wells. The undecidability of Mitchell's subtyping relation. Technical report, Computer Sci. Dept., Boston University, December 1995.

    Google Scholar 

  22. J. B. Wells. Typability is undecidable for F+eta. Technical Report 96-022, Boston University, March 9, 1996.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Informatics, Warsaw University, Poland

    Marcin Benke

Authors
  1. Marcin Benke
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Luboš Brim Jozef Gruska Jiří Zlatuška

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Benke, M. (1998). Predicative polymorphic subtyping. In: Brim, L., Gruska, J., Zlatuška, J. (eds) Mathematical Foundations of Computer Science 1998. MFCS 1998. Lecture Notes in Computer Science, vol 1450. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055782

Download citation

  • DOI: https://doi.org/10.1007/BFb0055782

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64827-7

  • Online ISBN: 978-3-540-68532-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation