monads in Haskell


A monad in Haskell is defined to be a type class with two methods:

> classMonadmwhere\mathbf{class}\;Monad\;m\;\mathbf{where}

> >>=::ma(amb)mb\gt\gt =::ma\to(a\to mb)\to mb

> return::amareturn::a\to ma

such that

> x>>=ffxx\gt\gt=f\equiv fx

> a>>=returnaa\gt\gt=return\equiv a

> (a>>=f)>>=ga>>=(λxfx>>=g)(a\gt\gt=f)\gt\gt=g\equiv a\gt\gt =(\lambda x\to fx\gt\gt =g)


mm being a monad (m:aa,μ:m 2m,ϵ:id am)(m:a\to a, \mu:m^2\to m,\epsilon:id_a\to m) on some object aa in a 2-category can be expressed in Haskell by

> classMonadmwhere\mathbf{class}\;Monad\;m\;\mathbf{where}

> map::(ab)mambmap::(a\to b)\to ma\to mb

> return::amareturn::a\to ma

> join::m(ma)majoin:: m(ma)\to ma

We have the following translation of Haskell and category theoretical language?:

> join:=μjoin:=\mu

> return:=ϵreturn :=\epsilon

Then from the category theoretical properties of (m,μ,ϵ)(m,\mu,\epsilon) we obtain (mixing the two languages)

> mapgϵϵgmap\; g\circ \epsilon\equiv \epsilon\circ g

> mapμμmap(mapg)map \; \circ \mu\equiv \mu\circ map(map\; g)

> μmapμμμ\mu\circ map\; \mu \equiv \mu\circ \mu

> μϵμmapϵ=id\mu\circ \epsilon\equiv \mu\circ map\;\epsilon =id

And with the following definitions

> mapf:=(λa>>=(returnf))map\; f :=(\lambda\to a\gt\gt=(return\circ f))

> joina=a>>id join \; a=a\gt\gt id

or alternatively

> a>>=f:=join(mapfa)a\gt\gt =f:=join (map\;fa)

one can verify that the two given definitions of a monad are equivalent.


category theory/monads, haskellwiki, wiki

Created on June 16, 2012 21:48:48 by Stephan Alexander Spahn (