partial application warning unreliable?

partial application warning unreliable?

[skaller]

I have this:

# let f x y = x + y;;
# let a = f 1; 1;;
Warning F: this function application is partial,
maybe some arguments are missing.
val a : int = 1

This is good -- I rely on it!
class cc = object (self) 
  method f x y = x + y 
  method g () = self#f 1;  
end;;

Warning F: this function application is partial,
maybe some arguments are missing.

yea, good ..


    method add_nonterminal (s:string) (sr:range_srcref) (toks:
Flx_parse.token list) (term:ast_term_t) =

...
    state#add_nonterminal tok (Flx_srcref.slift sr) t;

Method has 4 arguments, but the call applies to only 3.

Woops, no warning!! Bad! This error of mine caused a serious
bug -- the method call didn't do anything!

Really this just shouldn't be allowed at all!
We have ignore() function, IMHO its use should be required
(except at the top level interpreter where you want to see
the type of a term).

But the point is .. the warning is unreliable! Why?

In my real code the only difference is that the
method being called is not visible -- it is called
via a class interface.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] partial application warning unreliable?

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>

>     method add_nonterminal (s:string) (sr:range_srcref) (toks:
> Flx_parse.token list) (term:ast_term_t) =
> 
> ...
>     state#add_nonterminal tok (Flx_srcref.slift sr) t;
> 
> Method has 4 arguments, but the call applies to only 3.
> 
> Woops, no warning!! Bad! This error of mine caused a serious
> bug -- the method call didn't do anything!

Wait a minute, is there anything after the semicolon?
The point is that a trailing semicolon at the end of a method
definition does nothing: it still returns the result of the previous
expression!
I wonder whether this behaviour is good or not, but this also means
that there is no reason to have a warning here.

If there is an expression after the semicolon, and you have no
warning, then file a bug report: the type system is supposed to detect
all partial applications in statements, except for functions whose
result is a polymorphic type variable.

By the way, your other example with classes is wrong:

# class cc = object (self) 
    method f x y = x + y 
    method g () = self#f 1;  
  end;;
class cc :
  object method f : int -> int -> int method g : unit -> int -> int end

No warning, for the reason stated above: the semicolon does nothing.

Jacques Garrigue

Re: [Caml-list] partial application warning unreliable?

[skaller]

On Thu, 2005-12-08 at 12:10 +0900, Jacques Garrigue wrote:
> From: skaller <skaller@users.sourceforge.net>
> 
> >     method add_nonterminal (s:string) (sr:range_srcref) (toks:
> > Flx_parse.token list) (term:ast_term_t) =
> > 
> > ...
> >     state#add_nonterminal tok (Flx_srcref.slift sr) t;
> > 
> > Method has 4 arguments, but the call applies to only 3.
> > 
> > Woops, no warning!! Bad! This error of mine caused a serious
> > bug -- the method call didn't do anything!
> 
> Wait a minute, is there anything after the semicolon?

yes, it is followed by an empty list []

> The point is that a trailing semicolon at the end of a method
> definition does nothing: it still returns the result of the previous
> expression!

That's a bit weird, but I guess the decision is somewhat
arbitrary .. I actually wonder if using camlp4 changes this
result (since I guess it is an artefact of the parser/grammar
rather than a deliberate  choice .. :)

> I wonder whether this behaviour is good or not, but this also means
> that there is no reason to have a warning here.

IMHO an expression on the LHS of a semicolon expression
(possibly excluding the degenerate case the RHS is empty)
should have type unit**, and it should be *hard error* not a warning
if it doesn't: the ignore(expr) function can be used
to suppress the error if required.

** as you know I think the type should be void,
not unit. Other systems (such as FISh) has a special
type such as 'command' for this. But whichever type
is chosen, Ocaml should be *strict* about it. It is
strict everywhere else .. I don't understand why it
isn't strict here.

