On Jun 18, 2010, at 8:55 PM, Heinrich Apfelmus 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.
What a pity!
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
Nice example. Consider the given Definitions of `CMaybe r a` with
`fromCMaybe`, `mzero`, `mplus`, `orElse`, and additionally:
toCMaybe :: Maybe a -> CMaybe r a
toCMaybe a = CMaybe (\k -> a >>= k)
getCMaybe :: CMaybe r a -> (a -> Maybe r) -> Maybe r
getCMaybe (CMaybe a) = a
Much to my surprise, your example lead me to the following inequations:
a /= toCMaybe (fromCMaybe a)
because for ``a = return False `mplus` return True`` we have
getCMaybe a guard = Just ()
getCMaybe (toCMaybe (fromCMaybe a)) guard = Nothing
Also:
a /= mzero `orElse` a
because for the same `a` we have
getCMaybe a guard = Just ()
getCMaybe (mzero `orElse` a) guard = Nothing
Also:
a /= a `orElse` mzero
because for the same `a` we have
getCMaybe a guard = Just ()
getCMaybe (a `orElse` mzero) guard = Nothing
Pretty unfortunate. `mzero` is neither a left nor a right identity of
`orElse`.
Out of curiosity, I've implemented these semantics with operational .
Code attached.
Thanks!
It doesn't seem to be possible to implement this with just the
CMaybe r
a type, in particular since the implementation I gave cannot be
refunctionalized to said type. In other words, there is probably no
associative operation
orElse :: CMaybe r a -> CMaybe r a -> CMaybe r a
with identity `mzero` that satisfies the cancellation law. I don't
have
a proof, but the argument that it doesn't interact well with the
default
implementation of callCC seems strong to me.
Is `mzero` an identity for `orElse` in your code or can we create a
counter example like the one above? Can you add a distributive `mplus`
to your code that would behave differently in the examples above?
Cheers,
Sebastian
--
Underestimating the novelty of the future is a time-honored tradition.
(D.G.)
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
