The DOI matches its Crossref record.
Simple unification-based type inference for GADTs
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. 1.
Overview
Integrity signals
Registry
Cites
Statistics
Verification
Claims the paper makes
Claims other papers make about this one
Each is checked against this paper’s own text: does it say what the citing paper says it does?
In the citing paper
“As seen in Section 2, Granule supports algebraic and generalised algebraic data types (providing indexed types) in the style of Haskell [Peyton Jones et al. 2006].”
From Quantitative program reasoning with graded modal types (2019) · cites this paper as Peyton Jones et al. 2006
Citations
Cites
No references could be resolved yet.
Research works printed but not linked: 24
- 10.1145/289423.289451 · DOI
- 10.1145/581478.581494 · DOI
- Luca Cardelli . Basic polymorphic typechecking. Polymorphism, 2(1) , January 1985 . Luca Cardelli. Basic polymorphic typechecking. Polymorphism, 2(1), January 1985.
- James Cheney and Ralf Hinze . First-class phantom types. CUCIS TR2003-1901 , Cornell University , 2003 . James Cheney and Ralf Hinze. First-class phantom types. CUCIS TR2003-1901, Cornell University, 2003.
- Thierry Coquand . Pattern matching with dependent types . In Proceedings of the Workshop on Types for Proofs and Program , pages 66 -- 79 , Baastad, Sweden , June 1992 . Thierry Coquand. Pattern matching with dependent types. In Proceedings of the Workshop on Types for Proofs and Program, pages 66--79, Baastad, Sweden, June 1992.
- 10.5555/120477.120487 · DOI
- Ralf Hinze . Fun with phantom types . In Jeremey Gibbons and Oege de Moor, editors, The fun of programming , pages 245 -- 262 . Palgrave , 2003 . Ralf Hinze. Fun with phantom types. In Jeremey Gibbons and Oege de Moor, editors, The fun of programming, pages 245--262. Palgrave, 2003. · DOI · Paper page
- 10.1145/1034774.1034775 · DOI
- Lena Magnusson . The implementation of ALF - a proof editor based on Martin-Löf's monomorhic type theory with explicit substitution. PhD thesis, Chalmers University , 1994 . Lena Magnusson. The implementation of ALF - a proof editor based on Martin-Löf's monomorhic type theory with explicit substitution. PhD thesis, Chalmers University, 1994.
- 10.1017/S0956796803004829 · DOI · Paper page
- Erik Meijer and Koen Claessen . The design and implementation of Mondrian. In John Launchbury, editor , Haskell workshop , Amsterdam, Netherlands , 1997 . Erik Meijer and Koen Claessen. The design and implementation of Mondrian. In John Launchbury, editor, Haskell workshop, Amsterdam, Netherlands, 1997.
- Simon Peyton Jones . The Implementation of Functional Programming Languages . Prentice Hall , 1987 . Simon Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall, 1987.
- Simon Peyton Jones , Geoffrey Washburn , and Stephanie Weirich . Wobbly types: type inference for generalised algebraic data types . Microsoft Research , 2004 . Simon Peyton Jones, Geoffrey Washburn, and Stephanie Weirich. Wobbly types: type inference for generalised algebraic data types. Microsoft Research, 2004.
- 10.1145/1111037.1111058 · DOI
- 10.1145/1028664.1028711 · DOI
- 10.1145/1088348.1088356 · DOI
- Tim Sheard and Emir Pasalic . Meta-programming with built-in type equality . In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languaegs (LFM'04) , Cork , July 2004 . Tim Sheard and Emir Pasalic. Meta-programming with built-in type equality. In Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-languaegs (LFM'04), Cork, July 2004.
- Peter Stuckey and Martin Sulzmann . Type inference for guarded recursive data types. Technical report , National University of Singapore , 2005 . Peter Stuckey and Martin Sulzmann. Type inference for guarded recursive data types. Technical report, National University of Singapore, 2005.
- Martin Sulzmann , JeremyWazny, and Peter Stuckey . A framework for extended algebraic data types. Technical report , National University of Singapore , 2005 . Martin Sulzmann, JeremyWazny, and Peter Stuckey. A framework for extended algebraic data types. Technical report, National University of Singapore, 2005.
- 10.1145/1159803.1159838 · DOI
- 10.1007/978-3-540-24849-1_25 · DOI
- 10.1145/604131.604150 · DOI
- 10.1145/292540.292560 · DOI
- 10.1016/S0304-3975(97)00062-5 · DOI
Cited by
Sorted by citations
Quantitative program reasoning with graded modal types
Orchard, D., Liepelt, V.-B., & Eades III, H. (2019) · Proceedings of the ACM on Programming Languages · doi:10.1145/3341714 · Cited by 85
Metadata
- Authors
- Peyton Jones, S., Vytiniotis, D., Weirich, S., & Washburn, G.
- Affiliations
- Microsoft Research, Cambridge
- University of Pennsylvania (US)
- Venue
- Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming
- Publisher
- ACM
- Published
- 2006-09-16
- Pages
- 50-61
- OpenAlex
- W2140647971
- Cited by
- 335
- References
- 0
- Citations by year
- 2026: 2 · 2025: 2 · 2024: 3 · 2023: 1 · 2022: 6 · 2021: 9 · 2020: 8 · 2019: 15 · 2018: 11 · 2017: 17 · 2016: 7 · 2015: 19 · 2014: 21 · 2013: 15 · 2012: 23
- FWCI
- 26.57
- Type
- conference paper
- Language
- en
- Open access
- closed
- Locations
- ACM SIGPLAN International Conference on Functional Programming (ICFP) (publishedVersion)
- Topics
- Physical Sciences › Computer Science › Software › Logic, programming, and type systems
- Physical Sciences › Computer Science › Information Systems › Advanced Database Systems and Queries
- Social Sciences › Arts and Humanities › Language and Linguistics › Syntax, Semantics, Linguistic Variation
- Keywords
- generalized algebraic data types, type inference, unification, type annotations
About these checks
Registry, retraction, Cites and statistics results are computed, not judged, with one exception: a printed reference that no index lists is read once by a model before it counts as a citation error. Claims are extracted by a model and kept only when their quote appears verbatim in the text; each cited source is then checked, with a model’s help, for whether it says what the claim relies on. Those verdicts can be wrong — read the claim’s quote and the cited source before relying on one.
Statistics and arithmetic are recomputed, not judged.
Confidence bands are shown only for fields calibrated on our annotated test set. None is calibrated yet, so no band is shown.
What counts as a claim ›How we measure confidence ›How we check this ›
Are you an author, or do you see a problem with this page? Request a review
