## Stream: Is there code for X?

### Topic: Lift of binary function

#### Adam Topaz (Aug 08 2020 at 19:14):

Does something like this already exist?

def lift₂ (α β γ : Type*) (M : Type* → Type*) [monad M] (f : α → β → γ) : M α → M β → M γ :=

#### Patrick Massot (Aug 08 2020 at 19:36):

Yes, I was about to write there should be some ascii art doing it.

#### Adam Topaz (Aug 08 2020 at 19:39):

Thanks. I guss what I'm really hoping is that mathlib has a lemma that says something like this:

lemma foo (α β γ : Type*) (M : Type* → Type*) [monad M] [is_lawful_monad M]
(f : α → β → γ) (ma : M α) (mb : M β) :
do {a ← ma, b ← mb, return $f a b} = do {b ← mb, a ← ma, return$ f a b} := sorry


Any ideas?

#### Adam Topaz (Aug 08 2020 at 19:40):

one would think simp should solve this, right? (maybe not, but there should be a one line proof, I think.)

@Simon Hudon ?

#### Adam Topaz (Aug 08 2020 at 19:43):

Also, refl doesn't work for this:

lemma bar (α β γ : Type*) (M : Type* → Type*) [monad M] [is_lawful_monad M]
(f : α → β → γ) (ma : M α) (mb : M β) :
do {a ← ma, b ← mb, return $f a b} = f <$> ma <*> mb := by refl -- failed!


#### Simon Hudon (Aug 08 2020 at 19:46):

Manipulating applicative and monad can be a pain without the right set of simplification lemmas. There's functor_norm and monad_norm as lists of simplification lemmas to normalize those expressions. That should help. In your specific situation, you're going to need applicatives to commute

#### Patrick Massot (Aug 08 2020 at 19:46):

I guess the lemma is false in general.

#### Simon Hudon (Aug 08 2020 at 19:46):

foo is not going to hold for monads in general

#### Patrick Massot (Aug 08 2020 at 19:47):

We could imagine side effects ruining the lemma.

Exactly

Oh yeah!

#### Simon Hudon (Aug 08 2020 at 19:47):

for bar, you can prove it by normalizing using monad_norm

Okay, thanks!

#### Simon Hudon (Aug 08 2020 at 19:48):

@Patrick Massot I think I like this terminology even better than "monadology": ascii art. I think I'll find a way to put it on my resume

#### Simon Hudon (Aug 08 2020 at 19:52):

(you may need to import control.monad.basic)

#### Adam Topaz (Aug 08 2020 at 19:53):

simp with monad_norm proves bar, as you said.

#### Adam Topaz (Aug 08 2020 at 19:54):

Is there some natural typeclass extending a lawful monad where foo holds true?

#### Bhavik Mehta (Aug 08 2020 at 19:55):

I'm pretty sure you want a https://ncatlab.org/nlab/show/commutative+monad

#### Adam Topaz (Aug 08 2020 at 19:55):

yes that looks right!

#### Adam Topaz (Aug 08 2020 at 19:58):

Ha! Is it true that foo exactly characterizes commutative monads?

#### Simon Hudon (Aug 08 2020 at 20:02):

If you use applicative notation, is_comm_applicative will suffice

#### Adam Topaz (Aug 08 2020 at 20:04):

Perfect! That's what I'm looking for (I guess [monad M] [is_lawful_monad M] [is_comm_applicative M] is equivalent to [is_commutative_monad M])

#### Adam Topaz (Aug 08 2020 at 20:08):

In case it is useful for anyone else:

lemma foo (α β γ : Type*) (M : Type* → Type*) [monad M] [is_lawful_monad M] [is_comm_applicative M]
(f : α → β → γ) (ma : M α) (mb : M β) :
f <$> ma <*> mb = do {b ← mb, a ← ma, return$ f a b} :=
begin
rw is_comm_applicative.commutative_map,