GADTs have proven to be an invaluable language extension, but 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.
[Although it tackles exactly the same topic, we believe that this paper represents a significant step forward compared to the ICFP 2006 attempt (below).]
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.
[This paper is a much simplified and completely-rewritten version of our earlier paper "Wobbly types" paper below. Relative to the version published at ICFP 2006, the PDF above also includes an Appendix that describes a significant simplification to the type system, at the cost of extra annotation burden. This simpler system is the one actually implemented in GHC 6.8 and subsequently.]
Generalised algebraic data types (GADTs), sometimes known as "guarded recursive data types" or "first-class phantom types", are a simple but powerful generalisation 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.
It is time to pluck the fruit. Can GADTs be added to Haskell, without losing type inference, or requiring unacceptably heavy type annotations? Can this be done without completely rewriting the already-complex Haskell type-inference engine, and without complex interactions with (say) type classes? We answer these questions in the affirmative, giving a type system that explains just what type annotations are required, and a prototype implementation that implements it. 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.
[This paper was rejected by POPL'05. After thinking about it a lot more we greatly simplified the type system, and wrote "Simple unification-based type inference for GADTs" above. However, the original version has been cited quite a bit, so we made it into a Penn technical report, available from this page.]