Type checking with open type functions

ABSTRACT

We report on an extension of Haskell with open type-level functions and equality constraints that unifies earlier work on GADTs, functional dependencies, and associated types. The contribution of the paper is that we identify and characterise the key technical challenge of entailment checking; and we give a novel, decidable, sound, and complete algorithm to solve it, together with some practically-important variants. Our system is implemented in GHC, and is already in active use.

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: Leo Bachmair , Ashish Tiwari, Abstract Congruence Closure and Specializations, Proceedings of the 17th International Conference on Automated Deduction, p.64-78, June 17-20, 2000
• 3: Bernhard Beckert, A Completion-Based Method for Mixed Universal and Rigid E-Unification, Proceedings of the 12th International Conference on Automated Deduction, p.678-692, June 26-July 01, 1994
• 4: Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones, Associated type synonyms, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 5: Chiyan Chen , Hongwei Xi, Combining programming with theorem proving, Proceedings of the tenth ACM SIGPLAN international conference on Functional programming, September 26-28, 2005, Tallinn, Estonia
• 6: David A. Plaisted , Andrea Sattler-Klein, Proof lengths for equational completion, Information and Computation, v.125 n.2, p.154-170, March 15, 1996 [doi>10.1006/inco.1996.0028]
• 7: Iavor S. Diatchki. High-level abstractions for low-level programming. PhD thesis, OGI School of Science & Engineering, May 2007.
• 8: Thom Frühwirth. Theory and practice of Constraint Handling Rules. Journal of Logic Programming, 37(1-3):95--138, 1998.
• 9: Matthias Neubauer , Peter Thiemann , Martin Gasbichler , Michael Sperber, Functional logic overloading, Proceedings of the 29th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.233-244, January 16-18, 2002, Portland, Oregon
• 10: Louis-Julien Guillemette and Stefan Monnier. One vote for type families in Haskell! In Draft Proc. of TFP'08, pages 53--65, 2008.
• 11: Patricia Johann , Neil Ghani, Foundations for structured programming with GADTs, Proceedings of the 35th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages, January 07-12, 2008, San Francisco, California, USA
• 12: Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
• 13: Deepak Kapur, Shostak's Congruence Closure as Completion, Proceedings of the 8th International Conference on Rewriting Techniques and Applications, p.23-37, June 02-05, 1997
• 14: Sheng Liang , Paul Hudak , Mark Jones, Monad transformers and modular interpreters, Proceedings of the 22nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.333-343, January 23-25, 1995, San Francisco, California, United States [doi>10.1145/199448.199528]
• 15: Daniel R. Licata and Robert Harper. A formulation of Dependent ML with explicit equality proofs. Technical Report CMU-CS-05-178, Carnegie Mellon University Department of Computer Science, 2005.
• 16: Conor McBride. Epigram: A dependently typed functional programming language. http://www.dur.ac.uk/CARG/epigram/.
• 17: Matthias Neubauer, Peter Thiemann, Martin Gasbichler, and Michael Sperber. A functional notation for functional dependencies. In Proceedings of the 2001 Haskell Workshop, 2001.
• 18: Robert Nieuwenhuis and Albert Oliveras. Proof-producing congruence closure. In Proc. of RTA'05, volume 3467 of LNCS, pages 453--468. Springer-Verlag, 2005.
• 19: Pyotr S. Novikov. On the algorithmic unsolvability of the word problem in group theory. In the Steklov Institute of Mathematics 44, pages 1--143, 1955. (Russian).
• 20: 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
• 21: Tom Schrijvers and Martin Sulzmann. Restoring confluence of functional dependencies via type families. In Draft Proc. of TFP'08, pages 22--36, 2008.
• 22: Tom Schrijvers, Martin Sulzmann, Simon Peyton Jones, and Manuel Chakravarty. Towards open type functions for Haskell. In O. Chitil, editor, Proceedings of the 19th International Symposium on Implemantation and Application of Functional Languages, pages 233--251, 2007.
• 23: 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]
• 24: Tim Sheard. Type-level computation using narrowing in Omega. In Proceedings of the Programming Languages meets Program Verification (PLPV 2006), volume 174 of Electronic Notes in Computer Science, pages 105--128, 2006.
• 25: Vincent Simonet , François Pottier, A constraint-based approach to guarded algebraic data types, ACM Transactions on Programming Languages and Systems (TOPLAS), v.29 n.1, p.1-es, January 2007 [doi>10.1145/1180475.1180476]
• 26: Peter J. Stuckey , Martin Sulzmann, A theory of overloading, ACM Transactions on Programming Languages and Systems (TOPLAS), v.27 n.6, p.1216-1269, November 2005 [doi>10.1145/1108970.1108974]
• 27: Martin Sulzmann, Jeremy Wazny, and Peter J.Stuckey. A framework for extended algebraic data types. In Proc. of FLOPS'06, volume 3945 of LNCS, pages 47--64. Springer-Verlag, 2006.
• 28: Martin Sulzmann , Manuel M. T. Chakravarty , Simon Peyton Jones , Kevin Donnelly, System F with type equality coercions, Proceedings of the 2007 ACM SIGPLAN international workshop on Types in languages design and implementation, January 16-16, 2007, Nice, Nice, France [doi>10.1145/1190315.1190324]
• 29: Martin Sulzmann , Gregory J. Duck , Simon Peyton-Jones , Peter J. Stuckey, Understanding functional dependencies via constraint handling rules, Journal of Functional Programming, v.17 n.1, p.83-129, January 2007 [doi>10.1017/S0956796806006137]
• 30: Martin Sulzmann, Tom Schrijvers, and Peter Stuckey. Type inference for GADTs via Herbrand constraint abduction. Report CW 507, Department of Computer Science, K.U.Leuven, Leuven, Belgium, January 2008.
• 31: Ashish Tiwari , Leo Bachmair , Harald Rueß, Rigid E-Unification Revisited, Proceedings of the 17th International Conference on Automated Deduction, p.220-234, June 17-20, 2000
• 32: 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

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:
Haskell, type checking, type families, type functions