[Haskell-cafe] A free monad theorem?

[Daniel Fischer]

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
> >