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 474EB7F75C for ; Sun, 10 Aug 2014 20:07:12 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 74.125.82.175 as permitted sender) identity=mailfrom; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@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-we0-f175.google.com) identity=helo; client-ip=74.125.82.175; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-we0-f175.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah8CALOz51NKfVKvlGdsb2JhbABag19XBLB6hC6VYIFjh0gBfwgWEAEBAQEHCwsJEiuEAwEBAQMBDAYIDRkBFAcSCwEDAQsGBQsNDRMOIQEBEQEFAQoSBhMSCQeICwEDCQgNoB1qjRuDEIkoChknAwpmhHoRAQUOjRGBRWQEB4RMBYUCBY0NgyqEaIIJgVeMcgOEPRgphQ87Lw X-IPAS-Result: Ah8CALOz51NKfVKvlGdsb2JhbABag19XBLB6hC6VYIFjh0gBfwgWEAEBAQEHCwsJEiuEAwEBAQMBDAYIDRkBFAcSCwEDAQsGBQsNDRMOIQEBEQEFAQoSBhMSCQeICwEDCQgNoB1qjRuDEIkoChknAwpmhHoRAQUOjRGBRWQEB4RMBYUCBY0NgyqEaIIJgVeMcgOEPRgphQ87Lw X-IronPort-AV: E=Sophos;i="5.01,837,1400018400"; d="scan'208";a="74453983" Received: from mail-we0-f175.google.com ([74.125.82.175]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 10 Aug 2014 20:07:10 +0200 Received: by mail-we0-f175.google.com with SMTP id t60so7710110wes.20 for ; Sun, 10 Aug 2014 11:07:10 -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=os49mJGW/jw31K1FVxi3svW+hoY59qfPrBfRAXlU8K4=; b=aQLNsFK+FMv/ub82bVBaczY8Nsq96ruFpwx8GpvxldBVFqNYMBTsq7z2KegxjkWugf qWBdD6XXYjXyZmKaxoj1d81iA+87rMdz6e7ysAjMWxC3cPG0E+Y8JHMq0AwsO0ugiwDT fKZhxV0biZ5uNizND1JGpZ8WRt8c86b0fVwUkg2r87ZRMawuovlEwo5zb4dIoarYsJ56 H3LdyZnoCpTPg5FR9mek6Iatah/lIE2M4xVEwHSBtUNH8BsjcfY/6670iwnyvoPhdhuy srRsz5RiWjQTya9Yki5Vu3d7nl8yPkG5Y0ZFqF8WYnw+gWncrpxOZsd3ey8opwh5FGkr 0Ifg== X-Received: by 10.180.90.11 with SMTP id bs11mr13551650wib.47.1407694030106; Sun, 10 Aug 2014 11:07:10 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.166.132 with HTTP; Sun, 10 Aug 2014 11:06:50 -0700 (PDT) In-Reply-To: References: <1407522483.1213.2@mail.lakaban.net> <1407527123.1213.3@mail.lakaban.net> From: Philippe Veber Date: Sun, 10 Aug 2014 20:06:50 +0200 Message-ID: To: Markus Mottl Cc: =?ISO-8859-1?Q?Fr=E9d=E9ric_Bour?= , Gabriel Scherer , Ben Millwood , caml users Content-Type: multipart/alternative; boundary=f46d043c7e1c9df8e505004a4e0b X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] Not letting channels escape. --f46d043c7e1c9df8e505004a4e0b Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable 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 : > 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=E9d=E9ric 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=FBt 2014 =E0 20:30, Markus Mottl a > =E9crit : > > > > 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=E9d=E9ric 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 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=FBt 2014 =E0 > 19:23, > > Markus Mottl a =E9crit : How would you impleme= nt > 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 > > 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 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 ju= st > > 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 () -> igno= re > > (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 containi= ng > > 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_f= ile > > "safe.ml" ~f:{ f =3D fun c -> >> > return (f :=3D fun () -> >> > Fn.ign= ore > (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 :=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 s= truct > >> > > > > 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 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 n= ot > > 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 "simpl= e" > > datatypes (no closures, no lazy >> >>> expressions): >> >>> >> >>> modu= le > > 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 su= re > > 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 > --f46d043c7e1c9df8e505004a4e0b Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Thanks everyone for these particularly instructive answers= ! Now I understand better why things are the way they are in OCaml. The lit= terature 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=E9d=E9ric 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 inpu= t
> 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
> =A0 type ('a, 's) t
> =A0 val return : 'a -> ('a, 's) t
> =A0 val bind : ('a, 's) t -> ('a -> ('b, 's)= t) -> ('b, 's) t
> =A0 type 's chan
> =A0 type 'a f =3D { f : 's . 's chan -> ('a, 's= ) t }
> =A0 val with_file : string -> f:'a f -> 'a
>
> =A0 val input_line : 's chan -> (string, 's) t
> end =3D struct
> =A0 type ('a, 's) t =3D unit -> 'a
> =A0 let return x =3D fun () -> x
> =A0 let bind x f =3D fun () -> f (x ()) ()
>
> =A0 type 's chan =3D in_channel
> =A0 type 'a f =3D { f : 's . 's chan -> ('a, 's= ) t }
> =A0 let with_file fp ~f:{ f } =3D
> =A0 =A0 let ic =3D open_in fp in
> =A0 =A0 try
> =A0 =A0 =A0 let result =3D f ic () in
> =A0 =A0 =A0 close_in_noerr ic;
> =A0 =A0 =A0 result
> =A0 =A0 with exn ->
> =A0 =A0 =A0 close_in_noerr ic;
> =A0 =A0 =A0 raise exn
> =A0 let input_line c =3D fun () -> input_line c
> end
>
> Le ven. 8 ao=FBt 2014 =E0 20:30, Markus Mottl <markus.mottl@gmail.com> a =E9crit :
>
> The escaping value can still be manipulated through a closure, outside= of
> "with_file". The goal was to prevent this. On Fri, Aug 8, 20= 14 at 2:28 PM,
> Fr=E9d=E9ric Bour <fre= deric.bour@lakaban.net> wrote:
>
> ST.input_line is just a reified effect, it can't be executed outsi= de 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=FBt 2014 = =E0 19:23,
> Markus Mottl <markus.mott= l@gmail.com> a =E9crit : 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 t= rick here was to
> use the monadic "return" to return a closure that captures t= he existential
> variable, allowing me to execute the computation outside of the safe r= egion.
> 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 men= tion
> the ST region variable in their computation type). This is not the cas= e 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 stan= dard
> library and use a different base where all effectful functions have a<= br> > 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 t= ry (
> http://pro= tz.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 j= ust
> occurred to me that one can even break the monadic approach in a purel= y
> 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&= quot;, in which case
> it wouldn't be a monad anymore and not general enough for realisti= c uses of
> "with_file". Regards, Markus On Fri, Aug 8, 2014 at 12:01 PM= , Ben Millwood
> <bmillwood@janestreet.c= om> wrote: > I protected against that in my module by
> carrying the existential type > variable in the result of input_lin= e as
> well, because I stumbled into > exactly that example while original= ly
> 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 mak= e it a bit more
> fully-hearted, but it > would
>
> still be inconvenient to actually use. > > > On 8 August 2014= 16:44,
>
> Markus Mottl <markus.mott= l@gmail.com> wrote: >> >> It doesn't even require
> references to screw things up here. Just >> return the closure c= ontaining
> the channel from within "f": >> >> In_channel.wi= th_file "foo.txt" ~f:(fun ic
> () -> input_line ic) >> |> fun f -> f () >> >&= gt; The initial Stream-example is
> basically just an instance of this >> "returning a closure&= quot; problem. >> >>
> But the availability of references and exceptions arguably makes >&= gt; 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 per= fectly >> >
> secure. >> > E.g. >> > >> > let f =3D ref (= fun () -> ()) in >> > with_file
> "safe.ml" ~= f:{ f =3D fun c -> >> > return (f :=3D fun () -> >> &g= t; Fn.ignore (map
> (input_line c) ~f:print_string_option)) }; >> > !f () >>= ; > >> > gets
> Exception: (Sys_error "Bad file descriptor"). Even though th= e >> > 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 a= re >> >
>
> excited >> > about this sort of thing and you don't see i= t 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 ca= ses where you'd be
> defining all your own operations >> > anyway, >> > s= o >> > the duplication
> isn't an issue. >> > >> > >> > On 8 Aug= ust 2014 12:30, Ben Millwood
> <bmillwood@janestreet.c= om> >> > wrote: >> >> >> >> There&#= 39;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 &= gt;> >>
> it >> >> are >> >> parametrised by an existent= ial 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 . &#= 39;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 struct >>
>
> 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 I= n_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 Veber
> <philippe.veber@gmail.c= om> >> >> wrote: >> >>> >> >>= > Dear all, >> >>> >>
>
> many libraries like lwt, batteries or core provide a very nice >>= ; >>>
>
> idiom >> >>> to >> >>> be used when a fu= nction uses a resource (file,
> connection, mutex, >> >>> et >> >>> cete= ra), 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 >> >>> preve= nt >> >>> from >> >>>
> leaking resources. They fail, however, to prevent a user from using &g= t;> >>>
> the >> >>> resource after it has been released. For ins= tance, 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_c= hannel -> 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 >&g= t; >>> resources are not
> used after they are closed? I presume this can >> >>> o= nly >> >>> be >> >>>
> achieved by strongly restricting the kind of function passed to >&g= t; >>>
> [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): &g= t;> >>> >> >>> 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 >> >>&g= 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 &g= t;> >>> >> >>> I'm sure
> there are lots of smarter solutions out there. Would >> >>= > anyone >> >>>
> happen to know some? >> >>> >> >>> Cheer= s, >> >>> Philippe. >> >>> >> >> = >>
>
>>> >> >> >> -- >> Markus Mottl http://www.ocaml.info
>
> markus.mottl@gmail.com &= gt; > -- 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= 9;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= 9;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 =A0 =A0 =A0 =A0http://www.ocaml.info =A0 =A0 =A0 =A0markus.mottl@gmail.com

--f46d043c7e1c9df8e505004a4e0b--