Re: ergonomie du compilateur

[Pierre Weis <Pierre.Weis@inria.fr>]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain; charset=US-ASCII, Size: 4298 bytes --]

Bonjour,

> En effet, souvent une erreur de typage intervient à une ligne
> donnée pas à cause d'un problème à cette ligne, mais à
> cause d'un problè= me à une ligne antérieure. S'il est souvent
> assez facile de retrouver où a é= té typé un terme, cela
> devient quelquefois difficile, notamment avec les fonction=
> récursives, pour le type de la fonction.  Ne pourrait-on pas faire
> que, sur demande, le compilateur, lorsqu'il rencontre une erreur de
> type, ressorte d'où il a inféré les types q= ui lui posent
> problème?

 Une erreur de typage peut apparai^tre arbitrairement loin de l'endroit
qui la produit. A` l'extre^me: on de'finit une fonction f avec un
certain type dans un module et on l'utilise avec un type incompatible
dans un autre module. En ge'ne'ral c'est l'utilisation qui est
errone'e et c'est l'erreur qui va e^tre signale'e. Cependant dans
certains cas c'est la de'finition de f qui est fausse et pas son utilisation. 

 On peut e'videmment modifier l'exemple en remplac,ant module par
de'finition de fonctions mutuellement re'cursives. Pour montrer la
difficulte' du proble`me on peut tout aussi bien faire que la
de'finition de la fonction est correcte mais que son premier emploi
re'cursif est errone': c'est cet emploi errone' qui fixera un type
faux pour la fonction, et le compilateur rapportera une erreur sur
la de'finition de la fonction, encore une fois arbitrairement loin de
l'application errone'e de la fonction. Pire encore, il peut signaler une
erreur pour autre application re'cursive de la fonction, alors que
cette application la` est correcte (mais incompatible avec la
premie`re qui elle est fausse et fixe un type faux a` la fonction).

 Pour clore le de'bat, des essais ont eu lieu sur ce sujet: le
compilateur sortait des pages et des pages de raisonnement
incompre'hensibles sur les infe'rences qu'il avait faites, et cela
n'avanc,ait a` rien. Une ide'e plus plausible serait sans doute
d'imprimer le programme avec les types infe're's jusqu'a` l'erreur,
mais il n'est pas certain que ce soit plus simple a` comprendre.

> A typing problem in a line of code often happens not because this line is
> buggy, but because some previous line is, from which the types of terms i=
> the current line have been inferred. Often it's not too difficult to trac=
> where those inferences took place, but it's sometimes tedious, especially
> with recursive functions.
> Couldn't the Ocaml compiler be made to have, on request, more verbose
> messages on typing errors, including the trace of inferences of the terms
> to cause problems?

 A typing error may appear as far as desired from the program point
that implied the error. For instance: if you define f in a module, and
use it with another (incompatible) type, then it is probably the case
that the usage of f is erroneous, and the compiler reports it as
so. However, it may be the case that the application of f is correct
whereas the definition of f is boguous.

 This example does not require modules: a recursive definition of
functions exhibits the same behaviour. In this case, the first usage of
a recursively defined identifier fixes its type: if this first usage
is erroreous it is not reported by the typechecker, since it takes
the type deduced by the first usage for granted. In contrast, the
typechecker will report an error about the (incompatible but in fact
correct) definition of the function; or even worse, it will report an
error for each correct usage of the function, and no error for the
wrong usage!

 To end with, let's say that some experiments have been done on the
subject: a type-checker reporting the way it has found the errors was
designed, but it did not appear to be a significant progress. In the
case of simple errors, this mechanism was evidently overkill; in the
case of complex errors the situation was worse: it printed a huge
amount of material reporting deductions and type unifications, that
were as cumbersome to analyse as the usual (erroneous, but at least
more concise) type error report.

A possible solution could be to output the user's program with type
annotations, as found before the error was discovered. I'm not sure it
will be simpler to understand.

Pierre Weis

INRIA, Projet Cristal, Pierre.Weis@inria.fr, http://pauillac.inria.fr/~weis