But you can't do any meaningful computation with this value.<div>It's just a blackbox.</div><div><br></div><div>In your example, the (ST.input_line c) inside the closure just build a value of type (string option, '_s) t for a specific s.</div><div>In particular you will never be able to execute any action on the input channel.</div><div><br></div><div>This is not the case with the proposed implementation, because effects are executed immediately.</div><div>To ensure isolation, all effects should be "frozen":</div><div><br></div><div><div>module ST : sig</div><div>&nbsp; type ('a, 's) t</div><div>&nbsp; val return : 'a -&gt; ('a, 's) t</div><div>&nbsp; val bind : ('a, 's) t -&gt; ('a -&gt; ('b, 's) t) -&gt; ('b, 's) t</div><div>&nbsp; type 's chan</div><div>&nbsp; type 'a f = { f : 's . 's chan -&gt; ('a, 's) t }</div><div>&nbsp; val with_file : string -&gt; f:'a f -&gt; 'a</div><div><br></div><div>&nbsp; val input_line : 's chan -&gt; (string, 's) t</div><div>end = struct</div><div>&nbsp; type ('a, 's) t = unit -&gt; 'a</div><div>&nbsp; let return x = fun () -&gt; x</div><div>&nbsp; let bind x f = fun () -&gt; f (x ()) ()</div><div><br></div><div>&nbsp; type 's chan = in_channel</div><div>&nbsp; type 'a f = { f : 's . 's chan -&gt; ('a, 's) t }</div><div>&nbsp; let with_file fp ~f:{ f } =</div><div>&nbsp; &nbsp; let ic = open_in fp in</div><div>&nbsp; &nbsp; try</div><div>&nbsp; &nbsp; &nbsp; let result = f ic () in</div><div>&nbsp; &nbsp; &nbsp; close_in_noerr ic;</div><div>&nbsp; &nbsp; &nbsp; result</div><div>&nbsp; &nbsp; with exn -&gt;</div><div>&nbsp; &nbsp; &nbsp; close_in_noerr ic;</div><div>&nbsp; &nbsp; &nbsp; raise exn</div><div>&nbsp; let input_line c = fun () -&gt; input_line c</div><div>end</div><div><br></div>Le ven. 8 août 2014 à 20:30, Markus Mottl &lt;markus.mottl@gmail.com&gt; a écrit&nbsp;:<br>
<blockquote type="cite"><div class="plaintext" style="white-space: pre-wrap;">The escaping value can still be manipulated through a closure, outside
of "with_file".  The goal was to prevent this.

On Fri, Aug 8, 2014 at 2:28 PM, Frédéric Bour &lt;frederic.bour@lakaban.net&gt; wrote:
<blockquote> ST.input_line is just a reified effect, it can't be executed outside of the
 ST monad.
 You can make the value escape, but you can't do anything with it.

 And because of the existential variable being propagated, it can't be
 executed outside of this run of the ST value.

 Le ven. 8 août 2014 à 19:23, Markus Mottl &lt;markus.mottl@gmail.com&gt; a écrit :

 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 &lt;gabriel.scherer@gmail.com&gt; 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 ( <a href="http://protz.github.io/mezzo/">http://protz.github.io/mezzo/</a> ).
 On Fri, Aug 8, 2014 at 7:21 PM, Markus Mottl &lt;markus.mottl@gmail.com&gt; 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 -&gt; ST.return
 (fun () -&gt; 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 &lt;bmillwood@janestreet.com&gt; wrote: &gt; I
 protected against that in my module by carrying the existential type &gt;
 variable in the result of input_line as well, because I stumbled into &gt;
 exactly that example while originally drafting my e-mail :) &gt; &gt; In a sense
 I'm reinventing monadic IO but in a bit of a half-hearted &gt; way. It &gt;
 wouldn't take much work to make it a bit more fully-hearted, but it &gt; would
<blockquote> still be inconvenient to actually use. &gt; &gt; &gt; On 8 August 2014 16:44,
</blockquote> Markus Mottl &lt;markus.mottl@gmail.com&gt; wrote: &gt;&gt; &gt;&gt; It doesn't even require
 references to screw things up here. Just &gt;&gt; return the closure containing
 the channel from within "f": &gt;&gt; &gt;&gt; In_channel.with_file "foo.txt" ~f:(fun ic
 () -&gt; input_line ic) &gt;&gt; |&gt; fun f -&gt; f () &gt;&gt; &gt;&gt; The initial Stream-example is
 basically just an instance of this &gt;&gt; "returning a closure" problem. &gt;&gt; &gt;&gt;
 But the availability of references and exceptions arguably makes &gt;&gt; things
 worse, because you cannot even use monadic I/O + existential &gt;&gt; types to
 achieve guaranteed safety. &gt;&gt; &gt;&gt; Regards, &gt;&gt; Markus &gt;&gt; &gt;&gt; On Fri, Aug 8,
 2014 at 10:49 AM, Ben Millwood &gt;&gt; &lt;bmillwood@janestreet.com&gt; &gt;&gt; wrote: &gt;&gt; &gt;
 It's been pointed out to me that the above certainly isn't perfectly &gt;&gt; &gt;
 secure. &gt;&gt; &gt; E.g. &gt;&gt; &gt; &gt;&gt; &gt; let f = ref (fun () -&gt; ()) in &gt;&gt; &gt; with_file
 "safe.ml" ~f:{ f = fun c -&gt; &gt;&gt; &gt; return (f := fun () -&gt; &gt;&gt; &gt; Fn.ignore (map
 (input_line c) ~f:print_string_option)) }; &gt;&gt; &gt; !f () &gt;&gt; &gt; &gt;&gt; &gt; gets
 Exception: (Sys_error "Bad file descriptor"). Even though the &gt;&gt; &gt; channel
<blockquote><blockquote> &gt; and any operations on it can't escape the closure, the type of a &gt;&gt; &gt;
</blockquote></blockquote> function &gt;&gt; &gt; which uses them needn't mention them at all. &gt;&gt; &gt; &gt;&gt; &gt; It's
 pretty hard to do anything about this in the presence of &gt;&gt; &gt; unrestricted
<blockquote><blockquote> &gt; side effects, so perhaps there's a reason why the Haskellers are &gt;&gt; &gt;
</blockquote></blockquote> excited &gt;&gt; &gt; about this sort of thing and you don't see it in OCaml so much
 :) &gt;&gt; &gt; &gt;&gt; &gt; That said, you do seem to be forced to make a bit more of an
 effort &gt;&gt; &gt; to &gt;&gt; &gt; break &gt;&gt; &gt; things here, so I don't think the technique
 is completely without &gt;&gt; &gt; merit, &gt;&gt; &gt; perhaps in cases where you'd be
 defining all your own operations &gt;&gt; &gt; anyway, &gt;&gt; &gt; so &gt;&gt; &gt; the duplication
 isn't an issue. &gt;&gt; &gt; &gt;&gt; &gt; &gt;&gt; &gt; On 8 August 2014 12:30, Ben Millwood
 &lt;bmillwood@janestreet.com&gt; &gt;&gt; &gt; wrote: &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; There's a trick with
 existential types, as used in e.g. Haskell's ST &gt;&gt; &gt;&gt; monad. It uses the
 fact that an existentially-quantified type &gt;&gt; &gt;&gt; variable &gt;&gt; &gt;&gt; can't &gt;&gt; &gt;&gt;
 escape its scope, so if your channel type and results that depend on &gt;&gt; &gt;&gt;
 it &gt;&gt; &gt;&gt; are &gt;&gt; &gt;&gt; parametrised by an existential type variable, the
 corresponding &gt;&gt; &gt;&gt; values &gt;&gt; &gt;&gt; can't &gt;&gt; &gt;&gt; escape the scope of the
 callback either. &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; Something like: &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; module ST : sig &gt;&gt;
<blockquote><blockquote> type ('a, 's) t &gt;&gt; &gt;&gt; include Monad.S2 with type ('a, 's) t := ('a, 's) t
 &gt;&gt; type 's chan &gt;&gt; &gt;&gt; type 'a f = { f : 's . 's chan -&gt; ('a, 's) t } &gt;&gt;
 val with_file : string -&gt; f:'a f -&gt; 'a &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; val input_line : 's
</blockquote></blockquote> chan -&gt; (string option, 's) t &gt;&gt; &gt;&gt; end = struct &gt;&gt; &gt;&gt; module T = struct &gt;&gt;
<blockquote><blockquote> type ('a, 's) t = 'a &gt;&gt; &gt;&gt; let return x = x &gt;&gt; &gt;&gt; let bind x f = f x &gt;&gt;
 let map x ~f = f x &gt;&gt; &gt;&gt; end &gt;&gt; &gt;&gt; include T &gt;&gt; &gt;&gt; include Monad.Make2(T)
 &gt;&gt; type 's chan = In_channel.t &gt;&gt; &gt;&gt; type 'a f = { f : 's . 's chan -&gt;
</blockquote></blockquote> ('a, 's) t } &gt;&gt; &gt;&gt; let with_file fp ~f:{ f } = In_channel.with_file fp ~f &gt;&gt;
<blockquote><blockquote> let input_line c = In_channel.input_line c &gt;&gt; &gt;&gt; end &gt;&gt; &gt;&gt; ;; &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt;
</blockquote></blockquote> match ST.with_file "safe.ml" ~f:{ ST.f = fun c -&gt; ST.input_line c } &gt;&gt; &gt;&gt;
 with &gt;&gt; &gt;&gt; | None -&gt; print_endline "None" &gt;&gt; &gt;&gt; | Some line -&gt; print_endline
 line &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; On 8 August 2014 11:23, Philippe Veber
 &lt;philippe.veber@gmail.com&gt; &gt;&gt; &gt;&gt; wrote: &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; Dear all, &gt;&gt; &gt;&gt;&gt; &gt;&gt;
<blockquote><blockquote><blockquote> many libraries like lwt, batteries or core provide a very nice &gt;&gt; &gt;&gt;&gt;
</blockquote></blockquote></blockquote> idiom &gt;&gt; &gt;&gt;&gt; to &gt;&gt; &gt;&gt;&gt; be used when a function uses a resource (file,
 connection, mutex, &gt;&gt; &gt;&gt;&gt; et &gt;&gt; &gt;&gt;&gt; cetera), for instance in
 Core.In_channel, the function: &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; val with_file : ?binary:bool -&gt;
 string -&gt; f:(t -&gt; 'a) -&gt; 'a &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; opens a channel for [f] and
 ensures it is closed after the call to &gt;&gt; &gt;&gt;&gt; [f], &gt;&gt; &gt;&gt;&gt; even if it raises
 an exception. So these functions basically &gt;&gt; &gt;&gt;&gt; prevent &gt;&gt; &gt;&gt;&gt; from &gt;&gt; &gt;&gt;&gt;
 leaking resources. They fail, however, to prevent a user from using &gt;&gt; &gt;&gt;&gt;
 the &gt;&gt; &gt;&gt;&gt; resource after it has been released. For instance, writing: &gt;&gt;
<blockquote><blockquote><blockquote> &gt;&gt; &gt;&gt;&gt; input_char (In_channel.with_file fn (fun x -&gt; x)) &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt;
</blockquote></blockquote></blockquote> is perfectly legal type-wise, but will fail at run-time. There are &gt;&gt; &gt;&gt;&gt; of
<blockquote><blockquote> &gt;&gt;&gt; course less obvious situations, for instance if you define a &gt;&gt; &gt;&gt;&gt;
</blockquote></blockquote> function: &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; val lines : in_channel -&gt; string Stream.t &gt;&gt; &gt;&gt;&gt; &gt;&gt;
<blockquote><blockquote><blockquote> then the following will also fail: &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; Stream.iter f
</blockquote></blockquote></blockquote> (In_channel.with_file fn lines) &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; My question is the following:
 is there a way to have the compiler &gt;&gt; &gt;&gt;&gt; check &gt;&gt; &gt;&gt;&gt; resources are not
 used after they are closed? I presume this can &gt;&gt; &gt;&gt;&gt; only &gt;&gt; &gt;&gt;&gt; be &gt;&gt; &gt;&gt;&gt;
 achieved by strongly restricting the kind of function passed to &gt;&gt; &gt;&gt;&gt;
 [with_file]. &gt;&gt; &gt;&gt;&gt; One simple restriction I see is to define a type of
 immediate &gt;&gt; &gt;&gt;&gt; value, &gt;&gt; &gt;&gt;&gt; that &gt;&gt; &gt;&gt;&gt; roughly correspond to "simple"
 datatypes (no closures, no lazy &gt;&gt; &gt;&gt;&gt; expressions): &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; module
 Immediate : sig &gt;&gt; &gt;&gt;&gt; type 'a t = private 'a &gt;&gt; &gt;&gt;&gt; val int : int -&gt; int t
<blockquote><blockquote> &gt;&gt;&gt; val list : ('a -&gt; 'a t) -&gt; 'a list -&gt; 'a list t &gt;&gt; &gt;&gt;&gt; val tuple :
</blockquote></blockquote> ('a -&gt; 'a t) -&gt; ('b -&gt; 'b t) -&gt; ('a * 'b) -&gt; ('a * &gt;&gt; &gt;&gt;&gt; 'b) t &gt;&gt; &gt;&gt;&gt; (*
 for records, use the same trick than in &gt;&gt; &gt;&gt;&gt;
 <a href="http://www.lexifi.com/blog/dynamic-types">http://www.lexifi.com/blog/dynamic-types</a> *) &gt;&gt; &gt;&gt;&gt; ... &gt;&gt; &gt;&gt;&gt; end &gt;&gt; &gt;&gt;&gt; &gt;&gt;
<blockquote><blockquote><blockquote> and have the type of [with_file] changed to &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; val with_file
</blockquote></blockquote></blockquote> : string -&gt; f:(in_channel -&gt; 'a Immediate.t) -&gt; 'a &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; I'm sure
 there are lots of smarter solutions out there. Would &gt;&gt; &gt;&gt;&gt; anyone &gt;&gt; &gt;&gt;&gt;
 happen to know some? &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt;&gt; Cheers, &gt;&gt; &gt;&gt;&gt; Philippe. &gt;&gt; &gt;&gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt;
<blockquote> &gt;&gt; &gt;&gt; &gt;&gt; &gt;&gt; -- &gt;&gt; Markus Mottl <a href="http://www.ocaml.info">http://www.ocaml.info</a>
</blockquote> markus.mottl@gmail.com &gt; &gt; -- Markus Mottl <a href="http://www.ocaml.info">http://www.ocaml.info</a>
 markus.mottl@gmail.com -- Caml-list mailing list. Subscription management
 and archives: <a href="https://sympa.inria.fr/sympa/arc/caml-list">https://sympa.inria.fr/sympa/arc/caml-list</a> Beginner's list:
 <a href="http://groups.yahoo.com/group/ocaml_beginners">http://groups.yahoo.com/group/ocaml_beginners</a> Bug reports:
 <a href="http://caml.inria.fr/bin/caml-bugs">http://caml.inria.fr/bin/caml-bugs</a>

 --
 Markus Mottl <a href="http://www.ocaml.info">http://www.ocaml.info</a> markus.mottl@gmail.com
 --
 Caml-list mailing list. Subscription management and archives:
 <a href="https://sympa.inria.fr/sympa/arc/caml-list">https://sympa.inria.fr/sympa/arc/caml-list</a> Beginner's list:
 <a href="http://groups.yahoo.com/group/ocaml_beginners">http://groups.yahoo.com/group/ocaml_beginners</a> Bug reports:
 <a href="http://caml.inria.fr/bin/caml-bugs">http://caml.inria.fr/bin/caml-bugs</a>
</blockquote>


<div>-- 
</div>Markus Mottl        <a href="http://www.ocaml.info">http://www.ocaml.info</a>        markus.mottl@gmail.com

<div>-- 
</div>Caml-list mailing list.  Subscription management and archives:
<a href="https://sympa.inria.fr/sympa/arc/caml-list">https://sympa.inria.fr/sympa/arc/caml-list</a>
Beginner's list: <a href="http://groups.yahoo.com/group/ocaml_beginners">http://groups.yahoo.com/group/ocaml_beginners</a>
Bug reports: <a href="http://caml.inria.fr/bin/caml-bugs">http://caml.inria.fr/bin/caml-bugs</a></div></blockquote></div>