Monads and interaction, MGS 2021
Exercise class 1
Here are some little problems to tinker with.
1. Prove that the multiplication \mu of a monad structure on a functor
T determines its unit. I.e., if both (\eta, \mu) and (\eta', \mu') are
monad structures on T, then \eta = \eta'.
Prove also that the unit does not determine the multiplication.
(You can find two examples of this from the lecture.)
2. Functoriality of T and naturality of \eta and (-)^\star
are not required in the definition of Kleisli triple.
Prove that they follow from the 3 equations of a Kleisli triple.
3. For any category with finite coproducts (or just for Set), prove
that the "exceptions functor" Ex^E
Ex^E X = E + X
carries exactly one monad structure.
3'. Alternatively, prove that, for any category with finite products
(or just for Set), monad structures on the "writer functor" Wr^P
Wr^P X = P \times X
are in a bijection with monoid structures on the object P.
4. Prove that the alternative list monad from the lecture
is actually a monad.
4'. Convert it into a Kleisli triple.
Get an intuitive understanding of what sort of "notion"
of nondeterminism it stands for.
(You can take its formalization from Mnd.hs and
reformalize it in the style of Monad.hs.)
5. You can find many exotic list monads in Secs 3-4 of this paper:
McDermott, PirĂ³g, Uustalu, Degrading lists, PPDP '20
Check the paper, check Maciej's code, have fun.
http://cs.ioc.ee/~tarmo/papers/mcdermott-pirog-uustalu-ppdp20.pdf
https://github.com/maciejpirog/exotic-list-monads
6. The state monad St^S
St^S X = S \fun S \times X
has as maps of its Kleisli category maps
Y \to S \fun S \times X
These are in a bijection with maps
S \times Y \to S \times X
Describe the Kleisli category in these terms.
6'. Carry out a similar exercise for the monad Cnt^R
Cnt^R X = (X \fun R) \fun R
i.e., find a nice description of the Kleisli category of this monad.