I'd like to know if the following reasoning can be made more precise: As we all know, the monadic bind operation has type: bind :: Monad m => m a -> (a -> m b) -> m b My intuition says that in order to apply the second argument to some non-trivial (i.e. non-bottom) value of type a, the bind operator needs to be able to somehow 'extract' a value (of type a) from the first argument (of type m a). I would like to argue that this is because bind is polymorphic in a, which makes it impossible to construct values of type a 'out of thin air' (besides bottom). Thus, however bind is defined, the only place where it can obtain a 'real' value of type a is from its first argument. Although one might think that this implies the existence of some function extract :: Monad m => m a -> a it is obvious that this is too limiting, as the IO monad plainly shows. Even monads that can be implemented in Haskell itself (the vast majority, it seems) usually need some additional (monad-specific) argument to their 'extract' (or 'run') function. However, even a value of type IO a /does/ produce a value of type a, only the 'value producing computation' is not a (pure) function. But how can all this be made more precise with less handwaiving? The background for my question is an argument I had some time ago with someone about what the 'real nature' of monads is. He argued that monads are mainly about 'chaining' (somehow wrapped up) values in an associative way, refering to the monad laws. I argued that monadic values get 'chained' in a very specific way and that in order to get an intuition about what this monadic chaining really means on the most general level, the standard model of 'computation that returns a value of type a' is the appropriate one. I tried to use the above (handwaving) argument to convince him (and myself) that this model is indeed 'the right one'. Furthermore, if it really is, then one might conjecture that for /every/ monad there must be some natural interpretation as the representation of some kind of computation (effectful or not). So my second question is: Are there known 'counter-examples' where this intuition breaks down, i.e. monads for which a computational interpretation is unknown or at least obscure enough not to qalify as 'natural'? Cheers, Ben