Yes, that's pretty much the point I was trying to make. :) -- Lennart On Sep 4, 2006, at 07:03 , Daniel Fischer wrote:
Am Montag, 4. September 2006 07:44 schrieben Sie:
You are right, but I was using "extraction" in a rather non-technical sense. Look at it this way: we have 'x >>= f', let's assume it's the continuation monad. Assuming f has type 'a -> C b' we must have something of type a to be able to call the function be at all. Somehow >>= is able make sure that f is called (modulo non- termination), so I still claim it "extracts" an 'a'. It's not a value that >>= will actually ever get its hands on, it only manages to make sure its passed to f. So somewhere there is an 'a' lurking, or f could not be called.
Perhaps you don't want to call that "extraction", and that's fine by me. :)
-- Lennart
Let me see... (ommitting Cont/runCont for better readability)
ma :: (a -> r) -> r f :: a -> (b -> r) -> r start :: b -> r
ma >>= f = ma . flip f
(ma >>= f) start === ma (flip f start)
So we never apply f to a value of type a, we apply it (or rather flip f) to a value of type (b -> r) when we finally run our action to get a value of type (a -> r), which then ma can be applied to. Is that correct? Or what did I get wrong? However, in practice, I can only imagine ma defined a la
ma func = let consts :: [r] consts = ... vals :: [a] vals = ... in combine consts (map func vals)
so unless ma is constant (very uninteresting), f will in practice be indeed applied to values of type a which are in some sense 'extracted' from ma. Is that sufficiently close to what you mean or do I still not understand what you're trying to convey?
Cheers, Daniel
On Sep 3, 2006, at 12:32 , Daniel Fischer wrote:
Am Sonntag, 3. September 2006 15:39 schrieb Lennart Augustsson:
Well, bind is extracting an 'a'. I clearly see a '\ a -> ...'; it getting an 'a' so it can give that to g. Granted, the extraction is very convoluted, but it's there.
-- Lennart
But
instance Monad (Cont r) where return = flip id (>>=) = (. flip) . (.) -- or would you prefer (>>=) = (.) (flip (.) flip) (.) ?
if we write it points-free. No '\a -> ...' around. And, being more serious, I don't think, bind is extracting an 'a' from m. How could it? m does not produce a value of type a, like a (State f) does (if provided with an initial state), nor does it contain values of type a, like [] or Maybe maybe do. And to my eyes it looks rather as though the '\a -> ...' tells us that we do _not_ get an 'a' out of m, it specifies to which function we will eventually apply m, namely 'flip g k'. But I've never really understood the Continuation Monad, so if I'm dead wrong, would you kindly correct me?
And if anybody knows a nontrivial but not too advanced example which could help understanding CPS, I'd be glad to hear of it.
Cheers, Daniel