option is a monad

Stream: general

[Kevin Buzzard]

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]

Yes

[Reid Barton]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

this has got a bit out of hand.

[Reid Barton]

The category_theory monad would look more like what you expect

[Kevin Buzzard]

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

[Reid Barton]

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

[Kevin Buzzard]

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

[Jasmin Blanchette]

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

[Jasmin Blanchette]

To avoid all that stuff.

[Jasmin Blanchette]

Two fields, three proofs.

[Patrick Massot]

What's with the burrito?

[Kevin Buzzard]

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

[Johan Commelin]

Seriously?

[Johan Commelin]

@Patrick Massot Search for monad and burrito

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

@Kevin Buzzard Does Lean know what a burrito is?

[Reid Barton]

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

[Johan Commelin]

You could try proving that those are monads

[Kenny Lau]

Johan Commelin said:

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

I commend you for using duckduckgo.

[Kevin Buzzard]

Reminds me of this

@wilshipley git gets easier once you get the basic idea that branches are homeomorphic endofunctors mapping submanifolds of a Hilbert space.

- Isaac Wolkerstorfer (@agnoster)

[Patrick Massot]

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

[Anne Baanen]

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

[Kenny Lau]

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

[Kevin Buzzard]

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]

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

[Johan Commelin]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Kevin Buzzard]

Oh wow, so monad has this crazy evolution!

[Kevin Buzzard]

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

[Scott Morrison]

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]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

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]

Can you post a fixed version?

[Scott Morrison]

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]

Option is a monad!

[Scott Morrison]

in just three lines, plus comments :-)

[Kevin Buzzard]

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

[Kevin Buzzard]

this is so cool

[Kevin Buzzard]

Thanks @Shing Tak Lam

[Scott Morrison]

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

[Kevin Buzzard]

I see, so it's all there.

[Scott Morrison]

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]

The proof I wrote above is just for pedagogy.

[Kevin Buzzard]

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

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

[Mario Carneiro]

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]

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]

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]

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

[Kevin Buzzard]

and all the other funny emoticons like <*>?

[Mario Carneiro]

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

[Mario Carneiro]

actually do notation is just syntax for the former

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Mario Carneiro]

yes, everything would break

[Kevin Buzzard]

What exactly?

[Mario Carneiro]

all tactics

[Kevin Buzzard]

All tactics?

[Kevin Buzzard]

rofl

[Mario Carneiro]

taking away bind is like taking away function composition

[Kevin Buzzard]

But what would happen if Scott made his construction noncomputable?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Kevin Buzzard]

monad Option is not even the same monad as monad option

[Mario Carneiro]

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

[Kevin Buzzard]

Hence the two Wikipedia pages I guess

[Mario Carneiro]

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]

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

[Kevin Buzzard]

I don't care, I'm into ZFC

[Kevin Buzzard]

I know my small category from my large category

[Mario Carneiro]

It matters here for more than size reasons

[Mario Carneiro]

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

[Kevin Buzzard]

Yes but the generic mathematician chooses to ignore these foundational issues

[Kevin Buzzard]

We work in Type in Type.

[Mario Carneiro]

I'm saying it's more than that

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

they have a bind operator but not a join

[Kevin Buzzard]

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

[Mario Carneiro]

which one are we talking about now?

[Mario Carneiro]

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

[Kevin Buzzard]

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

[Mario Carneiro]

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

[Mario Carneiro]

(mu is also called join in the haskell tradition)

[Mario Carneiro]

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]

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]

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]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

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]

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