RE: Warnings in ocaml

RE: Warnings in ocaml

[Don Syme]

> Also it will be useful to produce warning when polymorphic comparison
> occurs.

Here's another problem: I wrote about 20,000 lines where I used the built in
equality for
a particular type (that represented terms in a theorem prover).  Now I want
to implement
my own equality function on the type, and never user built-in equality.  I
can see 
Ocaml has generally made the right choice in not having
equality types like SML, but in this situation some sort of annotation +
warning would
be incredibly useful, since as it stands the Ocaml type system doesn't help
me find all those horrible
uses of built-in equality that I coded into my program, when you really feel
like it should...

Don

------------------------------------------------------------------------
At the lab:                                     At home:
Microsoft Research Cambridge                    11 John St
St George House                                 CB1 1DT
Cambridge, CB2 3NH, UK
Ph: +44 (0) 1223 744797                         Ph: +44 (0) 1223 722244
http://research.microsoft.com/users/dsyme
email: dsyme@microsoft.com
------------------------------------------------------------------------

Re: Warnings in ocaml

[Pierre Weis]

> Here's another problem: I wrote about 20,000 lines where I used the built in
> equality for
> a particular type (that represented terms in a theorem prover).  Now I want
> to implement
> my own equality function on the type, and never user built-in equality.  I
[...]
> Don
[...]
> email: dsyme@microsoft.com
> ------------------------------------------------------------------------

A quick hack that may helps could be to use the compiler to detect
those applications by redefining the (=) predicate with a type that is
not compatible with the type term. For instance, you may redefine (=)
for integers only (or strings only), and this way you may statically
find applications of generic equality to your term values since they
become ill-typed. Admittedly, this is not perfect, but can be of some
help in a very symbolic code as a theorem prover, where application of
= to values that are not of type term may be sparse.

Pierre Weis

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

Re: Warnings in ocaml

[Andrew Kay]

> eg      let _ = List.map f
>         in print_endline "done map..."
>  
> Are there any plans to provide a warning for this in ocaml?  
 
To save anyone else the bother, I'll point out the error of
my ways myself.  

I think SML has (had?) a check which stopped you accidentally
ignoring a function value before a semi-colon.  However, since
functions are first class citizens, why shouldn't you want to ignore
them just as you might ignore a list or integer value?

So instead, I propose you write an explicit ignore function for each
type you want to ignore:

val ignore_int : int -> unit
val ignore_fred : fred -> unit
...

Andrew Kay
Sharp Labs Europe Ltd, Oxford Science Park, Oxford, UK, OX4 4GA
Andrew.Kay@sharp.co.uk  Tel:+44 1865 747711 FAX:+44 1865 747717

Re: Warnings in ocaml

[Andrew Kay]

Frank A. Christoph wrote:
> I copied from SML and defined a procedure "ignore":
> so now I would write:
>   ignore (f x y); ...

Yes, we did this too.  This certainly gets rid of the warning about
the type to the left of ";", but it doesn't address the problem of
accidentally using a partially applied function.

eg      let _ = List.map f
	in print_endline "done map..."

Are there any plans to provide a warning for this in ocaml?  

Andrew Kay
Sharp Labs Europe Ltd, Oxford Science Park, Oxford, UK, OX4 4GA
Andrew.Kay@sharp.co.uk  Tel:+44 1865 747711 FAX:+44 1865 747717

Re: Warnings in ocaml

[Frank A. Christoph]

 Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp> wrote:
>I have a few comments about new warnings in ocaml.
>
>* having a warning when a function doesn't return unit in a sequence
>may catch some bugs, but this is a pain with imperative programming
>style, where you may not be interested by the result of a function but
>just by its side-effects. Of course you can switch off the warning,
>but I'm not sure having it on is a good default, since the default
>mode should be normative.
>
>ex. wrong code
> x = 3; ...
>   ^ should be <-
>
>ex. right code
> f x y; ...
>where f: t1 -> t2 -> int has some interesting side-effect.

I copied from SML and defined a procedure "ignore":

  let ignore k =
    let _ = k in ()

so now I would write:

  ignore (f x y); ...

I agree that it can be a pain to be explicit about this sometimes, but "ignore" makes it fairly transparent.

BTW, this procedure is a good candidate for addition to the standard library.

