Zulip Chat Archive

Stream: general

Topic: option is a monad


Kevin Buzzard (Apr 01 2020 at 18:30):

I read in Programming in Lean that option is a monad. I rolled my own option and decided to try and define a term of type monad option. I seem to have to fill in a bunch of fields, I've done half of them, and it's just dawned on me that none of them are proofs :-/ I have map_const, seq_left and seq_right left to do. But I'm not doing the right thing because I'm sure there should be proofs involved. Should I be proving it's a lawful monad?

Reid Barton (Apr 01 2020 at 18:30):

Yes

Reid Barton (Apr 01 2020 at 18:33):

monad is for programming, and programmers don't need proofs

Patrick Massot (Apr 01 2020 at 18:34):

Kevin, what you're doing is called Haskell. To become Lean you need the lawfulness.

Kevin Buzzard (Apr 01 2020 at 18:35):

I was actually experimenting with things which I thought might be worth doing in the tutorial project

Kevin Buzzard (Apr 01 2020 at 18:35):

but for some reason I thought a monad had about two fields and two proofs

Kevin Buzzard (Apr 01 2020 at 18:36):

and currently I seem to have to prove map_const_eq, _id_map, bind_pure_comp_eq_map, bind_map_eq_seq, pure_bind, bind_assoc and I also have to guess definitions of map_const, seq_left and seq_right

Kevin Buzzard (Apr 01 2020 at 18:36):

this has got a bit out of hand.

Reid Barton (Apr 01 2020 at 18:37):

The category_theory monad would look more like what you expect

Kevin Buzzard (Apr 01 2020 at 18:37):

Furthermore I have no idea what all the notation means in the goals :-) x >>= pure ∘ f = f <$> x ?

Reid Barton (Apr 01 2020 at 18:37):

but I don't know whether it is suitable for your purposes

Kevin Buzzard (Apr 01 2020 at 18:37):

My purposes are trying to figure out if I can teach schoolkids what monads are

Jasmin Blanchette (Apr 01 2020 at 18:38):

At the VU, we just defined our own monad class.

Jasmin Blanchette (Apr 01 2020 at 18:38):

To avoid all that stuff.

Jasmin Blanchette (Apr 01 2020 at 18:38):

Two fields, three proofs.

Patrick Massot (Apr 01 2020 at 18:39):

What's with the burrito?

Kevin Buzzard (Apr 01 2020 at 18:39):

Is one of them (f >>= λ (_x : α → β), _x <$> x) = f <*> x

Johan Commelin (Apr 01 2020 at 18:39):

Seriously?

Johan Commelin (Apr 01 2020 at 18:39):

@Patrick Massot Search for monad and burrito

Johan Commelin (Apr 01 2020 at 18:39):

And brew yourself a cup of coffee.... you'll have a long evening

Johan Commelin (Apr 01 2020 at 18:40):

https://duckduckgo.com/?t=ffab&q=monad+burrito&atb=v1-1&ia=web

Johan Commelin (Apr 01 2020 at 18:40):

@Kevin Buzzard Does Lean know what a burrito is?

Reid Barton (Apr 01 2020 at 18:40):

This is the original source: https://byorgey.wordpress.com/2009/01/12/abstraction-intuition-and-the-monad-tutorial-fallacy/

Johan Commelin (Apr 01 2020 at 18:40):

You could try proving that those are monads

Kenny Lau (Apr 01 2020 at 18:41):

Johan Commelin said:

https://duckduckgo.com/?t=ffab&q=monad+burrito&atb=v1-1&ia=web

I commend you for using duckduckgo.

Kevin Buzzard (Apr 01 2020 at 18:43):

Reminds me of this

Patrick Massot (Apr 01 2020 at 18:48):

Oh, I remember now. I've met those before, but I forgot.

Anne Baanen (Apr 01 2020 at 20:13):

Today is the perfect day, and this is the perfect thread, to mention Burritos for the hungry mathematician

Kenny Lau (Apr 01 2020 at 20:43):

https://neoeinstein.github.io/monads-are-not-burritos/

Kevin Buzzard (Apr 02 2020 at 08:21):

