Re: ergonomie du compilateur

Re: ergonomie du compilateur

[Quercia]

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

> 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 qui lui
> posent problème?

Bonne idee ! En attendant, dans ce genre de situation, je place en
commentaire (ou je rajoute un failwith "") tous les cas sauf un pour
examiner le type de chaque cas.
Primaire mais efficace ...

> 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?

Good idea ! Meanwhile I comment out (or add a failwith "") every case
but one to see the type of the remaining case. Crude but effective ...

-- 
Michel Quercia
Lycee Carnot  16 bd Thiers  21000 Dijon
e-mail = querciam@l-carnot1.ac-dijon.fr
cc = 101702.425@compuserve.com (LG. Vidiani)

Re: ergonomie du compilateur

[Pierre Weis]

[-- 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

Re: ergonomie du compilateur

[Emmanuel Engel]

Quercia wrote:

> Bonne idee ! En attendant, dans ce genre de situation, je place en
> commentaire (ou je rajoute un failwith "") tous les cas sauf un pour
> examiner le type de chaque cas.
> Primaire mais efficace ...
> 


Cela me semble bien complique. Je suppose que vous avez une idee
du type attendu. Il suffit alors d'indiquer au compilateur le type
attendu et, il va vous montrer ou il infere le mauvais type. Le seul
repproche que l'on puisse faire a cette technique est que la syntaxe
du langage oblige parfois a faire quelques amenagements.

Exemple:

sun12:~/tmp> ocaml
        Objective Caml version 1.03

# let rec f x =       
    if x = 0 then f true else f (x-1);;  
                                 ^^^^        
This expression has type int but is here used with type bool
# let rec (f:int->int) x =
    if x =0 then f true else f (x-1);;
Syntax error
#  let rec (f:int->int) = fun x->
      if x =0 then f true else f (x-1);;
                     ^^^^
This expression has type bool but is here used with type int
# 



-- 

- Emmanuel Engel

Re: ergonomie du compilateur

[David Gurr]

I think that the biggest difficulty people have with types in ML is
conceptual.  Neither Lisp/Scheme nor C/C++/Pascal programmers are
likely to understand types and their role in ML.  Maybe the following
pedantic exposition would make things clearer.  A ML system has two
separate things that effectively execute code;ie two "interpreters". The
first is the value interpreter and is more or less the same as a Scheme
interpreter, the second is the type interpreter and can be thought of
as a very specialized Prolog interpreter.  When you enter a line of
code on a ML interpreter, it is executed by *both* interpreters.  The
type interpreter does a unification driven search for the type of the
code.  And the value interpreter does a reduction driven simplification
for the value of the code.  The single bit of subtilety is that the
value interpreter actually interpretes the code after it has been
rewritten with explicit types (using the type determined by the type
interpreter).

This points out three areas of conceptual difficulty.  Because type
inference is done at compile time, and because it resembles "type
checking" a la C etc, people often think of type checking as being part
of parsing rather than as part of the execution of the program.
Because types are trivial in the common languages, people do not
recognize that types are as integral to the meta-level execution of ML
(which takes place during compilation) as values are to the
iso/base-level execution of ML (which takes place during runtime).
Because logic programming is not common, people are befuddled by ML
type inference.

So what could the compiler do to help?  I suppose that it would be
possible for the toplevel to throw you into a prolog like interpreter
when it hits a type error.  You could enter type variables and it would
reply with the type that is the value of the type variable, etc.  There
would be a predefined predicate |- for type judgements.  This would make
the metalevel type inference as accessable and perhaps as understandable
as the baselevel values.

-D

My apologies for no French version, you would rather not find out how
bad my French is.

Re: ergonomie du compilateur

[Frank Christoph]

> So what could the compiler do to help?  I suppose that it would be possible
> for the toplevel to throw you into a prolog like interpreter when it hits a
> type error.  You could enter type variables and it would reply with the type
> that is the value of the type variable, etc.  There would be a predefined
> predicate |- for type judgements.  This would make the metalevel type
> inference as accessable and perhaps as understandable as the baselevel
> values.

  This is an interesting idea and I have some sympathy for it.  But I suspect
it might confuse some beginners even more, especially those who have never
used Prolog, since

  * the type unification has nothing to do with the execution model
  * it requires learning a new syntax for routine debugging .

But I could be wrong.  You have to learn a new command syntax to use existent
command-line debuggers anyway...

  I once suggested a related feature to Alastair Reid, but for Haskell program
editors.  I thought it would be useful if the user could click on an
identifier and have the type displayed.  This can be more useful in Haskell
than in ML because of type classes and the extended inference algorithm.  I
think he told me that, in an old release of the Yale Haskell system (when they
were still using LISP as a backend!), something of the sort was once possible
but Yale has sinced scrapped that implementation.

  Rice has a very nice Scheme programming environment called DrScheme which
includes a static debugger ("MrSpidey") that can do soft type inference.  It
essentially lets you do what I described above: you run the inferencer, click
on an identifier and it pops up a box next to it that displays a set
expression indicating what kinds of values the variable might hold at
run-time.  There is a description of it in the PLDI '96 proceedings, "Catching
Bugs in the Web of Program Invariants" by Matthew Flatt, et al. It's really
neat; if you have time, I recommend downloading it and checking it out for
yourself, even if you're not really a Scheme programmer.  (I'm not.)

