Re: [Caml-list] weird type behavior

[skaller <skaller@users.sourceforge.net>]

On Sun, 2006-10-29 at 03:12 +0200, Kirill wrote:
> Hi,
> 
> Unfortunately, I wasn't able to infer, how to solve my problem from the
> FAQ, nor from other sources. I can see that partial application somehow
> interferes with polymorphism, and partial application does look
> necessary for my task. Does it mean it's completely impossible in OCaml?
> Or is there still some way to overcome the problem?

A limitation of Hindley-Milner type inference: 
you cannot pass a polymorphic function to a function. 

The Ocaml run-time supports this fine, but the
type inference engine is only able to cope with universal
quantification. [To be clear: the Ocaml *type system* allows it
but the inference engine cannot infer it and there's currently
no way to override the inference engine: a coercion would be
unsafe, and an annotation on the argument is a constraint applied
after inference so doesn't help]

So when you DO pass a polymorphic function
to a function, it is specialised (monomorphised) inside
the function, depending on its use. For example:

# let g x = x,x in
        let f g x y = g x, g y in
        f g 1 1.2;;
This expression has type float but is here used with type int

# let g x = x,x in
  g 1, g 1.2;;
- : (int * int) * (float * float) = ((1, 1), (1.2, 1.2))

The function g really is polymorphic here, but not inside f.
The notation 

	'_a

generally means this monormorphised version of type variable 'a:
it happens to be 'int' in the first example, so the system
prints that instead: '_a means 'some ground type we don't
know' as opposed to 'a which means 'any type'.

Ocaml will allow you to pass a polymorphic function provided
you wrap it in a class or record:

# type poly = { h : 'a . 'a -> 'a * 'a };;
type poly = { h : 'a. 'a -> 'a * 'a; }

You can see here the quantifier 'a . is localised to
the record field. Note the type 'poly' is in fact
quite monomorphic -- there's no type parameter,
one of the fields just happens to be a polymorphic
function.


# let g x = x,x in
  let f k x y = k.h x, k.h y in
  f {h=g} 1 1.2;;
- : (int * int) * (float * float) = ((1, 1), (1.2, 1.2))



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