Heinrich Apfelmus apfelmus at quantentunnel.de
Fri Jun 18 14:55:13 EDT 2010

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

```