[Haskell-cafe] A free monad theorem?

[Benjamin Franksen]

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