On 2008-01-28, at 11:20, Nicolas Pouillard wrote:

> Excerpts from christophe.troestler+ocaml's message of Mon Jan 28  
> 17:06:10 +0100 2008:
>>
>
>> On Mon, 28 Jan 2008 15:25:12 +0000, Jon Harrop wrote:
>>
>>> So you write a "use" binding:
>>>
>>>  let read_first_line file =
>>>    use ch = open_in file in
>>>    input_line ch
>>>
>>> and it gets translated into:
>>>
>>>  let read_first_line file =
>>>    let ch = open_in file in
>>>    try input_line ch finally
>>>    ch#dispose
>>>
>>> where the "dispose" method that was automatically inserted at the  
>>> end of the
>>> scope of the "use" binding calls "close_in" in this case to  
>>> deallocate the
>>> external resource (a file handle in this case but it could be  
>>> anything with a
>>> dispose method).
>>
>> What is wrong with
>>
>>   let read_first_line file =
>>     with_open_in file begin fun ch ->
>>       input_line ch
>>     end
>
> This  code  has  nothing  wrong but with_open_in (even if it's very  
> useful) is
> not resource safe. This is because the in_channel can escape it's  
> scope.
>
> | let ch = with_open_in file (fun x -> x) in
> | input_line ch
>
> This program is obviously wrong but still show that with_open_in is  
> not safe.


This argument applies equally to Pervasives.close_in. Allowing the  
programmer to control the deallocation of external resources is much  
more important than attempting to prevent her from performing an  
invalid operation via a deallocated handle.

— Gordon