So it is a theorem in Lean, that what Leo de Moura thinks a monad is, is the same as what Scott Morrison thinks a monad is?

Kevin Buzzard (Apr 02 2020 at 08:23):

Category theory is some weird way for type theory to formally verify programming languages or something.

Johan Commelin (Apr 02 2020 at 08:23):

Kevin Buzzard said:

So it is a theorem in Lean, that what Leo de Moura thinks a monad is, is the same as what Scott Morrison thinks a monad is?

Not sure if this has been done.

Kevin Buzzard (Apr 02 2020 at 08:25):

Why is the Lean term option.monad a monad, Scott Morrison?

Scott Morrison (Apr 02 2020 at 08:27):

One answer is https://github.com/leanprover-community/mathlib/blob/master/src/category_theory/monad/types.lean

Scott Morrison (Apr 02 2020 at 08:27):

Which takes a type-level lawful monad and produces a category theoretic monad.

Scott Morrison (Apr 02 2020 at 08:28):

But we "just" need to understand why option is an algebra object in the monoidal category of endofunctors of Type.

Kevin Buzzard (Apr 02 2020 at 08:36):

Oh wow, so monad has this crazy evolution!

Kevin Buzzard (Apr 02 2020 at 08:39):

Johannes got it into what a computer scientist thought a category was?

Scott Morrison (Apr 02 2020 at 08:44):

If you wanted to prove that option was a monad purely in the category theoretic definition, you would start with:

import category_theory.monad.basic
import category_theory.functorial
import category_theory.types

open category_theory

@[reducible]
def Option := of_type_functor option.{0}

instance monad_Option : monad Option :=
{ η :=
    -- We need to provide `𝟭 Type ⟶ Option`,
    -- i.e. a natural transformation from the identity functor to the Option functor
    -- In components, this just means for each type `α` a morphism from `α` to `option α`.
    -- I can think of two good options, `some` and `none`.
    -- Let's guess `some` is the right answer!
    -- Hopefully the category theoretic automation is good enough we won't need to check naturality.
    { app := λ α x, some x, },
    -- Indeed, the naturality proof was provided "under the hood".
  μ :=
  -- Now we need to provide `Option ⋙ Option ⟶ Option`.
  { app := λ α x,
    begin
      dsimp [Option] at x, dsimp [Option],
      -- There's only one sensible thing to do:
      exact x.get_or_else none,
    end,
    -- Unfortunately, naturality doesn't happen automatically this time!
    naturality' := λ α β f,
    begin
      ext, dsimp,
      cases x,
      -- There appears to be a ridiculous lack of `simp` lemmas about the `option` functor...
      sorry,
      sorry,
    end},
  -- We still need to prove that what we wrote down constituted an algebra in `Type ⥤ Type`:
  left_unit' := sorry,
  right_unit' := sorry,
  assoc' := sorry, }

Scott Morrison (Apr 02 2020 at 08:46):

I've given up there because people have neglected to prove the obvious simp lemmas about the functor and is_lawful_functor instances they biult for option.

Scott Morrison (Apr 02 2020 at 08:46):

Maybe I should have just proved it was a functor by hand, and then the monad proof would be worked automatically.

Kevin Buzzard (Apr 02 2020 at 08:48):

Scott, you look at those proofs and think sigh, I must go and write more automation

Kevin Buzzard (Apr 02 2020 at 08:49):

I think I look at them and say "hey, we are five computer game puzzles away from proving that option is a monad, let's play some computer games"

Scott Morrison (Apr 02 2020 at 08:50):

Oh, actually the reason those proofs were breaking was that I wrote { app := λ α x, none, }, when I'd said in the comment that we were going to write { app := λ α x, some x, },

Kevin Buzzard (Apr 02 2020 at 08:50):

Can you post a fixed version?

Scott Morrison (Apr 02 2020 at 08:51):

Yes. Indeed, if you turn on case bashing then tidy just handles everything:

import category_theory.monad.basic
import category_theory.types

open category_theory

-- We turn on case bashing, to case split on `option` hypotheses.
attribute [tidy] tactic.case_bash

def Option := of_type_functor option.{0}

instance monad_Option : monad Option :=
{ η :=
    -- We need to provide `𝟭 Type ⟶ Option`,
    -- i.e. a natural transformation from the identity functor to the Option functor
    -- In components, this just means for each type `α` a morphism from `α` to `option α`.
    -- I can think of two good options, `some` and `none`.
    -- Let's guess `some` is the right answer!
    -- Hopefully the category theoretic automation is good enough we won't need to check naturality.
    { app := λ α x, some x, },
    -- Indeed, the naturality proof was provided "under the hood".
  μ :=
  -- Now we need to provide `Option ⋙ Option ⟶ Option`.
  { app := λ α x, x.get_or_else none, }, }

Kevin Buzzard (Apr 02 2020 at 08:52):

Option is a monad!

Scott Morrison (Apr 02 2020 at 08:52):

in just three lines, plus comments :-)

