Boxy types: inference for higher-rank types and impredicativity

ABSTRACT

Languages with rich type systems are beginning to employ a blend of type inference and type checking, so that the type inference engine is guided by programmer-supplied type annotations. In this paper we show, for the first time, how to combine the virtues of two well-established ideas: unification-based inference, and bidi-rectional propagation of type annotations. The result is a type system that conservatively extends Hindley-Milner, and yet supports both higher-rank types and impredicativity.

REFERENCES

• 1: Shail Aditya , Rishiyur S. Nikhil, Incremental Polymorphism, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.379-405, August 26-30, 1991
• 2: Luis Damas , Robin Milner, Principal type-schemes for functional programs, Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.207-212, January 25-27, 1982, Albuquerque, Mexico [doi>10.1145/582153.582176]
• 3: Jacques Garrigue , Didier Rémy, Semi-explicit first-class polymorphism for ML, Information and Computation, v.155 n.1-2, p.134-169, Nov./Dec. 1999 [doi>10.1006/inco.1999.2830]
• 4: Haruo Hosoya and Benjamin C. Pierce. How good is local type inference? Technical Report MS-CIS-99-17, University of Pennsylvania, June 1999.
• 5: ACM SIGPLAN International Conference on Functional Programming (ICFP'05), Tallinn, Estonia, September 2005. ACM.
• 6: Mark P. Jones, First-class polymorphism with type inference, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.483-496, January 15-17, 1997, Paris, France [doi>10.1145/263699.263765]
• 7: A. J. Kfoury , J. B. Wells, A direct algorithm for type inference in the rank-2 fragment of the second-order &lgr;-calculus, Proceedings of the 1994 ACM conference on LISP and functional programming, p.196-207, June 27-29, 1994, Orlando, Florida, United States
• 8: Ralf Lämmel , Simon Peyton Jones, Scrap your boilerplate: a practical design pattern for generic programming, Proceedings of the 2003 ACM SIGPLAN international workshop on Types in languages design and implementation, January 18-18, 2003, New Orleans, Louisiana, USA
• 9: Didier Le Botlan , Didier Rémy, ML^F: raising ML to the power of system F, Proceedings of the eighth ACM SIGPLAN international conference on Functional programming, p.27-38, August 25-29, 2003, Uppsala, Sweden
• 10: Oukseh Lee , Kwangkeun Yi, Proofs about a folklore let-polymorphic type inference algorithm, ACM Transactions on Programming Languages and Systems (TOPLAS), v.20 n.4, p.707-723, July 1998 [doi>10.1145/291891.291892]
• 11: Daan Leijen , Andres Löh, Qualified types for MLF, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 12: Xavier Leroy , Michel Mauny, Dynamics in ML, Proceedings of the 5th ACM Conference on Functional Programming Languages and Computer Architecture, p.406-426, August 26-30, 1991
• 13: R Milner. A theory of type polymorphism in programming. JCSS, 13(3), December 1978.
• 14: John C. Mitchell, Coercion and type inference, Proceedings of the 11th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.175-185, January 15-18, 1984, Salt Lake City, Utah, United States [doi>10.1145/800017.800529]
• 15: Martin Odersky , Konstantin Läufer, Putting type annotations to work, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.54-67, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237729]
• 16: Martin Odersky , Christoph Zenger , Matthias Zenger, Colored local type inference, Proceedings of the 28th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.41-53, January 2001, London, United Kingdom
• 17: N Perry. The implementation of practical functional programming languages. Ph. D. thesis, Imperial College, London, 1991.
• 18: Simon Peyton Jones , Dimitrios Vytiniotis , Stephanie Weirich , Geoffrey Washburn, Simple unification-based type inference for GADTs, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 19: Benjamin C. Pierce , David N. Turner, Local type inference, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.252-265, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268967]
• 20: François Pottier and Didier Rémy. The essence of ML type inference. In Benjamin C. Pierce, editor, Advanced Topics in Types and Programming Languages, chapter 10, pages 389--489. MIT Press, 2005.
• 21: Didier Rémy. Simple, partial type inference for System F, based on type containment. In ICFP05 {5}, pages 130--143.
• 22: Chung-chieh Shan, Sexy types in action, ACM SIGPLAN Notices, v.39 n.5, May 2004 [doi>10.1145/997140.997142]
• 23: Mark Shields and Simon Peyton Jones. Lexically scoped type variables. Microsoft Research, 2002.
• 24: D. Tarditi , G. Morrisett , P. Cheng , C. Stone , R. Harper , P. Lee, TIL: a type-directed optimizing compiler for ML, Proceedings of the ACM SIGPLAN 1996 conference on Programming language design and implementation, p.181-192, May 21-24, 1996, Philadelphia, Pennsylvania, United States
• 25: Jerzy Tiuryn , Pawel Urzyczyn, The Subtyping Problem for Second-Order Types is Undecidable, Proceedings of the 11th Annual IEEE Symposium on Logic in Computer Science, p.74, July 27-30, 1996
• 26: Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy type inference for higher-rank types and impredicativity, Technical Appendix. Technical Report MS-CIS-05-23, University of Pennsylvania, April 2006.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Abstract data types

Additional Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.3 Language Constructs and Features
          Subjects: Polymorphism

General Terms:
Languages, Theory

Keywords:
higher-rank types, impredicativity, type inference