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.