Re: [Caml-list] covariance newb question

[Christophe Raffalli <raffalli@univ-savoie.fr>]

Christophe Papazian a écrit :

> # type +'a t = 'a -> 'a;;
> In this definition, expected parameter variances are not satisfied.
> The 1st type parameter was expected to be covariant, but it is invariant
>
>
> But type t seems to be covariant :
>

nice question from a newb ;-) and no that trivial !!

fits 'a -> 'b is covariant in 'a and contravariant in 'b and Ocaml
is a stupid compiler (;-) and from this it thinks that 'a -> 'a is 
neither covariant nor contravariant.

But that does not prove that 'a -> 'a is not covariant, so we need to 
build a counter example.
We have to find two type a and b such that a <: b
and a function in a -> a that is not in b -> b.

That is easy with polymorphic variant:

type a = [ `A] and b = [`A | `B]

let f  `A = `A (f has type a -> a but not b -> b)

if you want to show that it is not contravariant, you can take

let g = function `A -> `B | `B -> `A (g has type b -> b but not a -> a)

... now the challenge ... prove that 'a -> 'a is not covariant using only
ML polymorphism (that is no polymorphic variant, modules, object, but only
subtyping on type scheme by substitution) which is probably what you had 
in mind with your exemple bellow:

> # let f : 'a t = (fun x -> x);;
> val f : 'a t = <fun>
> # let g : int t = f;;
> val g : int t = <fun>
>
I do not see a solution immediately, because ML polymorphism is too weak 
compared to system F

> Is there something wrong in my thought ?
>
Nothing it was a nice thought ... and may work in a small enough 
fragment of ML

> thank you,

>
>     Christophe Papazian
>
> _______________________________________________
> 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