[Haskell-cafe] Re: A free monad theorem?

[Brian Hulley]

Benjamin Franksen wrote:
> Tomasz Zielonka wrote:
>>         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.

I think the continuation monad might help to refine the intuition:

    Cont a_r_r >>= a_C_b_r_r = Cont $ \ b_r ->
          a_r_r (\a -> runCont (a_C_b_r_r   a)   b_r)

so it is clear that

1) The first computation (a_r_r  x) might involve running the second 
(applying b_r_r to b_r) so it gives a counterexample to the idea that the 
first computation is run to completion before the second one starts, though 
it preserves the intuition that at least the first computation is started 
first.

2) The bind operation has arranged that value(s) of type (a) are supplied in 
the course of running the first computation to the second (in the 
"non-trivial" case where the second computation is actually run)

Perhaps the argument could be that because the (a) is polymorphic, this 
implies that if the second computation is run at all, at least we know that 
the first computation has already started, and that the (a) came from the 
part of the first computation we've done so far, though of course this is 
still unfortunately very vague.

Regards, Brian.
-- 
Logic empowers us and Love gives us purpose.
Yet still phantoms restless for eras long past,
congealed in the present in unthought forms,
strive mightily unseen to destroy us.

http://www.metamilk.com