A framework for improving error messages in dependently-typed languages

Joseph Eremondi, Wouter Swierstra, Jurriaan Hage

Research output: Contribution to journalArticlepeer-review

2 Citations (Scopus)
12 Downloads (Pure)

Abstract

Dependently-typed programming languages provide a powerful tool for establishing code correctness. However, it can be hard for newcomers to learn how to employ the advanced type system of such languages effectively. For simply-typed languages, several techniques have been devised to generate helpful error messages and suggestions for the programmer. We adapt these techniques to dependently-typed languages, to facilitate their more widespread adoption. In particular, we modify a higher-order unification algorithm that is used to resolve and type-check implicit arguments. We augment this algorithm with replay graphs, allowing for a global heuristic analysis of a unification problem-set, error-tolerant typing, which allows type-checking to continue after errors are found, and counter-factual unification, which makes error messages less affected by the order in which types are checked. A formalization of our algorithm is presented with an outline of its correctness. We implement replay graphs, and compare the generated error messages to those from existing languages, highlighting the improvements we achieved.
Original languageEnglish
Pages (from-to)1-32
Number of pages32
JournalOpen Computer Science
Volume9
Issue number1
DOIs
Publication statusPublished - 24 Jan 2019

Keywords

  • higher-order unification
  • type error diagnosis
  • counter-factual typing
  • type-inference

Fingerprint

Dive into the research topics of 'A framework for improving error messages in dependently-typed languages'. Together they form a unique fingerprint.

Cite this