[Haskell-cafe] Re: Different choice operations in a continuation
monad
Sebastian Fischer
sebf at informatik.uni-kiel.de
Fri Jun 18 16:00:23 EDT 2010
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.)
More information about the Haskell-Cafe
mailing list