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

[Ben Millwood <bmillwood@janestreet.com>]

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

Yeah, that's roughly what I had in mind for a full-hearted approach,
although it turned out to be a bit simpler than I was expecting. Sorry, I
think my original not-quite-right approach probably only confused the issue
:)

Much more on the Haskell approaches:
http://okmij.org/ftp/Haskell/regions.html

I believe not all of them use type classes in an essential way, so may well
be translatable to OCaml.


On 8 August 2014 20:45, Frédéric Bour <frederic.bour@lakaban.net> wrote:

> But you can't do any meaningful computation with this value.
> It's just a blackbox.
>
> In your example, the (ST.input_line c) inside the closure just build a
> value of type (string option, '_s) t for a specific s.
> In particular you will never be able to execute any action on the input
> channel.
>
> This is not the case with the proposed implementation, because effects are
> executed immediately.
> To ensure isolation, all effects should be "frozen":
>
> module ST : sig
>   type ('a, 's) t
>   val return : 'a -> ('a, 's) t
>   val bind : ('a, 's) t -> ('a -> ('b, 's) t) -> ('b, '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, 's) t
> end = struct
>   type ('a, 's) t = unit -> 'a
>   let return x = fun () -> x
>   let bind x f = fun () -> f (x ()) ()
>
>   type 's chan = in_channel
>   type 'a f = { f : 's . 's chan -> ('a, 's) t }
>   let with_file fp ~f:{ f } =
>     let ic = open_in fp in
>     try
>       let result = f ic () in
>       close_in_noerr ic;
>       result
>     with exn ->
>       close_in_noerr ic;
>       raise exn
>   let input_line c = fun () -> input_line c
> end
>
> Le ven. 8 août 2014 à 20:30, Markus Mottl <markus.mottl@gmail.com> a
> écrit :
>
> The escaping value can still be manipulated through a closure, outside of
> "with_file". The goal was to prevent this. On Fri, Aug 8, 2014 at 2:28 PM,
> Frédéric Bour <frederic.bour@lakaban.net> wrote:
>
> ST.input_line is just a reified effect, it can't be executed outside of
> the ST monad. You can make the value escape, but you can't do anything with
> it. And because of the existential variable being propagated, it can't be
> executed outside of this run of the ST value. Le ven. 8 août 2014 à 19:23,
> Markus Mottl <markus.mottl@gmail.com> a écrit : How would you implement
> this safely with ST here? I wasn't using the standard input_line but
> "ST.input_line", which already returns a monadic type. The trick here was
> to use the monadic "return" to return a closure that captures the
> existential variable, allowing me to execute the computation outside of the
> safe region. Regards, Markus On Fri, Aug 8, 2014 at 1:37 PM, Gabriel
> Scherer <gabriel.scherer@gmail.com> wrote: The ST trick only works when
> all primitives affecting resource are in the monadic abstraction (they
> mention the ST region variable in their computation type). This is not the
> case in Markus example as "input_line" is a non-typed effect. Using ST
> safely would be possible in OCaml, but you would have to completely eschew
> the standard library and use a different base where all effectful functions
> have a monadic type. It is the library, not the language itself, that
> allows this. On the contrary, linear types are distinctly a language
> feature. Using monads to encapsulate a form of linearity is an old trick.
> If you want to have a taste of built-in linear typing, you may want to give
> Mezzo a try ( http://protz.github.io/mezzo/ ). On Fri, Aug 8, 2014 at
> 7:21 PM, Markus Mottl <markus.mottl@gmail.com> wrote: I see, I was
> replying to the "reference problem" and hadn't read your implementation,
> which, besides existentials, already requires monads as return values.
> Actually, it just occurred to me that one can even break the monadic
> approach in a purely functional way. You are just one "return" away from
> disaster: let f = ST.with_file "foo.txt" ~f:{ ST.f = fun c -> ST.return
> (fun () -> ignore (ST.input_line c)) } in f () You'd have to eliminate
> "return", in which case it wouldn't be a monad anymore and not general
> enough for realistic uses of "with_file". Regards, Markus On Fri, Aug 8,
> 2014 at 12:01 PM, Ben Millwood <bmillwood@janestreet.com> wrote: > 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 > > -- Markus Mottl http://www.ocaml.info
> markus.mottl@gmail.com -- Caml-list mailing list. Subscription management
> and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list:
> http://groups.yahoo.com/group/ocaml_beginners Bug reports:
> http://caml.inria.fr/bin/caml-bugs -- Markus Mottl http://www.ocaml.info
> markus.mottl@gmail.com -- Caml-list mailing list. Subscription management
> and archives: https://sympa.inria.fr/sympa/arc/caml-list Beginner's list:
> http://groups.yahoo.com/group/ocaml_beginners Bug reports:
> http://caml.inria.fr/bin/caml-bugs
>
> --
> Markus Mottl http://www.ocaml.info markus.mottl@gmail.com
> --
> Caml-list mailing list. Subscription management and archives:
> https://sympa.inria.fr/sympa/arc/caml-list Beginner's list:
> http://groups.yahoo.com/group/ocaml_beginners Bug reports:
> http://caml.inria.fr/bin/caml-bugs
>
>

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