Correcting type errors in the curry system

Abstract

In this paper, we address the problem of suggesting corrections to terms that are ill-typed in the Curry System. For this, we convert the term into a set of constraints over type expressions, and use a method due to Cox [3] to compute the maximal consistent subset of this set. The main result of this paper is an interesting correspondence between the automaton constructed in Cox's method and a graphical representation of the term called sharing graphs, which allows us to read back a term from the maximal consistent subset. We also characterise ill-typed terms using paths in the sharing graph.