[ACM Press the 14th ACM SIGPLAN international conference - Edinburgh, Scotland (2009.08.31-2009.09.02)] Proceedings of the 14th ACM SIGPLAN international conference on Functional programming - ICFP '09 - Complete and decidable type inference for GADTs

✍ Scribed by Schrijvers, Tom; Peyton Jones, Simon; Sulzmann, Martin; Vytiniotis, Dimitrios

• Book ID: 121213426
• Publisher: ACM Press
• Year: 2009
• Weight: 478 KB
• Category: Article
• ISBN: 1605583324
• DOI: 10.1145/1596550.1596599

✦ Synopsis

GADTs have proven to be an invaluable language extension, for ensuring data invariants and program correctness among others. Unfortunately, they pose a tough problem for type inference: we lose the principal-type property, which is necessary for modular type inference.

We present a novel and simplified type inference approach for local type assumptions from GADT pattern matches. Our approach is complete and decidable, while more liberal than previous such approaches.