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