On Sun, Dec 14, 2003 at 09:38:24PM +0000, Benjamin Geer wrote:
> Jean-Baptiste Rouquier wrote:
> >   compare_things : thing -> thing -> ('a -> 'a -> bool) -> bool
> >doesn't mean that comparison_fun has to be polymorphic, but it means 
> >that any function with type ('a -> 'a -> bool), where 'a is any type, is 
> >acceptable. For instance, the type checker would accept a function of 
> >the type (char -> char -> bool).
> 
> OK, but it seems that the type checker has inferred the type of 
> comparison_fun just by looking at its first use in compare_things, and 
> has decided that it must be monomorphic; this is an incorrect inference. 
>  My naive impression is that if the type checker was willing to accept 
> both uses of comparison_fun as valid (or perhaps if it also looked at 
> the places where compare_things is called), it would conclude that 
> comparison_fun does indeed have to be polymorphic.  In that case, I 
> would get a compile error if I tried to pass a non-polymorphic function 
> to compare_things.  Would this be this asking too much?  (I suspect the 
> answer is yes; I'm just curious...)

Polymorphism in ML is flat, that is all type variables are quantified
before the function, not in the arguments. The type ('a -> foo) -> bar
means forall 'a. ('a -> foo) -> bar, and not (forall 'a. 'a -> foo) -> bar.

This is one of the costs of type inference.

In OCaml you can simulate deep polymorphism with polymorphic records
(but you have to write explicit type then).

-- 
: Michal Moskal :: http://www.kernel.pl/~malekith : GCS {C,UL}++++$ a? !tv
: When in doubt, use brute force. -- Ken Thompson : {E-,w}-- {b++,e}>+++ h

-------------------
To unsubscribe, mail caml-list-request@inria.fr Archives: http://caml.inria.fr
Bug reports: http://caml.inria.fr/bin/caml-bugs FAQ: http://caml.inria.fr/FAQ/
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners