# Zulip Chat Archive

## Stream: maths

### Topic: kleisli vs kleisli

#### 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:

- Keep both versions, and add an equivalence of kleisli categories when the control.monad instance is lawful.
- 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. - 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 (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

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

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

#### Adam Topaz (Oct 08 2020 at 17:02):

Is the dependence of `mfoldl`

on `Kleisli`

really necessary?

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

#### 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]`

.

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