--FC

Re: Warnings in ocaml

[Xavier Leroy]

> I copied from SML and defined a procedure "ignore":
> so now I would write:
>   ignore (f x y); ...

I was considering adding this to the standard library, implemented in
such a way that no function call actually takes place.  It seems to
strike a reasonable balance between the safety of the warning and the
inconvenience of writing "let _ = ..."

- Xavier Leroy

Re: Warnings in ocaml

[Anton Moscal]

On Mon, 22 Feb 1999, Xavier Leroy wrote:

> > I copied from SML and defined a procedure "ignore":
> > so now I would write:
> >   ignore (f x y); ...
> 
> I was considering adding this to the standard library, implemented in
> such a way that no function call actually takes place.  It seems to
> strike a reasonable balance between the safety of the warning and the
> inconvenience of writing "let _ = ..."

Also it will be useful to produce warning when polymorphic comparison
occurs. Two days ago I got significant speedup in my program by
suppressing polymorphism. But I found it only by information from gprof.

Anton Moscal.

Re: Warnings in ocaml

[Michael Hicks]

> > I copied from SML and defined a procedure "ignore":
> > so now I would write:
> >   ignore (f x y); ...
> 
> I was considering adding this to the standard library, implemented in
> such a way that no function call actually takes place.  It seems to
> strike a reasonable balance between the safety of the warning and the
> inconvenience of writing "let _ = ..."

This is a nit, but I've noticed that for the bytecode compiler that 

let _ = foo() in ()

generates more instructions than for

foo(); ()

In particular, there is an extra "push" instruction (presumably for the
binding to _) in the former.  Is there any way to avoid this instruction
given that we know the binding is not going to really occur?
Mike

-- 
Michael Hicks
Ph.D. Candidate, the University of Pennsylvania
http://www.cis.upenn.edu/~mwh            mailto://mwh@dsl.cis.upenn.edu
"I worked with an individual who plugged his power strip back into itself
and for the life of him could not understand why his computer would not
turn on."

Re: Warnings in ocaml

[Ching-Tsun Chou]

   I copied from SML and defined a procedure "ignore":

     let ignore k =
       let _ = k in ()

   so now I would write:

     ignore (f x y); ...

How about instead of writing:

        (f x y) ; (g z w) ; ...

write:

        let _ = (f x y) in
        let _ = (g z w) in
        ...

In fact, I found it scarcely necessary to use ";" these days even when
I was doing imperative programming.

Cheers,
- Ching Tsun

=====================================================================
  Ching-Tsun Chou                   E-mail: ctchou@mipos2.intel.com  
  Intel Corporation                 Tel: (408) 765-5468              
  3600 Juliette Lane, SC12-401      Fax: (408) 653-7933              
  Santa Clara, CA 95052, U.S.A.     Sec: (408) 653-8849              
=====================================================================

Warnings in ocaml

[Jacques GARRIGUE]

I have a few comments about new warnings in ocaml.

* having a warning when a function doesn't return unit in a sequence
may catch some bugs, but this is a pain with imperative programming
style, where you may not be interested by the result of a function but
just by its side-effects. Of course you can switch off the warning,
but I'm not sure having it on is a good default, since the default
mode should be normative.

ex. wrong code
	x = 3; ...
	  ^ should be <-

ex. right code
	f x y; ...
where f: t1 -> t2 -> int has some interesting side-effect.
	

* another common error with imperative code is partial application in
a toplevel call inside a module

let _ =
  somefunc hsj hjfhfd

somefunc takes 3 arguments but is only given 2. Since this is a
let-definition no warning is printed while such a partial application
is pretty meaningless.

Regards,

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

Re: Warnings in ocaml

[Pierre Weis]

> * having a warning when a function doesn't return unit in a sequence
> may catch some bugs, but this is a pain with imperative programming
> style, where you may not be interested by the result of a function but
> just by its side-effects.

Could you please give me some interesting examples (Yes, I know you
can write this kind of functions, but I would like some examples where
it seems really painful to work it out otherwise).

Furthermore the point here is that this warning is useful, since we
had 2 undetected bugs into the Objective Caml system due to the lack
of this warning.

> Of course you can switch off the warning,
> but I'm not sure having it on is a good default, since the default
> mode should be normative.

