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

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

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