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

[Ben Millwood <bmillwood@janestreet.com>]

[-- Attachment #1: Type: text/plain, Size: 3023 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 4001 bytes --]