Unexpected '_a problem

Unexpected '_a problem

[Chris King]

Given this code:

# 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:

# let create_bar () = object method bar (_: 'a) = () end;;
val create_bar : unit -> < bar : ('a -> unit) -> unit > = <fun>
# let b = create_bar ();;
val b : < bar : ('_a -> unit) -> unit > = <obj>

does the compiler restrict b to be monomorphic?  If I wrap everything
up in a module and abstract the type returned by create_bar (),
create_bar () works as expected and returns a polymorphic value.

Thanks,
Chris King

Re: [Caml-list] Unexpected '_a problem

[Andreas Rossberg]

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

Also note that in the above code, it is the object that would be
polymorphic, not the method! If you want a polymorphic method, the proper
syntax is the following:

# let create_foo () = object method foo : 'a.'a -> unit = fun _ -> () end;;
val create_foo : unit -> < foo : 'a. 'a -> unit > = <fun>
# let a = create_foo ();;
val a : < foo : 'a. 'a -> unit > = <obj>
# a#foo 5; a#foo true;;
- : unit = ()

Here, `a' is a monomorphic object with a polymorphic method.

- Andreas

Re: [Caml-list] Unexpected '_a problem

[Remi Vanicat]

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

Re: [Caml-list] Unexpected '_a problem

[Alain Frisch]

Remi Vanicat wrote:
> 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>


See the paper _Relaxing the value restriction_ by Jacques Garrigue (
http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf
), page 15: dangerous type variables (which are not generalized when the
right-hand side of the let-binding is not a value) are not only those is
contravariant position - this would be enough to ensure type soundness -
but also those which appear in a contravariant branch (e.g. anywhere on
the left of an arrow) - this is necessary to ensure that the type system
has principal types.

Let me reformulate the example given in the paper. Consider the
top-level binding:

let f = print_newline (); fun x -> raise Exit

Semantically, it would be sound to give g a polymorphic type:
\forall 'a,'b. 'a -> 'b. However, the relaxed value restriction does not
try to be that clever; it decides which variables to generalize only by
looking at the type of the bound expression (when it is not a
syntactical value). Here are two possible types for the expression:

'a -> 'b
('c -> 'd) -> 'b

Generalizing all variables in covariant positions would give these two
type schemes:

\forall 'b.    'a -> 'b           ('a monomorphic)
\forall 'b,'c. ('c -> 'd) -> 'b   ('d monomorphic)

The only type-scheme which is more general than these two
would be \forall 'a,'b. 'a -> 'b, but this one is not ok (a
contravariant variable has been generalized).

To retrieve principality, the type system has been designed so that
the variable 'c above would not be generalized (it is on the left of an
arrow), which makes the type scheme \forall 'b. ('c -> 'd) -> 'b
less general than \forall 'b. ('a -> 'b) (which is the principal type
scheme inferred by OCaml).


-- Alain

Re: [Caml-list] Unexpected '_a problem

[Christophe Dehlinger]

[-- 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 --]

Re: [Caml-list] Unexpected '_a problem

[Andreas Rossberg]

Christophe Dehlinger wrote:
>On 8/2/06, Remi Vanicat <remi.vanicat@gmail.com > wrote:
>>2006/8/1, Andreas Rossberg <AndreasRossberg@web.de>:
>>
>> 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.

Oops, right, somehow I had forgotten about the relaxation. Thanks to you and
Alain for the correction.

- Andreas

Re: [Caml-list] Unexpected '_a problem

[Chris King]

On 8/2/06, Alain Frisch <Alain.Frisch@inria.fr> wrote:
> See the paper _Relaxing the value restriction_ by Jacques Garrigue (
> http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/papers/morepoly-long.pdf
> ), page 15: dangerous type variables (which are not generalized when the
> right-hand side of the let-binding is not a value) are not only those is
> contravariant position - this would be enough to ensure type soundness -
> but also those which appear in a contravariant branch (e.g. anywhere on
> the left of an arrow) - this is necessary to ensure that the type system
> has principal types.

Okay, that (and Christophe's explanation) explains why hiding
everything in a module works.  Thanks everyone for your help!  It
seems I will have to use Obj.magic to get the type I want but at least
its use in this situation seems both safe and warranted.

- Chris

Re: [Caml-list] Unexpected '_a problem

[Jacques Garrigue]

From: "Chris King" <colanderman@gmail.com>
> Okay, that (and Christophe's explanation) explains why hiding
> everything in a module works.  Thanks everyone for your help!  It
> seems I will have to use Obj.magic to get the type I want but at least
> its use in this situation seems both safe and warranted.

There are no "safe" uses of Obj.magic. It just happens to work in some
cases, but it is strongly discouraged to use it to get around the type
system, particularly when there are other ways to reach the same
result.

type 'a bar_t = Bar of <bar: ('a -> unit) -> unit> ;;
let create_bar () = Bar (object method bar (_: 'a) = () end);;
let b = create_bar ();;
let Bar b = b;;

Note that you need two definitions, as mixing the application with the
extraction would loose the polymorphism.
If you still want to use Obj.magic, remember to put complete type
annotions on both its input and output, as the lack of type
information may break the compiler.

Jacques Garrigue

Re: [Caml-list] Unexpected '_a problem

[Chris King]

On 8/3/06, Jacques Garrigue <garrigue@math.nagoya-u.ac.jp> wrote:
> type 'a bar_t = Bar of <bar: ('a -> unit) -> unit> ;;
> let create_bar () = Bar (object method bar (_: 'a) = () end);;
> let b = create_bar ();;
> let Bar b = b;;

Okay, that got the types to work out correctly.

> If you still want to use Obj.magic, remember to put complete type
> annotions on both its input and output, as the lack of type
> information may break the compiler.

Surprisingly putting a type annotation on its output caused it to
infer a monomorphic type - I was relying on the type in the module's
signature since the type there is abstract.