[Haskell-cafe] A free monad theorem?

[Lennart Augustsson]

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