> If there is an expression after the semicolon, and you have no
> warning, then file a bug report: the type system is supposed to detect
> all partial applications in statements, except for functions whose
> result is a polymorphic type variable.

I don't have a reduced example though, and the error is
already fixed in my code. 

> By the way, your other example with classes is wrong:
> 
> # class cc = object (self) 
>     method f x y = x + y 
>     method g () = self#f 1;  
>   end;;
> class cc :
>   object method f : int -> int -> int method g : unit -> int -> int end
> 
> No warning, for the reason stated above: the semicolon does nothing.

Ouch .. you're right -- I actually DID get an error F .. jumbled
up inside THREE copies of the text the top level printed trying
to underline the error. The toplevel is very sick ..

BTW: the error flags documentation is very confusing:

     A/a enable/disable all warnings
     X/x enable/disable all other warnings

other than what? I am using -w yz but STILL get
warning X, unused function argument .. some of this
happens in Frontc/CIL which I'm using and I would like
to minimise patches.

BTW: what is this for?

     S/s enable/disable non-unit statement

Isn't that going to be F partial application 99% of the time?
If I turn off F, will I get S instead?

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] partial application warning unreliable?

[Damien Doligez]

On Dec 8, 2005, at 08:11, skaller wrote:

> BTW: the error flags documentation is very confusing:
>
>      A/a enable/disable all warnings
>      X/x enable/disable all other warnings
>
> other than what?

Other than [B-WYZ], obviously.  There's only so much you can write
in the on-line help message before people stop reading it altogether.

> I am using -w yz but STILL get
> warning X, unused function argument .. some of this
> happens in Frontc/CIL which I'm using and I would like
> to minimise patches.

Warnings are orthogonal: disabling Y and Z does not disable X.
It has no impact on X.

> BTW: what is this for?
>
>      S/s enable/disable non-unit statement

IIRC, it's for non-unit statements that are not partial applications.

> If I turn off F, will I get S instead?

Warnings are orthogonal: disabling F does not make you get more S
warnings.  It has no impact on S.

-- Damien

Re: [Caml-list] partial application warning unreliable?

[malc]

On Thu, 8 Dec 2005, Jacques Garrigue wrote:

<snip>
>
> # class cc = object (self)
>    method f x y = x + y
>    method g () = self#f 1;
>  end;;
> class cc :
>  object method f : int -> int -> int method g : unit -> int -> int end
>
> No warning, for the reason stated above: the semicolon does nothing.

Here's a strange test case, i was bitten by it recently in a real code:

<mox.ml>
let y o =
   o#moo;
   1

let x (o:(<moo : string -> unit>)) =
   y o

let _ =
   print_int (x (object method moo s = print_endline s end));
   print_newline ()
</mox.ml>

# ocaml -warn-error A mox.ml
1

In my case method moo was actually a method that locked a mutex, the
implications were quite severe.

-- 
mailto:malc@pulsesoft.com

Re: [Caml-list] partial application warning unreliable?

[skaller]

On Fri, 2005-12-09 at 02:51 +0300, malc wrote:
> On Thu, 8 Dec 2005, Jacques Garrigue wrote:
> 
> <snip>
> >
> > # class cc = object (self)
> >    method f x y = x + y
> >    method g () = self#f 1;
> >  end;;
> > class cc :
> >  object method f : int -> int -> int method g : unit -> int -> int end
> >
> > No warning, for the reason stated above: the semicolon does nothing.
> 
> Here's a strange test case, i was bitten by it recently in a real code:
> 
> <mox.ml>
> let y o =
>    o#moo;
>    1
> 
> let x (o:(<moo : string -> unit>)) =
>    y o
> 
> let _ =
>    print_int (x (object method moo s = print_endline s end));
>    print_newline ()
> </mox.ml>
> 
> # ocaml -warn-error A mox.ml
> 1
> 
> In my case method moo was actually a method that locked a mutex, the
> implications were quite severe.

AHA. In trying to fill out your problem to a real test case
for a bug report .. I think I have discovered the problem!

