# Zulip Chat Archive

## 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 γ :=
λ ma mb, do {a ← ma, b ← mb, return $ f a b}
```

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

You can do `λ ma mb, f <$> ma <*> mb`

- this works for any applicative not just monads

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

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

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

Simon will tell us everything about monadic ascii art.

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

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

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

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

Exactly

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

Oh yeah!

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

for `bar`

, you can prove it by normalizing using `monad_norm`

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

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,
simp with monad_norm,
refl,
end
```

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

That sounds like a reasonable conclusion

Last updated: May 16 2021 at 05:21 UTC