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.