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 6312A7F747 for ; Fri, 8 Aug 2014 21:30:53 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.213.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.213.172 as permitted sender) identity=mailfrom; client-ip=209.85.213.172; receiver=mail3-smtp-sop.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 (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-ig0-f172.google.com) identity=helo; client-ip=209.85.213.172; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-ig0-f172.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkMBAFck5VPRVdWslGdsb2JhbABag19XBIIrSK4LhC6XQIdIAYENCBYQAQEBAQcLCwkSK4QEAQEEDAYRBBkBFAcSCwEDDAYDAgsNAgIJHQICIQEBEQEFAQoSBhMSCQeICwEDEQ2TRZAhaospgXKDEIpAChknAwpmhHoRAQUOgR6Lc4FFNTMHgnmBUgWFAAWNDIMqhGWCCYFWjHADhD0YKYUkIS8 X-IPAS-Result: AkMBAFck5VPRVdWslGdsb2JhbABag19XBIIrSK4LhC6XQIdIAYENCBYQAQEBAQcLCwkSK4QEAQEEDAYRBBkBFAcSCwEDDAYDAgsNAgIJHQICIQEBEQEFAQoSBhMSCQeICwEDEQ2TRZAhaospgXKDEIpAChknAwpmhHoRAQUOgR6Lc4FFNTMHgnmBUgWFAAWNDIMqhGWCCYFWjHADhD0YKYUkIS8 X-IronPort-AV: E=Sophos;i="5.01,827,1400018400"; d="scan'208";a="74344233" Received: from mail-ig0-f172.google.com ([209.85.213.172]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 21:30:51 +0200 Received: by mail-ig0-f172.google.com with SMTP id h15so1543522igd.5 for ; Fri, 08 Aug 2014 12:30: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=O1jG5fd66O4uS69uH6MyHyDzXwVC7kplbteTUk6TmVY=; b=GcHZtfqROMxuvXRF6q3KaqXiZ3A14A/ctj5cWUjShFL/i53soW7GyLhXRaGJBhlrPz 7Me9MZMTMic1bWsvYVN8WcXHehYJE3eDeYWKSykWbG88S/x8q6ApssfZupYg320gYiP2 Umc9MHy+C369DIn9N5xdG8t0c2kGcn7IjfzgoqUD/5YCMVy4mpeYNkDx/zX9TUGN6sD0 DSgnuFs0Ghiq9gIXmRoHpbULGhKzF58PCUfEJ1kYKEqhDVZtif+3ViIhIy2cXQ3gFRm6 3nmbd20ox6/8Z0jjKgmn2eGYxu5Q84umS+8WwGzcILXHbn/fVPHwGGuCsVuVPMus/ePv k/kw== MIME-Version: 1.0 X-Received: by 10.50.118.4 with SMTP id ki4mr8362822igb.16.1407526250269; Fri, 08 Aug 2014 12:30:50 -0700 (PDT) Received: by 10.107.135.133 with HTTP; Fri, 8 Aug 2014 12:30:50 -0700 (PDT) In-Reply-To: <1407522483.1213.2@mail.lakaban.net> References: <1407522483.1213.2@mail.lakaban.net> Date: Fri, 8 Aug 2014 15:30: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. 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 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=C3=BBt 2014 =C3=A0 19:23, Markus Mottl a =C3=A9crit : > > 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, 20= 14 > 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 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 wro= te: > > 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 t= he > monadic approach in a purely functional way. You are just one "return" aw= ay > 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 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 > wou= ld >> 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.Make= 2(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 --=20 Markus Mottl http://www.ocaml.info markus.mottl@gmail.com