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

[Philippe Veber <philippe.veber@gmail.com>]

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

Thanks everyone for these particularly instructive answers! Now I
understand better why things are the way they are in OCaml. The litterature
on linear types also seems very interesting, thanks again!


2014-08-08 22:34 GMT+02:00 Markus Mottl <markus.mottl@gmail.com>:

> That's how the state monad should be correctly implemented :-)
>
> Only "with_file" should be able to actually run the monadic
> computation and execute its side effects.
>
> On Fri, Aug 8, 2014 at 3:45 PM, 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
>
>
>
> --
> Markus Mottl        http://www.ocaml.info        markus.mottl@gmail.com
>

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