Alex Rivera | Logout

Monads as adjunctions

Asked 2011-01-15T00:31:01.290
86

I've been reading about monads in category theory. One definition of monads uses a pair of adjoint functors. A monad is defined by a round-trip using those functors. Apparently adjunctions are very important in category theory, but I haven't seen any explanation of Haskell monads in terms of adjoint functors. Has anyone given it a thought?

Edit
Report

1 Answer

10

Derek Elkins was showing me recently over dinner how the Cont Monad arises from composing the (_ -> k) contravariant functor with itself, since it happens to be self-adjoint. That's how you get (a -> k) -> k out of it. Its counit, however, leads to double negation elimination, which can't be written in Haskell.

For some Agda code that illustrates and proves this, please see http://hpaste.org/68257.

answered 2011-01-15T03:05:52.077

Your Answer