[Haskell-cafe] Can we come out of a monad?

[wren ng thornton]

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 
can exit a monad (provided the additional proof/arguments necessary for 
the particular monad in question). Indeed, almost every monad can be 
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 
adaptive algorithm that does things quickly when it has access to lots 
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 
demonstrated in some theoretical framework for reasoning about Haskell.

...

For what it's worth, this situation is reversed for comonads. Monads, 
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