feat: add a predicate for monad morphisms

[eric-wieser]

We show that various list operations are preserved under monad morphisms, and that FreeM.liftM is.

Note that PolyFun already has the bundled version, but having the unbundled version now does not preclude adding the bundled version later.

[kim-em]

Suggested change

	lemma liftM_map {α β : Type uB} (f : α → β) (interp : (a : P.A) → m (P.B a)) (x : P.FreeM α) :
	lemma liftM_map {α β : Type uB} (f : α → β) (x : P.FreeM α) :

to match the argument order of the other lemmas.

[eric-wieser]

I think the other lemmas have the wrong argument order, this matches the order for liftM itself.

[kim-em]

Maybe add

/-- A monad morphism out of `FreeM F` that agrees with `handler` on lifted operations is an
interpreter for `handler`, and hence (by `Interprets.eq`) equals `liftM handler`. -/
theorem _root_.Cslib.IsMonadHom.interprets {eval : ∀ {α}, FreeM F α → m α}
    (h : IsMonadHom (FreeM F) m eval)
    (handler : {ι : Type u} → F ι → m ι) (hl : ∀ {ι} (op : F ι), eval (lift op) = handler op)
    {α : Type u} : Interprets handler (eval : FreeM F α → m α) where
  apply_pure a := h.map_pure a
  apply_lift_bind op cont := by rw [h.map_bind, hl]

[eric-wieser]

I'm not super happy with this Interprets API in the first place, so haven't spent much time thinking about how best to capture this. Can we punt this to a follow-up?

[kim-em]

This is (accidentally?) in the CSLib namespace.

[eric-wieser]

This is deliberate, but if you think it's a bad idea I can move it back.

[kim-em]

attribute [grind .] map_map map_mapConst

Maybe these grind patterns work better?

-- namespace IsFunctorHom
grind_pattern map_map => IsFunctorHom m n f, g <$> x
grind_pattern map_mapConst => IsFunctorHom m n f, Functor.mapConst a x

-- namespace IsApplicativeHom
grind_pattern map_pure => IsApplicativeHom m n f, (pure a : m α)
grind_pattern map_seq => IsApplicativeHom m n f, Seq.seq x y
grind_pattern map_seqLeft => IsApplicativeHom m n f, SeqLeft.seqLeft x y
grind_pattern map_seqRight => IsApplicativeHom m n f, SeqRight.seqRight x y

-- namespace IsMonadHom
grind_pattern map_bind => IsMonadHom m n f, x >>= y

-- namespace IsAlternativeHom
grind_pattern map_failure => IsAlternativeHom m n f, (Alternative.failure : m α)
grind_pattern map_orElse => IsAlternativeHom m n f, HOrElse.hOrElse x y

[eric-wieser]

How do these compare to the patterns I already have? Can I print out the pattern generated by grind_pattern to compare with grind??