Re: [Caml-list] Unexpected '_a problem

["Remi Vanicat" <remi.vanicat@gmail.com>]

2006/8/1, Andreas Rossberg <AndreasRossberg@web.de>:
> "Chris King" <colanderman@gmail.com> wrote:
> >
> > # let create_foo () = object method foo (_: 'a) = () end;;
> > val create_foo : unit -> < foo : 'a -> unit > = <fun>
> > # let a = create_foo ();;
> > val a : < bar : '_a -> unit > = <obj>
> >
> > the compiler determines a is monomorphic, since 'a is in a
> > contravariant position.  But why, when 'a is placed in a covariant
> > position:
>
> This has nothing to do with contravariance, nor with subtyping or objects at
> all. What you observe is the infamous "value restriction": roughly, a
> definition can only be polymorphic when its right-hand side is syntactically
> a value (i.e. a function, tuple, constant, etc or combination thereof). In
> your case it's an application.

Nope :
# let f () = [];;
val f : unit -> 'a list = <fun>
# let x = f ();;
val x : 'a list = []

I have an application, but as it is covariant, the compiler lift the
value restriction, and make it covariant. But for a reson I don't
fully understood, one cannot do:

# let f () (_ : 'a -> unit) = ();;
val f : unit -> ('a -> unit) -> unit = <fun>
# f ();;
- : ('_a -> unit) -> unit = <fun>

and have full polymorphism (when f() type is covariant). Note that
this will work:
# type +'a t = Foo of ((('a -> unit) -> unit));;
type 'a t = Foo of (('a -> unit) -> unit)
# let f () = Foo (fun _ -> ());;
val f : unit -> 'a t = <fun>
# f ();;
- : 'a t = Foo <fun>
(we have full polymorphisme here, with a code that is mostly
equivalent to the first one, but not completely).