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]

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??

[kim-em]

set_option trace.grind.ematch.pattern true

[kim-em]

In particular grind . produces:

map_map:  [@Functor.map m _ α β g x,  @Functor.map n _ _ _ g _,  IsFunctorHom _ _ _ _ f]
map_pure: [@pure m _ α a,             @pure n _ _ a,             IsApplicativeHom _ _ _ _ f]
map_bind: [@bind m _ α β x k,         @bind n _ _ _ _ _,         IsMonadHom _ _ _ _ f]

but the proposed grind_patterns give:

map_map:  [IsFunctorHom m n f,     @Functor.map _ _ α β g x]
map_pure: [IsApplicativeHom m n f, @pure _ _ α a]
map_bind: [IsMonadHom m n f,       @bind _ _ α β x k]

[kim-em]

On second thoughts, maybe the proposed ones are too aggressive anyway. Without some actual proofs to try these out on, maybe it is premature optimization.

[eric-wieser]

I wasn't able to get either spelling to help with the proofs, so have left this as is for now.