<div>I think there is another way to view the ContT/Codensity/Monad generated by a functor, in terms of an accumulating parameter that may be informative. I kind of alluded to it in the post on Kan extensions.</div>
<div> </div>
<div>Take for a moment, Yoneda f given in:</div>
<div> </div>
<div><a href="http://comonad.com/haskell/category-extras/src/Control/Functor/Yoneda.hs">http://comonad.com/haskell/category-extras/src/Control/Functor/Yoneda.hs</a></div>
<div> </div>
<div>> newtype Yoneda f a = Yoneda { runYoneda :: forall b. (a -> b) -> f b }</div>
<div> </div>
<div>You can readily construct an instance of Functor for Yoneda without any concern for the underlying instance on f.</div>
<div> </div>
<div>> instance Functor (Yoneda f) where</div>
<div>> <font size="2">fmap f m = Yoneda (\k -> runYoneda m (k . f))</font></div>
<div> </div>
<div><font size="2">> lowerYoneda :: Yoneda f a -> f a</font></div>
<div><font size="2">> lowerYoneda m = runYoneda m id</font></div>
<div> </div>
<div>Basically the operation of creating a value of type Yoneda f a requires you to use the fmap for the functor, so there is a Mendler-style encoding going on here, no magic dictionaries are required to use the resulting value.<br>
</div>
<div>Now what I find interesting is that Yoneda is basically carrying around an accumulator for 'fmap' applications.</div>
<div> </div>
<div>Basically it enforces the fusion rule that fmap f . fmap g = fmap (f . g) by accumulating mappings and applying them in one go when you ask for the result.</div>
<div> </div>
<div>As an aside, when you extract a value out of (Yoneda f) uses the function it has accumulated so far, from pushing computations. And it has to use the secret valid version of fmap that you had to know to find a function that had the signature (forall a. (a -> b) -> f b) so no work is saved, its just fmap fusion. </div>
<div> </div>
<div>When you make a Monad out of Yoneda, that Monad can 'push' the map along to the next bind operation so it can come along for the ride, avoiding the need for an extra (>>=) to liftM the function you want to map. (It still has to appeal to the secret fmap you knew to make the Yoneda f a value!) Of course, this steps outside of the principles I'm espousing in this post by using a dictionary.</div>
<div> </div>
<div><font size="2">> instance Monad f => Monad (Yoneda f) where</font></div>
<div><font size="2">> return a = Yoneda (\f -> return (f a))</font></div>
<div><font size="2">> m >>= k = Yoneda (\f -> runYoneda m id >>= \a -> runYoneda (k a) f)</font></div>
<div> </div>
<div>When you look at the definition for Codensity f a, what it effectively supplies is a 'better accumulator', one which is large enough to encode (>>=). </div>
<div> </div>
<div><font size="2">> newtype Codensity m a = Codensity { runCodensity :: forall b. (a -> m b) -> m b }</font></div>
<div><font size="2"></font> </div>
<div><font size="2">> instance Monad (Codensity f) where</font></div>
<div><font size="2">> return x = Codensity (\k -> k x)</font></div>
<div><font size="2">> m >>= k = Codensity (\c -> runCodensity m (\a -> runCodensity (k a) c))</font></div>
<div> </div>
<div>You then have to pass it a function of the type (a -> m b) to get the value out. Effectively you tell it how to return by injecting something. And since it can return and bind, you can define liftM thanks to the monad laws, giving an admissable implementation of Functor: </div>
<div> </div>
<div>
<div><font size="2">> instance Functor (Codensity k) where</font></div>
<div><font size="2">> fmap f m = Codensity (\k -> runCodensity m (k . f))</font></div></div>
<div> </div>
<div>Again no dictionaries were harmed in the encoding of this function and the type is no bigger than it needs to be to express these properties.</div>
<div> </div>
<div>The Codensity monad above can be seen as just an instance of enforced bind fusion, enforcing choice of association of (>>=). This consequence is logical because the result of a CPS transform is invariant under choice of reduction order.</div>
<div> </div>
<div>The reason I mention this is that this scenario is just an instance of a very general pattern of Mendler-style encoding. I have another example of Mendler-style encoding, this time for recursion schemes near the bottom of: <a href="http://knol.google.com/k/edward-kmett/catamorphisms/">http://knol.google.com/k/edward-kmett/catamorphisms/</a></div>
<div> </div>
<div>I find this idiom to be rather effective when I want to enforce the equivalent of a rewrite rule or law about a type or work around the requirement that there can be only one instance of a particular typeclass. Yoneda doesn't care that f implements Functor, only that it satisfies the properties of a functor, and that fmap _could_ be defined for it. Codensity doesn't care that f is a monad. Well, it does if you want to do any computations with f, but you could have several different lifts to different monad/applicative 'instances' over f, as long as you lift into the codensity monad with a bind operation and lower back out with a return operation that agree. The dictionary for Monad m is irrelevant to the construction of Codensity m.</div>
<div><font size="2"></font> </div>
<div><font size="2">> liftCodensity :: Monad m => m a -> Codensity m a</font></div>
<div><font size="2">> liftCodensity m = Codensity (m >>=)</font></div>
<div><font size="2"><font size="2"></font></font> </div>
<div><font size="2"><font size="2">> lowerCodensity :: Monad m => Codensity m a -> m a</font></font></div>
<div><font size="2"><font size="2">> lowerCodensity a = runCodensity a return</font></font></div>
<div> </div>
<div>-Edward Kmett</div>
<div><br> </div>
<div class="gmail_quote">On Thu, Apr 9, 2009 at 5:22 AM, Sebastian Fischer <span dir="ltr"><<a href="mailto:sebf@informatik.uni-kiel.de">sebf@informatik.uni-kiel.de</a>></span> wrote:<br>
<blockquote class="gmail_quote" style="PADDING-LEFT: 1ex; MARGIN: 0px 0px 0px 0.8ex; BORDER-LEFT: #ccc 1px solid">Hi all,<br><br>thanks for pointing me at the Codensity monad and for mentioning the<br>lift operation! I'll try to sum up what I learned from this thread.<br>
<br>In short:<br><br>What I find interesting is<br><br> 1. you can express the results of monadic computations using<br> functors that do not themselves support the `>>=` operation. You<br> only need an equivalent of `return`.<br>
<br>and<br><br> 2. a variety of *non-*monadic effects (e.g., non-determinism) can be<br> lifted to this "monad for free", so you get, e.g., a<br> non-determinism *monad* even if all you have is a non-determinism<br>
*functor*.<br><br>Here is the long version:<br><br>Because `ContT` makes a monad out of anything with kind `* -> *`, we<br>also get instances for `Functor` and `Applicative` for free. We could<br>use the `Monad` instance to get them for free by<br>
`Control.Applicative.WrappedMonad` but defining them from scratch<br>might be insightful, so let's try.<br><br>We could define an instance of `Functor` for `ContT t` as follows.<br><br> instance Functor (ContT t)<br>
where<br> fmap = liftM<br><br>But let's see what we get if we inline this definition:<br><br> fmap f a<br> = liftM f a<br> = a >>= return . f<br> = ContT (\k -> unContT a (\x -> unContT (return (f x)) k))<br>
= ContT (\k -> unContT a (\x -> unContT (ContT ($f x)) k))<br> = ContT (\k -> unContT a (\x -> k (f x)))<br><br>That leads to the `Functor` instance described in the first post on<br>Kan extensions by Edward Kmett.<br>
<br>> instance Functor (ContT t)<br>> where<br>> fmap f a = ContT (\k -> unContT a (k.f))<br><br>We also get an Applicative instance for free:<br><br> instance Applicative (ContT t)<br> where<br> pure = return<br>
(<*>) = ap<br><br>If we inline `ap` we get<br><br> f <*> a<br> = f `ap` a<br> = f >>= \g -> a >>= \x -> return (g x)<br> = ContT (\k1 -> unContT f (\x1 -> unContT (a >>= \x -> return (x1 x)) k1))<br>
= ...<br> = ContT (\k -> unContT f (\g -> unContT a (\x -> k (g x))))<br><br>So, a direct Applicative` instance would be:<br><br>> instance Applicative (ContT t)<br>> where<br>> pure x = ContT ($x)<br>
> f <*> a = ContT (\k -> unContT f (\g -> unContT a (\x -> k (g x))))<br><br>The more interesting bits are conversions between the original and the<br>lifted types. As mentioned earlier, if `f` is a pointed functor, then<br>
we can convert values of type `ContT f a` to values of type `f a`.<br><br> runContT :: Pointed f => ContT f a -> f a<br> runContT a = unContT a point<br><br>Ryan Ingram pointed in the other direction:
<div class="im"><br><br> > You are missing one important piece of the puzzle for ContT:<br> ><br> > ~~~<br> > lift :: Monad m => m a -> ContT m a<br> > lift m = ContT $ \k -> m >>= k<br> > ~~~<br>
><br> > This >>= is the bind from the underlying monad. Without this<br> > operation, it's not very useful as a transformer!<br><br></div>That is a fine reason for the *class* declaration of `MonadTrans` to<br>
mention `Monad m` as a constraint for `lift`. But as `ContT t` is a<br>monad for any `t :: * -> *`, a constraint `Monad t` on the *instance*<br>declaration for `Monad (ContT t)` is moot. This constraint is not<br>necessary to define `lift`.<br>
<br>> instance MonadTrans ContT<br>> where<br>> lift m = ContT (m>>=)<br><br>Ryan continues:
<div class="im"><br><br> > Without lift, it's quite difficult to get effects from the<br> > underlying Applicative *into* ContT. Similarily, your MonadPlus<br> > instance would be just as good replacing with the "free"<br>
> alternative functor:<br> ><br> > ~~~<br> > data MPlus a = Zero | Pure a | Plus (MPlus a) (MPlus a)<br> > ~~~<br> ><br> > and then transforming MPlus into the desired type after runContT;<br> > it's the embedding of effects via lift that makes ContT useful.<br>
<br></div>Let's see whether I got your point here. If we have a computation<br><br> a :: Monad m => m a<br><br>and we have a pointed functor `f`, then we can get the result of the<br>computation `a` in our functor `f` because `runContT a :: f a`.<br>
<br>If we now have a computation with additional monadic effects (I use<br>non-determinism as a specific effect, but Edward Kmett shows in his<br>second post on Kan extensions how to lift other effects like Reader,<br>State, and IO)<br>
<br> b :: MonadPlus m => m b<br><br>then we have two possibilities to express the result using `f` if `f` is<br>also an alternative functor.<br><br> 1. If `f` is itself a monad (i.e. an instance of MonadPlus), then<br>
the expression `runContT (lift b)` has type `f b`. (Well, `b`<br> itself has type `f b`..)<br><br> 2. If `f` is *not* a monad, we can still get the result of `b` in<br> our functor `f` (using the `MonadPlus` instance from my previous<br>
mail), because `runContT b` also has type `f b`.<br><br>Clearly, `runContT (lift b)` (or `b` itself) and `runContT b` may<br>behave differently (even if they both (can) have the type `f b`)<br>because `ContT` 'overwrites' the definition for `>>=` of `f` if `f`<br>
has one. So it depends on the application which of those behaviours is<br>desired.<br><br>Ryan:
<div class="im"><br><br> > The CPS transfrom in ContT also has the nice property that it makes<br> > most applications of >>= in the underlying monad be<br> > right-associative.<br><br></div>Do you have a specific reason to say *most* (rather than *all*) here?<br>
Because if we have a left-associative application of `>>=` in `ContT`,<br>then we have:<br><br> (a >>= f) >>= g<br> = ContT (\k1 -> unContT (a >>= f) (\x1 -> unContT (g x1) k1))<br> = ContT (\k1 -><br>
unContT (ContT (\k2 -> unContT a (\x2 -> unContT (f x2) k2)))<br> (\x1 -> unContT (g x1) k1)<br> = ContT (\k1 -> unContT a (\x2 -> unContT (f x2) (\x1 -> unContT (g x1) k1)))<br> = ContT (\k1 -> unContT a (\x2 -><br>
unContT (ContT (\k2 -> unContT (f x2) (\x1 -> unContT (g x1) k2)))<br> k1))<br> = ContT (\k1 -> unContT a (\x2 -> unContT (f x2 >>= g) k1))<br> = a >>= (\x -> f x >>= g)<br>
<br>Cheers,<br><font color="#888888">Sebastian</font>
<div>
<div></div>
<div class="h5"><br><br><br>_______________________________________________<br>Haskell-Cafe mailing list<br><a href="mailto:Haskell-Cafe@haskell.org" target="_blank">Haskell-Cafe@haskell.org</a><br><a href="http://www.haskell.org/mailman/listinfo/haskell-cafe" target="_blank">http://www.haskell.org/mailman/listinfo/haskell-cafe</a><br>
</div></div></blockquote></div><br>