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 EDEBF7F747 for ; Fri, 8 Aug 2014 17:44:46 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of markus.mottl@gmail.com) identity=pra; client-ip=209.85.223.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of markus.mottl@gmail.com designates 209.85.223.181 as permitted sender) identity=mailfrom; client-ip=209.85.223.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="markus.mottl@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-ie0-f181.google.com) identity=helo; client-ip=209.85.223.181; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-ie0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AqICACPv5FPRVd+1lGdsb2JhbABag19XBIJzsjiXQIdIAYELCBYQAQEBAQcLCwkSK4QEAQEEEhEEGQEUBx0BAwwGBQsDCgICJgICIQEBEQEFARwGExsHiAsBAxENo0JqiymBcoMQikEKGScNZoR6EQEFDoEei3OBRWgHgnmBUgWSD4MohGWCCYFUjHCEPBgphSQhLw X-IPAS-Result: AqICACPv5FPRVd+1lGdsb2JhbABag19XBIJzsjiXQIdIAYELCBYQAQEBAQcLCwkSK4QEAQEEEhEEGQEUBx0BAwwGBQsDCgICJgICIQEBEQEFARwGExsHiAsBAxENo0JqiymBcoMQikEKGScNZoR6EQEFDoEei3OBRWgHgnmBUgWSD4MohGWCCYFUjHCEPBgphSQhLw X-IronPort-AV: E=Sophos;i="5.01,825,1400018400"; d="scan'208";a="74331094" Received: from mail-ie0-f181.google.com ([209.85.223.181]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 17:44:45 +0200 Received: by mail-ie0-f181.google.com with SMTP id rp18so6368534iec.26 for ; Fri, 08 Aug 2014 08:44:44 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=psljBk32m3Rp67718Hoix5/JPJBtyJQapOEAqUALM+M=; b=DKa8EHx6fZhQO9yxH543mSRheGLLH0twQRpOvTybL4OPPAQ6iEF/Ma4RmYp8+pSFd1 j4xTAT3m4fiEh9j6I2dqL/NO5xLR84zQpUYDfb1w9uGpywLYmjJCT0EJ6lSTzp7UZbQW vdmyebI7+d8ZSRuNaMs2hXE6+Mlr/34N7oniz4ZVqNiCyxEQFN26X1g9CjiFiI4u7IW6 rARUha8M5/wibQ3vwFbczpmRTTKFv+vwBaWmP8VpWR1wO3LlCANp/aD+2f5GqoKvFZu6 BJhaDVZ6z4xYp4eg6qTMIZYLIBaWqmyxURyLHO6WvNPuzw2Ms7XeXAeq4l3THOp793/M Ntrw== MIME-Version: 1.0 X-Received: by 10.50.118.4 with SMTP id ki4mr6525050igb.16.1407512684620; Fri, 08 Aug 2014 08:44:44 -0700 (PDT) Received: by 10.107.135.133 with HTTP; Fri, 8 Aug 2014 08:44:44 -0700 (PDT) In-Reply-To: References: Date: Fri, 8 Aug 2014 11:44:44 -0400 Message-ID: From: Markus Mottl To: Ben Millwood Cc: Philippe Veber , caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Not letting channels escape. 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