Functional - Undoing state in ML

Author

Undoing state in ML

Jon Harrop

2007-02-25, 8:03 am

What's the best idiomatic way to ensure that state changes get undone when
subcode completes?

I currently do something like:

let read file k =
let ch = open_in file in
try k ch finally
close_in ch

but there is always the possibility that a user will return the channel from
the continuation and try to read after it has been closed.

Is there a better way?

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

Neelakantan Krishnaswami

2007-02-25, 7:05 pm

In article <45e16026$0$8737$ed2619ec@ptn-nntp-reader02.plus.net>, Jon Harrop
wrote:
>
> What's the best idiomatic way to ensure that state changes get undone when
> subcode completes?
>
> I currently do something like:
>
> let read file k =
> let ch = open_in file in
> try k ch finally
> close_in ch
>
> but there is always the possibility that a user will return the
> channel from the continuation and try to read after it has been
> closed.
>
> Is there a better way?

This is not idiomatic Ocaml (for anyone except me, maybe), but there
is a way to ensure this. Basically, you can use a monad to hide the
channel from the user, and still let them read from the file. I also
wrote a pretty spiffy camlP4 macro to make writing monadic code very
pleasant.

module type FILE =
sig
type 'a t

val unit : (unit -> 'a) -> 'a t
val bind : ('a -> 'b t) -> 'a t -> 'b t

val read_char : char option t
val read_line : string option t

val run : string -> 'a t -> 'a
end

module File : FILE =
struct
type 'a t = in_channel -> 'a

let unit v = fun input -> v()

let bind f m = fun input ->
let v = m input in
f v input

let read_char input =
try Some(input_char input) with End_of_file -> None

let read_line input =
try Some(input_line input) with End_of_file -> None

let run filename f =
let input = open_in filename in
try
let ans = f input in (close_in input; ans)
with
e -> (close_in input; raise e)
end

An example of use (using my camlp4 extension) would look like:

let rec get_lines () =
monad(File) begin
match val File.read_line with
| None -> return []
| Some(s) -> let val rest = get_lines() in return (s :: rest)
end

let lines = File.run "foo.txt" (get_lines())

(A real get_lines would have a tail-recursive accumulator, but this is
just an example.)

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Torben Ægidius Mogensen

2007-02-26, 4:12 am

Jon Harrop <jon@ffconsultancy.com> writes:

> What's the best idiomatic way to ensure that state changes get undone when
> subcode completes?
>
> I currently do something like:
>
> let read file k =
> let ch = open_in file in
> try k ch finally
> close_in ch
>
> but there is always the possibility that a user will return the channel from
> the continuation and try to read after it has been closed.
>
> Is there a better way?

While they are not in ML, linear types are useful for such: File
handles are linearly typed, so a well-typed program can not leave
files unclosed, nor can it access a file after it is closed.

Neelakantan Krishnaswam suggested monads, which is another way to
enforce linearity.

Torben

Jon Harrop

2007-02-26, 8:06 am

Torben Ægidius Mogensen wrote:
> While they are not in ML, linear types are useful for such: File
> handles are linearly typed, so a well-typed program can not leave
> files unclosed, nor can it access a file after it is closed.

Right. I've heard of those in the context of concurrency, presumably to
enforce equivalent use for locks.

> Neelakantan Krishnaswam suggested monads, which is another way to
> enforce linearity.

Yep. Thanks Neel.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

Ivan Jager

2007-02-26, 7:08 pm

On Sun, 25 Feb 2007, Jon Harrop wrote:
> What's the best idiomatic way to ensure that state changes get undone when
> subcode completes?
>
> I currently do something like:
>
> let read file k =
> let ch = open_in file in
> try k ch finally
> close_in ch
>
> but there is always the possibility that a user will return the channel from
> the continuation and try to read after it has been closed.

I'm guessing you already know about ocaml's Gc.finalise?

Ivan

Neelakantan Krishnaswami

2007-02-26, 7:08 pm

In article <slrneu3mqp.n11.neelk@gs3106.sp.cs.cmu.edu>, Neelakantan
Krishnaswami wrote:
>
> An example of use (using my camlp4 extension) would look like:
>
> let rec get_lines () =
> monad(File) begin
> match val File.read_line with
> | None -> return []
> | Some(s) -> let val rest = get_lines() in return (s :: rest)
> end

It occurs to me that I should show what this elaborates into:

let rec get_lines () =
File.bind
(function
| None -> File.unit (fun () -> [])
| Some(s) ->
File.bind
(fun rest -> File.unit (fun () -> s :: rest))
(get_lines()))
File.read_line

The reason for using macrology to rewrite the convoluted style into
something more transparent should be clear. :)

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Jon Harrop

