nLab monads in Haskell

Definition

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

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

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

return::a→mareturn::a\to ma

such that

x>>=f≡fxx\gt\gt=f\equiv fx

a>>=return≡aa\gt\gt=return\equiv a

(a>>=f)>>=g≡a>>=(λx→fx>>=g)(a\gt\gt=f)\gt\gt=g\equiv a\gt\gt =(\lambda x\to fx\gt\gt =g)

Remark

mm being a monad (m:a→a,μ:m 2→m,ϵ:id a→m)(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::(a→b)→ma→mbmap::(a\to b)\to ma\to mb

return::a→mareturn::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>>=(return∘f))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.

References

category theory/monads, haskellwiki, wiki

Created on June 16, 2012 at 21:48:49. See the history of this page for a list of all contributions to it.