Re: [Caml-list] Unexpected '_a problem

["Christophe Dehlinger" <christophedehlinger@gmail.com>]

[-- Attachment #1: Type: text/plain, Size: 2936 bytes --]

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<http://wwwfun.kurims.kyoto-u.ac.jp/%7Egarrigue/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
>

[-- Attachment #2: Type: text/html, Size: 4957 bytes --]