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