http://www.cs.rice.edu/CS/PLT/packages/drscheme

Note:
I just checked the site and it looks like the newest release (47) is lacking
the debugger, so I recommend you get an earlier one, like version 42.

-- 
Frank Christoph                 Next Solution Co.      Tel: 0424-98-1811
christo@nextsolution.co.jp                             Fax: 0424-98-1500

Re: ergonomie du compilateur

[Jacques GARRIGUE]

>>>>> " " == Frank Christoph <christo@nextsolution.co.jp> writes:

 >   I once suggested a related feature to Alastair Reid, but for
 > Haskell program editors.  I thought it would be useful if the user
 > could click on an identifier and have the type displayed.  This can
 > be more useful in Haskell than in ML because of type classes and
 > the extended inference algorithm.  I think he told me that, in an
 > old release of the Yale Haskell system (when they were still using
 > LISP as a backend!), something of the sort was once possible but
 > Yale has sinced scrapped that implementation.

This is exactly what is possible with LablBrowser for O'Labl !
(Or OCamlBrowser for O'Caml)

You load a file in the editor, typecheck it, and then you can see the
type of any identifier, expression or pattern, by just clicking on it.

If typecheck fails, you can see types for all expressions preceding
the one that caused the error.

-- 
---------------------------------------------------------------------------
Jacques Garrigue	Kyoto University      garrigue@kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

ergonomie du compilateur

[David Monniaux]

-- VERSION FRANCAISE --
Bonjour à tous,
je trouve un aspect pénible au compilateur Ocaml, ou d'ailleurs au
toplevel, c'est son report d'erreur. En effet, il est quelquefois assez
difficile de retrouver l'origine du problème.
Si les messages du type "Parse error", bien que peu explicites, ne sont
toute de même pas trop pénibles quand on a l'habitude (il suffit
pratiquement de compter les parenthèses!), il n'en est pas de même pour
les messages d'erreur de typage.
En effet, souvent une erreur de typage intervient à une ligne donnée non
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 fonctions
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 qui lui
posent problème?

-- ENGLISH VERSION --
Hello all,
I find the Ocaml compiler, or the toplevel, sometimes quite tiresome with
its error reporting. It is sometimes difficult to trace the origin of an
error.
While the messages of the "Parse error" kind, if not very explicit, are
not too bothersome because with some experience one can fix that kind of
errors quite easily (most often, just count the parenthesises!), this is
not the case for typing errors.
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 in
the current line have been inferred. Often it's not too difficult to trace
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?

-- David Monniaux, student at ENS-Lyon
"Si l'informatique marchait, cela se saurait."

Re: ergonomie du compilateur

[Xavier Leroy]

[English summary: explaining type inference errors is a great idea,
but unfortunately something that no one knowns how to do right --
witness the number of papers published on this topic since 1982.]


> En effet, souvent une erreur de typage intervient à une ligne donnée
> non 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 fonctions
> 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 qui lui
> posent problème?

Bonne idee, mais personne ne sait faire. Il y a eu une bonne dizaine
d'articles publies la-dessus depuis 1982. Toutes les idees simples se
revelent marcher tres mal en pratique. Une bonne reference est
l'article de Duggan dans Science of Computer Programming 27(1).

- Xavier Leroy

Re: ergonomie du compilateur

[Claude Marche]

