Zulip Chat Archive

Stream: general

Topic: monadic merge


Patrick Massot (Mar 20 2018 at 22:19):

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

Patrick Massot (Mar 20 2018 at 22:19):

You can give us Lean 4 now :wink:

Sebastian Ullrich (Mar 20 2018 at 22:25):

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

Simon Hudon (Mar 20 2018 at 22:29):

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 (Mar 20 2018 at 22:31):

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

Moses Schönfinkel (Mar 20 2018 at 22:31):

list had better be a monad

Patrick Massot (Mar 20 2018 at 22:31):

And the IO monad that is used by leanpkg

Patrick Massot (Mar 20 2018 at 22:31):

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

Patrick Massot (Mar 20 2018 at 22:32):

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

Moses Schönfinkel (Mar 20 2018 at 22:32):

option had better be a monad

Simon Hudon (Mar 20 2018 at 22:32):

There's also state and option I believe

Moses Schönfinkel (Mar 20 2018 at 22:32):

let's try #print instances monad

Moses Schönfinkel (Mar 20 2018 at 22:33):

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 (Mar 21 2018 at 09:01):

I meant instances outside of core

Patrick Massot (Mar 21 2018 at 09:58):

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 (Mar 21 2018 at 10:02):

I guess I use the tactic monad...

Patrick Massot (Mar 21 2018 at 10:03):

Sure, but this one is not broken

Kevin Buzzard (Mar 21 2018 at 10:03):

...and the occasional list...

Patrick Massot (Mar 21 2018 at 10:06):

also not broken

Mario Carneiro (Mar 21 2018 at 10:08):

computation, roption, pfun, seq, wseq, filter

Patrick Massot (Mar 21 2018 at 10:08):

Are these names of monads in mathlib?

Patrick Massot (Mar 21 2018 at 10:08):

Is mathlib currently broken?

Mario Carneiro (Mar 21 2018 at 10:09):

probably, haven't had time to check

Mario Carneiro (Mar 21 2018 at 10:09):

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

Mario Carneiro (Mar 21 2018 at 22:35):

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

Mario Carneiro (Mar 21 2018 at 22:52):

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 (Mar 21 2018 at 23:03):

No, definitely not. Thanks for noticing.

Sebastian Ullrich (Mar 21 2018 at 23:03):

We should have some noticing tool for that :)

Kevin Buzzard (Mar 21 2018 at 23:05):

Looks like you do :-)

Sebastian Ullrich (Mar 21 2018 at 23:25):

@Mario Carneiro fixed

Mario Carneiro (Mar 22 2018 at 00:50):

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


Last updated: Dec 20 2023 at 11:08 UTC