From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id DB472BB81 for ; Mon, 28 Nov 2005 00:30:34 +0100 (CET) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jARNUX2x003368 for ; Mon, 28 Nov 2005 00:30:34 +0100 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id AAA01123 for ; Mon, 28 Nov 2005 00:30:33 +0100 (MET) Received: from smtp.cegetel.net (217-19-192-72.dti.cegetel.net [217.19.192.72]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id jARNUWXv003347 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=FAIL) for ; Mon, 28 Nov 2005 00:30:32 +0100 Received: from [192.168.144.128] (80-125-86-59.adslgp.cegetel.net [80.125.86.59]) by smtp.cegetel.net (Postfix) with ESMTP id DB98B1A40C9; Mon, 28 Nov 2005 00:30:31 +0100 (CET) Message-ID: <438A41B5.3060206@univ-savoie.fr> Date: Mon, 28 Nov 2005 00:31:01 +0100 From: Christophe Raffalli User-Agent: Mozilla Thunderbird 1.0.6 (Macintosh/20050716) X-Accept-Language: fr, en MIME-Version: 1.0 To: Christophe Papazian Cc: caml-list@inria.fr Subject: Re: [Caml-list] covariance newb question References: <5FABF242-1101-4499-8CF5-CF1559F6EECC@essi.fr> In-Reply-To: <5FABF242-1101-4499-8CF5-CF1559F6EECC@essi.fr> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 8bit X-Miltered: at concorde with ID 438A419A.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 438A4198.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 raffalli:01 univ-savoie:01 caml-list:01 covariance:01 christophe:01 trivial:01 ocaml:01 compiler:01 polymorphism:01 subtyping:01 val:01 val:01 polymorphism:01 X-Spam-Checker-Version: SpamAssassin 3.0.3 (2005-04-27) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.3 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 = > # let g : int t = f;; > val g : int t = > 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