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 02E3F7F747 for ; Fri, 8 Aug 2014 20:23:13 +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.182; 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.182 as permitted sender) identity=mailfrom; client-ip=209.85.223.182; 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-f182.google.com) identity=helo; client-ip=209.85.223.182; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="markus.mottl@gmail.com"; x-sender="postmaster@mail-ie0-f182.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjsBABkV5VPRVd+2lWdsb2JhbABag19NCgSCc64LhC6XQIdIAYENCBYQAQEBAQcNCQkSK4QEAQEEEhEEGQEUBxILAQMMBgULDQICCR0CAiEBAREBBQEKEgYTCAoJB4gLAQMRDaNdaospgXKDEIpEChknAwpmhHoRAQUOgR6Lc4FFaAeCeYFSBYUABY0MgyqEZYIJgVaMcAOEPRgphSQhLw X-IPAS-Result: AjsBABkV5VPRVd+2lWdsb2JhbABag19NCgSCc64LhC6XQIdIAYENCBYQAQEBAQcNCQkSK4QEAQEEEhEEGQEUBxILAQMMBgULDQICCR0CAiEBAREBBQEKEgYTCAoJB4gLAQMRDaNdaospgXKDEIpEChknAwpmhHoRAQUOgR6Lc4FFaAeCeYFSBYUABY0MgyqEZYIJgVaMcAOEPRgphSQhLw X-IronPort-AV: E=Sophos;i="5.01,826,1400018400"; d="scan'208";a="74341156" Received: from mail-ie0-f182.google.com ([209.85.223.182]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 20:23:12 +0200 Received: by mail-ie0-f182.google.com with SMTP id y20so7000504ier.13 for ; Fri, 08 Aug 2014 11:23:11 -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=3TWdZaJFPKZZ2qzMCCqYY85OPb4Hv4UK6qv2Wii1fBM=; b=exMWlOmGJ5YdYJe4v3S1kUrbwlZXrlt6O1OokGATqFD59Eqf66aX4CwIC7Tzg2F59z WxUn7kivkd1WXaI0eliXnBbCrqTUev5a/Fd4crfIazyalpESJf9cBxMmxOBtIXoy+MJi UevItz+k8vNXXEYYCj8q86xc/yS6h2z5jgX6gioo2wjr5VqiJUMo4b6alNphspQalSY7 WYnRHM7AM+Ikp93WPEq8L9tE9KPXQAUvUInPUXI30PDiztpj9s4xsGxGAT8jn0wCjt7f ch0FXXpjhoDF+R3Iygs7Ji/X01E1HswK5BYRBZ3hrfl9bLvaKoaMyz2UbyziY/OKkSCu e/Xg== MIME-Version: 1.0 X-Received: by 10.50.118.4 with SMTP id ki4mr7865748igb.16.1407522190916; Fri, 08 Aug 2014 11:23:10 -0700 (PDT) Received: by 10.107.135.133 with HTTP; Fri, 8 Aug 2014 11:23:10 -0700 (PDT) In-Reply-To: References: Date: Fri, 8 Aug 2014 14:23:10 -0400 Message-ID: From: Markus Mottl To: Gabriel Scherer Cc: Ben Millwood , Philippe Veber , caml users Content-Type: text/plain; charset=UTF-8 Subject: Re: [Caml-list] Not letting channels escape. 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 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 just 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 = >> ST.with_file "foo.txt" ~f:{ >> ST.f = fun c -> ST.return (fun () -> ignore (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 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 >> > >> > >> >> >> >> -- >> 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