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 Jan
|14:20 - 14:45|
|14:45 - 15:10|
|Link to publication Media Attached|
|15:10 - 15:35|
|15:35 - 16:00|
|Pre-print Media Attached File Attached|