In his message of Wed January 15, 1997, David Monniaux writes:
> -- VERSION FRANCAISE --
> Bonjour à tous,
> je trouve un aspect pénible au compilateur Ocaml, ou d'ailleurs au
> toplevel, c'est son report d'erreur. En effet, il est quelquefois assez
> difficile de retrouver l'origine du problème.
> Si les messages du type "Parse error", bien que peu explicites, ne sont
> toute de même pas trop pénibles quand on a l'habitude (il suffit
> pratiquement de compter les parenthèses!), il n'en est pas de même pour
> les messages d'erreur de typage.
> En effet, souvent une erreur de typage intervient à une ligne donnée non
> 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 fonctions
> 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 qui lui
> posent problème?

Une remarque a propos de ce problème qui revient souvent, en
particulier avec les étudiants auxquels on enseigne CAML : il existe
une possibilite que l'on oublie trop souvent, qui est d'ajouter des
contraintes de types. Par exemple on peut ecrire

#let rec fact (n:int) = (if n<= 1 then 1 else n*fact(n-1) : int);;
fact : int -> int = <fun>

Evidemment, et c'est souvent le cas avec CAML, la syntaxe n'est pas
tres pratique (mais peut-etre y a-t-il une meilleure facon de faire ?)
il faut mettre les parentheses obligatoirement...

L'important c'est que ca permet de detecter des erreurs de types a la
definition de la fonction, par exemple :

#let module (x:float) (y:float)  = (x*x + y*y : float);;
Toplevel input:
>let module (x:float) (y:float)  = (x*x + y*y : float);;
>                                   ^
This expression has type float,
but is used with type int.

bon sang mais c'est bien sur, j'ai oublie les points :

#let rec module (x:float) (y:float)  = (x*.x +. y*.y : float);;
module : float -> float -> float = <fun>

Sans les contraintes de types, CAML repond
module : int -> int -> int = <fun>
et l'on ne s'apercoit pas de l'erreur si on fait pas attention.

De facon generale, quand on a une erreur de typage dans une fonction
compliquee, quelles contraintes de type bien placees permettent de
trouver le pb.

> -- ENGLISH VERSION --
> Hello all,
> I find the Ocaml compiler, or the toplevel, sometimes quite tiresome with
> its error reporting. It is sometimes difficult to trace the origin of an
> error.
> While the messages of the "Parse error" kind, if not very explicit, are
> not too bothersome because with some experience one can fix that kind of
> errors quite easily (most often, just count the parenthesises!), this is
> not the case for typing errors.
> 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 in
> the current line have been inferred. Often it's not too difficult to trace
> 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?

#french_to_english previous_text;;
Toplevel input:
>french_to_english previous_text;;
>^^^^^^^^^^^^^^^^^
The value identifier french_to_english is unbound.

--
| Claude Marché           | mailto:Claude.Marche@lri.fr |
| LRI - Bât. 490          | http://www.lri.fr/~marche/  |
| Université de Paris-Sud | phoneto: +33 01 69 15 64 85  |
| F-91405 ORSAY Cedex     | faxto: +33 01 69 15 65 86    |

Re: ergonomie du compilateur

[Hendrik Tews]

Hello,

I do occasionally program in ocaml. Since David Monniaux started
a discussion about the error messages of the ocaml compiler I
would like to add my opinion as well.

Features I dislike:

- There is no error recovery in the compiler. Before I start the
first compile I have at least 5 syntax errors in the file. In
order to find them I have to go through at least 5 edit-compile
cycles, which I find very annoying.

- In case of a syntax error, the compiler never reports what it
was expecting. For an ocaml beginner which has some experience in
SML it can be a tough problem to find the error in a line like

    type 'a tree = node of 'a * 'a tree * 'a tree
		 | leaf;;

since the compiler only says

    File "a.ml", line 3, characters 13-14:
    Syntax error

I would consider a message like "Expecting a Constructor, but
found an identifier" extremely useful.

- I don't understand the behavior of "ocamlc -i" if an type error
occurs. Especially in this case, where any information about the
inferred types would be useful, it just prints nothing. I would
like it to behave like the top-level, which prints any information
available. 


Regarding the type errors David Monniaux wrote:

   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?

I saw type inferences traces of other languages and it was no
help for finding a type error. Inference traces might be
interesting for people, who are interested in the typing
algorithm. 

Instead I would suggest an additional option to the ocaml
compiler which causes the compiler to print the types of all
identifiers not just those of top-level. This would help me a lot,
because I very often simulate the typing algorithm in order to
find the types of local variables which might have caused the
error.


