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