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.