From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 EF888BBFA for ; Mon, 20 Jun 2005 18:06:19 +0200 (CEST) Received: from 26.mail-out.ovh.net (26.mail-out.ovh.net [213.186.42.179]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j5KG6JjY008102 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Mon, 20 Jun 2005 18:06:19 +0200 Received: (qmail 28110 invoked by uid 503); 20 Jun 2005 16:06:20 -0000 Received: (QMFILT: 1.0); 20 Jun 2005 16:06:19 -0000 Received: from b6.ovh.net (HELO mail155.ha.ovh.net) (213.186.33.56) by 26.mail-out.ovh.net with DES-CBC3-SHA encrypted SMTP; 20 Jun 2005 16:06:19 -0000 Received: from b0.ovh.net (HELO queue-out) (213.186.33.50) by b0.ovh.net with SMTP; 20 Jun 2005 16:06:13 -0000 Received: from mail155.ha.ovh.net (10.0.50.155) by mail155.ha.ovh.net with DES-CBC3-SHA encrypted SMTP; 20 Jun 2005 16:06:12 -0000 Received: from b0.ovh.net (HELO queue-pre) (213.186.33.50) by b0.ovh.net with SMTP; 20 Jun 2005 16:06:12 -0000 Received: from adsl-69-108-231-183.dsl.scrm01.pacbell.net (HELO ?192.168.1.103?) (postmaster%glondu.net@69.108.231.183) by ns0.ovh.net with SMTP; 20 Jun 2005 16:06:12 -0000 From: Stephane Glondu To: caml-list@yquem.inria.fr Subject: Re: [Caml-list] signature and 'a generic types Date: Mon, 20 Jun 2005 09:06:03 -0700 User-Agent: KMail/1.7.1 References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset="utf-8" Content-Transfer-Encoding: 7bit Content-Disposition: inline Message-Id: <200506200906.03718.steph@glondu.net> X-Ovh-Remote: 69.108.231.183 (adsl-69-108-231-183.dsl.scrm01.pacbell.net) X-Ovh-Local: 213.186.33.20 (ns0.ovh.net) X-Miltered: at concorde with ID 42B6E97B.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 damien:01 sig:01 val:01 func:01 struct:01 func:01 subtype:01 sig:01 val:01 struct:01 ocamlc:01 subtype:01 intuitively:01 terminate:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: On Monday 20 June 2005 08:20, Damien Bobillot wrote: > Hello, > > Look at the following code : > > module Module : (sig val func : 'a -> 'b end) = > struct let func a = a end > > Here Module.func's type is 'a -> 'a. According to me 'a -> 'a is a > subtype of 'a -> 'b, it's 'a -> 'b with 'a = 'b. It is not relevant. To write this, every 'a -> 'a object must be seeable as a 'a -> 'b object, which is obviously wrong (otherwise, e.g. func 0 would have any type). > I also try to use the reverse match : > > module Module : (sig val func : 'a -> 'a end) = struct > let l = ref [] > let func a = List.assoc a !l > end > > Where Module.func is of type 'a -> 'b. Ocamlc also give me an error, > but I completely understand it here : 'a -> 'b is really not a > subtype of 'a -> 'a. Again, the explanation is not relevant. Here, func is not of type 'a -> 'b, but '_a -> '_b instead, that means that the first usage of func will freeze the type (you won't be able to use func 4, then func true). It happens every time you use references. Otherwise, you could write e.g. l := [(1,1)]; func true. > In this case I also don't understand why neither " 'a -> 'b is > included in 'a -> 'a " nor " 'a -> 'a is included in 'a -> 'b " are > true. To my mind, one should be true. 'a -> 'b is included in 'a -> 'a, but not the contrary (intuitively, functions of the first type don't terminate properly, e.g. let f a = raise Exit). Stephane Glondu.