From: Romain Bardou <bardou@lsv.ens-cachan.fr>
To: caml-list@inria.fr
Subject: Re: [Caml-list] References and polymorphism
Date: Tue, 10 Jan 2012 16:45:55 +0100 [thread overview]
Message-ID: <4F0C5D33.7030405@lsv.ens-cachan.fr> (raw)
In-Reply-To: <1326209342.96423.YahooMailNeo@web111502.mail.gq1.yahoo.com>
Le 10/01/2012 16:29, Dario Teixeira a écrit :
> Hi,
>
> Consider functions foobar1 and foobar2:
>
>
> type 'a t = {id: int; x: 'a}
>
> let foobar1: 'a -> 'a t =
> fun x -> {id = 0; x}
>
> let foobar2: 'a -> 'a t =
> let ctr = ref 0 in
> fun x -> incr ctr; {id = !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 = { 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 =
> let ctr = ref 0 in
> fun () -> incr ctr; !ctr
>
> let foobar3: 'a -> 'a t =
> fun x -> {id = 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
next prev parent reply other threads:[~2012-01-10 15:45 UTC|newest]
Thread overview: 19+ messages / expand[flat|nested] mbox.gz Atom feed top
2012-01-10 15:29 Dario Teixeira
2012-01-10 15:45 ` Romain Bardou [this message]
2012-01-10 16:31 ` Arnaud Spiwack
2012-01-10 17:00 ` Dario Teixeira
2012-01-10 17:20 ` David Allsopp
2012-01-10 18:59 ` Gabriel Scherer
2012-01-11 10:48 ` [Caml-list] " Dawid Toton
2012-01-11 11:07 ` Gabriel Scherer
2012-01-11 13:00 ` Dawid Toton
2012-01-11 13:15 ` rossberg
2012-01-11 13:56 ` Dawid Toton
2012-01-11 15:42 ` rossberg
2012-01-12 9:55 ` Dawid Toton
2012-01-12 10:05 ` Andrej Bauer
2012-01-12 10:46 ` Romain Bardou
2012-01-11 11:43 ` rossberg
2012-01-11 13:34 ` Dawid Toton
2012-01-11 15:34 ` rossberg
2012-01-11 13:57 ` Dawid Toton
Reply instructions:
You may reply publicly to this message via plain-text email
using any one of the following methods:
* Save the following mbox file, import it into your mail client,
and reply-to-all from there: mbox
Avoid top-posting and favor interleaved quoting:
https://en.wikipedia.org/wiki/Posting_style#Interleaved_style
* Reply using the --to, --cc, and --in-reply-to
switches of git-send-email(1):
git send-email \
--in-reply-to=4F0C5D33.7030405@lsv.ens-cachan.fr \
--to=bardou@lsv.ens-cachan.fr \
--cc=caml-list@inria.fr \
/path/to/YOUR_REPLY
https://kernel.org/pub/software/scm/git/docs/git-send-email.html
* If your mail client supports setting the In-Reply-To header
via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line
before the message body.
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox