Tomasz Zielonka wrote:
On Thu, Aug 31, 2006 at 07:23:55PM +0200, Benjamin Franksen wrote:
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).
The bind operator doesn't have to neccesarily apply the second argument to anything. What if m is Maybe, and the first arguments is Nothing?
True, however if the instance for Maybe would have been defined without /ever/ applying the second argument to anything, then wouldn't this necessarily be a trivial monad (however one would need to define 'trivial' here)?
And if the bind operator "wants" to apply the second argument to something, it doesn't have to do it only once - consider the [] monad.
Yes, I should have said: Any non-trivial definition of bind has to apply its second argument at least in _some_ cases and _at least_ once to something non-bottom.
Other examples:
get :: State s s -- from Control.Monad.State
there is no way you can extract an 's' value from "get" alone - you have to supply the state to the whole computation
Cont (const ()) :: Cont () a -- from Control.Monad.Cont
whatever you do, you won't be able to extract an 'a' typed value, non-bottom from this computation. Cont is defined as:
newtype Cont r a = Cont {runCont :: (a -> r) -> r)}
So getting the value out of the monad is not a pure function (extract :: Monad m => m a -> a). I think I stated that, already, in my previous post. I'd even say that the monadic values alone can be completely meaningless. They often have a meaning only relative to some environment, thus are (usually) _effectful_ computations. But we already knew that, didn't we? The real question (the one that bugs me, anyway) is if one can give a precise meaning to the informal argument that if the definition of bind is to be non-trivial then its second argument must be applied to some non-trivial value at one point (but not, of course, in all cases, nor necessarily only once), and that this implies that the computation represented by the first argument must somehow be 'run' (in some environment) in order to produce such a value. -- And, of course, whether this is actually true in the first place. Would you say that your examples above are counter-examples to this statement (imprecise as it is, unfortunately)? Ben