CoChat
Sign Up
Cited by 335Logic, programming, and type systemsAdvanced Database Systems and QueriesSyntax, Semantics, Linguistic Variation

The DOI matches its Crossref record.

Simple unification-based type inference for GADTs

Peyton Jones, Simon, Vytiniotis, Dimitrios, Weirich, Stephanie, Washburn, Geoffrey·2006·Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming
DOI 10.1145/1159803.1159811
Open this paper in CoChat — free account

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

Crossref · 10.1145/1159803.1159811

Cites

Statistics

Recomputing p-values needs the paper’s full text.

Verification

Claims the paper makes

This paper’s full text isn’t openly available, so its claims and self-check weren’t run. The registry and citation checks still apply.

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?

Citations

Cites

No references could be resolved yet.

Research works printed but not linked: 24

  1. 10.1145/289423.289451 · DOI
  2. 10.1145/581478.581494 · DOI
  3. Luca Cardelli . Basic polymorphic typechecking. Polymorphism, 2(1) , January 1985 . Luca Cardelli. Basic polymorphic typechecking. Polymorphism, 2(1), January 1985.
  4. 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.
  5. 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.
  6. 10.5555/120477.120487 · DOI
  7. 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
  8. 10.1145/1034774.1034775 · DOI
  9. 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. 10.1017/S0956796803004829 · DOI · Paper page
  11. 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.
  12. Simon Peyton Jones . The Implementation of Functional Programming Languages . Prentice Hall , 1987 . Simon Peyton Jones. The Implementation of Functional Programming Languages. Prentice Hall, 1987.
  13. 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.
  14. 10.1145/1111037.1111058 · DOI
  15. 10.1145/1028664.1028711 · DOI
  16. 10.1145/1088348.1088356 · DOI
  17. 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.
  18. 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.
  19. 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.
  20. 10.1145/1159803.1159838 · DOI
  21. 10.1007/978-3-540-24849-1_25 · DOI
  22. 10.1145/604131.604150 · DOI
  23. 10.1145/292540.292560 · DOI
  24. 10.1016/S0304-3975(97)00062-5 · DOI

Cited by

Sorted by citations

See all 335

Metadata

Authors
Peyton Jones, S., Vytiniotis, D., Weirich, S., & Washburn, G.
Affiliations
  • Microsoft Research, Cambridge
  • University of Pennsylvania (US)
ORCID
Venue
Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming
Publisher
ACM
Published
2006-09-16
Pages
50-61
DOI
10.1145/1159803.1159811
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

How to cite

Cite CoChat for the checks on this page, and the paper for its own findings.

This page
CoChat. (2026). Citation check: Simple unification-based type inference for GADTs. https://app.cochat.ai/papers/10.1145/1159803.1159811
The paper
Peyton Jones, S., Vytiniotis, D., Weirich, S., & Washburn, G. (2006). Simple unification-based type inference for GADTs. Proceedings of the eleventh ACM SIGPLAN international conference on Functional programming. https://doi.org/10.1145/1159803.1159811