From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id EF8087F747 for ; Fri, 8 Aug 2014 19:38:25 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.220.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.220.173 as permitted sender) identity=mailfrom; client-ip=209.85.220.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-vc0-f173.google.com) identity=helo; client-ip=209.85.220.173; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-vc0-f173.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkABAFIK5VPRVdytlGdsb2JhbABag19XBIJzrguELpVdgWOHSAGBDQgWEAEBAQEHCwsJEiuEAwEBAQMBEhEEGQEUBxILAQMBCwYDAgsNDR0CAiEBAREBBQEKEgYTCAoJB4gLAQMJCA2TQZAhaospgXKDEIpEChknAwpmhHoRAQUOjRGBRWQEB4J5gVIFhQAFjQyDKoRlggmBVoxwA4Q9GCmFCjsv X-IPAS-Result: AkABAFIK5VPRVdytlGdsb2JhbABag19XBIJzrguELpVdgWOHSAGBDQgWEAEBAQEHCwsJEiuEAwEBAQMBEhEEGQEUBxILAQMBCwYDAgsNDR0CAiEBAREBBQEKEgYTCAoJB4gLAQMJCA2TQZAhaospgXKDEIpEChknAwpmhHoRAQUOjRGBRWQEB4J5gVIFhQAFjQyDKoRlggmBVoxwA4Q9GCmFCjsv X-IronPort-AV: E=Sophos;i="5.01,826,1400018400"; d="scan'208";a="74339002" Received: from mail-vc0-f173.google.com ([209.85.220.173]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 19:38:24 +0200 Received: by mail-vc0-f173.google.com with SMTP id hy10so8639842vcb.4 for ; Fri, 08 Aug 2014 10:38:23 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=ZeYrPtqshB83+RczFtyiFsf5s7vswIEDxO5ehKiORPU=; b=0WENW6DBBIPpZ64lBOeiD8PzkdNCyZdxkTXW37gdRsuls9CKNb0NRzO/kuNuwdbW8y oTbzgGZYGZ19uNFzgXaGkcFbqMM1TwR4rlxDo3mwp1ZoYSBwza1OL3nwACARMcrnC1M5 xjpTO4iInAO26x9x7eY+VLzrl1GyZL+sfJfbNhKWR+OA47DGGVSGfDcww/qkIuwSYC0N FS85n6H9dL8VD5/kXwigVufjFuSVB0IfK01GR3u8Q8UA7g4cTepQRBNuh1XVSQUiqIz9 eyVX9dOFAXtLySi7WbsjuCgoQ6/2BLsDuTB7aSorPPi3SZVinD+KejvjYqKNO/p4oKLR ptOg== X-Received: by 10.221.42.135 with SMTP id ty7mr23133470vcb.14.1407519503110; Fri, 08 Aug 2014 10:38:23 -0700 (PDT) MIME-Version: 1.0 Received: by 10.58.210.202 with HTTP; Fri, 8 Aug 2014 10:37:43 -0700 (PDT) In-Reply-To: References: From: Gabriel Scherer Date: Fri, 8 Aug 2014 19:37:43 +0200 Message-ID: To: Markus Mottl Cc: Ben Millwood , Philippe Veber , caml users Content-Type: multipart/alternative; boundary=001a11339974ff5750050021ab12 Subject: Re: [Caml-list] Not letting channels escape. --001a11339974ff5750050021ab12 Content-Type: text/plain; charset=UTF-8 The ST trick only works when all primitives affecting resource are in the monadic abstraction (they mention the ST region variable in their computation type). This is not the case in Markus example as "input_line" is a non-typed effect. Using ST safely would be possible in OCaml, but you would have to completely eschew the standard library and use a different base where all effectful functions have a monadic type. It is the library, not the language itself, that allows this. On the contrary, linear types are distinctly a language feature. Using monads to encapsulate a form of linearity is an old trick. If you want to have a taste of built-in linear typing, you may want to give Mezzo a try ( http://protz.github.io/mezzo/ ). On Fri, Aug 8, 2014 at 7:21 PM, Markus Mottl wrote: > I see, I was replying to the "reference problem" and hadn't read your > implementation, which, besides existentials, already requires monads > as return values. > > Actually, it just occurred to me that one can even break the monadic > approach in a purely functional way. You are just one "return" away > from disaster: > > let f = > ST.with_file "foo.txt" ~f:{ > ST.f = fun c -> ST.return (fun () -> ignore (ST.input_line c)) > } > in > f () > > You'd have to eliminate "return", in which case it wouldn't be a monad > anymore and not general enough for realistic uses of "with_file". > > Regards, > Markus > > On Fri, Aug 8, 2014 at 12:01 PM, Ben Millwood > wrote: > > I protected against that in my module by carrying the existential type > > variable in the result of input_line as well, because I stumbled into > > exactly that example while originally drafting my e-mail :) > > > > In a sense I'm reinventing monadic IO but in a bit of a half-hearted > way. It > > wouldn't take much work to make it a bit more fully-hearted, but it would > > still be inconvenient to actually use. > > > > > > On 8 August 2014 16:44, Markus Mottl wrote: > >> > >> It doesn't even require references to screw things up here. Just > >> return the closure containing the channel from within "f": > >> > >> In_channel.with_file "foo.txt" ~f:(fun ic () -> input_line ic) > >> |> fun f -> f () > >> > >> The initial Stream-example is basically just an instance of this > >> "returning a closure" problem. > >> > >> But the availability of references and exceptions arguably makes > >> things worse, because you cannot even use monadic I/O + existential > >> types to achieve guaranteed safety. > >> > >> Regards, > >> Markus > >> > >> On Fri, Aug 8, 2014 at 10:49 AM, Ben Millwood > > >> wrote: > >> > It's been pointed out to me that the above certainly isn't perfectly > >> > secure. > >> > E.g. > >> > > >> > let f = ref (fun () -> ()) in > >> > with_file "safe.ml" ~f:{ f = fun c -> > >> > return (f := fun () -> > >> > Fn.ignore (map (input_line c) ~f:print_string_option)) }; > >> > !f () > >> > > >> > gets Exception: (Sys_error "Bad file descriptor"). Even though the > >> > channel > >> > and any operations on it can't escape the closure, the type of a > >> > function > >> > which uses them needn't mention them at all. > >> > > >> > It's pretty hard to do anything about this in the presence of > >> > unrestricted > >> > side effects, so perhaps there's a reason why the Haskellers are > excited > >> > about this sort of thing and you don't see it in OCaml so much :) > >> > > >> > That said, you do seem to be forced to make a bit more of an effort to > >> > break > >> > things here, so I don't think the technique is completely without > merit, > >> > perhaps in cases where you'd be defining all your own operations > anyway, > >> > so > >> > the duplication isn't an issue. > >> > > >> > > >> > On 8 August 2014 12:30, Ben Millwood > wrote: > >> >> > >> >> There's a trick with existential types, as used in e.g. Haskell's ST > >> >> monad. It uses the fact that an existentially-quantified type > variable > >> >> can't > >> >> escape its scope, so if your channel type and results that depend on > it > >> >> are > >> >> parametrised by an existential type variable, the corresponding > values > >> >> can't > >> >> escape the scope of the callback either. > >> >> > >> >> Something like: > >> >> > >> >> module ST : sig > >> >> type ('a, 's) t > >> >> include Monad.S2 with type ('a, 's) t := ('a, 's) t > >> >> type 's chan > >> >> type 'a f = { f : 's . 's chan -> ('a, 's) t } > >> >> val with_file : string -> f:'a f -> 'a > >> >> > >> >> val input_line : 's chan -> (string option, 's) t > >> >> end = struct > >> >> module T = struct > >> >> type ('a, 's) t = 'a > >> >> let return x = x > >> >> let bind x f = f x > >> >> let map x ~f = f x > >> >> end > >> >> include T > >> >> include Monad.Make2(T) > >> >> type 's chan = In_channel.t > >> >> type 'a f = { f : 's . 's chan -> ('a, 's) t } > >> >> let with_file fp ~f:{ f } = In_channel.with_file fp ~f > >> >> let input_line c = In_channel.input_line c > >> >> end > >> >> ;; > >> >> > >> >> match ST.with_file "safe.ml" ~f:{ ST.f = fun c -> ST.input_line c } > >> >> with > >> >> | None -> print_endline "None" > >> >> | Some line -> print_endline line > >> >> > >> >> > >> >> On 8 August 2014 11:23, Philippe Veber > >> >> wrote: > >> >>> > >> >>> Dear all, > >> >>> > >> >>> many libraries like lwt, batteries or core provide a very nice idiom > >> >>> to > >> >>> be used when a function uses a resource (file, connection, mutex, et > >> >>> cetera), for instance in Core.In_channel, the function: > >> >>> > >> >>> val with_file : ?binary:bool -> string -> f:(t -> 'a) -> 'a > >> >>> > >> >>> opens a channel for [f] and ensures it is closed after the call to > >> >>> [f], > >> >>> even if it raises an exception. So these functions basically prevent > >> >>> from > >> >>> leaking resources. They fail, however, to prevent a user from using > >> >>> the > >> >>> resource after it has been released. For instance, writing: > >> >>> > >> >>> input_char (In_channel.with_file fn (fun x -> x)) > >> >>> > >> >>> is perfectly legal type-wise, but will fail at run-time. There are > of > >> >>> course less obvious situations, for instance if you define a > function: > >> >>> > >> >>> val lines : in_channel -> string Stream.t > >> >>> > >> >>> then the following will also fail: > >> >>> > >> >>> Stream.iter f (In_channel.with_file fn lines) > >> >>> > >> >>> My question is the following: is there a way to have the compiler > >> >>> check > >> >>> resources are not used after they are closed? I presume this can > only > >> >>> be > >> >>> achieved by strongly restricting the kind of function passed to > >> >>> [with_file]. > >> >>> One simple restriction I see is to define a type of immediate value, > >> >>> that > >> >>> roughly correspond to "simple" datatypes (no closures, no lazy > >> >>> expressions): > >> >>> > >> >>> module Immediate : sig > >> >>> type 'a t = private 'a > >> >>> val int : int -> int t > >> >>> val list : ('a -> 'a t) -> 'a list -> 'a list t > >> >>> val tuple : ('a -> 'a t) -> ('b -> 'b t) -> ('a * 'b) -> ('a * > 'b) t > >> >>> (* for records, use the same trick than in > >> >>> http://www.lexifi.com/blog/dynamic-types *) > >> >>> ... > >> >>> end > >> >>> > >> >>> and have the type of [with_file] changed to > >> >>> > >> >>> val with_file : string -> f:(in_channel -> 'a Immediate.t) -> 'a > >> >>> > >> >>> I'm sure there are lots of smarter solutions out there. Would anyone > >> >>> happen to know some? > >> >>> > >> >>> Cheers, > >> >>> Philippe. > >> >>> > >> >> > >> > > >> > >> > >> > >> -- > >> Markus Mottl http://www.ocaml.info markus.mottl@gmail.com > > > > > > > > -- > Markus Mottl http://www.ocaml.info markus.mottl@gmail.com > > -- > Caml-list mailing list. Subscription management and archives: > https://sympa.inria.fr/sympa/arc/caml-list > Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > Bug reports: http://caml.inria.fr/bin/caml-bugs > --001a11339974ff5750050021ab12 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
The ST trick only works when all primitives affecting= resource are in the monadic abstraction (they mention the ST region variab= le in their computation type). This is not the case in Markus example as &q= uot;input_line" is a non-typed effect. Using ST safely would be possib= le in OCaml, but you would have to completely eschew the standard library a= nd 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 wan= t to have a taste of built-in linear typing, you may want to give Mezzo a t= ry ( 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. =C2=A0You are just one "return&qu= ot; away
from disaster:

=C2=A0 let f =3D
=C2=A0 =C2=A0 ST.with_file "foo.txt" ~f:{
=C2=A0 =C2=A0 =C2=A0 ST.f =3D fun c -> ST.return (fun () -> ignore (S= T.input_line c))
=C2=A0 =C2=A0 }
=C2=A0 in
=C2=A0 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<= br> > exactly that example while originally drafting my e-mail :)
>
> In a sense I'm reinventing monadic IO but in a bit of a half-heart= ed way. It
> wouldn't take much work to make it a bit more fully-hearted, but i= t 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. = =C2=A0Just
>> return the closure containing the channel from within "f"= ;:
>>
>> =C2=A0 In_channel.with_file "foo.txt" ~f:(fun ic () ->= ; input_line ic)
>> =C2=A0 |> 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 + existentia= l
>> 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&= #39;t perfectly
>> > secure.
>> > E.g.
>> >
>> > let f =3D ref (fun () -> ()) in
>> > with_file "= safe.ml" ~f:{ f =3D fun c ->
>> > =C2=A0 return (f :=3D fun () ->
>> > =C2=A0 =C2=A0 Fn.ignore (map (input_line c) ~f:print_string_o= ption)) };
>> > !f ()
>> >
>> > gets Exception: (Sys_error "Bad file descriptor"). = Even though the
>> > channel
>> > and any operations on it can't escape the closure, the ty= pe of a
>> > function
>> > which uses them needn't mention them at all.
>> >
>> > It's pretty hard to do anything about this in the presenc= e of
>> > unrestricted
>> > side effects, so perhaps there's a reason why the Haskell= ers 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 ope= rations 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 tha= t depend on it
>> >> are
>> >> parametrised by an existential type variable, the corresp= onding values
>> >> can't
>> >> escape the scope of the callback either.
>> >>
>> >> Something like:
>> >>
>> >> module ST : sig
>> >> =C2=A0 type ('a, 's) t
>> >> =C2=A0 include Monad.S2 with type ('a, 's) t :=3D= ('a, 's) t
>> >> =C2=A0 type 's chan
>> >> =C2=A0 type 'a f =3D { f : 's . 's chan ->= ('a, 's) t }
>> >> =C2=A0 val with_file : string -> f:'a f -> '= ;a
>> >>
>> >> =C2=A0 val input_line : 's chan -> (string option,= 's) t
>> >> end =3D struct
>> >> =C2=A0 module T =3D struct
>> >> =C2=A0 =C2=A0 type ('a, 's) t =3D 'a
>> >> =C2=A0 =C2=A0 let return x =3D x
>> >> =C2=A0 =C2=A0 let bind x f =3D f x
>> >> =C2=A0 =C2=A0 let map x ~f =3D f x
>> >> =C2=A0 end
>> >> =C2=A0 include T
>> >> =C2=A0 include Monad.Make2(T)
>> >> =C2=A0 type 's chan =3D In_channel.t
>> >> =C2=A0 type 'a f =3D { f : 's . 's chan ->= ('a, 's) t }
>> >> =C2=A0 let with_file fp ~f:{ f } =3D In_channel.with_file= fp ~f
>> >> =C2=A0 let input_line c =3D In_channel.input_line c
>> >> end
>> >> ;;
>> >>
>> >> match ST.with_file "safe.ml" ~f:{ ST.f =3D fun c -> ST.input_line c }<= br> >> >> 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, connec= tion, mutex, et
>> >>> cetera), for instance in Core.In_channel, the functio= n:
>> >>>
>> >>> val with_file : ?binary:bool -> string -> f:(t = -> 'a) -> 'a
>> >>>
>> >>> opens a channel for [f] and ensures it is closed afte= r the call to
>> >>> [f],
>> >>> even if it raises an exception. So these functions ba= sically prevent
>> >>> from
>> >>> leaking resources. They fail, however, to prevent a u= ser from using
>> >>> the
>> >>> resource after it has been released. For instance, wr= iting:
>> >>>
>> >>> input_char (In_channel.with_file fn (fun x -> x))<= br> >> >>>
>> >>> is perfectly legal type-wise, but will fail at run-ti= me. There are of
>> >>> course less obvious situations, for instance if you d= efine 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 presu= me 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 i= mmediate value,
>> >>> that
>> >>> roughly correspond to "simple" datatypes (n= o closures, no lazy
>> >>> expressions):
>> >>>
>> >>> module Immediate : sig
>> >>> =C2=A0 type 'a t =3D private 'a
>> >>> =C2=A0 val int : int -> int t
>> >>> =C2=A0 val list : ('a -> 'a t) -> '= a list -> 'a list t
>> >>> =C2=A0 val tuple : ('a -> 'a t) -> (= 9;b -> 'b t) -> ('a * 'b) -> ('a * 'b) t
>> >>> =C2=A0 (* for records, use the same trick than in
>> >>> http://www.lexifi.com/blog/dynamic-types *)
>> >>> =C2=A0 ...
>> >>> 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,
>> >>> =C2=A0 Philippe.
>> >>>
>> >>
>> >
>>
>>
>>
>> --
>> Markus Mottl =C2=A0 =C2=A0 =C2=A0 =C2=A0http://www.ocaml.info =C2=A0 =C2=A0 =C2=A0 = =C2=A0markus.mottl@gmail.com<= br> >
>



--
Markus Mottl =C2=A0 =C2=A0 =C2=A0 =C2=A0http://www.ocaml.info =C2=A0 =C2=A0 =C2=A0 =C2=A0markus.mottl@gmail.com

--
Caml-list mailing list. =C2=A0Subscription management and archives:
ht= tps://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

--001a11339974ff5750050021ab12--