Kevin Buzzard (Apr 02 2020 at 08:53):

Now what about the theorem that _root_.monad is a monad?

Kevin Buzzard (Apr 02 2020 at 08:53):

this is so cool

Kevin Buzzard (Apr 02 2020 at 08:53):

Thanks @Shing Tak Lam

Scott Morrison (Apr 02 2020 at 08:54):

@Kevin, what do you mean? That's the proof Johannes wrote that I linked above.

Kevin Buzzard (Apr 02 2020 at 08:54):

I see, so it's all there.

Scott Morrison (Apr 02 2020 at 08:55):

Yes. To prove option is a category-theoretic monad you should of course just combine the fact people have proved it's a computer science monad already, and the generic translation to category-theoretic monads.

Scott Morrison (Apr 02 2020 at 08:56):

The proof I wrote above is just for pedagogy.

Kevin Buzzard (Apr 02 2020 at 11:28):

@Simon Hudon would you ever need to import category_theory.monad.types when you are, say, writing meta code? Do you ever use option.monad? Presumably you use monads? What would happen if they were tagged noncomputable?

Mario Carneiro (Apr 02 2020 at 11:35):

option.monad is used whenever you write opt >>= f where opt : option A

Mario Carneiro (Apr 02 2020 at 11:35):

actually that's not quite correct because there is a has_bind superclass that provides that, but monad gives you other haskelly notations like <*> and *>

Mario Carneiro (Apr 02 2020 at 11:40):

actually monad is basically just the join of other typeclasses, so it doesn't contribute anything new but other functions are written to that interface. So for instance you can't write return a : option A without using option.monad

Mario Carneiro (Apr 02 2020 at 11:41):

but you can write pure a : option A which is the name contributed by applicative (thank you haskell for having not one but two nonintuitive names for the same function), or of course some a : option A

Kevin Buzzard (Apr 02 2020 at 11:48):

I don't have a clue what >>= means. Is this notation commonly used? This is some meta thing, right? :wink:

Kevin Buzzard (Apr 02 2020 at 11:49):

and all the other funny emoticons like <*>?

Mario Carneiro (Apr 02 2020 at 11:49):

a >>= \lam b. f means the same as do b <- a, f, which is how you will normally see it

Mario Carneiro (Apr 02 2020 at 11:50):

actually do notation is just syntax for the former

Kevin Buzzard (Apr 02 2020 at 11:50):

OK so I must confess that I have seen b <- a before.

Kevin Buzzard (Apr 02 2020 at 11:50):

And what would happen if I made it noncomputable? Would anything break?

Mario Carneiro (Apr 02 2020 at 11:50):

yes, everything would break

Kevin Buzzard (Apr 02 2020 at 11:51):

What exactly?

Mario Carneiro (Apr 02 2020 at 11:51):

all tactics

Kevin Buzzard (Apr 02 2020 at 11:51):

All tactics?

Kevin Buzzard (Apr 02 2020 at 11:51):

rofl

Mario Carneiro (Apr 02 2020 at 11:51):

taking away bind is like taking away function composition

Kevin Buzzard (Apr 02 2020 at 11:52):

But what would happen if Scott made his construction noncomputable?

