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

[David Menendez]

On Fri, Jun 18, 2010 at 12:44 PM, Heinrich Apfelmus
<apfelmus at quantentunnel.de> wrote:
> Sebastian Fischer wrote:
>> Edward Kmett wrote:
>>> Sebastian Fischer wrote:
>>>> Heinrich Apfelmus wrote:
>>>> newtype CMaybe a = CMaybe (forall r. (a -> Maybe r) -> Maybe r)
>>> Yes, with this type `orElse` has the same type as `mplus`, which is
>>> very nice.
>>>
>>> This type is the same as "Codensity Maybe" using category-extras which
>>> is a 'bit bigger than Maybe'. (To see why, figure out how Codensity
>>> Reader is isomorphic to State!) This is the wiggle room you're using
>>> to get the distributive operator.
>>
>> I encounter the Codensity type constructor every now and then. I used it
>> to Reinvent Haskell Backtracking, learned about implementing a state
>> monad with a reader monad wrapped in Codensity when implementing  Lazy
>> Nondeterministic Programming and Janis Voigtländer also used it to
>> improve the asymptotics of free monads.
>>
>> 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.

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)

-- 
Dave Menendez <dave at zednenem.com>
<http://www.eyrie.org/~zednenem/>