\[ \require{mathtools} \let\DeclarePairedDelimiter\DeclarePairedDelimiters % MathJax typo %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % symbol %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % sets \newcommand{\N}{\mathbb{N}} % natural numbers \newcommand{\Z}{\mathbb{Z}} % integers \newcommand{\Q}{\mathbb{Q}} % rational numbers \newcommand{\R}{\mathbb{R}} % real numbers \newcommand{\C}{\mathbb{C}} % complex numbers % category \newcommand{\catf}[1]{{\mathbf{#1}}} \newcommand{\cA}{\catf{A}} \newcommand{\cB}{\catf{B}} \newcommand{\cC}{\catf{C}} \newcommand{\cD}{\catf{D}} \newcommand{\cE}{\catf{E}} \newcommand{\cF}{\catf{F}} \newcommand{\cG}{\catf{G}} \newcommand{\cH}{\catf{H}} \newcommand{\cI}{\catf{I}} \newcommand{\cJ}{\catf{J}} \newcommand{\cK}{\catf{K}} \newcommand{\cL}{\catf{L}} \newcommand{\cM}{\catf{M}} \newcommand{\cN}{\catf{N}} \newcommand{\cO}{\catf{O}} \newcommand{\cP}{\catf{P}} \newcommand{\cQ}{\catf{Q}} \newcommand{\cR}{\catf{R}} \newcommand{\cS}{\catf{S}} \newcommand{\cT}{\catf{T}} \newcommand{\cU}{\catf{U}} \newcommand{\cV}{\catf{V}} \newcommand{\cW}{\catf{W}} \newcommand{\cX}{\catf{X}} \newcommand{\cY}{\catf{Y}} \newcommand{\cZ}{\catf{Z}} \newcommand{\cZero}{\catf{0}} \newcommand{\cOne}{\catf{1}} \newcommand{\cTwo}{\catf{2}} \newcommand{\cArr}{\catf{Arr}} % arrow \newcommand{\cPSh}{\catf{PSh}} % presheaf \newcommand{\cCone}{\catf{Cone}} % cone \newcommand{\cCocone}{\catf{Cocone}} % cocone \newcommand{\cFin}{\catf{Fin}} % finite prefix \newcommand{\cSet}{\catf{Set}} % functions \newcommand{\cRel}{\catf{Rel}} % relations \newcommand{\cPos}{\catf{Pos}} % posets \newcommand{\cMon}{\catf{Mon}} % monoids \newcommand{\cCMon}{\catf{CMon}} % commutative monoids \newcommand{\cGrp}{\catf{Grp}} % groups \newcommand{\cAb}{\catf{Ab}} % abelian groups \newcommand{\cCat}{\catf{Cat}} % categories \newcommand{\cGrpd}{\catf{Grpd}} % groupoids \newcommand{\cVect}{\catf{Vect}} % vector spaces \newcommand{\cMat}{\catf{Mat}} % matrices \newcommand{\cTop}{\catf{Top}} % topological spaces and continuous maps \newcommand{\cMet}{\catf{Met}} % metric spaces and metric maps \newcommand{\cMeas}{\catf{Meas}} % measurable spaces and measurable functions \newcommand{\cStoch}{\catf{Stoch}} % measurable spaces and stochastic maps \newcommand{\cProb}{\catf{Prob}} % probability measures and measure-preserving functions \newcommand{\cSub}{\catf{Sub}} % subobjects %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % supscript %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\op}{^\mathrm{op}} \newcommand{\inv}{^{-1}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % function %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclareMathOperator{\lcm}{lcm} \DeclareMathOperator{\logsumexp}{log-sum-exp} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % arrow %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % morphism \newcommand{\xto}{\xrightarrow} % -> \newcommand{\xot}{\xleftarrow} % <- \newcommand{\toot}{\rightleftarrows} % <=> \newcommand{\iso}{\cong} % ~= \newcommand{\klto}{\rightsquigarrow} % ~> \newcommand{\mono}{\rightarrowtail} % >-> \newcommand{\epi}{\twoheadrightarrow} % ->> \newcommand{\ihom}{\multimap} % -o % category \newcommand{\incl}{\hookrightarrow} \newcommand{\adjto}[2]{\overset{{}\xto[]{#1}{}}{\underset{{}\xot[#2]{}{}}{\bot}}} % functor \newcommand{\nat}{\Rightarrow} % => \newcommand{\xnat}{\xRightarrow} % => \newcommand{\comma}{\downarrow} \newcommand{\adj}{\dashv} % -| %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % delimiter %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \DeclarePairedDelimiter{\parens}{(}{)} % parentheses ( ) \DeclarePairedDelimiter{\bracks}{[}{]} % brackets [ ] \DeclarePairedDelimiter{\braces}{\{}{\}} % braces { } \DeclarePairedDelimiter{\angles}{\langle}{\rangle} % angles \DeclarePairedDelimiter{\floor}{\lfloor}{\rfloor} \DeclarePairedDelimiter{\ceil}{\lceil}{\rceil} \newcommand{\set}{\braces} \newcommand{\singleton}{{\set{*}}} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % operator %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\compL}{\mathbin{\circ}} \newcommand{\compR}{\mathbin{;}} \newcommand{\Kl}{\mathrm{Kl}} \DeclareMathOperator{\Obj}{Obj} \DeclareMathOperator{\Hom}{Hom} \DeclareMathOperator{\Eq}{Eq} \DeclareMathOperator{\Coeq}{Coeq} \DeclareMathOperator{\Pull}{Pull} \DeclareMathOperator{\Push}{Push} \DeclareMathOperator{\Lan}{Lan} \DeclareMathOperator{\Ran}{Ran} \DeclareMathOperator{\Lift}{Lift} \DeclareMathOperator{\Rift}{Rift} \DeclareMathOperator{\id}{id} \DeclareMathOperator{\act}{act} \DeclareMathOperator{\colim}{colim} % exponential \DeclareMathOperator{\partf}{partial} \DeclareMathOperator{\curry}{curry} % natural number \DeclareMathOperator{\zero}{zero} \DeclareMathOperator{\successor}{succ} % list \DeclareMathOperator{\nil}{nil} \DeclareMathOperator{\cons}{cons} \newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}} % fold \DeclareMathOperator{\fold}{fold} \DeclareMathOperator{\map}{map} \DeclareMathOperator{\filter}{filter} % bool \DeclareMathOperator{\cond}{cond} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % order %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\meet}{\wedge} \newcommand{\join}{\vee} \newcommand{\bigmeet}{\bigwedge} \newcommand{\bigjoin}{\bigvee} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % logic %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% \newcommand{\lfal}{\bot} \newcommand{\ltru}{\top} \newcommand{\lcon}{\wedge} \newcommand{\lncon}{\uparrow} \newcommand{\ldis}{\vee} \newcommand{\lndis}{\downarrow} \newcommand{\limp}{\rightarrow} \newcommand{\lnimp}{\nrightarrow} \newcommand{\lcim}{\leftarrow} \newcommand{\lncim}{\nleftarrow} \newcommand{\leqv}{\leftrightarrow} \newcommand{\lneqv}{\nleftrightarrow} \newcommand{\lproves}{\vdash} % |- \newcommand{\lmodels}{\vDash} % |= \newcommand{\lnproves}{\nvdash} % |/- \newcommand{\lnmodels}{\nvDash} % |/= \]
A monad is a structure that describes generalized objects and morphisms.
1 Monad
The category \([\cC, \cC]\) of endofunctors is a strict monoidal category with the functor composition as the monoidal product and the identity functor \(\id_\cC\) as the monoidal unit.
A monad in a category \(\cC\) is an endofunctor \(T: \cC \to \cC\) equipped with two natural transformations:
- composition \(\mu: TT \nat T\)
- unit \(\eta: \id_\cC \nat T\)
subject to
- associativity: \(\mu (T \mu) = \mu (\mu T)\)
- identity: \(\mu (\eta T) = \id_T = \mu (T \eta)\)
In other words, a monad is a monoid in the category of endofunctors.
-- bind
(>>=) :: Monad m => m a -> (a -> m b) -> m b
(=<<) :: Monad m => (a -> m b) -> m a -> m b
(>>) :: Monad m => m a -> m b -> m b
(>=>) :: Monad m => (a -> m b) -> (b -> m c) -> (a -> m c)
(<=<) :: Monad m => (b -> m c) -> (a -> m b) -> (a -> m c)2 Algebra
2.1 F-algebra
For an endofunctor \(F: \cC \to \cC\), an algebra over an endofunctor (F-algebra) \((A, \act_A)\) consists of an object \(A\) (carrier) and a morphism \(\act_A: FA \to A\).
An F-algebra homomorphism from \((A, \act_A)\) to \((B, \act_B)\) is a morphism \(f: A \to B\) such that \(\act_B \compL Ff = f \compL \act_A\).
For an endofunctor \(F: \cC \to \cC\), a coalgebra over an endofunctor (F-coalgebra) \((A, \act_A)\) consists of an object \(A\) (carrier) and a morphism \(\act_A: A \to FA\).
An F-coalgebra homomorphism from \((A, \act_A)\) to \((B, \act_B)\) is a morphism \(f: A \to B\) such that \(\act_B \compL f = Ff \compL \act_A\).
2.1.1 Initial F-algebra
An initial F-algebra of an endofunctor \(F\) is an initial object in the category of F-algebras.
If an endofunctor \(F\) has an initial F-algebra \((\mu F, i)\), then \(F \mu F \iso \mu F\).
- \((F \mu F, Fi)\) is an F-algebra, so there exists a unique F-algebra homomorphism \(u: \mu F \to F \mu F\).
- \(i \compL u: \mu F \to \mu F\) is an F-algebra homomorphism from the initial F-algebra and thus is unique, \(i \compL u = \id_{\mu F}\).
- \(u \compL i = Fi \compL Fu = F(i \compL u) = F \id_{\mu F} = \id_{F \mu F}\).
In a category \(\cC\) with a terminal object \(1\), a natural numbers object (NNO) \(\N\) is an initial F-algebra of the endofunctor \(X \mapsto 1 + X\).
\[\begin{aligned} \begin{array}{rccccc} & 1 &+& \N &\to& \N \\ \zero: & * && &\mapsto& 0 \\ \successor: && & n &\mapsto& n+1 \end{array} \end{aligned}\]
In a category \(\cC\) with a terminal object \(1\) and binary products, an \(A\)-valued list object \([A]\) is an initial F-algebra of the endofunctor \(X \mapsto 1 + A \times X\).
\[\begin{aligned} \begin{array}{rccccc} & 1 &+& A \times [A] &\to& [A] \\ \nil: & * && &\mapsto& [] \\ \cons: & && (x, xs) &\mapsto& x:xs \end{array} \end{aligned}\]
2.2 M-algebra
For a monoid object \((M, \mu, \eta)\) in a monoidal category \((\cC, \otimes, I, \alpha, \lambda, \rho)\), a (left) algebra over a monoid object (M-algebra) is an F-algebra \((A, \act_A: M \otimes A \to A)\) for the endofunctor
\[\begin{aligned} (M \otimes -): \cC &\to \cC \\ A &\mapsto M \otimes A \\ f &\mapsto \id_M \otimes f \end{aligned}\]
that is compatible with
- monoid product: \(\act \compL (\mu \otimes \id) = \act \compL (\id \otimes \act) \compL \alpha\)
- monoid unit: \(\act \compL (\eta \otimes \id) = \lambda\)
An M-algebra homomorphism is an F-algebra homomorphism.
2.3 T-algebra
For a monad \((T, \mu, \eta)\), a (left) algebra over a monad (T-algebra) is an M-algebra \((A, \act_A: TA \to A)\) in the category of endofunctors over the constant functor \(\Delta A\).
Thus, a T-algebra is compatible with
- monad composition: \(\act_A \compL T \act_A = \act_A \compL \mu_A\)
- monad unit: \(\act_A \compL \eta_A = \id_A\)
A T-algebra homomorphism is an F-algebra homomorphism.
For a monad \((T, \mu, \eta)\) in a category \(\cC\), the Eilenberg–Moore category \(\cC^T\) is a category of T-algebras and T-algebra homomorphisms.
3 Kleisli category
For a monad \((T, \mu, \eta)\) in a category \(\cC\), the Kleisli category \(\cC_T\) is a category whose
- objects are \(\cC\)-objects \(\Obj_{\cC_T} := \Obj_\cC\)
- morphisms are Kleisli morphisms \(\Hom_{\cC_T}(A, B) := \Hom_\cC(A, TB)\)
- composition is the Kleisli composition \(g_\Kl \compL_T f_\Kl := \mu_C \compL Tg_\Kl \compL f_\Kl\)
- identity morphism is the monad unit \(\id_A := \eta_A: A \to TA\)
4 Monadic adjunction
4.1 Adjunction to monad
An adjunction
\[(F: \cC \toot \cD: G, \epsilon: FG \nat \id_\cD, \eta: \id_\cC \nat GF)\]
gives rise to a monad
\[(GF: \cC \to \cC, G \epsilon F: GFGF \nat GF, \eta: \id_\cC \nat GF)\]
and a comonad
\[(FG: \cD \to \cD, F \eta G: FG \nat FGFG, \epsilon: FG \nat \id_\cD)\]
4.2 Monad to adjunction
5 Examples
5.1 Maybe
- \(MA = 1 + A\) nothing or values
- \(Mf = 1 + f\) computation with failure
- \(\mu: MM \nat M\) failure propagation
- \(\eta: \id \nat M\) just
- \(A \to MB\) partial function
- \(MA \to A\) pointed object
5.2 List
free monoid
- \([]: 1 \to LA\) empty list
- \(\concat: LA \times LA \to LA\) concatenation
free monoid monad
- \(LA\) list
- \(Lf\) list map
- \(\mu: LL \nat L\) concatenation
- \(\eta: \id \nat L\) singleton
- \(A \to LB\) list function
- \(LA \to A\) monoid \((A, \fold [e: 1 \to A, \cdot: A \times A \to A])\)
- right identity \([a]\)
- left identity \([[], [a]]\)
- associativity \([[a, b], [c]]\)
5.3 Powerset
- \(PA = 2^A\) powerset
- \(Pf\) set map
- \(\mu: PP \nat P\) union
- \(\eta: \id \nat P\) singleton
- \(A \to PB\) set function
- \(PA \to A\) suplattice
5.4 Multiset
- \(NA = \N^A\) multiset
- \(Nf\) sum map
- \(\mu: NN \nat N\) multiplication
- \(\eta: \id \nat N\) singleton
- \(A \to NB\) multiset function
- \(NA \to A\) commutative monoid
5.5 Probability
- \(PA\) probability measures
- \(Pf\) pushforward measure
- \(\mu: PP \nat P\) marginalization
- \(\eta: \id \nat P\) Dirac measure
- \(A \to PB\) conditional probability
- \(PA \to A\) expectation
5.6 State
- \([S, S \times A]\)
5.7 Continuation
- \([[A, R], R]\)
6 Monoidal monad
A monoidal monad is a monad in the 2-category of monoidal categories, lax monoidal functors, and monoidal natural transformations.
7 Monoidal Kleisli category
For a monoidal monad \((T, \mu_T, \eta_T, \mu, \eta)\) in \((\cC, \otimes, I)\), the Kleisli category \(\cC_T\) inherits the monoidal structure from \(\cC\), whose
monoidal product \(\otimes_\Kl\) on objects is the monoidal product \(\otimes\) on \(\cC\)
monoidal product \(\otimes_\Kl\) on morphisms is obtained by \(f_\Kl \otimes_\Kl g_\Kl := \mu (f_\Kl \otimes g_\Kl)\)
\[(A \xto{f_\Kl} TB) \otimes_\Kl (C \xto{g_\Kl} TD) = A \otimes C \xto{f_\Kl \otimes_\Kl g_\Kl} T(B\otimes D) = A \otimes C \xto{f_\Kl \otimes g_\Kl} TB \otimes TD \xto{\mu_{B, D}} T(B \otimes D)\]
monoidal unit, associator, and left/right unitors are those of \(\cC\)