Mario Carneiro (Apr 02 2020 at 11:52):

you can have a function, but only one. two is too many

Mario Carneiro (Apr 02 2020 at 11:52):

That said, category_theory.monad.types has very little impact if any on the lean programmer

Kevin Buzzard (Apr 02 2020 at 11:53):

monad Option is not even the same monad as monad option

Mario Carneiro (Apr 02 2020 at 11:53):

because we don't use category_theory.monad for any of that

Kevin Buzzard (Apr 02 2020 at 11:53):

Hence the two Wikipedia pages I guess

Mario Carneiro (Apr 02 2020 at 11:54):

Also, it should be noted that it is not an exact match (between Leo's monad and Scott's monad in the category of types) because of universe issues

Mario Carneiro (Apr 02 2020 at 11:54):

Leo's monad has two universe parameters, Scott's has one

Kevin Buzzard (Apr 02 2020 at 11:55):

I don't care, I'm into ZFC

Kevin Buzzard (Apr 02 2020 at 11:55):

I know my small category from my large category

Mario Carneiro (Apr 02 2020 at 11:55):

It matters here for more than size reasons

Mario Carneiro (Apr 02 2020 at 11:55):

it's the difference between asking for a function f : X -> Y and f : X -> X

Kevin Buzzard (Apr 02 2020 at 11:56):

Yes but the generic mathematician chooses to ignore these foundational issues

Kevin Buzzard (Apr 02 2020 at 11:56):

We work in Type in Type.

Mario Carneiro (Apr 02 2020 at 11:56):

I'm saying it's more than that

Kevin Buzzard (Apr 02 2020 at 11:56):

We're careful not to press the bad self-destruct button in Type-in-Type.

Mario Carneiro (Apr 02 2020 at 11:56):

Leo's monads literally contain objects that are not monads in Scott's sense because they don't have a multiplication

Mario Carneiro (Apr 02 2020 at 11:57):

they have a bind operator but not a join

Kevin Buzzard (Apr 02 2020 at 11:57):

Oh you're just saying that Johannes proved something about lawful monads?

Mario Carneiro (Apr 02 2020 at 11:57):

which one are we talking about now?

Mario Carneiro (Apr 02 2020 at 11:58):

monad is a predicate on functions F : Type u -> Type v. Crucially, unlike the category theory monad situation, you cannot iterate F

Kevin Buzzard (Apr 02 2020 at 11:58):

So monads are like topoi, the word is used by different people to mean literally different things?

Mario Carneiro (Apr 02 2020 at 11:59):

The definition of category theory monad uses a function mu : F (F X) -> F X which doesn't typecheck

Mario Carneiro (Apr 02 2020 at 11:59):

(mu is also called join in the haskell tradition)

Mario Carneiro (Apr 02 2020 at 12:00):

Instead, the "multiplication operator" is written in a sort of continuation passing style, bind : F A -> (A -> F B) -> F B, which doesn't require iterating F

Mario Carneiro (Apr 02 2020 at 12:02):

The proof that bind and join are equivalent defines join x = bind x id but id doesn't typecheck here because one side is in Type u and the other is in Type v

Mario Carneiro (Apr 02 2020 at 12:07):

I'm not sure how you could capture this in a category theory setting, since it is like you have two categories and some of the arrows in the diagram are spanning both categories

Mario Carneiro (Apr 02 2020 at 12:11):

Perhaps you could go for Kleisli (F : Type u -> Type v) := {obj := Type u, hom := \lam A B, A -> F B} with bind as composition

Mario Carneiro (Apr 02 2020 at 12:12):

and the statement that F is a lawful monad is the same as the claim that this forms a category

Scott Morrison (Apr 02 2020 at 13:31):

Do we know of any monad that intrinsically change universe? (i.e. where you can only define with v \ne u)

Mario Carneiro (Apr 02 2020 at 13:40):

There was a time when io was a universe changing monad, although right now that's not necessary because it is implemented with meta constants

Mario Carneiro (Apr 02 2020 at 13:42):

there is a way to make the collection of all monad_io's a universe changing monad


Last updated: Dec 20 2023 at 11:08 UTC