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

[Ben Millwood <bmillwood@janestreet.com>]

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

I protected against that in my module by carrying the existential type
variable in the result of input_line as well, because I stumbled into
exactly that example while originally drafting my e-mail :)

In a sense I'm reinventing monadic IO but in a bit of a half-hearted way.
It wouldn't take much work to make it a bit more fully-hearted, but it
would still be inconvenient to actually use.


On 8 August 2014 16:44, Markus Mottl <markus.mottl@gmail.com> wrote:

> It doesn't even require references to screw things up here.  Just
> return the closure containing the channel from within "f":
>
>   In_channel.with_file "foo.txt" ~f:(fun ic () -> input_line ic)
>   |> fun f -> f ()
>
> The initial Stream-example is basically just an instance of this
> "returning a closure" problem.
>
> But the availability of references and exceptions arguably makes
> things worse, because you cannot even use monadic I/O + existential
> types to achieve guaranteed safety.
>
> Regards,
> Markus
>
> On Fri, Aug 8, 2014 at 10:49 AM, Ben Millwood <bmillwood@janestreet.com>
> wrote:
> > 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.
> >>>
> >>
> >
>
>
>
> --
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com
>

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