Aleksey Nogin wrote:
> On 31.10.2008 07:57, Martin Jambon wrote:
> 
>> let x = (1, 2);;
>> let wa = Weak.create 10;;
>> Weak.set wa 0 (Some x);;
>> ...
>> print_int (fst x);;
>>
>> (fst x) would certainly cause funny effects if x were GC'ed at an
>> arbitrary time after it has been added to the weak array.
>>
>> An object can be reclaimed by the GC only if there is no reference to
>> it. This remains true. Adding an object to a weak array just doesn't
>> count as a reference.
>>
> Martin,
> 
> You are answering the wrong question - you are answering "could x be
> GCed too early?" - the answer is obviously "no". However, the initial
> question was "could (Some x) be removed from wa too early by GC - before
> x is orphaned?" The answer is "we'd hope not", but the documentation is
> somewhat ambiguous.

OK. I think now I understand the question :-)
And we all agree that the documentation could be clearer.

What I'm wondering is why there is one Weak.set function that takes an
option as argument rather than a pair Weak.set/Weak.clear.

What is certain is that some (re)boxing is done by Weak.get:

# let a = Weak.get wa 0;;
val a : (int * int) option = Some (1, 2)
# let b = Weak.get wa 0;;
val b : (int * int) option = Some (1, 2)
# a == b;;
- : bool = false

Of course it doesn't tell whether the original (Some x) is stored as-is
but copied by Weak.get or if x is stored unwrapped.

I think I'll just take a look at the implementation. That can only be a
good thing.


Martin
-- 
http://mjambon.com/