Principal Type Inference for GADTs
We present a new method for GADT type inference that improves the precision of previous approaches. In particular, our approach accepts more type-correct programs than previous approaches when they do not employ type annotations. A side benefit of our approach is that can detect a wide range of runtime errors that are missed by previous approaches.
Our method is based on the idea to represent type refinements in pattern-matching branches by choice types, which facilitate a separation of the typing and reconciliation phases and thus support for case expressions. This idea is formalized in a type system, which is both sound and a conservative extension of the classical Hindley-Milner system. We present the results of an empirical evaluation that compares our algorithm with previous approaches.
Thu 21 JanDisplayed time zone: Guadalajara, Mexico City, Monterrey change
14:20 - 16:00
Track 2: Types, Generally or GraduallyResearch Papers at Grand Bay South
Chair(s): Tiark Rompf Purdue & Oracle Labs
|Principal Type Inference for GADTs|
Sheng Chen University of louisiana at Lafayette, Martin Erwig Oregon State UniversityMedia Attached
|Abstracting Gradual Typing|
Ronald Garcia University of British Columbia, Alison M. Clark , Éric Tanter University of Chile, ChileLink to publication Media Attached
|The Gradualizer: a methodology and algorithm for generating gradual type systems|
Matteo Cimini Indiana University, Jeremy G. Siek Indiana UniversityMedia Attached
|Is Sound Gradual Typing Dead?|
Asumu Takikawa Northeastern University, Daniel Feltey Northeastern University, Ben Greenman Northeastern University, Max New , Jan Vitek Northeastern University, Matthias Felleisen Northeastern UniversityPre-print Media Attached File Attached