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 4CD2C7F75C for ; Mon, 11 Aug 2014 11:08:03 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of bmillwood@janestreet.com) identity=pra; client-ip=38.105.200.112; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of bmillwood@janestreet.com designates 38.105.200.112 as permitted sender) identity=mailfrom; client-ip=38.105.200.112; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.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@mxout1.mail.janestreet.com) identity=helo; client-ip=38.105.200.112; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout1.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AkYCAIaH6FMmachwnGdsb2JhbABag19XBIIsSK4Ymg6BY4dIAYEPCBYQAQEBAQEIFAk9hAMBAQEDAQwGCAkEGQEBExkLAQQLCQILDQ0TCgICIQESAQUBChIGExIJB4gMAwkIAwqPP5Ahaooyd4UCAQWKCwMKhWARBgqNFR2BKGQEB4J5gVOFBwWQN4RoggmBV4VQhyIDhD0YKYUOaw X-IPAS-Result: AkYCAIaH6FMmachwnGdsb2JhbABag19XBIIsSK4Ymg6BY4dIAYEPCBYQAQEBAQEIFAk9hAMBAQEDAQwGCAkEGQEBExkLAQQLCQILDQ0TCgICIQESAQUBChIGExIJB4gMAwkIAwqPP5Ahaooyd4UCAQWKCwMKhWARBgqNFR2BKGQEB4J5gVOFBwWQN4RoggmBV4VQhyIDhD0YKYUOaw X-IronPort-AV: E=Sophos;i="5.01,840,1400018400"; d="scan'208";a="74492939" Received: from mxout1.mail.janestreet.com ([38.105.200.112]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 11 Aug 2014 11:08:00 +0200 Received: from tot-smtp.delacy.com ([172.27.22.15] helo=tot-smtp) by mxout1.mail.janestreet.com with esmtps (TLSv1.2:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.82) (envelope-from ) id 1XGlaB-0004kZ-0c for caml-list@inria.fr; Mon, 11 Aug 2014 05:07:59 -0400 Received: from [172.27.229.230] (helo=mxgoog1.mail.janestreet.com) by tot-smtp with esmtps (UNKNOWN:AES256-GCM-SHA384:256) (Exim 4.72) (envelope-from ) id 1XGla7-0007C9-RD for caml-list@inria.fr; Mon, 11 Aug 2014 05:07:55 -0400 Received: from mail-qa0-f44.google.com ([209.85.216.44]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1:RC4-SHA:128) (Exim 4.72) (envelope-from ) id 1XGla7-0007pb-L0 for caml-list@inria.fr; Mon, 11 Aug 2014 05:07:55 -0400 Received: by mail-qa0-f44.google.com with SMTP id f12so7675777qad.31 for ; Mon, 11 Aug 2014 02:07:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=xFHUwVlOwkwymN9BG+3sXFObk7PRp3tYgmjeKVMdaOo=; b=SUxbb0d9C6CPLDb/t3VkMmSsC1ym9GSkSTur8pFf8ZEa5IiHblUVdReXnCiGKww8CR FHDtEjSaANo0CsOiq+7KYw/awHIPbx2Z28zgiMSzB5tlheW/BFBj/X6HlGKBmeIjqbBt AVHf/w+FaJF0tmsCDlN+HYZujsxWSpDSQmO4Y= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=xFHUwVlOwkwymN9BG+3sXFObk7PRp3tYgmjeKVMdaOo=; b=mHmOVOgr3Afeip1eHejrZdiQfg+5WFv8qGWCUe3FcL38AoPxObf93NAExh4jh2Hfc4 6t+U7QM5JngBqEjvSXB5Ht/0ieeRmxBESF3vPqpqETHyKeP3QZXywbRe1E0Caxd1bjXj 2FPABr0z7CzrGd4mipVQIxQMArA1YftpNFfgzGloBZC+EEp2gh1PHkbTCWK0buJiFK8p s8RuuFU92wpof536oaIjrrfmIAqCjqsUFj8+EKJp2YxLQuHbVEorsZIc6kb4yjFiq0S9 jTIkcqjvQRWOsFBLuQI99aVe9H8g/EX/OJ/PU0a8y2bFxCq553rQ5tW/8Msrs4TO0dn6 Hhiw== X-Gm-Message-State: ALoCoQnOmZQKx36GpNYMWXYQw9tt9Jfy8Ocz4pFKFtxL+LJY9KZAdBCjJ1IOYfVVo8HG2e59TFaNJ1Ipbj5h60aiMya4vhwM5f00xXPh00jiuOBQ/QHrA+pIDFjiHEyFRZnMoIwsKK1s X-Received: by 10.140.88.243 with SMTP id t106mr43432368qgd.12.1407748075420; Mon, 11 Aug 2014 02:07:55 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.140.88.243 with SMTP id t106mr43432333qgd.12.1407748075027; Mon, 11 Aug 2014 02:07:55 -0700 (PDT) Received: by 10.140.82.41 with HTTP; Mon, 11 Aug 2014 02:07:54 -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: Mon, 11 Aug 2014 10:07:54 +0100 Message-ID: From: Ben Millwood To: =?UTF-8?B?RnLDqWTDqXJpYyBCb3Vy?= Cc: Markus Mottl , Gabriel Scherer , Philippe Veber , caml users Content-Type: multipart/alternative; boundary=001a11c12cf0f269d7050056e360 Subject: Re: [Caml-list] Not letting channels escape. --001a11c12cf0f269d7050056e360 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: quoted-printable 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=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 > 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 =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 > the ST monad. You can make the value escape, but you can't do anything wi= th > 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 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 t= he > safe region. 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 would be possible in OCaml, but you would have to completely eschew > the standard library and use a different base where all effectful functio= ns > 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 gi= ve > 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.retu= rn > (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 exceptio= ns > arguably makes >> things worse, because you cannot even use monadic I/O + > existential >> types to achieve guaranteed safety. >> >> Regards, >> Mark= us > >> >> 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 > =3D ref (fun () -> ()) in >> > with_file "safe.ml" ~f:{ f =3D fun c -> >>= > > return (f :=3D fun () -> >> > Fn.ignore (map (input_line c) > ~f:print_string_option)) }; >> > !f () >> > >> > gets Exception: (Sys_err= or > "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 sco= pe > 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_endline line >> >> >> >> >> >> On 8 August 2014 11:23, Philippe Veb= er > >> >> 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 > 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 functi= on > 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 -> 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 > > --001a11c12cf0f269d7050056e360 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
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, s= o may well be translatable to OCaml.


On 8 Au= gust 2014 20:45, Fr=C3=A9d=C3=A9ric Bour <frederic.bour@lakaban.ne= t> 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 inpu= t channel.

This is not the case with the proposed = implementation, because effects are executed immediately.
To ensu= re isolation, all effects should be "frozen":

module ST : sig
=C2=A0 t= ype ('a, 's) t
=C2=A0 val return : 'a -> (&#= 39;a, 's) t
=C2=A0 val bind : ('a, 's) t -> ('= a -> ('b, 's) t) -> ('b, '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

<= /div>
=C2=A0 val input_line : 's chan -> (string, 's) t
end =3D struct
=C2=A0 type ('a, 's) t =3D unit ->= 'a
=C2=A0 let return x =3D fun () -> x
=C2=A0 l= et bind x f =3D fun () -> f (x ()) ()

