Simple unification-based type inference for GADTs
- 16 September 2006
- journal article
- Published by Association for Computing Machinery (ACM) in ACM SIGPLAN Notices
- Vol. 41 (9) , 50-61
- https://doi.org/10.1145/1160074.1159811
Abstract
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.Keywords
This publication has 13 references indexed in Scilit:
- Boxy typesPublished by Association for Computing Machinery (ACM) ,2006
- Stratified type inference for generalized algebraic data typesPublished by Association for Computing Machinery (ACM) ,2006
- Putting curry-howard to workPublished by Association for Computing Machinery (ACM) ,2005
- The pattern calculusACM Transactions on Programming Languages and Systems, 2004
- Languages of the futurePublished by Association for Computing Machinery (ACM) ,2004
- The view from the leftJournal of Functional Programming, 2004
- Applied Type SystemPublished by Springer Nature ,2004
- Typing dynamic typingPublished by Association for Computing Machinery (ACM) ,2002
- Cayenne—a language with dependent typesPublished by Association for Computing Machinery (ACM) ,1998
- Indexed typesTheoretical Computer Science, 1997