On 8/2/06, Remi Vanicat <remi.vanicat@gmail.com > wrote:

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.

This is Wright's value restriction, that is used in SML (maybe in Alice ML too ?). OCaml uses Garrigue's relaxed value restriction, which does care about variance (see http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf ). I haven't read that paper recently, but IIRC Garrigue's value restriction allows generalisation of some of the type parameters that are in covariant position.

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).

IIRC, when binding to something that is not a value (like here, where the toplevel output is bound to the application f()), type parameters that are on the left of arrows are not generalized, regardless of variance; if the type system allowed generalization of all covariant types it would lose its principality property.

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).

Maybe algebraic constructors are a special case of function application ? After all, they can never "go wrong", can they ?

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs