covariance newb question

covariance newb question

[Christophe Papazian]

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

# let f : 'a t = (fun x -> x);;
val f : 'a t = <fun>
# let g : int t = f;;
val g : int t = <fun>

Is there something wrong in my thought ?

thank you,

	Christophe Papazian

Re: [Caml-list] covariance newb question

[Keiko Nakata]

From: Christophe Papazian <christophe.papazian@gmail.com>
> But type t seems to be covariant :
> 
> # let f : 'a t = (fun x -> x);;
> val f : 'a t = <fun>
> # let g : int t = f;;
> val g : int t = <fun>

To my understanding, 
this is an instantiation of the type variable 'a to int,
not subtyping.

Hope this helps.

Keiko NAKATA

Re: [Caml-list] covariance newb question

[Christophe Raffalli]

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

Re: [Caml-list] covariance newb question

[Olivier Andrieu]

 Christophe Raffalli [Monday 28 November 2005] :
 > first 'a -> 'b is covariant in 'a and contravariant in 'b and Ocaml

It's the opposite (contravariant in 'a, covariant in 'b) :

,----
| # type (+'a, -'b) t = 'a -> 'b  ;;
| Characters 5-28:
|   type (+'a, -'b) t = 'a -> 'b  ;;
|        ^^^^^^^^^^^^^^^^^^^^^^^
| In this definition, expected parameter variances are not satisfied.
| The 1st type parameter was expected to be covariant,
| but it is contravariant
| # type (-'a, +'b) t = 'a -> 'b  ;;
| type ('a, 'b) t = 'a -> 'b
`----

-- 
   Olivier