The Caml system example shows that this warning is useful, even for
the most experienced programmers, let alone the beginners that do not
know how to get the warning on if they know that it exists...

> ex. wrong code
> 	x = 3; ...
> 	  ^ should be <-

Or even x := 3.

> ex. right code
> 	f x y; ...
> where f: t1 -> t2 -> int has some interesting side-effect.

In this case the warning tells you that you may be have a further look
to your f function: is it necessary to mix side effects and purely
functional computation ? Very often, this is not necessary and
rewriting the code to avoid the mixing gets it clearer. If it is not
the case, you can tell it to the reader and write

let _ = f x y in
...

> * another common error with imperative code is partial application in
> a toplevel call inside a module
> 
> let _ =
>   somefunc hsj hjfhfd
> 
> somefunc takes 3 arguments but is only given 2. Since this is a
> let-definition no warning is printed while such a partial application
> is pretty meaningless.
> 
> Regards,
> 
> 	Jacques
> ---------------------------------------------------------------------------
> Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
> 		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

So you want another warning for dummy definitions at the toplevel of
modules when the application if partial ? Or may be you want to extend
the sequence warning to this case when the result is not unit ?

Best regards,

Pierre Weis

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

Re: Warnings in ocaml

[Markus Mottl]

Hello,

> > * having a warning when a function doesn't return unit in a sequence
> > may catch some bugs, but this is a pain with imperative programming
> > style, where you may not be interested by the result of a function but
> > just by its side-effects.
> 
> Could you please give me some interesting examples (Yes, I know you
> can write this kind of functions, but I would like some examples where
> it seems really painful to work it out otherwise).

There are two examples, which fit well to this subject (non-unit-functions
in a unit-context), where problems arise.

Consider:

  let rec bar = function
    | [] -> ()
    | h::t -> h 0; bar t

  let _ =
    let f n : int = Printf.printf "%d\n" n; n in
    bar [f;f;f]

The inferred type of "bar" is:
  val bar : (int -> 'a) list -> unit

In "bar [f;f;f]", where function f is not a unit-function (it has
side-effects, but returns a value), there is no warning that the return
value of "f" is actually discarded in "bar", because it occurs in a
unit-context there.
One could mark functions like "bar" with an attribute that allows the
type checker to see that inference of a non-unit type for 'a should
generate a warning (maybe one can call this a "weak" constraint - I am
not sure about the correct terminology in this discipline).

Although the first example is not so severe (missing warning only) the
second example is a bit more of a problem, because in this case type
inference that yields such a general type ('a) results in an error:

  class foo_incorrect = object (self)
    method bar = function
      | [] -> ()
      | h::t -> h self; self#bar t
  end

  class foo_correct = object (self)
    method bar = function
      | [] -> ()
      | h::t -> ((h self) : unit); self#bar t
  end

Error message:
Some type variables are unbound in this type:
  class foo_incorrect : object ('a) method bar : ('a -> 'b) list -> unit end
The method bar has type (< bar : 'a; .. > -> 'b) list -> unit as 'a where 'b
is unbound

The reason for the error is that the (return-) type of "h" is inferred
as 'b, which corresponds to the behaviour in the non-OO example.
But here, the 'b would have to be explicitely bound in the class, which
is definitely not what the programmer intends -> it is (intuitively)
obvious that a unit-function is desired in this place.

Of course, one can help the compiler by explicitely telling it the return
type of h (as in foo_correct). Still, it can be quite difficult to track
down such "mistakes" in more complicated expressions than those given
in the example.

I don't know whether there is a truly elegant solution to this. Maybe
one could proceed as stated above:
Mark such functions (in this case: methods) as "weakly contrained" to
unit-values and automatically infer the type of all methods (probably not
desirable with functions) with all occurrences of the "weakly constrained"
type parameters replaced by type "unit".

This proposition will probably interact in a bad way with seperate
compilation: although it is possible to include such information in
compiled interface files (.cmi), if those are derived not from the
implementation (.ml) but from the interface (.mli), correct handling
would require the user to somehow declare such "weak constraints".
I am not sure whether the effort for such an extension really pays off...

Best regards,
Markus Mottl

-- 
Markus Mottl, mottl@miss.wu-wien.ac.at, http://miss.wu-wien.ac.at/~mottl