Re: [Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction
Derek Elkins wrote: There is another very closely related adjunction that is less often mentioned. ((-)-C)^op -| (-)-C or a - b - C ~ b - a - C This gives rise to the monad, M a = (a - C) - C this is also exactly the comonad it gives rise to (in the op category which ends up being the above monad in the normal category). That looks very like the type of mfix. Is this related to MonadFix? Thanks, Yitz ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction
On Dec 17, 2007 4:34 AM, Yitzchak Gale [EMAIL PROTECTED] wrote: Derek Elkins wrote: There is another very closely related adjunction that is less often mentioned. ((-)-C)^op -| (-)-C or a - b - C ~ b - a - C This gives rise to the monad, M a = (a - C) - C this is also exactly the comonad it gives rise to (in the op category which ends up being the above monad in the normal category). That looks very like the type of mfix. Is this related to MonadFix? I think that's the continuation monad. -- Dave Menendez [EMAIL PROTECTED] http://www.eyrie.org/~zednenem/ ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction
On Mon, 2007-12-17 at 09:58 -0500, David Menendez wrote: On Dec 17, 2007 4:34 AM, Yitzchak Gale [EMAIL PROTECTED] wrote: Derek Elkins wrote: There is another very closely related adjunction that is less often mentioned. ((-)-C)^op -| (-)-C or a - b - C ~ b - a - C This gives rise to the monad, M a = (a - C) - C this is also exactly the comonad it gives rise to (in the op category which ends up being the above monad in the normal category). That looks very like the type of mfix. Is this related to MonadFix? I think that's the continuation monad. Let's do some (more) category theory. The unit of an adjunction (which is the unit of the monad it gives rise to) is the image of id in the isomorphism of hom-sets that defines an adjunction. In this case that isomorphism is (a - b - c) ~ (b - a - c), and the type completely determines the implementation (if you don't immediately recognize it), the isomorphism (in both ways actually) is flip. So the unit of the adjunction (return) is flip id and indeed that is exactly what Cont's definition of return is. (a - C) is a contravariant functor in a, so class ContraFunctor f where cofmap :: (b - a) - f a - f b instance ContraFunctor (- c) where -- not legal cofmap f = (. f) This obviously satisfies the (contravariant) functor laws, cofmap id = id and cofmap (f . g) = cofmap g . cofmap f instance Functor M where fmap = cofmap . cofmap This obviously satisfies the functor laws, fmap id = id and fmap (f . g) = fmap f . fmap g join is then join :: M (M a) - M a join = cofmap (flip id) -- flip id is also the counit This implementation is also forced by the types. (=) then has it's standard definition in terms of join and fmap, m = f = join (fmap f m) and if this is expanded out, this is indeed seen to be the implementation of (=) for the continuation monad. ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
[Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction
Dan Weston wrote: newtype O f g a = O (f (g a)) -- Functor composition: f `O` g instance (Functor f, Functor g) = Functor (O f g) where ... instance Adjunction f g = Monad (O g f) where ... instance Adjunction f g = Comonad (O f g) where ... class (Functor f, Functor g) = Adjunction f g | f - g, g - f where leftAdjunct :: (f a - b) - a - g b rightAdjunct :: (a - g b) - f a - b -- Functors are associative but not generally commutative. Apparently a Monad is also a Comonad if there exist left (f) and right (g) adjuncts that commute. Yes, but that's only sufficient, not necessary. Jules and David already pointed out that while every monad comes from an adjunction, this adjunction usually involves categories different from Hask. So, there are probably no adjoint functors f and g in Hask such that [] ~= g `O` f or data L a = One a | Cons a (L a) -- non-empty list L ~= g `O` f (proof?) Yet, both are monads and the latter is even a comonad. Moreover, f and g can only commute if they have the same source and target category (Hask in our case). And even when they don't commute, the resulting monad could still be a comonad, too. My category theory study stopped somewhere between Functor and Adjunction, but is there any deep magic you can describe here in a paragraph or two? I feel like I will never get Monad and Comonad until I understand Adjunction. Alas, I wish I could, but I have virtually no clue about adjoint functors myself :) I only know the classic example that conjunction and implication f a = (a,S) g b = S - b are adjoint (a,S) - b = a - (S - b) which is just well-known currying. We get the state monad (g `O` f) a = S - (S,a) and the stream comonad (f `O` f) a = (S, S - a) out of that. Regards apfelmus ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
Re: [Haskell-cafe] Re: Monads that are Comonads and the role of Adjunction
On Sun, 2007-12-16 at 13:49 +0100, apfelmus wrote: Dan Weston wrote: newtype O f g a = O (f (g a)) -- Functor composition: f `O` g instance (Functor f, Functor g) = Functor (O f g) where ... instance Adjunction f g = Monad (O g f) where ... instance Adjunction f g = Comonad (O f g) where ... class (Functor f, Functor g) = Adjunction f g | f - g, g - f where leftAdjunct :: (f a - b) - a - g b rightAdjunct :: (a - g b) - f a - b -- Functors are associative but not generally commutative. Apparently a Monad is also a Comonad if there exist left (f) and right (g) adjuncts that commute. Yes, but that's only sufficient, not necessary. Jules and David already pointed out that while every monad comes from an adjunction, this adjunction usually involves categories different from Hask. So, there are probably no adjoint functors f and g in Hask such that [] ~= g `O` f or data L a = One a | Cons a (L a) -- non-empty list L ~= g `O` f (proof?) Yet, both are monads and the latter is even a comonad. Moreover, f and g can only commute if they have the same source and target category (Hask in our case). And even when they don't commute, the resulting monad could still be a comonad, too. My category theory study stopped somewhere between Functor and Adjunction, but is there any deep magic you can describe here in a paragraph or two? I feel like I will never get Monad and Comonad until I understand Adjunction. Alas, I wish I could, but I have virtually no clue about adjoint functors myself :) Learn about representability. Representability is the core of category theory. (Though, of course, it is closely related to adjunctions.) I only know the classic example that conjunction and implication f a = (a,S) g b = S - b are adjoint (a,S) - b = a - (S - b) which is just well-known currying. We get the state monad (g `O` f) a = S - (S,a) and the stream comonad (f `O` f) a = (S, S - a) out of that. There is another very closely related adjunction that is less often mentioned. ((-)-C)^op -| (-)-C or a - b - C ~ b - a - C This gives rise to the monad, M a = (a - C) - C this is also exactly the comonad it gives rise to (in the op category which ends up being the above monad in the normal category). ___ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe
