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.
>>
>>
>