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