On 10 January 2012 16:45, Romain Bardou
<bardou@lsv.ens-cachan.fr> wrote:
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
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