From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 87704BBFA for ; Tue, 21 Jun 2005 00:31:53 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j5KMVq4Y013643 for ; Tue, 21 Jun 2005 00:31:53 +0200 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 AAA21720 for ; Tue, 21 Jun 2005 00:31:52 +0200 (MET DST) Received: from us17.unix.fas.harvard.edu ([140.247.35.197]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j5KMVVgC014021 for ; Tue, 21 Jun 2005 00:31:52 +0200 Received: from localhost (us31.unix.fas.harvard.edu [140.247.35.251]) by us17.unix.fas.harvard.edu (8.12.11/8.12.11) with ESMTP id j5KMVBFQ007014; Mon, 20 Jun 2005 18:31:11 -0400 Received: from tide519.microsoft.com (tide519.microsoft.com [131.107.0.89]) by webmail.fas.harvard.edu (IMP) with HTTP for ; Mon, 20 Jun 2005 18:31:11 -0400 Message-ID: <1119306671.42b743af64539@webmail.fas.harvard.edu> Date: Mon, 20 Jun 2005 18:31:11 -0400 From: Michael Alexander Hamburg To: Damien Bobillot Cc: caml-list@inria.fr Subject: Re: [Caml-list] signature and 'a generic types References: In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 8bit User-Agent: Internet Messaging Program (IMP) 3.2.5 X-Originating-IP: 131.107.0.89 X-Miltered: at nez-perce with ID 42B743D8.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 42B743C3.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 quoting:01 damien:01 damien:01 sig:01 val:01 func:01 struct:01 func:01 subtype:01 ocamlc:01 val:01 subtype:01 compiler:01 ocaml: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: Quoting Damien Bobillot : > 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. Nevertheless ocamlc > give the following error : > > Values do not match: > val func : 'a -> 'a > is not included in > val func : 'a -> 'b > > Why ? > The module signature requires that the function have type 'a -> 'b for all 'a and 'b, i.e. the declared type must be a subtype of the actual type, not vice versa. Imagine if the compiler let you use that module definition, someone calling the module would be able to say "hello" ^ Module.func 1, and OCaml would try to treat 1 as a string because func is declared to have type 'a -> 'b. > 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. Ah, but the function you declared is not of type 'a -> 'b but rather of type '_a -> '_b, because ref [] does not refer to _every_type_ ('a ref), but rather _one_single_type_ ('_a ref). This is the infamous "value polymorphism restriction". Here's why it's there: let l = ref [] (* type of l is '_a list ref, not 'a list ref *) let () = l := ["hello"] (* if there were no VPR, l would still have type 'a list ref here, but because it has one single type, it is now a string list ref *) let x = 1+List.head !l (* if there were no VPR, this would be allowed, and try to compute 1+"hello" *) let () = l := [7] (* this is also disallowed by the type of l. You can't get it back to being an '_a list ref *) In any case, 'a -> 'a is not a subtype of '_a -> '_b. If your func had been Obj.magic, or a -> List.assoc a [], or a -> failwith "Hello world", it would have worked (I think, I don't have OCaml in front of me). > 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. > > Is it a caml limitation/bug, or am I wrong somewhere ? Sort of. First, the VPR is somewhat more restrictive than it has to be for type safety, but analyzing exactly how restrictive is has to be in a particular case is hard (very hard in this case; it's hard for the compiler to know that a particular piece of mutable state will never be mutated anywhere), and would require extra notation to avoid breaking across module boundaries. The current restriction is sort of a happy medium. Second, in OCaml, polymorphic types are abbreviated. "'a -> 'a" is an abbreviation of "for all types 'a, 'a -> 'a", whereas "'_a -> '_a" is an abbrevation of "for one single arbitrary type 'a, 'a -> 'a". These abbreviations are somewhat confusing. They also assume knowledge of a restriction of so-called Hindley-Milner types, which is that all the "forall"s go out in front. This restriction is required for automatic type detection to be computable, so it can be lifted only if the user specifies the type. For some reason, in OCaml the syntax only allows you to do this in record declarations, which could probably be considered a "limitation/bug". Mike Hamburg > -- > Damien Bobillot > >