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 8726C7F747 for ; Fri, 8 Aug 2014 16:49:24 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of bmillwood@janestreet.com) identity=pra; client-ip=38.105.200.112; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="bmillwood@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.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=mail2-smtp-roc.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 (mail2-smtp-roc.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=mail2-smtp-roc.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: AqgCAHni5FMmachwnGdsb2JhbABag19XBIJzyBWBY4dIAYELCBYQAQEBAQEGFgk9hAMBAQEDARIRBBkBATcBBAsLCw0qAgIhARIBBQEcBhMIEweIDAMJCAMKo0hqijJ3hQIBBYsADYVgEQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IPAS-Result: AqgCAHni5FMmachwnGdsb2JhbABag19XBIJzyBWBY4dIAYELCBYQAQEBAQEGFgk9hAMBAQEDARIRBBkBATcBBAsLCw0qAgIhARIBBQEcBhMIEweIDAMJCAMKo0hqijJ3hQIBBYsADYVgEQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IronPort-AV: E=Sophos;i="5.01,825,1400018400"; d="scan'208";a="88732876" Received: from mxout1.mail.janestreet.com ([38.105.200.112]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Aug 2014 16:49:23 +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 1XFlTt-00055A-Rc for caml-list@inria.fr; Fri, 08 Aug 2014 10:49:21 -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 1XFlTt-0005Ri-Nm for caml-list@inria.fr; Fri, 08 Aug 2014 10:49:21 -0400 Received: from mail-qg0-f52.google.com ([209.85.192.52]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1:RC4-SHA:128) (Exim 4.72) (envelope-from ) id 1XFlTt-00041D-KC for caml-list@inria.fr; Fri, 08 Aug 2014 10:49:21 -0400 Received: by mail-qg0-f52.google.com with SMTP id f51so6198568qge.11 for ; Fri, 08 Aug 2014 07:49:21 -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=8kabpPQ/qHXigA1kHNfnka5S7yOJlpwEcx23FqqLEyc=; b=bRUTFOFfaThJmKCiy4E0RH5f+dEa79uCHvBmM1T0H55AscPwm+v1GPpCzckOgJPcz3 yAhLMOWPNHjs25jOIcb8wcg/kcVtFEk+gMHmqLiJ7V7O0lraJy5e12JW0bfoUXLH8kEM feUMXGv+NPBM3Q0qU7mrRNhvIK5ylO6Z5m+vg= 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=8kabpPQ/qHXigA1kHNfnka5S7yOJlpwEcx23FqqLEyc=; b=aFNqtorXS3vBrtg20xWvtRiV2UEHE72atf0An7t2bjh+jKNgjIZfg61JJg6Sxz9/l0 EMOAixuJ3+m77AZMp/M5pLjFWYSeSTx9Lsnq+z+I20AC0rd6UHefZJIHiwHDSEeJZT1m LOohQViY4qIm7U/JI28zPeUVHtcyWBiooq78w8xEb3SBFxvWPmP2PiOEQYOdts89kMAK 5sHK7DJ/wY3zoV9reoaShhHJaMXE7A2MoDnieo1ZgNURBO8M3gxEwTTKFJlOO18rKq+L EbNJevyTfEkMoWAZL6MBGgVNyqmuOGJhL5btrYGJAO3QGzLgJGA+9VVlvO4kx6Hl4lY/ z6Lw== X-Gm-Message-State: ALoCoQmWovGBTYxxCHttNMh88YBuTGnkFVVPTs9pIoQdSHyJ3F11hvYI+Y/IHosZnFldibsHJrf2LsbecRyliEs1wKxvQldQxLwtxkgH7vPOBHmJgldYxb/Ap6uKgxJgS5MskXkLx7KQ X-Received: by 10.224.61.144 with SMTP id t16mr39150775qah.2.1407509361425; Fri, 08 Aug 2014 07:49:21 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.224.61.144 with SMTP id t16mr39150758qah.2.1407509361314; Fri, 08 Aug 2014 07:49:21 -0700 (PDT) Received: by 10.140.82.41 with HTTP; Fri, 8 Aug 2014 07:49:21 -0700 (PDT) In-Reply-To: References: Date: Fri, 8 Aug 2014 15:49:21 +0100 Message-ID: From: Ben Millwood To: Philippe Veber Cc: caml users Content-Type: multipart/alternative; boundary=047d7bdc7cae7ff28605001f4f55 Subject: Re: [Caml-list] Not letting channels escape. --047d7bdc7cae7ff28605001f4f55 Content-Type: text/plain; charset=UTF-8 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. >> >> > --047d7bdc7cae7ff28605001f4f55 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
It's been pointed out to me that the ab= ove certainly isn't perfectly secure. E.g.

let f =3D ref (fun ()= -> ()) in
with_file "safe.ml&quo= t; ~f:{ f =3D fun c ->
=C2=A0 return (f :=3D fun () ->
=C2=A0=C2=A0=C2=A0 Fn.ignore (map (in= put_line c) ~f:print_string_option)) };
!f ()

gets Exceptio= n: (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 Haskell= ers 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 complet= ely without merit, perhaps in cases where you'd be defining all your ow= n operations anyway, so the duplication isn't an issue.


O= n 8 August 2014 12:30, Ben Millwood <bmillwood@janestreet.com&g= t; 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 esca= pe its scope, so if your channel type and results that depend on it are par= ametrised by an existential type variable, the corresponding values can'= ;t escape the scope of the callback either.

Something like:

module ST : sig
=C2=A0 type ('a, &#= 39;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 : &= #39;s . 's chan -> ('a, 's) t }
=C2=A0 val with_file : string -> f:'a f -> 'a

=C2=A0 v= al input_line : 's chan -> (string option, 's) t
end =3D stru= ct
=C2=A0 module T =3D struct
=C2=A0=C2=A0=C2=A0 type ('a, 's= ) t =3D 'a
=C2=A0=C2=A0=C2=A0 let return x =3D x
=C2=A0=C2=A0=C2=A0 let bind x f =3D f x
=C2=A0=C2=A0=C2=A0 let map x ~f = =3D f x
=C2=A0 end
=C2=A0 include T
=C2=A0 include Monad.Make2(T)<= br>=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
;;

mat= ch ST.with_file "safe.ml<= /a>" ~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, 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 p= revent from leaking resources. They fail, however, to prevent a user from u= sing the resource after it has been released. For instance, writing:

input_char (In_channel.with_file fn (fun x -> x))

is perfectl= y legal type-wise, but will fail at run-time. There are of course less obvi= ous situations, for instance if you define a function:

val lines : i= n_channel -> string Stream.t

then the following will also fail:

Stream.iter f (In_channel.wit= h_file fn lines)

My question is the following: is there a way to hav= e the compiler check resources are not used after they are closed? I presum= e this can only be achieved by strongly restricting the kind of function pa= ssed to [with_file]. One simple restriction I see is to define a type of im= mediate value, that roughly correspond to "simple" datatypes (no = closures, 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 -> 'a list t
=C2=A0 val tuple : ('a ->= ; 'a t) -> ('b -> 'b t) -> ('a * 'b) -> (&#= 39;a * 'b) t
=C2=A0 (* for records, use the same trick than in http://www.lexifi.com/blog/dy= namic-types *)
=C2=A0 ...
end

and have the type of [with_f= ile] changed to

val with_file : string -> f:(in_channel -> 'a Immediate.t) -&= gt; 'a

I'm sure there are lots of smarter solutions out there. Would anyon= e happen to know some?

Cheers,
=C2=A0 Philippe.



--047d7bdc7cae7ff28605001f4f55--