Spahn monads in Haskell (changes)

Showing changes from revision #1 to #2: Added | Removed | Changed

Haskell

Definition

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)

Remark

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.

References

category theory/monads, haskellwiki, wiki

Last revised on June 16, 2012 at 21:34:56. See the history of this page for a list of all contributions to it.