kleisli vs kleisli

Stream: maths

[Bhavik Mehta]

(continuing conversation from https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/lintsprint.205.20Oct/near/212366576) I had a go at changing the existing Kleisli to work for category theory monads rather than control monads, which works (just about) okay in principle, but it ends up breaking mfoldl in control.fold. In particular, that uses monad m (and no is_lawful_) instances, which is problematic if (category theory) Kleisli is defined as def kleisli (T : C ⥤ C) [category_theory.monad.{v} T] := C, because the conversion of m : Type u -> Type u with [control.monad m] to a [category_theory.monad m] requires is_lawful_monad m. The obvious fix is to remove the monad requirement here, but unfortunately this doesn't fix it, since we still need is_lawful_functor m in order to lift m to a category theory functor. As I see it, there are two ways of moving forward now:

1. Keep both versions, and add an equivalence of kleisli categories when the control.monad instance is lawful.
2. Change of_type_functor to produce a "pre"functor if there is no lawful functor instance (and a functor if there is such an instance), and set category_theory.kleisli to accept a prefunctor instead of a functor.
3. Make mfoldl use the stronger is_lawful_monad m requirement.

My instinct is towards 1, but I'm happy with 2 as well, and for 3 it strongly depends on what mfoldl is actually used for. Pinging @Scott Morrison since you brought this up and @Simon Hudon since you wrote mfoldl.

[Simon Hudon]

I'd like to avoid 3. A lot of classes used for programming separate the laws from the functions. One useful effect of that is that, I can use the classes in writing automation that would be useful to prove the laws

[Simon Hudon]

I think 1 is simpler. 2 risks contaminating the category theory library with the same set of design constraints. There is a little of that already with category_struct and has_hom, I'm not sure it's good idea to keep pushing in that direction.

[Simon Hudon]

On the other hand, I would like a richer connection between programming and category theory. There's a class I'm working on which I call reified_monad (it comes with reified_functor) in order to embed a monad in Type (from control) into a different category. It might be that the separation would be useful then. But we can also just cross that bridge when we get there.

[Adam Topaz]

Is the dependence of mfoldl on Kleisli really necessary?

[Kyle Miller]

Simon Hudon said:

I'd like to avoid 3. A lot of classes used for programming separate the laws from the functions. One useful effect of that is that, I can use the classes in writing automation that would be useful to prove the laws

For sake of reducing the sizes of variable lists, would it make any sense to rename things like is_lawful_X to lawful_X and make them extend X rather than taking an [X f] parameter? (Or even rename is_lawful_X to X and X to pre_X? Then there ought to be an understanding that functions should use pre_X when possible.)

[Adam Topaz]

Whatever happened with this [[foo]] proposal? I.e. writing [[is_lawful_monad M]] is supposed to be equivalent to [monad M] [is_lawful_monad M].

[Scott Morrison]

This would be lovely, but it would be a big change, and without hearing that there was enthusiasm for it in Lean 4 we wouldn't even start trying to make it happen in Lean 3.