From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBGAGWtX030912 for ; Fri, 16 Dec 2011 11:16:32 +0100 X-IronPort-AV: E=Sophos;i="4.71,362,1320620400"; d="scan'208";a="135706461" Received: from arbois.inria.fr (HELO [128.93.11.104]) ([128.93.11.104]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 16 Dec 2011 11:16:27 +0100 Message-ID: <4EEB1A7A.6030906@inria.fr> Date: Fri, 16 Dec 2011 11:16:26 +0100 From: Didier Remy Reply-To: Didier.Remy@inria.fr Organization: INRIA Rocquencourt User-Agent: Mozilla/5.0 (X11; U; Linux x86_64; en-US; rv:1.9.2.23) Gecko/20110921 Thunderbird/3.1.15 MIME-Version: 1.0 To: caml-list@inria.fr References: In-Reply-To: Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] The value restriction On 12/16/2011 10:39 AM, Gabriel Scherer wrote: > The following example, derived from yours, is probably more surprised (I didn't > understand your issue at first): > > # ((fun a -> a), (fun b -> b));; > - : ('a -> 'a) * ('b -> 'b) = (, ) > # ((fun a -> a), (fun b -> b) (fun c -> c));; > - : ('_a -> '_a) * ('_b -> '_b) = (, ) > > Here is how I explain this from the paper "Relaxing the value restriction", > Jacques Garrigue, 2004: > http://caml.inria.fr/about/papers.en.html > No guarantee that this matches the actual typing behavior. > > There are two different typing rules: one for the form "let x = v in e", where a > value is bound, all typing variables are generalized, and one other for the form > "let x = e1 in e2", where an *expression* is bound, and all non-negative > variables are generalized. > > In the ((fun a -> a), (fun b -> b)) example, this is a value, everything gets > generalized. In the ((fun a -> a), (fun b -> b) (fun c -> c)) example, this is > not a value anymore, and both components use a type variable in negative > position, so nothing gets generalized. In the ([], (fun b -> b) (fun c -> c)) > example, this is not a value but [] is covariant in its type variable, so it > still gets generalized. Yes, this is the reason. The only influence of the second component is that the pair itself is not a value, in both cases. The differences you observed is only due to the differences in the (types of the) first component. Perhaps, you expected that the type of first component of the pair could be generalized in both cases because it is a value. There is a known improvement of the value restriction that would allow this generalization: the rule would say "type variables appearing in the type of *expansive* expressions cannot be generalized". Intuitively, expansive expressions are expressions whose evaluation could allocate a piece of mutable store. In the example above the pair itself is non expansive (it is a constructor), the first component is not expansive (it is a value); only the second component is expansive (it is an application). Hence, only type variables appearing in the second component cannot be generalized. However, this improvement is not implemented in OCaml. Didier