Simple, partial type-inference for System F based on type-containment

ABSTRACT

We explore partial type-inference for System F based on type-containment. We consider both cases of a purely functional semantics and a call-by-value stateful semantics. To enable type-inference, we require higher-rank polymorphism to be user-specified via type annotations on source terms. We allow implicit predicative type-containment and explicit impredicative type-instantiation. We obtain a core language that is both as expressive as System F and conservative over ML. Its type system has a simple logical specification and a partial type-reconstruction algorithm that are both very close to the ones for ML. We then propose a surface language where some annotations may be omitted and rebuilt by some algorithmically defined but logically incomplete elaboration mechanism.

REFERENCES

• 1: Kim B. Bruce , Luca Cardelli , Benjamin C. Pierce, Comparing object encodings, Information and Computation, v.155 n.1-2, p.108-133, Nov./Dec. 1999 [doi>10.1006/inco.1999.2829]
• 2: Jacques Garrigue. Relaxing the value restriction. In International Symposium on Functional and Logic Programming, volume 2998 of Lecture Notes in Computer Science, Nara, April 2004. Springer-Verlag.
• 3: Jacques Garrigue , Didier Rémy, Extending ML with Semi-Explicit Higher-Order Polymorphism, Proceedings of the Third International Symposium on Theoretical Aspects of Computer Software, p.20-46, September 23-26, 1997
• 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: Didier Le Botlan. MLF: Une extension de ML avec polymorphisme de second ordre et instanciation implicite. PhD thesis, University of Paris 7, June 2004. (english version).
• 6: 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
• 7: Daniel Leivant, Finitely stratified polymorphism, Information and Computation, v.93 n.1, p.93-113, July 1991 [doi>10.1016/0890-5401(91)90053-5]
• 8: Konstantin Läfer , Martin Odersky, Polymorphic type inference and abstract data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.16 n.5, p.1411-1430, Sept. 1994 [doi>10.1145/186025.186031]
• 9: John C. Mitchell, Polymorphic type inference and containment, Information and Computation, v.76 n.2-3, p.211-249, February/March 1988 [doi>10.1016/0890-5401(88)90009-0]
• 10: 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]
• 11: Martin Odersky , Christoph Zenger , Matthias Zenger, Colored local type inference, ACM SIGPLAN Notices, v.36 n.3, p.41-53, March 2001
• 12: Frank Pfenning, Partial polymorphic type inference and higher-order unification, Proceedings of the 1988 ACM conference on LISP and functional programming, p.153-163, July 25-27, 1988, Snowbird, Utah, United States [doi>10.1145/62678.62697]
• 13: François Pottier and Didier Rémy. The essence of ML type inference. Extended version of {PR05} (in preparation).
• 14: 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.
• 15: Simon Peyton Jones and Mark Shields. Lexically-scoped type variables. Submitted to ICFP 2004, March 2003.
• 16: Benjamin C. Pierce , David N. Turner, Local type inference, ACM Transactions on Programming Languages and Systems (TOPLAS), v.22 n.1, p.1-44, Jan. 2000 [doi>10.1145/345099.345100]
• 17: Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. Submitted to the Journal of Functional Programming, June 2005.
• 18: Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, and Mark Shields. Practical type inference for arbitrary-rank types. technical appendix. Private communication, June 2005.
• 19: Didier Rémy, Programming Objects with ML-ART, an Extension to ML with Abstract and Record Types, Proceedings of the International Conference on Theoretical Aspects of Computer Software, p.321-346, April 19-22, 1994
• 20: Didier Rémy. Simple, partial type-inference for System F based on type-containment. Full version, September 2005.
• 21: Jerzy Tiuryn , Pawel Urzyczyn, The subtyping problem for second-order types is undecidable, Information and Computation, v.179 n.1, p.1-18, November 25, 2002 [doi>10.1006/inco.2001.2950]
• 22: Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Boxy type inference for higher-rank types and impredicativity. Available electronically at http://www.cis.upenn.edu/~dimitriv/boxy/boxy.ps, April 2005.
• 23: Joe B. Wells. Typability and type checking in the second-order λ-calculus are equivalent and undecidable. In Proceedings of the Ninth Annual IEEE Symposium on Logic in Computer Science (LICS), pages 176--185, 1994.
• 24: Joe B. Wells. The undecidability of Mitchell's subtyping relation. Technical Report 95--019, Computer Science Department, Boston Univiversity, December 1995.
• 25: J. B. Wells, Typability is Undecidable for F+Eta, Boston University, Boston, MA, 1996
• 26: Andrew K. Wright, Simple imperative polymorphism, Lisp and Symbolic Computation, v.8 n.4, p.343-355, Dec. 1995 [doi>10.1007/BF01018828]

INDEX TERMS

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

General Terms:
Design, Languages, Reliability, Theory, Verification

Keywords:
System F, elaboration, polymorphism, type containment, type inference, type reconstruction