Processing math: 100%

Monad

Collection

context C … category
definiendum T,η,μ in it
inclusion T in CC
inclusion η:1CT
inclusion μ:TTT
postulate μTμ=μμT
postulate μTη=μηT=1T

Discussion

A monad is functor together with two natural transformations that fulfill some algebraic relations.

Elaboration

Written out in component form, the postulates read

Picture the following chain of objects and notice that the axioms merely say the following: All ways ending up at TX must be the same.

XηXTXT(ηTX) or ηTX  μXTTXT(μX) or μTXTTTX

Alternative definition

From adjunctions

All monads arise by transferring some co-unit into the other category: Set T:=GF and μY:=G(εFY) and you got yourself a monad T,η,μ.

Terminology/Notation

The forward arrows ηX are called „unit“ or, in programmer circles, „return“. The backwards arrows μX are called „join“ and from the counit-unit adjunction perspective, they are the arrow images of the functor applied to the „co-unit“ components.

Algebraic characterization

Recall that Set can be equipped with a monoidal structure where units are singletons (= final objects in Set, e.g. 1:={0}) and the product can be taken to be the Cartesian product MN:=M×N (= categorical product for Set). Here, a monoid object is a triple given by

M,

e:1M,

:M×MM.

Now a monad is given by

T,

η:1CT,

μ:TTT

and is also a monoid object, namely in the category of endofunctors CC, with the monoidal product (not the categorical product) given by concatenation of functors ST:=ST.

Reference

Wikipedia: Monad (category theory), Monade (Informatik)


Context

Requirements

Functor, Natural transformation, Identity functor

Monoid