Subtyping constrained types

  • Valery Trifonov
  • Scott Smith
Contributed Papers
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1145)


A constrained type is a type that comes with a set of subtyping constraints on variables occurring in the type. Constrained type inference systems are a natural generalization of Hindley/Milner type inference to languages with subtyping. This paper develops several subtyping relations on polymorphic constrained types of a general form that allows recursive constraints and multiple bounds on type variables. Subtyping constrained types has applications to signature matching and to constrained type simplification.


Type Variable Type Scheme Regular Tree Typing Rule Type Inference 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    A. Aiken and E. L. Wimmers. Type inclusion constraints and type inference. In Proceedings of the International Conference on Functional Programming Languages and Computer Architecture, pages 31–41, 1993.Google Scholar
  2. 2.
    A. Aiken, E. L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Conference Record of the Twenty-First Annual ACM Symposium on Principles of Programming Languages, pages 163–173, 1994.Google Scholar
  3. 3.
    R. Amadio and L. Cardelli. Subtyping recursive types. ACM Transactions on Programming Languages and Systems, 15(4):575–631, September 1993. Extended abstract in POPL 1991.Google Scholar
  4. 4.
    FranÇois Bourdoncle and Stephan Merz. On the integration of functional programming, class-based object-oriented programming, and multi-methods. Technical Report 26, Centre des Mathématiques Appliquées, Ecole des Mines de Paris, 1996. Available at Scholar
  5. 5.
    Kim Bruce, Luca Cardelli, Giuseppe Castagna, The Hopkins Objects Group, Gary T. Leavens, and Benjamin Pierce. On binary methods. Theory and Practice of Object Systems, 1(3):217–238, 1995.Google Scholar
  6. 6.
    L. Cardelli. A semantics of multiple inheritance. In Semantics of Data Types, volume 173 of Lecture notes in Computer Science, pages 51–67. Springer-Verlag, 1984.Google Scholar
  7. 7.
    B. Courcelle. Fundamental properties of infinite trees. Theoretical Computer Science, 25:95–169, 1983.CrossRefGoogle Scholar
  8. 8.
    Pavel Curtis. Constrained quantification in polymorphic type analysis. Technical Report CSL-90-1, XEROX Palo Alto Research Center, CSLPubs.parc@xerox. com, 1990.Google Scholar
  9. 9.
    J. Eifrig, S. Smith, and V. Trifonov. Sound polymorphic type inference for objects. In OOPSLA '95, pages 169–184, 1995.Google Scholar
  10. 10.
    J. Eifrig, S. Smith, and V. Trifonov. Type inference for recursively constrained types and its application to OOP. In Proceedings of the 1995 Mathematical Foundations of Programming Semantics Conference, volume 1 of Electronic Notes in Theoretical Computer Science. Elsevier, 1995. http: // Scholar
  11. 11.
    J. Eifrig, S. Smith, V. Trifonov, and A. Zwarico. An interpretation of typed OOP in a language with state. Lisp and Symbolic Computation, 8(4):357–397, 1995.Google Scholar
  12. 12.
    Y.-C. Fuh and P. Mishra. Type inference with subtypes. In European Symposium on Programming, 1988.Google Scholar
  13. 13.
    Trevor Jim. Principal typings and type inference. PhD thesis, MIT, 1996. (to appear).Google Scholar
  14. 14.
    S. Kaes. Type inference in the presence of overloading, subtyping and recursive types. In ACM Conference on Lisp and Functional Programming, pages 193–204, 1992.Google Scholar
  15. 15.
    D. B. MacQueen, G. Plotkin, and R. Sethi. An ideal model for recursive polymorphic types. Information and Control, 71:95–130, 1986.CrossRefGoogle Scholar
  16. 16.
    P. Mishra and U. Reddy. Declaration-free type checking. In Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, pages 7–21, 1985.Google Scholar
  17. 17.
    John C. Mitchell. Coercion and type inference (summary). In Conference Record of the Eleventh Annual ACM Symposium on Principles of Programming Languages, 1984.Google Scholar
  18. 18.
    John C. Mitchell. Type inference with simple subtypes. Journal of Functional Programming, 1:245–285, 1991.Google Scholar
  19. 19.
    Jens Palsberg and Scott Smith. Constrained types and their expressiveness. TOPLAS, 18(5), September 1996.Google Scholar
  20. 20.
    FranÇois Pottier. Simplifying subtyping constraints. In First International Conference on Functional Programming, pages 122–133, 1996.Google Scholar
  21. 21.
    Geoffrey S. Smith. Principal type schemes for functional programs with overloading and subtyping. Science of Computer Programming, 23, 1994.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1996

Authors and Affiliations

  • Valery Trifonov
    • 1
  • Scott Smith
    • 1
  1. 1.Department of Computer ScienceJohns Hopkins UniversityBaltimoreUSA

Personalised recommendations