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 0EAC3BB81 for ; Tue, 7 Dec 2004 22:04:22 +0100 (CET) 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 iB7L4LJd004091 for ; Tue, 7 Dec 2004 22:04:21 +0100 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id WAA11281 for ; Tue, 7 Dec 2004 22:04:21 +0100 (MET) Received: from [IPv6:::1] (yquem.inria.fr [128.93.8.37]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id iB7L4KLd004080 for ; Tue, 7 Dec 2004 22:04:21 +0100 Mime-Version: 1.0 (Apple Message framework v619) In-Reply-To: <41B5F1B2.3000503@inria.fr> References: <20041206195527.GA32094@draco.skynet> <41B557D4.2000306@inria.fr> <076FEF06-4856-11D9-8195-000D9345235C@inria.fr> <41B5C4C8.9040701@ps.uni-sb.de> <41B5F1B2.3000503@inria.fr> Content-Type: text/plain; charset=US-ASCII; format=flowed Message-Id: <9296F5C2-4893-11D9-8195-000D9345235C@inria.fr> Content-Transfer-Encoding: 7bit From: Damien Doligez Subject: Re: [Caml-list] Type constraints Date: Tue, 7 Dec 2004 22:04:24 +0100 To: caml users X-Mailer: Apple Mail (2.619) X-Miltered: at nez-perce with ID 41B61AD5.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 41B61AD4.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; damien:01 damien:01 caml-list:01 frisch:01 wrote:01 struct:01 sig:01 val:01 sig:01 val:01 struct:01 generalizing:01 xavier's:01 ...:98 ...:98 X-Spam-Checker-Version: SpamAssassin 3.0.0 (2004-09-13) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.0 X-Spam-Level: On 7 Dec 2004, at 19:08, Alain Frisch wrote: > I still don't understand. Compare: > > # module M = struct let v = ref [] end;; > module M : sig val v : '_a list ref end > # module M : sig val v : 'a -> 'a end = struct let v x = x end;; > module M : sig val v : 'a -> 'a end > > Of course, the type variable in the first example must not be > generalized, and it isn't. In the second example, there is no problem. > We get: > > # M.v;; > - : 'a -> 'a = > > So why not give the same type scheme to: > > let module M : sig val v : 'a -> 'a end = struct let v x = x end in M.v The typing algorithm is very simple (really!): 1. Type the module. Generalization occurs and the v field gets a polymorphic type. 2. Type "M.v". This takes an instance of the polymorphic type. 3. Can we generalize it? Look at the syntactic shape of the expression (in this case, let module ... in ...). If it is always safe to generalize such expressions, OK. If not, do not generalize. That's the beauty of the Wright criterion: it's very easy to implement and to understand (because it is syntactic), and works well in almost all cases (with a little eta-expansion if needed). So the answer to your original question is: the type is not generalized because in some cases the let-module construct is not safely polymorphic. Of course, there must be some criteria for generalizing more expressions. Check out Xavier's thesis for example. They are usually not worth the trouble. -- Damien