Bye,

Hendrik Tews

Re: ergonomie du compilateur

[Ian T Zimmerman]

In article <199701211254.NAA13357@ithif18.inf.tu-dresden.de> Hendrik
Tews <tews@tcs.inf.tu-dresden.de> writes:

> 
> Hello,
> 
> I do occasionally program in ocaml. Since David Monniaux started a
> discussion about the error messages of the ocaml compiler I would
> like to add my opinion as well.
> 
> Features I dislike:
> 
> - There is no error recovery in the compiler. Before I start the
> first compile I have at least 5 syntax errors in the file. In order
> to find them I have to go through at least 5 edit-compile cycles,
> which I find very annoying.
> 
> - In case of a syntax error, the compiler never reports what it
> was expecting. For an ocaml beginner which has some experience in
> SML it can be a tough problem to find the error in a line like
> 
>     type 'a tree = node of 'a * 'a tree * 'a tree
> 		 | leaf;;
> 
> since the compiler only says
> 
>     File "a.ml", line 3, characters 13-14:
>     Syntax error
> 
> I would consider a message like "Expecting a Constructor, but found
> an identifier" extremely useful.
> 

I am working on these (among millions of other non-Caml things), in
the context of Caml Light.  If I ever finish it, I'll certainly
contact Ocaml maintainers about a possible port.

-- 
Ian T Zimmerman                        <itz@rahul.net>
I fully support the President's proposal to test driver's license
applicants for drugs.  Any plan to reduce driving is worth a try.

Re: ergonomie du compilateur

[Xavier Leroy]

> - There is no error recovery in the compiler. Before I start the
> first compile I have at least 5 syntax errors in the file. In
> order to find them I have to go through at least 5 edit-compile
> cycles, which I find very annoying.

My experience with ML compilers that attempt error recovery is that
they usually get it wrong and report many spurious syntax errors after
the first actual error, which is even more annoying than stopping at
the first error. Perhaps that's because of the ML syntax, which
has fewer obvious resynchronization points than, say, C syntax.

Also, as an implementor, I must say that I find parsing extremely
boring and prefer to concentrate on semantic issues. But all the usual
Yacc error recovery machinery is there, and any work on the OCaml
parser is welcome.

> - In case of a syntax error, the compiler never reports what it
> was expecting.

My understanding is that this can be done on a case by case basis,
using error productions. But I'm not sure it can be done in a
systematic way by reporting all tokens that the LALR tables are
expecting at that point. My recollection is that various Yacc
optimizations make this information (the set of expected tokens) hard
to recover from the transition tables.

> - I don't understand the behavior of "ocamlc -i" if an type error
> occurs. Especially in this case, where any information about the
> inferred types would be useful, it just prints nothing.

The "-i" option means ``typecheck the whole compilation unit, then
print out the inferred signature''. If the typing fails, nothing is
printed. Remember that a compilation unit, in OCaml, is parsed as a
whole, then typechecked as a whole, etc. There is no such thing as a
"phrase" or "toplevel definition" in a compilation unit.

In Caml Light there is actually a notion of "phrase" in a compilation
unit, and the "-i" option reports types on a phrase by phrase
basis. This is better for understanding type errors, but can alos lead
to inconsistent typings being printed. Consider:

        let r = ref []
        let f x = ... r := [1] ...

camlc -i reports

        value r : '_a list ref
        value f : ... -> ...

which is not right (the type of r is actually int list ref), while
ocamlc -i reports the correct types

        val r : int list ref
        val f : ... -> ...

Regards,

- Xavier Leroy

Re: ergonomie du compilateur

[Donald Syme]

> > - There is no error recovery in the compiler. Before I start the
> > first compile I have at least 5 syntax errors in the file. In
> > order to find them I have to go through at least 5 edit-compile
> > cycles, which I find very annoying.
> 
> My experience with ML compilers that attempt error recovery is that
> they usually get it wrong and report many spurious syntax errors after
> the first actual error, which is even more annoying than stopping at
> the first error. Perhaps that's because of the ML syntax, which
> has fewer obvious resynchronization points than, say, C syntax.

I've found the lack of error recovery (in Moscow ML) particularly tiresome 
when reporting mismatches between signatures and structures, and also
when multiple undefined identifiers exist.  Error recovery certainly
improves productivity in these cases, from my experience with NJSML.
I also think it helps with syntax, at least for the SML syntax.

Cheers,
Don Syme