Simple unification-based type inference for GADTs

ABSTRACT

Generalized algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalization of the data types of Haskell and ML. Recent works have given compelling examples of the utility of GADTs, although type inference is known to be difficult. Our contribution is to show how to exploit programmer-supplied type annotations to make the type inference task almost embarrassingly easy. Our main technical innovation is wobbly types, which express in a declarative way the uncertainty caused by the incremental nature of typical type-inference algorithms.

REFERENCES

• 1: Lennart Augustsson, Cayenne—a language with dependent types, Proceedings of the third ACM SIGPLAN international conference on Functional programming, p.239-250, September 26-29, 1998, Baltimore, Maryland, United States
• 2: Lennart Augustsson and Kent Petersson. Silly type families. Available as http://www.cs.pdx.edu/~sheard/papers/silly. pdf, 1994.
• 3: Arthur I. Baars , S. Doaitse Swierstra, Typing dynamic typing, Proceedings of the seventh ACM SIGPLAN international conference on Functional programming, p.157-166, October 04-06, 2002, Pittsburgh, PA, USA
• 4: Luca Cardelli. Basic polymorphic typechecking. Polymorphism, 2(1), January 1985.
• 5: James Cheney and Ralf Hinze. First-class phantom types. CUCIS TR2003-1901, Cornell University, 2003.
• 6: Thierry Coquand. Pattern matching with dependent types. In Proceedings of the Workshop on Types for Proofs and Program, pages 66--79, Baastad, Sweden, June 1992.
• 7: Peter Dybjer, Inductive sets and families in Martin-Lo¨f's type theory and their set-theoretic semantics, Logical frameworks, Cambridge University Press, New York, NY, 1991
• 8: Ralf Hinze. Fun with phantom types. In Jeremey Gibbons and Oege de Moor, editors, The fun of programming, pages 245--262. Palgrave, 2003.
• 9: C. Barry Jay, The pattern calculus, ACM Transactions on Programming Languages and Systems (TOPLAS), v.26 n.6, p.911-937, November 2004 [doi>10.1145/1034774.1034775]
• 10: Lena Magnusson. The implementation of ALF - a proof editor based on Martin-Löf's monomorhic type theory with explicit substitution. PhD thesis, Chalmers University, 1994.
• 11: Conor McBride , James McKinna, The view from the left, Journal of Functional Programming, v.14 n.1, p.69-111, January 2004 [doi>10.1017/S0956796803004829]
• 12: Erik Meijer and Koen Claessen. The design and implementation of Mondrian. In John Launchbury, editor, Haskell workshop, Amsterdam, Netherlands, 1997.
• 13: Simon L. Peyton Jones, The Implementation of Functional Programming Languages (Prentice-Hall International Series in Computer Science), Prentice-Hall, Inc., Upper Saddle River, NJ, 1987
• 14: Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Microsoft Research, 2004.
• 15: François Pottier , Yann Régis-Gianas, Stratified type inference for generalized algebraic data types, Conference record of the 33rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.232-244, January 11-13, 2006, Charleston, South Carolina, USA
• 16: Tim Sheard, Languages of the future, Companion to the 19th annual ACM SIGPLAN conference on Object-oriented programming systems, languages, and applications, October 24-28, 2004, Vancouver, BC, CANADA [doi>10.1145/1028664.1028711]
• 17: Tim Sheard, Putting curry-howard to work, Proceedings of the 2005 ACM SIGPLAN workshop on Haskell, p.74-85, September 30-30, 2005, Tallinn, Estonia [doi>10.1145/1088348.1088356]
• 18: Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languaegs (LFM'04), Cork, July 2004.
• 19: Peter Stuckey and Martin Sulzmann. Type inference for guarded recursive data types. Technical report, National University of Singapore, 2005.
• 20: Martin Sulzmann. A Haskell programmer's guide to Chameleon. Available at http://www.comp.nus.edu.sg/sulzmann/chameleon/download/haskell. html, 2003.
• 21: Martin Sulzmann, JeremyWazny, and Peter Stuckey. A framework for extended algebraic data types. Technical report, National University of Singapore, 2005.
• 22: Dimitrios Vytiniotis , Stephanie Weirich , Simon Peyton Jones, Boxy types: inference for higher-rank types and impredicativity, Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming, September 16-21, 2006, Portland, Oregon, USA
• 23: Dimitrios Vytiniotis, Stephanie Weirich, and Simon Peyton Jones. Simple unification-based type inference for GADTs, Technical Appendix. Technical Report MS-CIS-05-22, University of Pennsylvania, April 2006.
• 24: Hongwei Xi. Applied type system. In Proceedings of TYPES 2003, volume 3085 of Lecture Notes in Computer Science, pages 394--408. Springer Verlag, 2004.
• 25: Hongwei Xi , Chiyan Chen , Gang Chen, Guarded recursive datatype constructors, Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.224-235, January 15-17, 2003, New Orleans, Louisiana, USA
• 26: Hongwei Xi , Frank Pfenning, Dependent types in practical programming, Proceedings of the 26th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.214-227, January 20-22, 1999, San Antonio, Texas, United States [doi>10.1145/292540.292560]
• 27: Christoph Zenger, Indexed types, Theoretical Computer Science, v.187 n.1-2, p.147-165, Nov. 15, 1997 [doi>10.1016/S0304-3975(97)00062-5]

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:
generalized algebraic data types, type inference