Escaping monads and topological spaces of computation

So I got to thinking about monads for computation, in particular about the "no escape" clause. In practice you actually can escape from most monads (ST, State, List, Logic (for backtracking search), Maybe, Cont, even IO) and these monads all have some "run" function for doing so (though it may be "unsafe"). These functions all have different signatures because there are different ways of catamorphing the computation away in arriving at your result, but in principle it's possible to subtype these computations into having appropriate generic execution functions.

The simplest computation is a constant computation which successfully returns a value, ST and Identity are just such computations. One way of extending this is to say that a computation is nondeterministic and can return many answers[1]. A different way of extending it is to say that the computation might fail to return any value, Maybe is just such a monad. And of course we could take both those extensions and either fail to return any answers or return nondeterministically many answers, List and Logic are our examples here. Another extension is that a computation may have different kinds of failure, like (Either e), and this is where things start to get interesting.

( Read more... )