=C2=A0 ty= pe 's chan =3D in_channel
=C2=A0 type 'a f =3D { f : 's . 's chan -&= gt; ('a, 's) t }
=C2=A0 let with_file fp ~f:{ f } =3D
=C2=A0 =C2=A0 let ic =3D open_in fp in
=C2=A0 =C2=A0= try
=C2=A0 =C2=A0 =C2=A0 let result =3D f ic () in
=C2=A0 =C2=A0 =C2=A0 close_in_noerr ic;
=C2=A0 =C2=A0 =C2=A0= result
=C2=A0 =C2=A0 with exn ->
=C2=A0 =C2=A0 =C2= =A0 close_in_noerr ic;
=C2=A0 =C2=A0 =C2=A0 raise exn
= =C2=A0 let input_line c =3D fun () -> input_line c
end

Le ven. 8 ao=C3=BBt 2014 =C3=A0 20:30, Markus Mottl <markus.mottl@gmail.com= > a =C3=A9crit=C2=A0:

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 <frederic.bour@lakaban.net> wrote:
ST.input_line is just a reified effect, it can't be execut= ed 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=C3=BBt 2014 =C3=A0 19:23, Markus Mottl <markus.mottl@gmail.com> 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, 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_l= ine" 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 a= re 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 =3D ST.with_file "foo.txt" ~f:{ ST.f =3D fu= n c -> ST.return (fun () -> ignore (ST.input_line c)) } in f () You'd have to elimin= ate "return", in which case it wouldn't be a monad anymore and n= ot 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 &g= t; would
still be inconvenient to actually use. > > > On 8 Aug= ust 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 conta= ining the channel from within "f": >> >> In_channel.with_f= ile "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 >> type= s to achieve guaranteed safety. >> >> Regards, >> Markus >= > >> On Fri, Aug 8, 2014 at 10:49 AM, Ben Millwood >> <bmillwood@janestreet.com> >> w= rote: >> > It's been pointed out to me that the above certainly isn't perfect= ly >> > secure. >> > E.g. >> > >> > let f =3D ref (fun = () -> ()) in >> > with_file "safe.ml" ~f:{ = f =3D fun c -> >> > return (f :=3D fun () -> >> > F= n.ignore (map (input_line c) ~f:print_string_option)) }; >> > !f () >> &g= t; >> > gets Exception: (Sys_error "Bad file descriptor"). Even though the &g= t;> > 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 >> > unr= estricted
> side effects, so perhaps there's a reason= why the Haskellers are >> >
excited >> > about this sort of thing a= nd 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 &g= t;> > the duplication isn't an issue. >> > >> > >> > On 8 August = 2014 12:30, Ben Millwood <bmillwoo= d@janestreet.com> >> > wrote: >> >> >> &g= t;> There's a trick with existential types, as used in e.g. Haskell's ST >> >> mona= d. 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 >&= gt; >> it >> >> are >> >> parametrised by an existential = type variable, the corresponding >> >> values >> >> can't >>= ; >> escape the scope of the callback either. >> >> >> >> Something like: >&= gt; >> >> >> 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 >> &g= t;> end =3D struct >> >> module T =3D struct >>
type ('a, 's) t =3D 'a >> >&g= t; 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 >&= gt; >> 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_endline line >> >> >> >> >> >> On 8 August 201= 4 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 &= gt;> >>> from >> >>> leaking resources. They fail, however, to prevent a user from using >&g= t; >>> the >> >>> resource after it has been released. For instanc= e, writing: >>
>> >>> input_char (In_c= hannel.with_file fn (fun x -> x)) >> >>> >> >>= ;>
is perfectly legal type-wise, but w= ill fail at run-time. There are >> >>> of
>>> course less obvious situations, for i= nstance if you define a >> >>>
function: >> >>> >> >>= ;> val lines : in_channel -> string Stream.t >> >>> &g= 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 >> &= gt;>> resources are not used after they are closed? I presume this can >> >>> only = >> >>> be >> >>> achieved by strongly restricting the kind of function passed to >> &= gt;>> [with_file]. >> >>> One simple restriction I see is to defi= ne a type of immediate >> >>> value, >> >>> that >>= >>> roughly correspond to "simple" datatypes (no closures, no lazy >> >>> expressions): >&g= t; >>> >> >>> module Immediate : sig >> >>> type 'a t =3D private 'a >= ;> >>> val int : int -> int t
>>> val list : ('a -> 'a t) -&= gt; '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 >> >>> htt= p://www.lexifi.com/blog/dynamic-types *) >> >>> ... >= > >>> end >> >>> >>
and have the type of [with_file] chang= ed 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, &= gt;> >>> Philippe. >> >>> >> >> >= >
>> >> >> >> -- >> Markus Mottl <= a href=3D"http://www.ocaml.info" target=3D"_blank">http://www.ocaml.info
m= arkus.mottl@gmail.com > > -- Markus Mottl http://www.ocaml.info markus.mottl@g= mail.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://ca= ml.inria.fr/bin/caml-bugs -- Markus Mottl http://ww= w.ocaml.info markus.mottl@gmail.com -- Caml-list mailing list. Subscription management and archives: h= ttps://sympa.inria.fr/sympa/arc/caml-list Beginner's list: http://groups.yahoo.com/group/ocaml_beginners Bug reports: http://ca= ml.inria.fr/bin/caml-bugs
--=20
Markus Mottl http://www.ocaml.info markus.mottl@gmail.com
--=20
Caml-list mailing list. Subscription 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

--001a11c12cf0f269d7050056e360--