GADT's revisited

Simon Peyton Jones has a new paper about type inferencing and GADT's: Simple unification-based type inference for GADTs

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 his earlier paper Wobbly types: type inference for generalised algebraic data types

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Typo in section 5.1?

I would have expected the "Just Eq -> Eq" case to have read "Just Eq -> Just Eq", or did I miss something?

New and improved

The paper mentioned in this thread has been updated as of April 2006.
Simple unification-based type inference for GADTs