2007-02-26, 10:07 pm

Neelakantan Krishnaswami wrote:
> let rec get_lines () =
> File.bind
> (function
> | None -> File.unit (fun () -> [])
> | Some(s) ->
> File.bind
> (fun rest -> File.unit (fun () -> s :: rest))
> (get_lines()))
> File.read_line
>
> The reason for using macrology to rewrite the convoluted style into
> something more transparent should be clear. :)

Thanks for the clarification. I assume the macro is used because the same
factoring cannot be expressed with OCaml's type system?

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

Jon Harrop

2007-02-26, 10:07 pm

Ivan Jager wrote:
> I'm guessing you already know about ocaml's Gc.finalise?

Yes, that really solves a slightly different problem though (although it
might be preferable to no solution). I want to guarantee that, after I
explicitly dispose of the file handle and close it, nobody can try to use
the handle to the closed file.

As Torben says, linear types solve this and OCaml doesn't yet have them.

Using a finaliser doesn't give any assurance about when the file gets closed
but it does guarantee that nobody can use a handle to a closed file. You
can use both explicit dispose and the finaliser (as IDisposable does
in .NET) but you don't get the assurance I'm after.

I think the solution I proposed (factoring open and close into a HOF,
equivalent to RAII) is better than using a finaliser because you get
lifetime guarantees. In particular, the finaliser approach can suffer from
closures capturing the file handle and keeping it alive indefinitely.

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

Neelakantan Krishnaswami

2007-02-27, 7:08 pm

In article <45e39f30$0$8745$ed2619ec@ptn-nntp-reader02.plus.net>, Jon
Harrop wrote:
>
> Thanks for the clarification. I assume the macro is used because the
> same factoring cannot be expressed with OCaml's type system?

No, the type system expresses the idea perfectly well. The basic idea
is that we define an abstract type of actions which return a value,
possibly reading from a file to do so:

type 'a t

There's an operation to turn a thunk into an action:

