David Menendez wrote:
> Heinrich Apfelmus wrote:
>> Sebastian Fischer wrote:
>>>
>>> I wonder whether for every monad `m` and `a :: Codensity m a`
>>>
>>> getCodensity a f = getCodensity a return >>= f
>>>
>>> Is this true? Why (not)?
>>
>> It's not true.
>>
>> a = Codensity $ \x -> Just 42
>> f = return . (+1)
>>
>> getCodensity a f = Just 42
>> ≠ getCodensity a return >>= f = Just 42 >>= f = Just 43
>
> What definition are you using for Codensity? Under the definition I'm
> familiar with, that definition of a is invalid.
Oops, silly me! I was thinking of
Codensity r a = Codensity ((a -> m r) -> m r)
which is wrong, of course.
> newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m
> b) -> m b }
>
> Which is not to say that you can't come up with improper values of
> Codensity. E.g.,
>
> Codensity (\k -> k () >> k ())
>
> \m -> Codensity (\k -> k () >>= \b -> m >> return b)
An example that is not generic in the base monad m , i.e. that makes
use of m = Maybe is
a = Codensity $ \k -> k 0 `orElse` k 1 -- orElse on plain Maybe
f n = if even n then Nothing else Just n
runCodensity a f = Just 1
runCodensity a return >>= f = Just 0 >>= f = Nothing
Regards,
Heinrich Apfelmus
--
http://apfelmus.nfshost.com
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
