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 2ADBA7F747 for ; Fri, 8 Aug 2014 18:01:30 +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.229; 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.229 as permitted sender) identity=mailfrom; client-ip=38.105.200.229; 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@mxout3.mail.janestreet.com) identity=helo; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout3.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqgCANDz5FMmacjlnGdsb2JhbABag19XBIJzyBWBY4dIAYELCBYQAQEBAQEGFgk9hAMBAQEDARIRBBkBARMkAQQLCQILDSoCAiEBEgEFARwGExsHiAwDCQgDCpMtkCFqijJ3hQIBBYsDDYVgEQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IPAS-Result: AqgCANDz5FMmacjlnGdsb2JhbABag19XBIJzyBWBY4dIAYELCBYQAQEBAQEGFgk9hAMBAQEDARIRBBkBARMkAQQLCQILDSoCAiEBEgEFARwGExsHiAwDCQgDCpMtkCFqijJ3hQIBBYsDDYVgEQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IronPort-AV: E=Sophos;i="5.01,825,1400018400"; d="scan'208";a="74332506" Received: from mxout3.mail.janestreet.com ([38.105.200.229]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Aug 2014 18:01:28 +0200 Received: from tot-oib-smtp1 ([172.27.22.15] helo=tot-smtp) by mxout3.mail.janestreet.com with esmtps (UNKNOWN:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.82) (envelope-from ) id 1XFmbe-0001HG-4n for caml-list@inria.fr; Fri, 08 Aug 2014 12:01:26 -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 1XFmbb-0005WH-1G for caml-list@inria.fr; Fri, 08 Aug 2014 12:01:23 -0400 Received: from mail-qa0-f49.google.com ([209.85.216.49]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1:RC4-SHA:128) (Exim 4.72) (envelope-from ) id 1XFmba-0007Ej-TV for caml-list@inria.fr; Fri, 08 Aug 2014 12:01:22 -0400 Received: by mail-qa0-f49.google.com with SMTP id dc16so5649804qab.22 for ; Fri, 08 Aug 2014 09:01:22 -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=lBf84X/g7rgWh9SP7sMA7EcWYlthDNziD3gF0LCGFmk=; b=oEMKVm8DFVIaP6bVTfit40Er6iwCinIQHEPd9YtTFcaEYTSREjr7I+Sc0YyA72YBdH 0RA7qrDUSMjdw+1SmcJCNs1pOZToI8G5NZjJoK6YQ5u36r+sPvR+MgTl/+use2Xu3ciN nr7k6fdcvSqVyeEafHOB1JVSlRKhKYn2ezzIw= 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=lBf84X/g7rgWh9SP7sMA7EcWYlthDNziD3gF0LCGFmk=; b=iHmDe73RPpwr2PXuydTrbesr0AzFxdBgL4NF4NIV0Lmc9JtaQ68EKCojeDBMut5ZAQ slrHCqDj8NuLYXf0wsoSAEEk/L6Vh3w4dicVJJo/BTohEm2SpDgUseDk0AgsjsE7Ta42 ku9xouPYC841RklnLI4YSh/dOWSniEZ8IHBo7H0vNFT+8NlVKpx6Je801pJ8BhY3ojuy zhXnh29wwlFEMIyfYVm3RWvAHQ6R98YBB/TUaT5BqnnZxU+s4zkLX4pWsB3JMbuSk2IC cIZd743BatRJAFfbrxgN44/9iO6zCGz1anD8Up1wESk4ZkDyU/Yn3Eu0rY9X0qJs5Wly feEA== X-Gm-Message-State: ALoCoQlkLM8cw+Njz8/V8v/y/RfuvianJh5JQ0FHK81enL1fmtiTKf84IVuQ4W3PyN5U9yWiIs+uSnc1hT77ZK7T7YwbXY8FDX3v6kw+U5rKjUTZvEX7G+4N5h/8DVyR8fHSUX9ffdmd X-Received: by 10.224.95.6 with SMTP id b6mr39867027qan.17.1407513682668; Fri, 08 Aug 2014 09:01:22 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.224.95.6 with SMTP id b6mr39867007qan.17.1407513682554; Fri, 08 Aug 2014 09:01:22 -0700 (PDT) Received: by 10.140.82.41 with HTTP; Fri, 8 Aug 2014 09:01:22 -0700 (PDT) In-Reply-To: References: Date: Fri, 8 Aug 2014 17:01:22 +0100 Message-ID: From: Ben Millwood To: Markus Mottl Cc: Philippe Veber , caml users Content-Type: multipart/alternative; boundary=001a11c1bcdc10f1ef0500205143 Subject: Re: [Caml-list] Not letting channels escape. --001a11c1bcdc10f1ef0500205143 Content-Type: text/plain; charset=UTF-8 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 > --001a11c1bcdc10f1ef0500205143 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
I protected against that in my module by carrying the exis= tential type variable in the result of input_line as well, because I stumbl= ed 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 wa= y. 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 Au= gust 2014 16:44, Markus Mottl <markus.mottl@gmail.com> = wrote:
It doesn't even require references to sc= rew 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_l= ine 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 + 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 ->
> =C2=A0 return (f :=3D fun () ->
> =C2=A0 =C2=A0 Fn.ignore (map (input_line c) ~f:print_string_option)) }= ;
> !f ()
>
> gets Exception: (Sys_error "Bad file descriptor"). Even thou= gh the channel
> and any operations on it can't escape the closure, the type of a f= unction
> which uses them needn't mention them at all.
>
> It's pretty hard to do anything about this in the presence of unre= stricted
> side effects, so perhaps there's a reason why the Haskellers are e= xcited
> about this sort of thing and you don't see it in OCaml so much :)<= br> >
> 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 a= nyway, 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. Haskel= l's ST
>> monad. It uses the fact that an existentially-quantified type vari= able 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 va= lues 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 } 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, connection, mut= ex, et
>>> cetera), for instance in Core.In_channel, the function:
>>>
>>> val with_file : ?binary:bool -> string -> f:(t -> = 9;a) -> 'a
>>>
>>> opens a channel for [f] and ensures it is closed after the cal= l to [f],
>>> even if it raises an exception. So these functions basically p= revent 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 f= unction:
>>>
>>> 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 compi= ler check
>>> resources are not used after they are closed? I presume this c= an only be
>>> achieved by strongly restricting the kind of function passed t= o [with_file].
>>> One simple restriction I see is to define a type of immediate = value, that
>>> roughly correspond to "simple" datatypes (no closure= s, 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 -&= gt; 'a list t
>>> =C2=A0 val tuple : ('a -> 'a t) -> ('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 Immedi= ate.t) -> 'a
>>>
>>> I'm sure there are lots of smarter solutions out there. Wo= uld 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

--001a11c1bcdc10f1ef0500205143--