Complete and decidable type inference for GADTs

ABSTRACT

GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the principal-type property, which is necessary for modular type inference.

We present a novel and simplified type inference approach for local type assumptions from GADT pattern matches. Our approach is complete and decidable, while more liberal than previous such approaches.

REFERENCES

• 1: J. Cheney and R. Hinze. First-class phantom types. TR 1901, Cornell University, 2003.
• 2: A. Degtyarev and A. Voronkov. Simultaneous regid E-unification is undecidable. In Proc. of CSL'95, volume 1092 of LNCS, pages 178--190. Springer, 1995.
• 3: J. H. Gallier, P. Narendran, S. Raatz, and W. Snyder. Theorem proving using equational matings and rigid e-unification. J. ACM, 39(2):377--429, 1992.
• 4: J. R. Lewis, J. Launchbury, E. Meijer, and M. Shields. Implicit parameters: Dynamic scoping with static types. In POPL, pages 108--118, 2000.
• 5: M. Maher. Herbrand constraint abduction. In Proc. of LICS'05, pages 397--406. IEEE Comp. Soc., 2005.
• 6: F. Pottier and D. 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.
• 7: F. Pottier and Y. Régis-Gianas. Stratified type inference for generalized algebraic data types. In Proc. of POPL'06, pages 232--244. ACM, 2006.
• 8: S. Peyton Jones, D. Vytiniotis, S. Weirich, and M. Shields. Practical type inference for arbitrary-rank types. J. of Func. Prog., 17:1--82, January 2007.
• 9: S. Peyton Jones, D. Vytiniotis, S. Weirich, and G. Washburn. Simple unification-based type inference for GADTs. In Proc. of ICFP'06, pages 50--61. ACM, 2006.
• 10: M. Sulzmann, M. Chakravarty, S. Peyton Jones, and K. Donnelly. System F with type equality coercions. In Proc. of TLDI'07. ACM, 2007.
• 11: T. Schrijvers, S. Peyton Jones, M. Chakravarty, and M. Sulzmann. Type checking with open type functions. SIGPLAN Not., 43(9):51--62, 2008.
• 12: V. Simonet and F. Pottier. A constraint-based approach to guarded algebraic data types. ACM Trans. Prog. Languages Systems, 29(1), January 2007.
• 13: M. Sulzmann, T. Schrijvers, and P. J. Stuckey. Principal type inference for GHC-style multi-parameter type classes. In Proc. of APLAS'06, volume 4279 of LNCS, pages 26--43. Springer, 2006.
• 14: M. Sulzmann, T. Schrijvers, and P. Stuckey. Type inference for GADTs via Herbrand constraint abduction. Report CW 507, K.U.Leuven, Belgium, 2008.

INDEX TERMS

Primary Classification:
  D. Software
  D.3 PROGRAMMING LANGUAGES
      D.3.2 Language Classifications
          Subjects: Applicative (functional) languages

Additional Classification:
  F. Theory of Computation
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.3 Studies of Program Constructs
          Subjects: Type structure

General Terms:
Algorithms, Languages

Keywords:
GADTs, Haskell, type inference