monadic merge

Stream: general

[Patrick Massot]

The monad refactoring PR was merged! Congratulations @Sebastian Ullrich !

[Patrick Massot]

You can give us Lean 4 now :wink:

[Sebastian Ullrich]

Breaking every existing monad instance with that merge should provide a small taste of Lean 4 :stuck_out_tongue:

[Simon Hudon]

I have a sense you may experience what the Haskell implementers experienced. The Haskell users act like addicts when breaking change occurs. Instead of yelling "You bastards! You broke my code" they say "Amazing! Where's the rest?"

[Patrick Massot]

Are there existing monad instances? Besides the tactic monad of course (you didn't break that one, did you?)

[Moses Schönfinkel]

list had better be a monad

[Patrick Massot]

And the IO monad that is used by leanpkg

[Patrick Massot]

I'm sure you also didn't break that one

[Patrick Massot]

Come on, Leo wouldn't merge a Lean branch with broken list

[Moses Schönfinkel]

option had better be a monad

[Simon Hudon]

There's also state and option I believe

[Moses Schönfinkel]

let's try #print instances monad

[Moses Schönfinkel]

native.resultT_monad : Π {M : Type → Type} [m : monad M] (E : Type), monad (native.resultT M E)
native.result_monad : Π (E : Type), monad (native.result E)
list.monad : monad list
smt_tactic.monad : monad smt_tactic
vm_core.monad : monad vm_core
option_t.monad : Π {m : Type u → Type v} [_inst_1 : monad m], monad (option_t m)
conv.monad : monad conv
monad.transformed_monad : Π (m : Type → Type u_1) (t : Π (m : Type → Type u_1) [_inst_1 : monad m], Type → Type)
[_inst_1 : monad.monad_transformer t] [_inst_2 : monad m], monad (t m)
state_t.monad : Π (σ : Type u) (m : Type u → Type v) [_inst_1 : monad m], monad (state_t σ m)
state.monad : Π (σ : Type u), monad (state σ)
option.monad : monad option
task.monad : monad task
interaction_monad.monad : Π {state : Type}, monad (interaction_monad state)
exceptional.monad : monad exceptional
monad_fail.to_monad : Π (m : Type u → Type v) [c : monad_fail m], monad m

[Sebastian Ullrich]

I meant instances outside of core

[Patrick Massot]

Are there any in mathlib? My limited understanding is that monads are important in core or for people doing programming in Lean, but not for mathematicians

[Kevin Buzzard]

I guess I use the tactic monad...

[Patrick Massot]

Sure, but this one is not broken

[Kevin Buzzard]

...and the occasional list...

[Patrick Massot]

also not broken

[Mario Carneiro]

computation, roption, pfun, seq, wseq, filter

[Patrick Massot]

Are these names of monads in mathlib?

[Patrick Massot]

Is mathlib currently broken?

[Mario Carneiro]

probably, haven't had time to check

[Mario Carneiro]

seems very unlikely that sebastian's huge merge didn't break mathlib

[Mario Carneiro]

@Sebastian Ullrich What happened to the proofs of is_lawful_functor option?

[Mario Carneiro]

Oh, found it - init.data.option.instances. This is the first time I've seen a file in init import namespace which is not imported by default. Was that deliberate?

[Sebastian Ullrich]

No, definitely not. Thanks for noticing.

[Sebastian Ullrich]

We should have some noticing tool for that :)

[Kevin Buzzard]

Looks like you do :-)

[Sebastian Ullrich]

@Mario Carneiro fixed

[Mario Carneiro]

mathlib should now be fixed, although I built against sebastian's commit which won't appear until tomorrow's nightly build