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

[Lennart Augustsson]

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

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
>
>>
>> On Sep 2, 2006, at 19:44 , Udo Stenzel wrote:
>>> Benjamin Franksen wrote:
>>>> Sure. Your definition of bind (>>=):
>>>> ...
>>>> applies f to something that it has extracted from m, via
>>>> deconstructor
>>>> unpack, namely a. Thus, your bind implementation must know how to
>>>> produce
>>>> an a from its first argument m.
>>>
>>> I still have no idea what you're driving at, but could you  
>>> explain how
>>> the CPS monad 'extracts' a value from something that's missing
>>> something
>>> that's missing a value (if that makes sense at all)?
>>>
>>> For reference (newtype constructor elided for clarity):
>>>> type Cont r a = (a -> r) -> r
>>>>
>>>> instance Monad (Cont r) where
>>>> 	return a = \k -> k a
>>>> 	m >>= g = \k -> m (\a -> g a k)
>>>
>>> Udo.
>>> --
>>> Streitigkeiten dauerten nie lange, wenn nur eine Seite Unrecht  
>>> hätte.
>>> 	-- de la Rochefoucauld
>>> _______________________________________________
>>> Haskell-Cafe mailing list
>>> Haskell-Cafe at haskell.org
>>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>>
>> _______________________________________________
>> Haskell-Cafe mailing list
>> Haskell-Cafe at haskell.org
>> http://www.haskell.org/mailman/listinfo/haskell-cafe
>
> -- 
>
> "In My Egotistical Opinion, most people's C programs should be
> indented six feet downward and covered with dirt."
> 	-- Blair P. Houghton
>