Write a Blog >>
ICFP 2018
Sun 23 - Sat 29 September 2018 St. Louis, Missouri, United States
Thu 27 Sep 2018 15:50 - 16:10 at New York Central - Error Messages & Contexts Chair(s): David Darais

Dependently typed languages allow programmers to establish the correctness of their code, accessing the full power of higher-order logic via the Curry-Howard correspondence. However, a major barrier to their widespread adoption is their complexity. Since they impose a rigid type discipline, a significant portion of development time is spent reading, understanding, and responding to compiler error messages.

For Hindley-Milner style functional languages, such as Haskell or ML, several techniques have been developed to improve the quality of error messages. Our work adapts these techniques to dependently typed languages. We present replay graphs, which provide a representation of a unification algorithm run as a graph, allowing for the use of heuristics to generate error messages and repair hints, and counter-factual unification, which makes unification resistant to bias, so that when conflicting assumptions are encountered, the first one is not necessarily assumed to be correct.

Improving Error Messages for Dependent Types (error-messages.pdf)468KiB

Thu 27 Sep

15:30 - 16:10: TyDe 2018 - Error Messages & Contexts at New York Central
Chair(s): David DaraisUniversity of Vermont
tyde-2018153805500000015:30 - 15:50
Robert AtkeyUniversity of Strathclyde, James WoodUniversity of Strathclyde
File Attached
tyde-2018153805620000015:50 - 16:10
Joseph EremondiUniversity of British Columbia, Wouter SwierstraUtrecht University, Netherlands, Jurriaan HageUtrecht University
File Attached