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 : > 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 > 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 >> >> 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 > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com >