Zulip Chat Archive

Stream: Is there code for X?

Topic: Lift of binary function


view this post on Zulip 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}

view this post on Zulip Bhavik Mehta (Aug 08 2020 at 19:36):

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

view this post on Zulip Patrick Massot (Aug 08 2020 at 19:36):

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

view this post on Zulip Patrick Massot (Aug 08 2020 at 19:37):

Simon will tell us everything about monadic ascii art.

view this post on Zulip 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?

view this post on Zulip 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.)

view this post on Zulip Patrick Massot (Aug 08 2020 at 19:40):

@Simon Hudon ?

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Aug 08 2020 at 19:46):

I guess the lemma is false in general.

view this post on Zulip Simon Hudon (Aug 08 2020 at 19:46):

foo is not going to hold for monads in general

view this post on Zulip Patrick Massot (Aug 08 2020 at 19:47):

We could imagine side effects ruining the lemma.

view this post on Zulip Simon Hudon (Aug 08 2020 at 19:47):

Exactly

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:47):

Oh yeah!

view this post on Zulip Simon Hudon (Aug 08 2020 at 19:47):

for bar, you can prove it by normalizing using monad_norm

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:47):

Okay, thanks!

view this post on Zulip 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

view this post on Zulip Simon Hudon (Aug 08 2020 at 19:52):

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

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:53):

simp with monad_norm proves bar, as you said.

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:54):

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

view this post on Zulip Bhavik Mehta (Aug 08 2020 at 19:55):

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

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:55):

yes that looks right!

view this post on Zulip Adam Topaz (Aug 08 2020 at 19:58):

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

view this post on Zulip Simon Hudon (Aug 08 2020 at 20:02):

If you use applicative notation, is_comm_applicative will suffice

view this post on Zulip 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])

view this post on Zulip 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

view this post on Zulip Simon Hudon (Aug 08 2020 at 20:08):

That sounds like a reasonable conclusion


Last updated: May 16 2021 at 05:21 UTC