# class cow = object(self) method moo (s:string)= print_endline s
  end;;
class cow : object method moo : string -> unit end

# let y o = o#moo; 1;;
val y : < moo : 'a; .. > -> int = <fun>

And there we have it .. an uncaught partial application!

The reason is clear .. we don't know the arity of the
function yet -- we don't even know its type.

The type of a statement is currently 'a, which is just 
plain wrong. The correct type is void, however unit
will catch more errors than 'a.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] partial application warning unreliable?

[Jacques Garrigue]

From: skaller <skaller@users.sourceforge.net>

> AHA. In trying to fill out your problem to a real test case
> for a bug report .. I think I have discovered the problem!
> 
> # class cow = object(self) method moo (s:string)= print_endline s
>   end;;
> class cow : object method moo : string -> unit end
> 
> # let y o = o#moo; 1;;
> val y : < moo : 'a; .. > -> int = <fun>
> 
> And there we have it .. an uncaught partial application!
> 
> The reason is clear .. we don't know the arity of the
> function yet -- we don't even know its type.
> 
> The type of a statement is currently 'a, which is just 
> plain wrong. The correct type is void, however unit
> will catch more errors than 'a.

This behaviour has been known for long.
This is for instance why, in the standard library, List.iter is
explicitly given type
   ('a -> unit) -> 'a list -> unit
rather than the inferred
   ('a -> 'b) -> 'a list -> unit
(which actually it had a long time ago, in Caml Special Light)

The trouble is that any change to this behaviour would not be
principal (from the type inference point of view).
That is, we might choose to instantiate 'a to unit when generalizing
the type of y, but actually #moo might be of type int, which we will
discover later, when applying it. As long as returning non-unit in a
statement grades only a warning, we cannot do that.
So, saying that the type of y above is wrong means that all statements
should be forced by type checking to return unit and nothing else.
This is not the default, but this could indeed be done with
-warn-error S.

Note that, for objects, there was before ocaml 3.05 a warning, turned
on only in -labels mode, that ensured that every method was known
before being called. This would have caught the above error. It is now
commented out :-(

Jacques Garrigue

Re: [Caml-list] partial application warning unreliable?

[skaller]

On Fri, 2005-12-09 at 11:15 +0900, Jacques Garrigue wrote:
> From: skaller <skaller@users.sourceforge.net>

> > The type of a statement is currently 'a, which is just 
> > plain wrong. The correct type is void, however unit
> > will catch more errors than 'a.
> 
> This behaviour has been known for long.

> The trouble is that any change to this behaviour would not be
> principal (from the type inference point of view).

I'm not sure I understand that (what a principal type is .. ;(

> That is, we might choose to instantiate 'a to unit when generalizing
> the type of y, but actually #moo might be of type int, which we will
> discover later, when applying it. As long as returning non-unit in a
> statement grades only a warning, we cannot do that.

> So, saying that the type of y above is wrong means that all statements
> should be forced by type checking to return unit and nothing else.

Yes. The only case I can think of where this would 
cause a problem is raising an exception -- since that
is allowed ALSO in non-statement position.

Of course some legacy code may break. And that is, IMHO,
a good thing. Some C programmers even write:

	extern int f(int);
	(void) f(1);

to make the casting away of the return value explicit,
clearly believing that silently throwing away a return
value is a bug in ISO C. In Ocaml we have

	ignore (f 1);

if we really want side effects but not the return value.
Its use should be mandatory. IMHO.

> This is not the default, but this could indeed be done with
> -warn-error S.

Hmm ..

When you see some code in a statement, you cannot
report an error if the type is 'a, because it may later
be specialised to type unit, and the error would then
be premature.

And secondly I asked:

> If I turn off F, will I get S instead?

and Damien replied:

"Warnings are orthogonal: disabling F does not make you get more S
warnings.  It has no impact on S."

so you'd need to -warn-error SF not just S ;(

You surely wouldn't want -warn-error to actually change
the way the inference engine worked!

> Note that, for objects, there was before ocaml 3.05 a warning, turned
> on only in -labels mode, that ensured that every method was known
> before being called. This would have caught the above error. It is now
> commented out :-(

Is this particular problem specific to class methods?
It seems to be a general typing problem to me, BUT,
with objects you can call a method before seeing it,
which you cannot do with ordinary functions.

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] partial application warning unreliable?

[malc]

On Fri, 9 Dec 2005, Jacques Garrigue wrote:

> From: skaller <skaller@users.sourceforge.net>
>
>> AHA. In trying to fill out your problem to a real test case
>> for a bug report .. I think I have discovered the problem!
>>
>> # class cow = object(self) method moo (s:string)= print_endline s
>>   end;;
>> class cow : object method moo : string -> unit end
>>
>> # let y o = o#moo; 1;;
>> val y : < moo : 'a; .. > -> int = <fun>
>>
>> And there we have it .. an uncaught partial application!
>>
>> The reason is clear .. we don't know the arity of the
>> function yet -- we don't even know its type.
>>
>> The type of a statement is currently 'a, which is just
>> plain wrong. The correct type is void, however unit
>> will catch more errors than 'a.
>
> This behaviour has been known for long.
> This is for instance why, in the standard library, List.iter is
> explicitly given type
>   ('a -> unit) -> 'a list -> unit
> rather than the inferred
>   ('a -> 'b) -> 'a list -> unit
> (which actually it had a long time ago, in Caml Special Light)
>
> The trouble is that any change to this behaviour would not be
> principal (from the type inference point of view).
> That is, we might choose to instantiate 'a to unit when generalizing
> the type of y, but actually #moo might be of type int, which we will
> discover later, when applying it. As long as returning non-unit in a
> statement grades only a warning, we cannot do that.
> So, saying that the type of y above is wrong means that all statements
> should be forced by type checking to return unit and nothing else.
> This is not the default, but this could indeed be done with
> -warn-error S.
>
> Note that, for objects, there was before ocaml 3.05 a warning, turned
> on only in -labels mode, that ensured that every method was known
> before being called. This would have caught the above error. It is now
> commented out :-(

I gather all this means that the only "safe" way to call a unit method
on an implictily typed object is via:

let () = o#moo in ...

-- 
mailto:malc@pulsesoft.com

Re: [Caml-list] partial application warning unreliable?

[Jacques Garrigue]

From: malc <malc@pulsesoft.com>

> I gather all this means that the only "safe" way to call a unit method
> on an implictily typed object is via:
> 
> let () = o#moo in ...

Yes, but only if the type of o is unknown.
If o itself was defined by a let statement, or there was a type
annotation
  let f (o : c) = ...
then the warnings will work properly (fortunately.)

Personally, I annotate almost all objects received as function
arguments. It may be seen as defeating the purpose of type inference, but
this produces better error messages, and avoids the above problem.
It is also necessary with polymorphic methods or optional arguments.

Jacques Garrigue

Re: [Caml-list] partial application warning unreliable?

[malc]

On Sat, 10 Dec 2005, Jacques Garrigue wrote:

> From: malc <malc@pulsesoft.com>
>
>> I gather all this means that the only "safe" way to call a unit method
>> on an implictily typed object is via:
>>
>> let () = o#moo in ...
>
> Yes, but only if the type of o is unknown.
> If o itself was defined by a let statement, or there was a type
> annotation
>  let f (o : c) = ...
> then the warnings will work properly (fortunately.)

I haven't done that because in my particular case that would have
required recursive modules (and not inside the same source unit).
And having two set of class types that described type of o didn't
really appeal to me all that much.

>
> Personally, I annotate almost all objects received as function
> arguments. It may be seen as defeating the purpose of type inference, but
> this produces better error messages, and avoids the above problem.
> It is also necessary with polymorphic methods or optional arguments.

-- 
mailto:malc@pulsesoft.com

Re: [Caml-list] partial application warning unreliable?

[Andreas Rossberg]

skaller wrote:
> 
> The correct type is void, however unit
> will catch more errors than 'a.

IIRC, this has been discussed in the past, but since you iterate this 
statement repeatedly, let me reinforce that it is incorrect.

Void is the empty type. No value of this type can be constructed. Since 
in ML, everything is an expression, and every "procedure" a function, 
they all have to evaluate to something. Hence, the only possible 
functions with result type void are those that do not return. The only 
possible functions with argument type void are those that can never be 
called.

The type unit on the other hand, is the trivial type. It carries just 
one value, and hence no information. Consequently, it is the canonical 
type to use for functions that do not require or do not return any 
information.

Type theory wasn't well developed in the 60s, when Algol 68 (I think) 
introduced its notion of void type that was later inherited, in even 
more abusive ways, by C and friends. The name is just historical 
accident, it really ought to be unit.

   - Andreas

-- 
Andreas Rossberg, rossberg@ps.uni-sb.de

Let's get rid of those possible thingies!  -- TB

Re: [Caml-list] partial application warning unreliable?

[skaller]

On Fri, 2005-12-09 at 13:21 +0100, Andreas Rossberg wrote:
> skaller wrote:
> > 
> > The correct type is void, however unit
> > will catch more errors than 'a.
> 
> IIRC, this has been discussed in the past, but since you iterate this 
> statement repeatedly, let me reinforce that it is incorrect.

Well it seems to achieve the desired result in Felix.

In particular, neither malc nor myself would have had
our bugs slip past the Felix type system the way they
slipped past Ocaml. However using unit instead would
have caught both our bugs I think, but fail to
eliminate:

	f: int -> 1
	g: 1 -> int

	let x = g ( f 1 ) in

which is clearly still wrong -- you should be required to write
this as

	f 1;
	let x = g () in

to explicitly sequence the side effects. Felix allows

	f: int -> 0

but not

	g: 0 -> int

and thus, the expression:

	g (f 1)

cannot type check (for any g). This forces you to explicitly
sequence side effects, which is the intended result.
BTW: it isn't clear this is entirely desirable!

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net

Re: [Caml-list] partial application warning unreliable?

[Andrej Bauer]

It seems unwise to me to try to capture the notion of side-effects via a
type like "0" or "1". Skaller is talking as if the type

  int -> 0

means "a command with side-effects". But "int -> int" can have plenty
side effects, too. A better solution would be to refine types so that
they keep track of which things have side-effects (monads!).

A discussion along the lines "do commands return void or unit?" is
flawed. The type void, in any reasonable semantics (assuming eager
language here), will be inhabited exactly by non-terminating
expressions, whereas "unit" will be inhabited by non-terminating and
terminating ones. Neither of these say anything about side-effects.

I understand ocaml's solution to be as follows: it is understood that
expressions of _all_ types may involve side effects (as well as
exceptions). While the result of a command may be ignored, as it is
uninteresting, the cruical bit is that a command may terminate or not.
This means that its type must posses terminating as well as
non-terminating values, i.e., _unit_ is the right choice. Void would be
the right choice only if all commands were non-terminating, or if all
were terminating.

Andrej Bauer

Re: [Caml-list] partial application warning unreliable?

[Andreas Rossberg]

"skaller" <skaller@users.sourceforge.net> wrote:

> Felix allows
>
> f: int -> 0
>
> but not
>
> g: 0 -> int

Then your "0" is not a proper type in the usual formal sense. Even less is
it the type-theoretic 0.

As Andrej Bauer points out, void vs unit has nothing to do with side
effects. If you want to capture side effects properly in a type system the
known approaches are effect systems or monads. In fact, your 0 looks
somewhat like a monad type with implicit injection and semicolon as a kind
of forgetting bind operator. But it seems sufficiently adhoc to make any
type-theoretic interpretation difficult.

  - Andreas