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 B74F07F747 for ; Fri, 8 Aug 2014 12:24:14 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.212.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of philippe.veber@gmail.com designates 209.85.212.180 as permitted sender) identity=mailfrom; client-ip=209.85.212.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.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@mail-wi0-f180.google.com) identity=helo; client-ip=209.85.212.180; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-wi0-f180.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ak4DACSk5FPRVdS0lGdsb2JhbABag19XBIVTr0SXQIVQgwYIFhABAQEBBwsLCRIrhBwVGQEbHgMSCQddAREBBQEiLgeICwEDEQ2feIMYao0bgxCKNwoZJw1mhSIBBQ6OVoU6BY8DgwyKFpMAGCmFCjsv X-IPAS-Result: Ak4DACSk5FPRVdS0lGdsb2JhbABag19XBIVTr0SXQIVQgwYIFhABAQEBBwsLCRIrhBwVGQEbHgMSCQddAREBBQEiLgeICwEDEQ2feIMYao0bgxCKNwoZJw1mhSIBBQ6OVoU6BY8DgwyKFpMAGCmFCjsv X-IronPort-AV: E=Sophos;i="5.01,824,1400018400"; d="scan'208";a="88706031" Received: from mail-wi0-f180.google.com ([209.85.212.180]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 08 Aug 2014 12:24:14 +0200 Received: by mail-wi0-f180.google.com with SMTP id n3so761067wiv.7 for ; Fri, 08 Aug 2014 03:24:14 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:from:date:message-id:subject:to:content-type; bh=blIj3ApJyflX7+lQuuqvChDsmjAx9iazPlpFS4h3YB4=; b=pWv+QEfruQKqrjVVlKzIcbygG+L34PkLb2e9axtDlX/fhrO3nuVkeoK4brHNgoRbRR PHtpIvz6jCHDSdSwWjf65GlZBV1vMPZFEw+c8RfL6IH16ngQ7vduUqn/Nm94BRJc/DBT YA4vbS4UZR8Ns0JfMLS9HDs1kwY5LELyUaNGVbUx/DLCXHx3DLtgtk1LWR80ah+v3/Uy ogp9mobRurAHqOjHEFSeRzhieKxyZqzMh95YjtuRlYre9zf+8XRxn6031OYRLb/nshWE Bm0WBH48tK5xIAwmzgQbP8TeyO+dLlrIpJUVZnotdiPHzWh4F1gaRqOz/qhYbrkXXM8O 8dhw== X-Received: by 10.180.90.11 with SMTP id bs11mr3132467wib.47.1407493454018; Fri, 08 Aug 2014 03:24:14 -0700 (PDT) MIME-Version: 1.0 Received: by 10.194.166.132 with HTTP; Fri, 8 Aug 2014 03:23:53 -0700 (PDT) From: Philippe Veber Date: Fri, 8 Aug 2014 12:23:53 +0200 Message-ID: To: caml users Content-Type: multipart/alternative; boundary=f46d043c7e1c59bea905001b9bb9 X-Validation-by: philippe.veber@gmail.com Subject: [Caml-list] Not letting channels escape. --f46d043c7e1c59bea905001b9bb9 Content-Type: text/plain; charset=ISO-8859-1 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. --f46d043c7e1c59bea905001b9bb9 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Dear all,

many libraries like lwt, batte= ries or core provide a very nice idiom to be used when a function uses a re= source (file, connection, mutex, et cetera), for instance in Core.In_channe= l, 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
=A0 type 'a t =3D private 'a
=A0 v= al int : int -> int t
=A0 val list : ('a -> 'a t) -> &#= 39;a list -> 'a list t
=A0 val tuple : ('a -> 'a t) -&= gt; ('b -> 'b t) -> ('a * 'b) -> ('a * 'b)= t
=A0 (* for records, use the same trick than in http://www.lexifi.com/blog/dynamic-types *)=A0 ...
end

and have the type of [with_file] changed to

v= al with_file : string -> f:(in_channel -> 'a Immediate.t) -> &= #39;a

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

Cheers,
=A0 Philippe.

--f46d043c7e1c59bea905001b9bb9--