Lift of binary function

Stream: Is there code for X?

[Adam Topaz]

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]

You can do λ ma mb, f <$> ma <*> mb- this works for any applicative not just monads

[Patrick Massot]

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

[Patrick Massot]

Simon will tell us everything about monadic ascii art.

[Adam Topaz]

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]

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

[Patrick Massot]

@Simon Hudon ?

[Adam Topaz]

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]

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]

I guess the lemma is false in general.

[Simon Hudon]

foo is not going to hold for monads in general

[Patrick Massot]

We could imagine side effects ruining the lemma.

[Simon Hudon]

Exactly

[Adam Topaz]

Oh yeah!

[Simon Hudon]

for bar, you can prove it by normalizing using monad_norm

[Adam Topaz]

Okay, thanks!

[Simon Hudon]

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

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

[Adam Topaz]

simp with monad_norm proves bar, as you said.

[Adam Topaz]

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

[Bhavik Mehta]

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

[Adam Topaz]

yes that looks right!

[Adam Topaz]

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

[Simon Hudon]

If you use applicative notation, is_comm_applicative will suffice

[Adam Topaz]

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]

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]

That sounds like a reasonable conclusion