\[ \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 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 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{\xtoot}[2]{\xrightleftharpoons[#2]{#1}} \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{\Sub}{Sub} \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{\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{\lT}{\top} \newcommand{\lF}{\bot} % logical connective \newcommand{\binop}[1]{\mathbin{#1}} % conjunction AND \newcommand{\lcon}{\binop{\wedge}} % not conjunction NAND \newcommand{\lncon}{\binop{\uparrow}} % disjunction OR \newcommand{\ldis}{\binop{\vee}} % not disjunction NOR \newcommand{\lndis}{\binop{\downarrow}} % implication \newcommand{\limp}{\binop{\rightarrow}} % not implication \newcommand{\lnimp}{\binop{\nrightarrow}} % converse implication \newcommand{\lcim}{\binop{\leftarrow}} % not converse implication \newcommand{\lncim}{\binop{\nleftarrow}} % equivalence XNOR \newcommand{\leqv}{\binop{\leftrightarrow}} % not equivalence XOR \newcommand{\lneqv}{\binop{\nleftrightarrow}} \newcommand{\lproves}{\binop{\vdash}} % |- \newcommand{\lmodels}{\binop{\vDash}} % |= \newcommand{\lnproves}{\binop{\nvdash}} % |/- \newcommand{\lnmodels}{\binop{\nvDash}} % |/= \newcommand{\truth}{{\set{\lT, \lF}}} \newcommand{\quant}{{[0, \infty]}} \newcommand{\inter}{{[0, 1]}} \newcommand{\qnot}{\mathord{\sim}} \newcommand{\qcon}{\binop{\otimes}} \newcommand{\qdis}{\binop{\oplus}} \newcommand{\qimp}{\binop{\multimap}} \DeclareMathOperator*{\qforall}{\triangledown} \DeclareMathOperator*{\qexists}{\vartriangle} \]
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 Endofunctor algebra
For an endofunctor \(F: \cC \to \cC\), an algebra over an endofunctor \((A, \alpha_A)\) consists of an object \(A\) (carrier) and a morphism \(\alpha_A: FA \to A\).
An endofunctor algebra homomorphism from \((A, \alpha_A)\) to \((B, \alpha_B)\) is a morphism \(f: A \to B\) such that \(\alpha_B \compL Ff = f \compL \alpha_A\).
For an endofunctor \(F: \cC \to \cC\), a coalgebra over an endofunctor \((A, \alpha_A)\) consists of an object \(A\) (carrier) and a morphism \(\alpha_A: A \to FA\).
An endofunctor coalgebra homomorphism from \((A, \alpha_A)\) to \((B, \alpha_B)\) is a morphism \(f: A \to B\) such that \(\alpha_B \compL f = Ff \compL \alpha_A\).
2.1.1 Initial algebra
An initial algebra of an endofunctor \(F\) is an initial object in the category of endofunctor algebras.
If an endofunctor \(F\) has an initial algebra \((\mu F, i)\), then \(F \mu F \iso \mu F\).
- \((F \mu F, Fi)\) is an endofunctor algebra, so there exists a unique endofunctor algebra homomorphism \(u: \mu F \to F \mu F\).
- \(i \compL u: \mu F \to \mu F\) is an endofunctor algebra homomorphism from the initial 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 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 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 Monoid algebra
For a monoid object \((M, \mu, \eta)\) in a monoidal category \((\cC, \otimes, I, \alpha, \lambda, \rho)\), a (left) algebra over a monoid is an endofunctor algebra \((A, \alpha_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: \(\alpha_A \compL (\id_M \otimes \alpha_A) \compL \alpha_{M, M, A} = \alpha_A \compL (\mu \otimes \id_A)\)
- monoid unit: \(\alpha_A \compL (\eta \otimes \id_A) = \lambda_A\)
An monoid algebra homomorphism is an endofunctor algebra homomorphism.
2.3 Monad algebra
For a monad \((T, \mu, \eta)\), a (left) algebra over a monad is a monoid algebra \((A, \alpha_A: TA \to A)\) in the category of endofunctors over the constant functor \(\Delta A\).
Thus, a monad algebra is compatible with
- monad composition: \(\alpha_A \compL T \alpha_A = \alpha_A \compL \mu_A\)
- monad unit: \(\alpha_A \compL \eta_A = \id_A\)
A monad algebra homomorphism is an endofunctor algebra homomorphism.
For a monad \((T, \mu, \eta)\) in a category \(\cC\), the Eilenberg–Moore category \(\cC^T\) is a category of monad algebras and monad 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
Giry monad \(\text{measurable space } (A, \Sigma_A) \mapsto (\set{\text{probability measure } \mu: \Sigma_A \to [0, 1]}, \set{\epsilon_U: \mu \mapsto \mu(U) \mid U \in \Sigma_A})\)
- \(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\)