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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id EC2F17F747 for ; Fri, 8 Aug 2014 22:34:52 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.174 as permitted sender) identity=mailfrom; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ie0-f174.google.com) identity=helo; client-ip=209.85.223.174; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-ie0-f174.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkMBAJEz5VPRVd+ulGdsb2JhbABag19XBIIrSK4LhC6XQIdIAYENCBYQAQEBAQcLCwkSK4QEAQEEDAYRBBkBFAcSCwEDDAYDAgsNAgIJHQICIQEBEQEFAQoSBhMSCQeICwEDEQ2TTpAhaospgXKDEIo7ChknAwpmhHoRAQUOgR6Lc4FFNTMHgnmBUgWFAAWNDIMqhGWCCYFWjHADhD0YKYUkIS8 X-IPAS-Result: AkMBAJEz5VPRVd+ulGdsb2JhbABag19XBIIrSK4LhC6XQIdIAYENCBYQAQEBAQcLCwkSK4QEAQEEDAYRBBkBFAcSCwEDDAYDAgsNAgIJHQICIQEBEQEFAQoSBhMSCQeICwEDEQ2TTpAhaospgXKDEIo7ChknAwpmhHoRAQUOgR6Lc4FFNTMHgnmBUgWFAAWNDIMqhGWCCYFWjHADhD0YKYUkIS8 X-IronPort-AV: E=Sophos;i="5.01,827,1400018400"; d="scan'208";a="88762749" Received: from mail-ie0-f174.google.com ([209.85.223.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 22:34:51 +0200 Received: by mail-ie0-f174.google.com with SMTP id rp18so7121719iec.19 for ; Fri, 08 Aug 2014 13:34:50 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type:content-transfer-encoding; bh=/YBTish9i3CmUAIIaytY/O7JOKmlytK47VUqTdR8Wkc=; b=lTlfUARDYl20JN2rPWuNeVKUgMzazsBEyN5+yTRoA7IpVEO9fonBFjyU3Q1GN9WvSS kZ+wWcV8/ySUqI7RdyWaRpOO/uOwNYj8OMnv+CjuFDKH+owwihXs3MMopoe3rQ4qrzHJ 28fZzgQez6tf13TvIKp+3N9S+/2yEv8ofGJtQ9+yYcgd9+KWnrln/JpWH50PBljf4TKG 3gaNyk0hGDh2PPBnxTPmoe8WJDHzYPVK/Oknr/o7BNd/V1qgNO4tPj89av9vVRvTIeHn 8PSd5E59hwclaJY3/4xa8lRcNAh9gTYbQkbUGbJvKLPuDb2vMe6xu/KCVQNq90w3WRgy FATQ== MIME-Version: 1.0 X-Received: by 10.50.143.65 with SMTP id sc1mr8495116igb.19.1407530090368; Fri, 08 Aug 2014 13:34:50 -0700 (PDT) Received: by 10.107.135.133 with HTTP; Fri, 8 Aug 2014 13:34:50 -0700 (PDT) In-Reply-To: <1407527123.1213.3@mail.lakaban.net> References: <1407522483.1213.2@mail.lakaban.net> <1407527123.1213.3@mail.lakaban.net> Date: Fri, 8 Aug 2014 16:34:50 -0400 Message-ID: From: Markus Mottl To: =?UTF-8?B?RnLDqWTDqXJpYyBCb3Vy?= Cc: Gabriel Scherer , Ben Millwood , Philippe Veber , caml users Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Not letting channels escape. 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=C3=A9d=C3=A9ric Bour wrote: > But you can't do any meaningful computation with this value. > It's just a blackbox. > > In your example, the (ST.input_line c) inside the closure just build a va= lue > 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 =3D { f : 's . 's chan -> ('a, 's) t } > val with_file : string -> f:'a f -> 'a > > val input_line : 's chan -> (string, 's) t > end =3D struct > type ('a, 's) t =3D unit -> 'a > let return x =3D fun () -> x > let bind x f =3D fun () -> f (x ()) () > > type 's chan =3D in_channel > type 'a f =3D { f : 's . 's chan -> ('a, 's) t } > let with_file fp ~f:{ f } =3D > let ic =3D open_in fp in > try > let result =3D f ic () in > close_in_noerr ic; > result > with exn -> > close_in_noerr ic; > raise exn > let input_line c =3D fun () -> input_line c > end > > Le ven. 8 ao=C3=BBt 2014 =C3=A0 20:30, Markus Mottl a =C3=A9crit : > > 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=C3=A9d=C3=A9ric Bour wrote: > > ST.input_line is just a reified effect, it can't be executed outside of t= he > ST monad. You can make the value escape, but you can't do anything with i= t. > 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=C3=BBt 2014 = =C3=A0 19:23, > Markus Mottl a =C3=A9crit : How would you implem= ent 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 regi= on. > Regards, Markus On Fri, Aug 8, 2014 at 1:37 PM, Gabriel Scherer > wrote: The ST trick only works when all > primitives affecting resource are in the monadic abstraction (they mention > the ST region variable in their computation type). This is not the case in > Markus example as "input_line" is a non-typed effect. Using ST safely wou= ld > 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 thi= s. > 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 =3D > ST.with_file "foo.txt" ~f:{ ST.f =3D fun c -> ST.return (fun () -> ignore > (ST.input_line c)) } in f () You'd have to eliminate "return", in which c= ase > 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 mo= re > 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 =3D ref (fun () -> ()) in >> > with_file > "safe.ml" ~f:{ f =3D fun c -> >> > return (f :=3D fun () -> >> > Fn.ignor= e (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 mu= ch > :) >> > >> > 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 :=3D ('a, 's)= t >> > type 's chan >> >> type 'a f =3D { 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 =3D struct >> >> module T =3D str= uct >> > > type ('a, 's) t =3D 'a >> >> let return x =3D x >> >> let bind x f =3D f = x >> let > map x ~f =3D f x >> >> end >> >> include T >> >> include Monad.Make2(T) >> > type 's chan =3D In_channel.t >> >> type 'a f =3D { f : 's . 's chan -> > > ('a, 's) t } >> >> let with_file fp ~f:{ f } =3D In_channel.with_file fp = ~f >> > > 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 } >> = >> > with >> >> | None -> print_endline "None" >> >> | Some line -> print_endl= ine > 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 rais= es > 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 followin= g: > 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 =3D private 'a >> >>> val int : int -> i= nt 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 --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com