Practical type inference for Generalised
Algebraic Data Types
Abstract:
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
(e.g. Xi, Hinze, Sheard), although type inference is known to be
difficult.
It is time to pluck the fruit. Can GADTs be added to languages
like ML and Haskell, without losing type inference, or requiring
unacceptably heavy type annotations? Can this be done without
completely rewriting the already-complex 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. 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. GADTs are implemented in GHC using this technique.
Practical type inference for Generalised Algebraic Data Types is joint
work with Stephanie Weirich and Geoff Washburn of the University of
Pennsylvania.