Sciweavers

Share
ICFP
2006
ACM

Simple unification-based type inference for GADTs

11 years 6 months ago
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. Categories and Subject Descriptors D.3.3 [PROGRAMMING S]: Language Constructs and Features--abstract data types, polymorphism General Terms Languages, Theory Keywords generalized algebraic data types, type inference
Simon L. Peyton Jones, Dimitrios Vytiniotis, Steph
Added 13 Dec 2009
Updated 13 Dec 2009
Type Conference
Year 2006
Where ICFP
Authors Simon L. Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Geoffrey Washburn
Comments (0)
books