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
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
