Re: [Caml-list] Not letting channels escape.

[Markus Mottl <markus.mottl@gmail.com>]

It doesn't even require references to screw things up here.  Just
return the closure containing the channel from within "f":

  In_channel.with_file "foo.txt" ~f:(fun ic () -> input_line ic)
  |> fun f -> f ()

The initial Stream-example is basically just an instance of this
"returning a closure" problem.

But the availability of references and exceptions arguably makes
things worse, because you cannot even use monadic I/O + existential
types to achieve guaranteed safety.

Regards,
Markus

On Fri, Aug 8, 2014 at 10:49 AM, Ben Millwood <bmillwood@janestreet.com> wrote:
> It's been pointed out to me that the above certainly isn't perfectly secure.
> E.g.
>
> let f = ref (fun () -> ()) in
> with_file "safe.ml" ~f:{ f = fun c ->
>   return (f := fun () ->
>     Fn.ignore (map (input_line c) ~f:print_string_option)) };
> !f ()
>
> gets Exception: (Sys_error "Bad file descriptor"). Even though the channel
> and any operations on it can't escape the closure, the type of a function
> which uses them needn't mention them at all.
>
> It's pretty hard to do anything about this in the presence of unrestricted
> side effects, so perhaps there's a reason why the Haskellers are excited
> about this sort of thing and you don't see it in OCaml so much :)
>
> That said, you do seem to be forced to make a bit more of an effort to break
> things here, so I don't think the technique is completely without merit,
> perhaps in cases where you'd be defining all your own operations anyway, so
> the duplication isn't an issue.
>
>
> On 8 August 2014 12:30, Ben Millwood <bmillwood@janestreet.com> wrote:
>>
>> There's a trick with existential types, as used in e.g. Haskell's ST
>> monad. It uses the fact that an existentially-quantified type variable can't
>> escape its scope, so if your channel type and results that depend on it are
>> parametrised by an existential type variable, the corresponding values can't
>> escape the scope of the callback either.
>>
>> Something like:
>>
>> module ST : sig
>>   type ('a, 's) t
>>   include Monad.S2 with type ('a, 's) t := ('a, 's) t
>>   type 's chan
>>   type 'a f = { f : 's . 's chan -> ('a, 's) t }
>>   val with_file : string -> f:'a f -> 'a
>>
>>   val input_line : 's chan -> (string option, 's) t
>> end = struct
>>   module T = struct
>>     type ('a, 's) t = 'a
>>     let return x = x
>>     let bind x f = f x
>>     let map x ~f = f x
>>   end
>>   include T
>>   include Monad.Make2(T)
>>   type 's chan = In_channel.t
>>   type 'a f = { f : 's . 's chan -> ('a, 's) t }
>>   let with_file fp ~f:{ f } = In_channel.with_file fp ~f
>>   let input_line c = In_channel.input_line c
>> end
>> ;;
>>
>> match ST.with_file "safe.ml" ~f:{ ST.f = fun c -> ST.input_line c } with
>> | None -> print_endline "None"
>> | Some line -> print_endline line
>>
>>
>> On 8 August 2014 11:23, Philippe Veber <philippe.veber@gmail.com> wrote:
>>>
>>> Dear all,
>>>
>>> many libraries like lwt, batteries or core provide a very nice idiom to
>>> be used when a function uses a resource (file, connection, mutex, et
>>> cetera), for instance in Core.In_channel, the function:
>>>
>>> val with_file : ?binary:bool -> string -> f:(t -> 'a) -> 'a
>>>
>>> opens a channel for [f] and ensures it is closed after the call to [f],
>>> even if it raises an exception. So these functions basically prevent from
>>> leaking resources. They fail, however, to prevent a user from using the
>>> resource after it has been released. For instance, writing:
>>>
>>> input_char (In_channel.with_file fn (fun x -> x))
>>>
>>> is perfectly legal type-wise, but will fail at run-time. There are of
>>> course less obvious situations, for instance if you define a function:
>>>
>>> val lines : in_channel -> string Stream.t
>>>
>>> then the following will also fail:
>>>
>>> Stream.iter f (In_channel.with_file fn lines)
>>>
>>> My question is the following: is there a way to have the compiler check
>>> resources are not used after they are closed? I presume this can only be
>>> achieved by strongly restricting the kind of function passed to [with_file].
>>> One simple restriction I see is to define a type of immediate value, that
>>> roughly correspond to "simple" datatypes (no closures, no lazy expressions):
>>>
>>> module Immediate : sig
>>>   type 'a t = private 'a
>>>   val int : int -> int t
>>>   val list : ('a -> 'a t) -> 'a list -> 'a list t
>>>   val tuple : ('a -> 'a t) -> ('b -> 'b t) -> ('a * 'b) -> ('a * 'b) t
>>>   (* for records, use the same trick than in
>>> http://www.lexifi.com/blog/dynamic-types *)
>>>   ...
>>> end
>>>
>>> and have the type of [with_file] changed to
>>>
>>> val with_file : string -> f:(in_channel -> 'a Immediate.t) -> 'a
>>>
>>> I'm sure there are lots of smarter solutions out there. Would anyone
>>> happen to know some?
>>>
>>> Cheers,
>>>   Philippe.
>>>
>>
>



-- 
Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com