Improving Error Messages for Dependent Types

Joseph Eremondi, J. Hage, Wouter Swierstra

Research output: Contribution to conferencePaperpeer-review


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.
Original languageEnglish
Publication statusPublished - 2018
EventInternational Conference on Functional Programming 2018 - St. Louis, United States
Duration: 23 Sept 201829 Sept 2018


ConferenceInternational Conference on Functional Programming 2018
Abbreviated titleICFP 2018
Country/TerritoryUnited States
CitySt. Louis


Dive into the research topics of 'Improving Error Messages for Dependent Types'. Together they form a unique fingerprint.

Cite this