[Caml-list] Not letting channels escape.

[Caml-list] Not letting channels escape.

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 1758 bytes --]

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.

[-- Attachment #2: Type: text/html, Size: 2156 bytes --]

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

[Peter Zotov]

On 2014-08-08 14:23, Philippe Veber wrote:
> Dear all,
> 
> My question is the following: is there a way to have the compiler
> check resources are not used after they are closed?

Linear types[1] are designed to enforce this invariant. They're used
in e.g. Rust, Cyclone or LinearML.

[1]: http://c2.com/cgi/wiki?LinearTypes

-- 
Peter Zotov

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 3023 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 4001 bytes --]

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 4135 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 5575 bytes --]

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

[Markus Mottl]

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

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 5685 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 8144 bytes --]

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

[Markus Mottl]

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

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

[Gabriel Scherer]

[-- Attachment #1: Type: text/plain, Size: 8160 bytes --]

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
>

[-- Attachment #2: Type: text/html, Size: 12537 bytes --]

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

[Markus Mottl]

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

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

[Frédéric Bour]

[-- Attachment #1: Type: text/plain, Size: 10737 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 12462 bytes --]

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

[Markus Mottl]

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

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

[Frédéric Bour]

[-- Attachment #1: Type: text/plain, Size: 11744 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 15103 bytes --]

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

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

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

[Philippe Veber]

[-- Attachment #1: Type: text/plain, Size: 12216 bytes --]

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 <markus.mottl@gmail.com>:

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

[-- Attachment #2: Type: text/html, Size: 18102 bytes --]

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

[Ben Millwood]

[-- Attachment #1: Type: text/plain, Size: 11545 bytes --]

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

[-- Attachment #2: Type: text/html, Size: 17720 bytes --]

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

[Goswin von Brederlow]

Hi,

as a side node: There is not just the danger of an escaped channel giving runtime errors. Think what happens when you

 let fd1 = Unix.open_file file1 in
 let () = Unix.close fd in
 let fd2 = Unix.open_file file2 in
 Unix.write fd1

Suddenly you write to the wrong file.

MfG
	Goswin