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 56BBE7F747 for ; Fri, 8 Aug 2014 13:30:42 +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.233; 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.233 as permitted sender) identity=mailfrom; client-ip=38.105.200.233; 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@mxout4.mail.janestreet.com) identity=helo; client-ip=38.105.200.233; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="bmillwood@janestreet.com"; x-sender="postmaster@mxout4.mail.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqgCAFq05FMmacjpnGdsb2JhbABag19XBIJzyAmBY4dIAYEOCBYQAQEBAQEGFgk9hAQBAQMBEhEEGQEBNwEECwsLNwICIQESAQUBHAYTGweIDAMJCAMKoyZqijJ3hQIBBYp4DYV3EQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IPAS-Result: AqgCAFq05FMmacjpnGdsb2JhbABag19XBIJzyAmBY4dIAYEOCBYQAQEBAQEGFgk9hAQBAQMBEhEEGQEBNwEECwsLNwICIQESAQUBHAYTGweIDAMJCAMKoyZqijJ3hQIBBYp4DYV3EQYKjRWBRWgHgnmBUpU8hGWCCYFUhVCHIIQ8GCmFCWs X-IronPort-AV: E=Sophos;i="5.01,824,1400018400"; d="scan'208";a="74308250" Received: from mxout4.mail.janestreet.com ([38.105.200.233]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 08 Aug 2014 13:30:40 +0200 Received: from tot-oib-smtp1.delacy.com ([172.27.22.15] helo=tot-smtp) by mxout4.mail.janestreet.com with esmtps (UNKNOWN:DHE-RSA-AES256-GCM-SHA384:256) (Exim 4.82) (envelope-from ) id 1XFiNa-0004ot-Lf for caml-list@inria.fr; Fri, 08 Aug 2014 07:30:38 -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 1XFiNa-0004qb-Iy for caml-list@inria.fr; Fri, 08 Aug 2014 07:30:38 -0400 Received: from mail-qg0-f50.google.com ([209.85.192.50]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1:RC4-SHA:128) (Exim 4.72) (envelope-from ) id 1XFiNa-0003r9-GM for caml-list@inria.fr; Fri, 08 Aug 2014 07:30:38 -0400 Received: by mail-qg0-f50.google.com with SMTP id q108so5732694qgd.23 for ; Fri, 08 Aug 2014 04:30:38 -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=q4d0b5xkrvPQCDv0kHveaV5wiTWzqYcpgpjuZ+ByP+I=; b=pmUSumlt+107DDf0EcG6zIU3ulHFshPcoKtL48ZlpvMaT7I2Z0lVNYdwdG//4B5LXO MONiOeX7ZoFKwKn5I+KnGqdN47Ed3bPheNNcxR4I9nZZ6JQ7KXdrPXpzJGKbcpMhBtj/ cexEb/QgGnxkjeDVv334Kzw+mUdESQaaoUltk= 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=q4d0b5xkrvPQCDv0kHveaV5wiTWzqYcpgpjuZ+ByP+I=; b=jRVjHqjHLjQ+pjO/1Gizc7HXvY6VZhSANlYM4NcnvPFRWUBexrrPiOyJ0ZkT3x5/GL GOY3CW3rZH+68akvfGxaHNX4z1MojKbt1ZZHe/7M8BgWNrX8TLvBbUXCI5s408oEMXc/ UEtl2SNpM0M1m4ivT36FQQ+lwth3xNIJbWds/iW6OTL5DXU4f3A/wdGjXm2linTrsstO PAdUbDC1BCUZ8tplX/oUkTto5C8Zge5LqroQ7+d4gQirEJO0MxWb3wJVcSARcjjcBIF2 htZa7AKbF2D9yWbeYNs8/QHFI4PmTw4t1umBUQkfkB+Sejnf5JvTAh2pvC1aLTRIbP7A 4F5w== X-Gm-Message-State: ALoCoQmE3/kWhxwv1DPA5p6NHxj4YQ3De5sZPl0jJujETRGQw6gg5nIanqFgeCnaBGIWPl/6/+OIm8Uk+MjK+iSGnAZ9uNek6AwIf4qaeUSg71ROyCAphmfTqeFgHVhtu2Sg5lVtjPAp X-Received: by 10.140.84.231 with SMTP id l94mr21855330qgd.84.1407497438304; Fri, 08 Aug 2014 04:30:38 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.140.84.231 with SMTP id l94mr21855316qgd.84.1407497438101; Fri, 08 Aug 2014 04:30:38 -0700 (PDT) Received: by 10.140.82.41 with HTTP; Fri, 8 Aug 2014 04:30:38 -0700 (PDT) In-Reply-To: References: Date: Fri, 8 Aug 2014 12:30:38 +0100 Message-ID: From: Ben Millwood To: Philippe Veber Cc: caml users Content-Type: multipart/alternative; boundary=001a11c1198ad2183905001c8869 Subject: Re: [Caml-list] Not letting channels escape. --001a11c1198ad2183905001c8869 Content-Type: text/plain; charset=UTF-8 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. > > --001a11c1198ad2183905001c8869 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
There's a trick with existential types,= as used in e.g. Haskell's ST monad. It uses the fact that an existenti= ally-quantified type variable can't escape its scope, so if your channe= l type and results that depend on it are parametrised by an existential typ= e variable, the corresponding values can't escape the scope of the call= back 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" ~f:{ ST.= f =3D fun c -> ST.input_line c } with
| None -> print_endline &quo= t;None"
| Some line -> print_endline line


On 8 August 2014 11:23, Philippe V= eber <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.


--001a11c1198ad2183905001c8869--