From mboxrd@z Thu Jan 1 00:00:00 1970 X-Sympa-To: caml-list@inria.fr 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 q0AGWHMp028750 for ; Tue, 10 Jan 2012 17:32:17 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjoDAPtmDE/RVdS2kGdsb2JhbABDhQ+XGIghAYgICCIBAQEBCQkNBxQEIYFyAQEBAwESAg8EGQEtCwEDAQsBBQMCCxodAgIiEgEFAQoSBhMIChCHWAiaDAqLIoM3hFyJMAIFC4NyhwCBFgSCW5IxjgM9gU1/gS8 X-IronPort-AV: E=Sophos;i="4.71,487,1320620400"; d="scan'208";a="126288136" Received: from mail-wi0-f182.google.com ([209.85.212.182]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Jan 2012 17:32:11 +0100 Received: by wibhr1 with SMTP id hr1so6811672wib.27 for ; Tue, 10 Jan 2012 08:32:11 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:cc:content-type; bh=+xd2Ar5WpG9eazMhJrFEUu8FY8cgTgIU8sLC/jxFV5s=; b=QZrR/S411P3ub9EFjcu0AECKo1zTV0uWURTn4O6aTy5QLAzwtkbcATfod7sho+/vrE kGlUGVZqVwk+/N8Rz2vVMEUi+0/lU/MEssSpk7xsPFRxn1Wijv6J/yJ9MTKI+v8RLxqu smAJRGwaa1+esmhMtIEzlgypPu9wAQhMJb3bs= Received: by 10.180.77.136 with SMTP id s8mr13100382wiw.0.1326213131760; Tue, 10 Jan 2012 08:32:11 -0800 (PST) MIME-Version: 1.0 Sender: arnaud.spiwack@gmail.com Received: by 10.227.112.137 with HTTP; Tue, 10 Jan 2012 08:31:18 -0800 (PST) In-Reply-To: <4F0C5D33.7030405@lsv.ens-cachan.fr> References: <1326209342.96423.YahooMailNeo@web111502.mail.gq1.yahoo.com> <4F0C5D33.7030405@lsv.ens-cachan.fr> From: Arnaud Spiwack Date: Tue, 10 Jan 2012 17:31:18 +0100 X-Google-Sender-Auth: HoY0SgBwLc6Ni6INIJnCvlK9x68 Message-ID: To: Romain Bardou Cc: caml-list@inria.fr Content-Type: multipart/alternative; boundary=f46d043c80ee9d74f304b62f0eea X-Validation-by: aspiwack@lix.polytechnique.fr Subject: Re: [Caml-list] References and polymorphism --f46d043c80ee9d74f304b62f0eea Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I guess a canonical example of the reason behind this restriction would be the following: let put =3D let r =3D ref [] in fun x -> r :=3D x::!r OCaml will tell you that it has type '_a -> unit. It would be unsound (exercise!) to decide it has type 'a -> unit. Of course, your example is perfectly sound, but the typing algorithm doesn't know that. -- Arnaud Spiwack On 10 January 2012 16:45, Romain Bardou wrote: > Le 10/01/2012 16:29, Dario Teixeira a =C3=A9crit : > > Hi, >> >> Consider functions foobar1 and foobar2: >> >> >> type 'a t =3D {id: int; x: 'a} >> >> let foobar1: 'a -> 'a t =3D >> fun x -> {id =3D 0; x} >> >> let foobar2: 'a -> 'a t =3D >> let ctr =3D ref 0 in >> fun x -> incr ctr; {id =3D !ctr; x} >> >> >> >> I would expect them to have the same type, because foobar2's >> use of a reference cell is kept private. However, they don't. >> In fact, foobar2 is not really polymorphic: >> >> >> type 'a t =3D { id : int; x : 'a; } >> val foobar1 : 'a -> 'a t >> val foobar2 : '_a -> '_a t >> >> >> It's easy to get around this issue by putting the reference cell >> outside of foobar2. Function foobar3 does just this, and behaves >> as expected: >> >> >> let next =3D >> let ctr =3D ref 0 in >> fun () -> incr ctr; !ctr >> >> let foobar3: 'a -> 'a t =3D >> fun x -> {id =3D next (); x} >> >> >> >> Could someone point me to a good explanation of what's going on? >> (I have the feeling I've read about this restriction before.) >> >> Best regards, >> Dario Teixeira >> >> >> >> > Hello, > > This is, basically, the value restriction: you cannot let-generalize > something which is not *syntactically* a value. Function foobar1 is > syntactically a function, and a function is a value. Function foobar2 is > not: it starts with a let-binding. It computes something before returning= a > function. It cannot be generalized. > > Cheers, > > -- > Romain Bardou > > > -- > 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 > > --f46d043c80ee9d74f304b62f0eea Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable I guess a canonical example of the reason behind this restriction would be = the following:

let put =3D let r =3D ref [] in fun x -> r :=3D x:= :!r

OCaml will tell you that it has type '_a -> unit. It woul= d be unsound (exercise!) to decide it has type 'a -> unit.

Of course, your example is perfectly sound, but the typing algorithm do= esn't know that.

--
Arnaud Spiwack

On 10 January 2012 16:45, Romain Bardou <bardou@lsv.ens-cachan.fr> wrote:
Le 10/01/2012 16:29, Dario Teixeira a =C3=A9= crit :

Hi,

Consider functions foobar1 and foobar2:


type 'a t =3D {id: int; x: 'a}

let foobar1: 'a -> =C2=A0'a t =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fun x -> =C2=A0{id =3D 0; x}

let foobar2: 'a -> =C2=A0'a t =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 let ctr =3D ref 0 in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fun x -> =C2=A0incr ctr; {id =3D !ctr; x}


I would expect them to have the same type, because foobar2's
use of a reference cell is kept private. =C2=A0However, they don't.
In fact, foobar2 is not really polymorphic:


type 'a t =3D { id : int; x : 'a; }
val foobar1 : 'a -> =C2=A0'a t
val foobar2 : '_a -> =C2=A0'_a t


It's easy to get around this issue by putting the reference cell
outside of foobar2. =C2=A0Function foobar3 does just this, and behaves
as expected:


let next =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 let ctr =3D ref 0 in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fun () -> =C2=A0incr ctr; !ctr

let foobar3: 'a -> =C2=A0'a t =3D
=C2=A0 =C2=A0 =C2=A0 =C2=A0 fun x -> =C2=A0{id =3D next (); x}



Could someone point me to a good explanation of what's going on?
(I have the feeling I've read about this restriction before.)

Best regards,
Dario Teixeira




Hello,

This is, basically, the value restriction: you cannot let-generalize someth= ing which is not *syntactically* a value. Function foobar1 is syntactically= a function, and a function is a value. Function foobar2 is not: it starts = with a let-binding. It computes something before returning a function. It c= annot be generalized.

Cheers,

--
Romain Bardou


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


--f46d043c80ee9d74f304b62f0eea--