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

[Markus Mottl <markus.mottl@gmail.com>]

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