surprising type error with labels

surprising type error with labels

[Jake Donham]

Hi list,

Why does

 ListLabels.find (fun _ -> true) [];;

produce

 Characters 16-31:
   ListLabels.find (fun _ -> true) [];;
                   ^^^^^^^^^^^^^^^
 This expression should not be a function, the expected type is
 ('a -> 'b) list

I thought the rule was that "if an application is total, labels may be
omitted." (4.1 in the manual). (I was trying to do module List =
ListLabels at the top of a file.) Thanks,

Jake

Re: [Caml-list] surprising type error with labels

[Jeremy Yallop]

Jake Donham wrote:
> Why does
> 
>  ListLabels.find (fun _ -> true) [];;
> 
> produce
> 
>  Characters 16-31:
>    ListLabels.find (fun _ -> true) [];;
>                    ^^^^^^^^^^^^^^^
>  This expression should not be a function, the expected type is
>  ('a -> 'b) list
> 
> I thought the rule was that "if an application is total, labels may be
> omitted." (4.1 in the manual). (I was trying to do module List =
> ListLabels at the top of a file.) Thanks,

Applications of functions whose return types are type variables are 
never considered total, since it's possible to pass extra arguments if 
the type variable is instantiated to a function type.  For example, 
ListLabels.find has type

    f:('a -> bool) -> 'a list -> 'a

If the type variable is instantiated to `bool -> bool', say, then you 
can pass more than two arguments:

    ListLabels.find ~f:(fun f -> f false) [not] false

You can use the function without labels if you fix its return type:

    (ListLabels.find :  f:_ -> _ -> int) (fun _ -> true) []

Jeremy.

Re: [Caml-list] surprising type error with labels

[Mark Shinwell]

On Thu, Jun 19, 2008 at 10:58:59PM +0100, Jeremy Yallop wrote:
> Jake Donham wrote:
> >Why does
> >
> > ListLabels.find (fun _ -> true) [];;
> >
> >produce
> >
> > Characters 16-31:
> >   ListLabels.find (fun _ -> true) [];;
> >                   ^^^^^^^^^^^^^^^
> > This expression should not be a function, the expected type is
> > ('a -> 'b) list
> >
> >I thought the rule was that "if an application is total, labels may be
> >omitted." (4.1 in the manual). (I was trying to do module List =
> >ListLabels at the top of a file.) Thanks,
> 
> Applications of functions whose return types are type variables are 
> never considered total, since it's possible to pass extra arguments if 
> the type variable is instantiated to a function type.  For example, 
> ListLabels.find has type
> 
>    f:('a -> bool) -> 'a list -> 'a
> 
> If the type variable is instantiated to `bool -> bool', say, then you 
> can pass more than two arguments:
> 
>    ListLabels.find ~f:(fun f -> f false) [not] false

I'm not really sure that this behaviour (which is highly non-obvious from
the error message) is to do with applying future unlabelled arguments.
As far as I can see it's probably this way so you can apply future
_labelled_ arguments, meaning you can write things like:

# ListLabels.find [] (fun x -> x);;
- : f:((('a -> 'a) -> 'b) -> bool) -> 'b = <fun>

and also:

# ListLabels.find ~f:(fun (f:(z:int -> int)) -> true) ~z:42 [fun ~z -> 1];;
- : int = 1

(note that the ~z:42 has been commuted with the list).  This seems kinda
cool, but the code is somewhat obfuscated, and error messages are potentially
confusing as Jake witnessed.

Is there any theoretical reason why the compiler couldn't just deem
applications of the form given by the original poster as total, even though
it results in the loss of some expressibility?  Perhaps it would be easier
to improve the error messages in that case... or perhaps it just results in
too little expressibility for some reason.

Mark

Re: [Caml-list] surprising type error with labels

[Jeremy Yallop]

Mark Shinwell wrote:
> Is there any theoretical reason why the compiler couldn't just deem
> applications of the form given by the original poster as total, even though
> it results in the loss of some expressibility?  Perhaps it would be easier
> to improve the error messages in that case... or perhaps it just results in
> too little expressibility for some reason.

You'd have to distinguish between terms which refer to polymorphic 
functions and terms whose type is only partially known.  I suspect it 
might be quite difficult to do that in a way that interacts 
satisfactorily with type inference.  Even the current design has a 
rather unfortunate dependence on the particular order of execution of 
the type inference algorithm.  For example, given a definition

    let h = fun ~x:() () -> ()

the following program is allowed

    let g f x = ([f; h], f x)

whereas the following rather similar program is not

    let g f x = (f x, [f; h])

If the type inference algorithm sees `[f; h]' first then it gives f a 
fully-known labeled type and allows it to be applied without a label 
when it subsequently encounters `f x'.  If it sees `f x' first then it 
assigns an unlabeled type to f, which subsequently fails to unify with 
the type of h.

I agree that the current behaviour is surprising, but I'm not sure that 
it's easy to make it much less surprising, even if you're willing to 
give up some expressiveness.

Jeremy.