Zulip Chat Archive

Stream: maths

Topic: kleisli vs kleisli


view this post on Zulip Bhavik Mehta (Oct 08 2020 at 16:15):

(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.

view this post on Zulip Simon Hudon (Oct 08 2020 at 16:22):

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

view this post on Zulip Simon Hudon (Oct 08 2020 at 16:48):

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.

view this post on Zulip Simon Hudon (Oct 08 2020 at 16:50):

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.

view this post on Zulip Adam Topaz (Oct 08 2020 at 17:02):

Is the dependence of mfoldl on Kleisli really necessary?

view this post on Zulip Kyle Miller (Oct 08 2020 at 17:35):

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.)

view this post on Zulip Adam Topaz (Oct 08 2020 at 17:42):

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].

view this post on Zulip Scott Morrison (Oct 09 2020 at 00:09):

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.


Last updated: May 14 2021 at 19:21 UTC