understanding type errors - was: Compiler error using IO

[Olaf Chitil]

Bjorn Lisper wrote:
> ...
> Is there any work being done on "intelligent" error messages for
> higher-order implicitly typed languages? One could perhaps come up with
> search strategies that tries to find a minimal number of program
> transformations ("edit distance") that yields a syntactically correct and
> well-typed program. For instance, in the case of type errors one could try
> to search for the minimal number of definitions that have to be removed to
> make the remaining program well-typed, and then report the removed
> definitions as likely sources of the errors. Has anyone done this?

Quite a number of people have published work on helping the programmer
to locate the source of type errors in Hindley-Milner typed languages. I
presented a paper about this subject at last ICFP. Mainly my paper is
about a way of viewing the types of arbitrary subexpressions of a
program. Note that you can only attach a type to an expression such as
"f x" if you know the types of "f" and "x". However, "f x" may appear in
the definition body of "f". You don't want cyclic explanations of
types...

I propose to have the user either browse freely through the typings of
arbitrary expressions, or use a method called algorithmic debugging to
locate the source of a type error. The algorithmic debugger asks the
user if certain typings for certain expressions are correct according to
his/her intentions. After some yes/no answers the debugger gives the
location of the error.

Other people have developed methods for more "intelligent" error
messages, although not exactly in the way you propose. Have a look at
the Related Work Section of my paper. You can get it from my web page
(URL below). I am a bit doubtful about  the practical usefulness of
"intelligent" error messages. It is easy to create examples where a
program can be made type correct by one of many rather different small
transformations, all of similar complexity. I believe such examples do
occur in practise and hence knowledge of the intended semantics is
necessary to locate errors. However, with all the many proposals for
better error location, there is definitely a lack of practical
evaluation. Basically for each proposed method there exists only a toy
implementation for a toy language, each method for a different language
(and most of these implementations don't even seem to be available). I
want to extend my prototype, replacing the type inference phase of
nhc98, but I haven't yet had the time...

Ciao,
Olaf


-- 
OLAF CHITIL, 
 Dept. of Computer Science, The University of York, York YO10 5DD, UK. 
 URL: http://www.cs.york.ac.uk/~olaf/
 Tel: +44 1904 434756; Fax: +44 1904 432767