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