A 3-Part Type Inference Engine

  • François Pottier
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1782)


Extending a subtyping-constraint-based type inference framework with conditional constraints and rows yields a powerful type inference engine. We illustrate this claim by proposing solutions to three delicate type inference problems: “accurate” pattern matchings, record concatenation, and “dynamic” messages. Until now, known solutions required significantly different techniques; our theoretical contribution is in using only a single (and simple) set of tools. On the practical side, this allows all three problems to benefit from a common set of constraint simplification techniques, leading to efficient solutions.


Type Scheme Reduction Rule Type Inference Type Constructor Type Algebra 
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.


  1. [1]
    Alexander S. Aiken and Edward L. Wimmers. Type inclusion constraints and type inference. In Functional Programming & Computer Architecture, pages 31–41. ACM Press, June 1993. URL:
  2. [2]
    Alexander S. Aiken, Edward L. Wimmers, and T. K. Lakshman. Soft typing with conditional types. In Principles of Programming Languages, pages 163–173, January 1994. URL:
  3. [3]
    Michele Bugliesi and Silvia Crafa. Object calculi for dynamic messages. In The Sixth International Workshop on Foundations of Object-Oriented Languages, FOOL 6, San Antonio, Texas, January 1999. URL:
  4. [4]
    Luca Cardelli and John Mitchell. Operations on records. Mathematical Structures in Computer Science, 1:3–48, 1991. Also in Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design, MIT Press, 1994. URL: Scholar
  5. [5]
    Manuel Fähndrich. Bane: A Library for Scalable Constraint-Based Program Analysis. PhD thesis, University of California at Berkeley, 1999. URL:
  6. [6]
    Cormac Flanagan and Matthias Felleisen. Componential set-based analysis. In Proceedings of the ACM SIGPLAN’ 97 Conference on Programming Language Design and Implementation, pages 235–248, Las Vegas, Nevada, June 1997. URL:
  7. [7]
    Robert Harper and Benjamin Pierce. A record calculus based on symmetric concatenation. In Conference Record of the 18th Annual ACM Symposium on Principles of Programming Languages (POPL’ 91), pages 131–142, Orlando, Florida, January 1991. ACM Press. URL:
  8. [8]
    Nevin Heintze. Set based analysis of ML programs. Technical Report CMU-CS-93-193, Carnegie Mellon University, School of Computer Science, July 1993. URL:
  9. [9]
    Martin Müller, Joachim Niehren, and Andreas Podelski. Ordering constraints over feature trees. Constraints, an International Journal, Special Issue on CP’97, Linz, Austria, 1999. URL:
  10. [10]
    Martin Müller and Susumu Nishimura. Type inference for first-class messages with feature constraints. In Jieh Hsiang and Atsushi Ohori, editors, Asian Computer Science Conference (ASIAN 98), volume 1538 of LNCS, pages 169–187, Manila, The Philippines, December 1998. Springer-Verlag. URL: Scholar
  11. [11]
    Susumu Nishimura. Static typing for dynamic messages. In Conference Record of POPL’ 98: The 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 266–278, San Diego, California, January 1998. URL:
  12. [12]
    Martin Odersky, Martin Sulzmann, and Martin Wehr. Type inference with constrained types. Theory and Practice of Object Systems, 5(1), 1999. URL:
  13. [13]
    Atsushi Ohori. A polymorphic record calculus and its compilation. ACM Transactions on Programming Languages and Systems, 17(6):844–895, November 1995.CrossRefGoogle Scholar
  14. [14]
    François Pottier. Wallace: an efficient implementation of type inference with subtyping. URL:
  15. [15]
    François Pottier. Simplifying subtyping constraints: a theory. Submitted for publication, December 1998. URL:
  16. [16]
    François Pottier. Type inference in the presence of subtyping: from theory to practice. Technical Report 3483, INRIA, September 1998. URL:
  17. [17]
    François Pottier. Subtyping-constraint-based type inference with conditional constraints: algorithms and proofs. Unpublished draft, July 1999. URL:
  18. [18]
    Didier Rémy. Projective ML. In 1992 ACM Conference on Lisp and Functional Programming, pages 66–75, New-York, 1992. ACM Press. URL:
  19. [19]
    Didier Rémy. Typing record concatenation for free. In Carl A. Gunter and John C. Mitchell, editors, Theoretical Aspects Of Object-Oriented Programming Types, Semantics and Language Design. MIT Press, 1993. URL:
  20. [20]
    Didier Rémy. A case study of typechecking with constrained types: Typing record concatenation. Presented at the workshop on Advances in Types for Computer Science at the Newton Institute, Cambridge, UK, August 1995. URL:
  21. [21]
    John C. Reynolds. Automatic computation of data set definitions. In A. J. H. Morrell, editor, Information Processing 68, volume 1, pages 456–461, Amsterdam, 1969. North-Holland.Google Scholar
  22. [22]
    Valery Trifonov and Scott Smith. Subtyping constrained types. In Proceedings of the Third International Static Analysis Symposium, volume 1145 of LNCS, pages 349–65. SV, September 1996. URL: Scholar
  23. [23]
    Mitchell Wand. Type inference for record concatenation and multiple inheritance. Information and Computation, pages 1–15, 1993. A preliminary version appeared in Proc. 4th IEEE Symposium on Logic in Computer Science (1989), pp. 92–97. URL:

Copyright information

© Springer-Verlag Berlin Heidelberg 2000

Authors and Affiliations

  • François Pottier
    • 1
  1. 1.INRIA RocquencourtLe Chesnay CedexFrance

Personalised recommendations