Skip to main content
SpringerLink
Log in

Satisfying subtype inequalities in polynomial space

  • Functional Programming II
  • Conference paper
  • First Online:
Static Analysis (SAS 1997)

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

Included in the following conference series:

Abstract

This paper studies the complexity of type inference in λ-calculus with subtyping. Type inference is equivalent to solving systems of subtype inequalities. We consider simple types ordered structurally from an arbitrary set of base subtype assumptions. In this case, we give a PSPACE upper bound. Together with the known lower bound, this result settles completely the complexity of type inference over simple types, which is PSPACE-complete. We use a technique of independent theoretical interest that simplifies existing methods developed in the literature. Finally the algorithm, although mainly theoretical, can lead to a slight practical improvement of existing implementations.

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. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993.

    Google Scholar 

  2. Marcin Benke. Efficient type reconstruction in the presence of inheritance. Technical Report TR 94-10(199), Institute of Informatics, Warsaw University, December 1994.

    Google Scholar 

  3. Marcin Benke. Some complexity bounds for subtype inequalities. Technical Report TR 95-20(220), Institute of Informatics, Warsaw University, 1995.

    Google Scholar 

  4. François Bourdoncle and Stephan Merz. Type checking higher-order polymorphic multi-methods. In Conference Record of the 24th Annual ACM Symposium on Principles of Programming Languages, pages 302–315, Paris, January 1997. ACM.

    Google Scholar 

  5. Franz Baader and Jörg H. Siekmann. Unification theory. In D.M. Gabbay, C.J. Hogger, and J.A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming. Oxford University Press, Oxford, UK, 1994.

    Google Scholar 

  6. Bruno Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.

    Google Scholar 

  7. You-Chin Fuh and Prateek Mishra. Type inference with subtypes. In H. Ganzinger, editor, Proceedings of the European Symposium on Programming, volume 300 of Lecture Notes in Computer Science, pages 94–114. Springer Verlag, 1988.

    Google Scholar 

  8. You-Chin Fuh and Prateek Mishra. Polymorphic subtype inference: Closing the theory-practice gap. In J. Díaz and F. Orejas, editors, Proceedings of the International Joint Conference on Theory and Practice of Software Development: Vol. 2, pages 167–183. LNCS 352. Springer, March 1989.

    Google Scholar 

  9. My Hoang and John C. Mitchell. Lower bounds on type inference with subtypes. In Conference Record of POPL '95: 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 176–185, San Francisco, California, January 1995.

    Google Scholar 

  10. D. Kozen, J. Palsberg, and M. I. Schwartzbach. Efficient recursive subtyping. In ACM, editor, Conference Record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 419–428, Charleston, South Carolina, January 1993.

    Google Scholar 

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

    Google Scholar 

  12. J. Mitchell. Coercion and type inference (summary). In Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, pages 175–185. ACM, ACM, January 1984.

    Google Scholar 

  13. Christos H. Papadimitriou. Computational Complexity. Addison-Wesley, 1994.

    Google Scholar 

  14. Jens Palsberg and Patrick O'Keefe. A type system equivalent to flow analysis. In Conference Record of POPL '95:22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 367–378, San Francisco, California, January 1995.

    Google Scholar 

  15. Vaughan Pratt and Jerzy Tiuryn. Satisfiability of inequalities in a poset. Technical Report TR 95-15(215), Institute of Informatics, Warsaw University, 1995.

    Google Scholar 

  16. Jerzy Tiuryn. Subtype inequalities. In Proceedings, Seventh Annual IEEE Symposium on Logic in Computer Science, pages 308–315, Santa Cruz, California, 22–25 June 1992. IEEE Computer Society Press.

    Google Scholar 

  17. Valery Trifonov and Scott Smith. Subtyping constrained types. In Springer Verlag, editor, Proceedings of the Third International Symposium on Static Analysis (SAS' 96), number 1145 in Lecture Notes in Computer Science, pages 349–365, Aachen, Germany, September 1996.

    Google Scholar 

  18. Jerzy Tiuryn and Mitchell Wand. Type reconstruction with recursive 1655 0699 V 2 types and atomic subtyping. In CARP '93: 18th Colloquium on Trees in Algebra and Programming, July 1993.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Centre de Mathématiques Appliquées, École des Mines de Paris, Paris

    Alexandre Frey

Authors
  1. Alexandre Frey
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Pascal Van Hentenryck

Rights and permissions

Reprints and permissions

Copyright information

© 1997 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Frey, A. (1997). Satisfying subtype inequalities in polynomial space. In: Van Hentenryck, P. (eds) Static Analysis. SAS 1997. Lecture Notes in Computer Science, vol 1302. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0032747

Download citation

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

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-63468-3

  • Online ISBN: 978-3-540-69576-9

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation