Moggi used monads in category theory to define computations with side effects in functional programming. The basic insight is that in addition to the values of various types in functional programming, there are "computations" of various types. Examples of "computations" would be exceptions or continuations. Each monad defines for each value type a computation "containing" that type, and the whole type system of values you started with can be embedded in a new type system with new computation types.
Monads in category theory are an algebraic device for embedding a category--usually a cartesian closed category--of types of values into a new category with types of computations. However, the correspondence between Haskell monads and category monads are related by a series of adjunctions.
Suppose that C is a cartesian closed category and M:C->C is a monad with natural transformations e:1->M
(the unit) and u:MM->M (the multiplication).
We assume a fixed choice of products and compatible exponentials: for each type A of C,
A x ( ) -| [A -> ( )]
Here's the adjunction
MA -> [[A->MB] -> MB]
---------------------
MA x [A -> MB] -> MB
---------------------
[MA -> MB] x MA -> MB
-----------------------
[A -> MB] -> [MA -> MB]
The final map is given by currying, but it can also be motivated as follows if you think of the exponentials as internal hom sets. If g:A -> MB is in C, so
that g:A->B is in the Kleisli category C^M, then u_{MB}oM(g):MA->MB. We can write this as the lambda term \lambda x\in A A -> MB.u_{MB} oM x
This lambda term corresponds to composition in the Kleisli category C^M of C, and belongs to the internal language LL(C), the simply typed lambda calculus determined by C. Under the Curry-Howard-Lambek correspondence, the lambda term corresponds to the required map of C.
Monads in category theory are an algebraic device for embedding a category--usually a cartesian closed category--of types of values into a new category with types of computations. However, the correspondence between Haskell monads and category monads are related by a series of adjunctions.
Suppose that C is a cartesian closed category and M:C->C is a monad with natural transformations e:1->M (the unit) and u:MM->M (the multiplication).
We assume a fixed choice of products and compatible exponentials: for each type A of C,
Here's the adjunction The final map is given by currying, but it can also be motivated as follows if you think of the exponentials as internal hom sets. If g:A -> MB is in C, so that g:A->B is in the Kleisli category C^M, then u_{MB}oM(g):MA->MB. We can write this as the lambda term \lambda x\in A A -> MB.u_{MB} oM xThis lambda term corresponds to composition in the Kleisli category C^M of C, and belongs to the internal language LL(C), the simply typed lambda calculus determined by C. Under the Curry-Howard-Lambek correspondence, the lambda term corresponds to the required map of C.