[Haskell-cafe] Re: Different choice operations in a continuation monad

[Sebastian Fischer]

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