From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id pBG9dr4O029368 for ; Fri, 16 Dec 2011 10:39:53 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: At8CALoQ605KfVIqimdsb2JhbABDh3aTIYgZAYcNgQ4IIgEBAQoJDQcSBiGBcgEBAQMBEgITGQEbEgsBAwELBgUEBxohIgERAQUBChIGExIQh1gIm3AKi2WCa4R1P4hxAgULg26ICwSCWZIdjXY9gkuBLg X-IronPort-AV: E=Sophos;i="4.71,362,1320620400"; d="scan'208";a="123616241" Received: from mail-ww0-f42.google.com ([74.125.82.42]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 16 Dec 2011 10:39:48 +0100 Received: by wgbds13 with SMTP id ds13so2693906wgb.3 for ; Fri, 16 Dec 2011 01:39:48 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=ugelEOwEmqprz0qPgHh72kY0WUrTD6FqTKr42Sj3DMk=; b=AZVIuc+Pbqn9TaIBFw33aCsaiGaERXZB7tbZt7GsDY84woWjM+hbvwoYpMxRuThjg9 PQbywgHXVv0glYSfF3oee5ZQHDnelyBkgBOyyQ7PJhnfA87puust39EOE7DuGGcvMtHz Hs/CPR8ukdk3GI186qB9tahi3jx7QdGH0Xtpk= Received: by 10.180.3.37 with SMTP id 5mr10967077wiz.43.1324028387191; Fri, 16 Dec 2011 01:39:47 -0800 (PST) MIME-Version: 1.0 Received: by 10.227.43.4 with HTTP; Fri, 16 Dec 2011 01:39:26 -0800 (PST) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 16 Dec 2011 10:39:26 +0100 Message-ID: To: Andrej Bauer Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d0413916bb0eb0a04b43261d0 Subject: Re: [Caml-list] The value restriction --f46d0413916bb0eb0a04b43261d0 Content-Type: text/plain; charset=ISO-8859-1 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. On Fri, Dec 16, 2011 at 10:18 AM, Andrej Bauer wrote: > Can someone explain this behavior? > > # ([], (fun x -> x) (fun y -> y)) ;; > - : 'a list * ('_b -> '_b) = ([], ) > > # ((fun a -> a), (fun x -> x) (fun y -> y)) ;; > - : ('_a -> '_a) * ('_b -> '_b) = (, ) > > Why does the second component influence the first one (in a non-obvious > way)? > > With kind regards, > > Andrej > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa-roc.inria.fr/wws/info/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > > --f46d0413916bb0eb0a04b43261d0 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable The following example, derived from yours, is probably more surprised (I di= dn't understand your issue at first):

=A0 # ((fun a -> a), (f= un b -> b));;
=A0 - : ('a -> 'a) * ('b -> 'b) = =3D (<fun>, <fun>)
=A0 # ((fun a -> a), (fun b -> b) (fun c -> c));;
=A0 - : ('= ;_a -> '_a) * ('_b -> '_b) =3D (<fun>, <fun>)=

Here is how I explain this from the paper "Relaxing the value = restriction", Jacques Garrigue, 2004:
=A0 http://caml.inria= .fr/about/papers.en.html
No guarantee that this matches the actual t= yping behavior.

There are two different typing rules: one for the fo= rm "let x =3D v in e", where a value is bound, all typing variabl= es are generalized, and one other for the form "let x =3D e1 in e2&quo= t;, where an *expression* is bound, and all non-negative variables are gene= ralized.

In the ((fun a -> a), (fun b -> b)) example, this is a value, eve= rything 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 ty= pe variable in negative position, so nothing gets generalized. In the ([], = (fun b -> b) (fun c -> c)) example, this is not a value but [] is cov= ariant in its type variable, so it still gets generalized.


On Fri, Dec 16, 2011 at 10:18 AM, Andrej= Bauer <and= rej.bauer@andrej.com> wrote:

--
Caml-list mailing list. =A0Subscription management and archives:
https://sympa-roc.inria.fr/wws/info/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs


--f46d0413916bb0eb0a04b43261d0--