### Wobbly types: type inference for generalised algebraic data types

Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich.

July 2004

Postscript
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.

**Edit:** Made the title into a hyperlink, as the "Postscript" link could easily get lost in a sea of blue text...

**Edit 2:**Quoted the article with a plain-ol' <blockquote> instead. Better?

## Recent comments

11 min 12 sec ago

2 hours 18 min ago

6 hours 30 min ago

19 hours 3 min ago

19 hours 5 min ago

19 hours 34 min ago

1 day 2 hours ago

1 day 2 hours ago

1 day 3 hours ago

1 day 14 hours ago