Monads and interaction, MGS 2021
Exercise class 2
1. Show that, if (T_0, \eta_0, \mu_0), (T_1, \eta_1, \mu_1) are monads,
then T_0 \times T_1 is also has a *canonical* monad structure.
Prove that this resulting monad is the *product* of the two given
monads (product in Monad(\C)).
2. Describe the Kleisli category of the product monad T_0 \times T_1.
3. From the isomorphism NEList = Id \times List,
produce a monad structure on the nonempty list functor.
4. Instantiate the definition of monad algebra for the writer monad
for a monoid P:
Wr^P X = P x X
Do you recognize what you get?
5. Check that the following triple (X, get, put) is a mnemoid for the
state set S.
X = S => S
get : S => S => S -> S => S
get f = \lambda s. f s s
put : S x (S => S) -> S => S
put (s, g) = \lambda _. g s
You can do this by checking the mnemoid equations. But
there's also another way.
Develop an intuition for what this means.
6. Let PreSt^S be the free-algebras monad of the functor
F X = (S => X) + S x X, i.e.,
PreSt^S X = mu Z. X + (S => Z) + S x Z.
PreSt^S X = X + (S => PreSt^S X) + S x (PreSt^S X)
The algebras of this monad are objects X with maps
get : S => X -> X and put : S x X -> X, call them premnemoids.
They are similar to mnemoids, but subject to no equations.
Hence there is a carrier-preserving functor from Mnem^S \cong Alg(St^S) to
PreMnem^S = Alg(PreSt^S).
Give an explicit definition of the corresponding monad map from
PreSt^S to St^S.