wren ng thornton wren at freegeek.org
Fri Jul 30 23:04:03 EDT 2010

```Tillmann Rendel wrote:
> C K Kashyap wrote:
>> I am of the
>> understanding that once you into a monad, you cant get out of it?
>
> That's not correct.

Indeed. The correct formulation of the statement is that it's not "safe"
to leave a monad. Where "safe" has the same connotation as in all the
unsafeFoo functions--- namely, you have additional proof obligations.

In other words, there is no general function:

escape :: forall a m. (Monad m) => m a -> a

Or any variant that takes additional arguments of a fixed type. But
really, the nonexistence of this function is the only claim we're making
about it not being safe to escape a monad. It's certainly true that we
exited. The tricky bit is, they all require some *different* kind of
"proof", so we can't write a general version that works for every monad.

For example, in the Maybe monad we will either have an A, or we will
not. So how can we extract an A? Well, if the monadic value is Just a,
then we can use pattern matching to extract the A. But if the monadic
value is Nothing, then what? Well, in order to provide an A, we'll need
to have some default A to provide when the Maybe A doesn't contain one.
So this default A is our "proof" of safety for exiting Maybe:

exitMaybe :: forall a. a -> Maybe a -> a
exitMaybe default Nothing = default
exitMaybe _ (Just something) = something

For another example, in the list monad we will have zero or more A. So
how can we return an A? Here we have a number of options. We could write
a function similar to exitMaybe, where we select some value in the list
arbitrarily or else return the default value if the list is empty. This
would match the idea that the list monad encapsulates nondeterministic
computations. But we loose some information here. Namely, why are we
carrying this list of all possible values around when we're just going
to select one arbitrarily? Why not select it earlier and save ourselves
some baggage? The idea of using a list as nondeterminism means that we
want to know *all* possible values our nondeterministic machine could
return. In that case, we need some way of combining different A values
in order to get an aggregate value as our output. Thus,

exitList :: forall a. a -> (a -> a -> a) -> [a] -> a
exitList x f [] = x
exitList x f (a:as) = f a (exitList x f as)

Of course we could also implement different versions for returning the
elements of the list in a different order. And if we wanted to be more
general we could allow the type of x and the return type of f to be any
arbitrary type B. Here, our "proof" is the two arguments for eliminating
a list.

The reason IO is special is, what kind of proof do we require in order
to exit the IO monad and return a pure result? Ah, that's a tricky one
isn't it. This really comes down to asking what the meaning of the IO
monad really is; if we knew what kind of structure IO has, then we could
derive a way of deconstructing that structure, just like we did for list
and Maybe. Because it includes disk access, in order to exit the IO
monad in general we would need (among other things) to be able to
predict/provide the values of all files, including ones got via the
network, and default values for all disk or network failures. Actually,
we need those proofs for every moment in time, because IO is volatile
and someone might do something like enter a loop trying to read a file
over and over again until it finally succeeds.

Clearly we cannot provide those kinds of proof in practice. They'd be
too big! Actually, this bigness might even be a theoretical problem
since the program has to fit in a file on disk, but the program must
include (some non-IO way of getting) the values of all the files on the
disk or the network. So we cannot exit the IO monad in general. But IO
is a sin bin that does a lot of other stuff too, like give reflection on
the state of the runtime system. It's perfectly possible to write an
of memory, but does things more optimally when memory is constrained.
Provided it gives the same answers regardless of resources, then it's
perfectly safe and referentially transparent to run this algorithm to
return a pure value, despite it using IO operations to monitor how much
memory is free while it runs. Things like this are what unsafePerformIO
is for. In order to use that function we must still provide "proof" that
it's safe to exit the monad, only this time it's not a token that's
passed around within the code, it's an actual proof that we've

...

which represent a kind of structure-around-values, can be freely entered
with return (by giving them trivial structure) but they're not "safe" to
exit (because every structure has a different shape to get out of).
Whereas for comonads, which represent a kind of being-in-context, you
can exit freely with coreturn (because you can always choose not to look
at your surroundings) but it's not "safe" to enter them (because every
context has a different shape to get into).

--
Live well,
~wren
```