val unit : (unit -> 'a) -> 'a t

And then there's an operation to sequence a pair of actions:

val bind : ('a -> 'b t) -> 'a t -> 'b t

The way to read this is that if you have a function which takes a value 'a
and returns an action 'b t, you can construct a function 'a t -> 'b t by
running the first action and then handing its value to the function.

So this function captures the idea of sequencing actions.

Then, there are some primitive actions to read from a file:

val read_char : char option t
val read_line : string option t

These will return a character or a line from the file (or None if the
file is at its end). Notice that they don't explicitly take the file
as an argument -- we're keeping that implicit to accidentally returning
it.

Finally, you have a function that will open a file and run an action
on it:

val run : string -> 'a t -> 'a

This is everything you need to construct arbitrary actions over files.

The only trouble is that it's syntactically awkward to express binding
and sequential execution using lambdas:

File.bind (fun x -> e2) e1

is much harder to read than

let val x = e1 in e2

So that's what the macro does -- it rewrites some more familiar syntax
into the primitive constructor calls of our library.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Jon Harrop

2007-02-28, 4:06 am

Neelakantan Krishnaswami wrote:
> In article <45e39f30$0$8745$ed2619ec@ptn-nntp-reader02.plus.net>, Jon
> Harrop wrote:
>
> No, the type system expresses the idea perfectly well.

Ok.

> Then, there are some primitive actions to read from a file:
>
> val read_char : char option t
> val read_line : string option t

This was the bit I was thinking of. You potentially have to wrap all IO
functions.

Do you think the IO interface should have been written this way in the first
place?

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

oleg@pobox.com

2007-02-28, 4:06 am

Jon Harrop wrote:
> What's the best idiomatic way to ensure that state changes get undone when
> subcode completes?

Not to expose the state is a good idea. Neelakantan Krishnaswami
illustrated this by building a Reader monad. However, the monadic
syntax seems ugly, even with the syntactic sugar. Incidentally, the
following
http://www.cas.mcmaster.ca/~carette/pa_monad/

shows Haskell do notation in OCaml (complete with do-let). The
distribution also includes the IO monad. But even with this sugar, the
monadic style is quite ugly. Mainly, in a strict language with a good
library monads are totally unnecessary. The reader monad corresponds
to a dynamic binding effect, which can be implemented directly. The
following test is deliberately patterned after Neelakantan
Krishnaswami's code, for ease of comparison.

(* Please see http://pobox.com/~oleg/ftp/ML/index.html#dynvar
for the Dynvar library
*)
open Dynvar;;
#load "dynvar.cmo";;

module type FILE = sig
val read_char : unit -> char option
val read_line : unit -> string option
val run : string -> (unit -> 'a) -> 'a
end;;

module File : FILE = struct
let dv = dnew () (* hidden, not exported, not available *)

let read_char () =
try Some(input_char (dref dv)) with End_of_file -> None

let read_line () =
try Some(input_line (dref dv)) with End_of_file -> None

let run filename f =
let input = open_in filename in
try
let ans = dlet dv input f in (close_in input; ans)
with
e -> (close_in input; raise e)
end;;

(* Neelakantan Krishnaswami's example *)

let rec get_lines () =
match File.read_line () with
| None -> []
| Some s -> s :: get_lines()
;;

let lines = File.run "/etc/motd" get_lines;;

rossberg@ps.uni-sb.de

2007-02-28, 4:06 am

On 28 Feb., 08:28, o...@pobox.com wrote:
>
> monadic style is quite ugly. Mainly, in a strict language with a good
> library monads are totally unnecessary.

> open Dynvar;;
> #load "dynvar.cmo";;
>
> module type FILE = sig
> val read_char : unit -> char option
> val read_line : unit -> string option
> val run : string -> (unit -> 'a) -> 'a
> end;;

This does not seem to be any safer than Jon's original version. The
advantage is that you do not have to pass the file operations to the
client function explicitly. But it does not statically guarantee
proper sequencing of file operations, and hence does not address Jon's
concern that a file access may accidentally be attempted out-of-scope.

- Andreas

Neelakantan Krishnaswami

2007-02-28, 7:06 pm

In article <45e51e6e$0$8725$ed2619ec@ptn-nntp-reader02.plus.net>, Jon Harrop
wrote:
>Neelakantan Krishnaswami wrote:
>
>
> This was the bit I was thinking of. You potentially have to wrap all IO
> functions.

Yes, that's right. You could also have a function that pushes file
operations into the monad:

val wrap : (in_chan -> 'a) -> 'a t

> Do you think the IO interface should have been written this way in
> the first place?

I think so, but monadic interfaces were not really well-understood
until some time after Caml had been invented, so it's a bit much to
hope that the API would be that way from the beginning. :)

As an aside, I don't think monadic interfaces are the last word;
they're just the best I know of right now.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Chris F Clark

2007-02-28, 7:06 pm

rossberg@ps.uni-sb.de writes:

> On 28 Feb., 08:28, o...@pobox.com wrote:
>
>
> This does not seem to be any safer than Jon's original version. The
> advantage is that you do not have to pass the file operations to the
> client function explicitly. But it does not statically guarantee
> proper sequencing of file operations, and hence does not address Jon's
> concern that a file access may accidentally be attempted out-of-scope.
>
> - Andreas

Please continue discussing this. This topic I find very interesting,
even if my feeble brain can barely follow it. In particular, it seems
to me that one "intention" of monads is to impose "ordering" on
operations (that have state/side effects). Now, if I understand the
conversation, the suggestion previously made is that strict languages
already have mechanisms that order things (the arguments must get
evaluated before the function they are being passed to, for instance)
and that the need for monads is lessened. I take this response as
saying that isn't enough....

Thanks,
-Chris

Jon Harrop

2007-02-28, 7:06 pm

Neelakantan Krishnaswami wrote:
> Yes, that's right. You could also have a function that pushes file
> operations into the monad:
>
> val wrap : (in_chan -> 'a) -> 'a t

I'm a little

about something: what is to stop the inner code from
returning one of these functions (e.g. read_line) as part of its result?
Surely that closure will capture the file handle and violate the constraint
that I'm trying to enforce?

--
Dr Jon D Harrop, Flying Frog Consultancy
OCaml for Scientists
http://www.ffconsultancy.com/produc...dex.html?usenet

oleg@pobox.com

2007-02-28, 7:06 pm

Andreas Rossberg wrote:

> module type FILE = sig
> val read_char : unit -> char option
> val read_line : unit -> string option
> val run : string -> (unit -> 'a) -> 'a
> end;;

> But it does not statically guarantee proper sequencing of file
> operations, and hence does not address Jon's concern that a file
> access may accidentally be attempted out-of-scope.

I disagree. I think the code does what is advertised, that is, making
sure that the file cannot be accessed after it is closed, accident or
not. You probably have in mind the following scenario (if not, I'd
very much like to see the code):

> (* Try to leak the closure *)
> let bad = (File.run "/etc/motd" (fun () -> File.read_char)) ();;

That is, we incorporate the file operation into a closure, return that
closure out of scope of File.run, and then run this closure. Or,
similarly, assign the closure to some (global) mutable variable. That
trick does NOT leak the opened input channel. This is because the
input channel is a dynamically scoped variable, and dynamic variables
are NOT captured in closures. That is precisely why they are so
complex to reason about, and precisely why they are useful. The input
channel for the file is accessible *only* when control is within the
_dynamic_ scope of File.run. Once File.run is finished, the channel is
closed and the dynamic binding is removed. So, attempt to run the
above code will cause

> Exception: Failure "Empty prompt stack: no prompt set".

Perhaps your remark stems from the fact that the attempt to leak and
use the channel is not flagged statically, by the compiler. Indeed,
that is the drawback -- the type system of OCaml does not track
dynamic variables, just as it doesn't track exceptions. An attempt to
raise an exception out of the scope of a try block is similarly
permitted by the type system, and similarly is a run-time error. There
are tools (written by Xavier Leroy and his students) that can
statically prevent this. Likewise, there are type systems that can
statically prevent access to a dynamic variable outside of its binding
region.

The only real problem occurs when we also capture continuations (and
don't do something like dynamic-wind to adequately `protect'
dynvars). But this problem also exists in the monadic solution.

In any event, the claim is that the shown technique guarantees [modulo
first-class continuation capture, where dynamic wind must be used]
that a resource cannot be used after it has been disposed of. An
attempt to do that, by accident or otherwise, leads to a well-defined
exception (rather than an undefined behavior and a segmentation
fault). An effect system can make this guarantee static.

Chris Clark wrote:
> Now, if I understand the conversation, the suggestion previously made
> is that strict languages already have mechanisms that order things
> (the arguments must get evaluated before the function they are being
> passed to, for instance) and that the need for monads is lessened. I
> take this response as saying that isn't enough....

Actually, the observation that the need for monads in a strict
language is indeed lessened (if not at all removed) has been made by
Moggi himself, as mentioned by Filinksi. Here's the paragraph from the
first page of Filinski's `Representing Monads' (POPL94)

"It is somewhat remarkable that monads have had no comparable impact
on
``impure'' functional programming. Perhaps the main reason is that --
as clearly observed by Moggi, but perhaps not as widely appreciated in
the ``purely functional'' community -- the monadic framework is
already built into the semantic core of eager functional languages
with effects, and need not be expressed explicitly. ``Impure''
constructs, both linguistic (e.g., updatable state, exceptions, or
first?class continuations) and external to the language (I/O, OS
interface, etc.), all obey a monadic discipline. The only aspect that
would seem missing is the ability for programmers to use their own,
application?specific monadic abstractions -- such as nondeterminism or
parsers [31] -- with the same ease and naturality as built?in
effects."

Filinski then goes to show that with delimited control, _every_
computational monad is expressible is a strict language and so can be
used in `direct' style. That is practically important: the direct
style is not only visually pleasing but it is also fast. Only the
parts of the programs that need effect use it. The other parts are not
penalized. There is no need to build closures for each operation.

Neelakantan Krishnaswami

2007-03-01, 4:14 am

In article <45e61536$0$8731$ed2619ec@ptn-nntp-reader02.plus.net>, Jon
Harrop wrote:
> Neelakantan Krishnaswami wrote:
>
> I'm a little

about something: what is to stop the inner code from
> returning one of these functions (e.g. read_line) as part of its result?
> Surely that closure will capture the file handle and violate the constraint
> that I'm trying to enforce?

Yes, you're right -- I had a brain-o. All the IO operations you want
to use need to be wrapped by the library, because they're part of your
trusted base (because they directly access the file handle).

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Dirk Thierbach

2007-03-01, 4:14 am

Jon Harrop <jon@ffconsultancy.com> wrote:
> Chris F Clark wrote:

[color=darkred]
> Exactly. The problem isn't with the order of operations. The problem is
> guaranteeing that the file handle no longer exists after it is closed so
> you can't call input_line on a closed handle.

In Haskell, the state monad can prevent the state from "leaking" out
of the monad by existentially quantifying the type of the state. I
suppose one could do something similar with the file handle (which
basically is part of the state in the "file handle monad") in OCaml.
Combined with a mandatory close in the "run" function of the monad
that should have the required effect.

> I don't understand how Neel's monads do this.

I don't, either, but OTOH I didn't look very closely :-)

- Dirk

rossberg@ps.uni-sb.de

2007-03-01, 8:07 am

On 1 Mrz., 01:23, o...@pobox.com wrote:
>
> I disagree. I think the code does what is advertised, that is, making
> sure that the file cannot be accessed after it is closed, accident or
> not.

Well, yes, but I think the original question rather was about
precluding erroneous *attempts* of accessing it. Nothing dangerous can
happen either way, because the lib checks all accesses to closed file
handles anyway.

> You probably have in mind the following scenario (if not, I'd
> very much like to see the code):
>

Even simpler: is is possible to accidentally call File.read_char
anywhere, and get a runtime error.
[color=darkred]
> So, attempt to run the
> above code will cause
>
>
> Perhaps your remark stems from the fact that the attempt to leak and
> use the channel is not flagged statically, by the compiler.

Exactly. I don't see how getting the dynvar exception is any better
better than

Exception: Sys_error "Bad file descriptor".

which is what you would get with the simple h.o. functional. There is
no actual "leak" of anything, at least not in this application (I see
that that the dynvar solution is superior where you don't want to
allow the object to be accessible at all, but that does not buy you
anything in this particular case).

In fact, I would argue that the simple solution is safer, because it
at least requires some conscious programming to transfer the handle
out of scope and apply an input function to it, while in the dynvar
solution it is much easier to accidentally call read_line() in the
wrong place.

- Andreas

rossberg@ps.uni-sb.de

2007-03-01, 7:12 pm

On 1 Mrz., 00:50, Jon Harrop <j...@ffconsultancy.com> wrote:
> Chris F Clark wrote:

Well, there are two kinds of sequencing we talk about here that are
only loosely related. Monads allow you to enforce a certain order of
execution which you do not automatically have in a lazy language. As
others have observed, this is no issue in an eager language.

However, what I (maybe confusingly) referred to with sequencing is
performing file operations in the right order, i.e. following the
pattern

open; input*; close

Jon's question - as I interpret it - basically was if there is a way
to statically enforce that this order is always maintained, and in
particular, that the final close is performed. His solution guarantees
that the close is performed, but cannot guarantee that it is the final
operation on the file handle, because you might return the file handle
from his function and call input on it afterwards.

Incidentally, monads also provide a solution to this problem: by
encapsulating the file handle in an abstract state monad you preclude
that the handle is passed out of that monad.
[color=darkred]
> I don't understand how Neel's monads do this. Indeed, I think that all of
> the proposed solutions (apart from a type system extension to support
> linear types as Torben said) fail to do this. Instead, they just wrap IO
> functions with the handle using a monad, which is just a poor-man's object
> (AFAICT).

No. Neel's solution (apart from the wrap function, which would break
it), does solve your problem. It works because the only operations to
access the file are the monadic read operations from the FILE
signature. You can only "execute" them by running them within the
monad - which guarantees proper opening and closing of the
corresponding file.

Note in particular that the client code is free to return any of the
monadic operations from the run function (or store them in a global
reference, for that matter), but that does NOT violate the
abstraction, because they are not themselves bound to a specific file
and you cannot do anything with them except for running them in
another monad (and in fact, passing them out is pointless since they
are directly accessible from the FILE signature anyway).

- Andreas

rossberg@ps.uni-sb.de

2007-03-01, 7:12 pm

On 1 Mrz., 08:45, Dirk Thierbach <dthierb...@usenet.arcornews.de>
wrote:
>
> In Haskell, the state monad can prevent the state from "leaking" out
> of the monad by existentially quantifying the type of the state.

And that's what is happening here, too, except that the existential
quantification comes in disguise of the type abstraction performed on
the monad type File.t.

- Andreas

oleg@pobox.com

2007-03-03, 4:05 am

Dirk Thierbach wrote:
> In Haskell, the state monad can prevent the state from "leaking" out
> of the monad by existentially quantifying the type of the state. I
> suppose one could do something similar with the file handle (which
> basically is part of the state in the "file handle monad") in OCaml.
> Combined with a mandatory close in the "run" function of the monad
> that should have the required effect.

First of all, Neel's monad is a Reader monad rather than the state
monad -- with an important distinction that there is no operation to
obtain the environment (the channel) and temper with the
environment. In Haskell terms, Neel's monad has no `ask' and `local'
morphisms. Rather, there are operations like read_char that use that
channel -- but they do not make it available to the user.

Perhaps you're thinking about the ST s monad? It does expose the state
(STRef to the user), and that is why it needs a way to ensure STRef
can only be used within the `scope' of the runST where is has been
allocated. This is achieved by the _universal_ (rather than
existential) quantification over s. That is, any action ST s a must be
parametric over s (universally quantified). The universal
quantification can too be accomplished in OCaml, via polymorphic
records. The type ('a,'v) code of MetaOCaml is another example: the
universally quantified 'a parameter (the environment classifier) makes
sure we aren't trying to evaluate the open code or the code we haven't
constructed yet.

Andreas Rossberg wrote:
> Exactly. I don't see how getting the dynvar exception is any better
> better than
>
> Exception: Sys_error "Bad file descriptor".
>
> which is what you would get with the simple h.o. functional. There is
> no actual "leak" of anything, at least not in this application (I see
> that that the dynvar solution is superior where you don't want to
> allow the object to be accessible at all, but that does not buy you
> anything in this particular case).

In this particular case, I agree. Indeed, the OCaml library checks the
status of the input channel before every access, so leaking the
channel will not lead to undefined behavior. In general however, one
may interface with other resources such as communication channels and
pieces of data allocated outside of the OCaml heap. The dynvar
solution offers [not currently static, see below] guarantee of the
regional access to the resource. The resource can only be accessed
within the dynamic scope of the run operation. Once `run' is finished,
we can dispose of the resource and free its memory right away. We
don't have to worry about stale references and dangling pointers.

Now, what about static guarantees? One may observe that executing
File.read_char outside of the dynamic scope of File.run is _precisely_
the same kind of error as executing `raise e' outside of the dynamic
scope of a try block. That is, unhandled exception. There has been an
effect system designed to statically prevent such an error. The system
has been implemented. Some may wonder if it may become a part of
OCaml, given that Xavier Leroy was involved.

Xavier Leroy, Franc,ois Pessaux
Type-based analysis of uncaught exceptions
http://doi.acm.org/10.1145/349214.349230

An uncaught exceptions analyzer for Objective Caml
http://caml.inria.fr/pub/old_caml_s...xc/ocamlexc.htm

With this tool, the guarantees provided with the dynvar solution will
be static.

This brings me back to Filinkski's POPL94 paper, which expresses, in
my view, a sentiment that too much attention is being devoted to
monads and too little to alternatives. It seems Greg Morrisett's
ML2005 talk echoed the same sentiment, and put forward effect systems
rather than monads for the `new ML'.

Dirk Thierbach

2007-03-03, 4:06 am

oleg@pobox.com wrote:
> This is achieved by the _universal_ (rather than existential)
> quantification over s.

Universal quantification in a "negative" position is the same as
existential quantification on the outside (just pretend it's a logic
formula, then the equivalence is obvious). That's why it's called
existential quantification, even if it's written with a "forall"
quantifier.

- Dirk

Ben Rudiak-Gould

2007-03-03, 7:03 pm

Jon Harrop wrote:
> I currently do something like:
>
> let read file k =
> let ch = open_in file in
> try k ch finally
> close_in ch
>
> but there is always the possibility that a user will return the channel from
> the continuation and try to read after it has been closed.

This requires higher-rank types, and isn't foolproof, but does provide an
extra line of defense: use your function, but with a type like

forall a. FilePath -> (forall s. SHandle s -> IO a) -> IO a

where SHandle is just a newtype wrapper for an ordinary Handle with a
phantom type argument. You don't want to provide a way to extract the Handle
from an SHandle, so you need to provide wrappers for all file operations.

The idea is that the caller has to choose a before your wrapper chooses s,
and so the wrapper can foil any attempt by the caller to choose a type
capable of accommodating SHandle s. Unfortunately you can get around it with
an existential box:

data Handle = forall s. MkHandle (SHandle s)

So this technique is useless if you're up against an adversary, but
potentially useful if you're just trying to catch mistakes. You can make it
bulletproof with an ST-like monad, but it's a lot more cumbersome that way.

Come to think of it, I'm not sure you need higher-rank types for this. I
think you can just use a type like

FilePath -> (SHandle a -> IO a) -> IO a

provided the compiler doesn't support recursive types.

-- Ben

Neelakantan Krishnaswami

2007-03-03, 7:03 pm

In article <1172896769.544809.43860@s48g2000cws.googlegroups.com>,
oleg@pobox.com wrote:
> Dirk Thierbach wrote:
>
> First of all, Neel's monad is a Reader monad rather than the state
> monad -- with an important distinction that there is no operation to
> obtain the environment (the channel) and temper with the
> environment.

It actually is a state monad, though the type signature is confusing:

type 'a t = in_chan -> 'a

The input channel is a mutable data structure, so you don't need to
explicitly return the updated data structure. If you look at the bind
operation:

let bind f m =
fun input ->
let v = m input in
f v input

you can see that the updated state is getting passed through, since
the same (albeit possibly-mutated) input gets passed to f.

However, you're definitely right that there is no way for the user to
get ahold of the input channel -- that's the whole point of the
design:

> In Haskell terms, Neel's monad has no `ask' and `local' morphisms.
> Rather, there are operations like read_char that use that channel --
> but they do not make it available to the user.

What are 'ask' and 'local'? I've never heard of them before. Are they
how you get direct access to the state?

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

oleg@pobox.com

2007-03-06, 4:22 am

Neel Krishnaswami wrote:
> It actually is a state monad, though the type signature is confusing:
> type 'a t = in_chan -> 'a
> he input channel is a mutable data structure, so you don't need to
> explicitly return the updated data structure.

I guess this is the matter of the point of a view. If we build a
Reader monad with an IORef as the environment (useful to implement
state that persists across exception handling, etc), is it a reader or
a state monad?

> What are 'ask' and 'local'? I've never heard of them before. Are they
> how you get direct access to the state?

These are the operations of the Reader monad. The Reader monad is the
dual of dynamic binding with only one (and, hence, implicit) dynamic
variable. Thus `ask' corresponds to the dereferencing of the dynamic
variable (obtaining the current value of the environment) and `local'
corresponds to dynamic-let, or fluid-let.

Neelakantan Krishnaswami

2007-03-06, 7:04 pm

In article <1173167432.471284.51910@c51g2000cwc.googlegroups.com>,
oleg@pobox.com wrote:
> Neel Krishnaswami wrote:
>
> I guess this is the matter of the point of a view. If we build a
> Reader monad with an IORef as the environment (useful to implement
> state that persists across exception handling, etc), is it a reader or
> a state monad?

Yeah, this is probably a matter of what the ambient semantic category
is. Eg, nontermination is not a monadic effect in Haskell's semantics,
though my preference is to think of that as a kind of side-effect.

>
> These are the operations of the Reader monad. The Reader monad is the
> dual of dynamic binding with only one (and, hence, implicit) dynamic
> variable. Thus `ask' corresponds to the dereferencing of the dynamic
> variable (obtaining the current value of the environment) and `local'
> corresponds to dynamic-let, or fluid-let.

So ask has a type like:

ask : M state

and local has a type like

local : state -> M a -> M a

I've used a local-like operation a lot when writing typecheckers; it's
very convenient way to temporarily add a binding to the environment as
you cross scopes.

--
Neel R. Krishnaswami
neelk@cs.cmu.edu

Sponsored Links