covariance newb question

Christophe Papazian
 Keiko Nakata
 Christophe Raffalli
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20051127 (23:30) 
From:  Christophe Raffalli <raffalli@u...> 
Subject:  Re: [Camllist] covariance newb question 
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 > > _______________________________________________ > Camllist mailing list. Subscription management: > http://yquem.inria.fr/cgibin/mailman/listinfo/camllist > Archives: http://caml.inria.fr > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/camlbugs