Zulip Chat Archive

Stream: general

Topic: monadic merge


view this post on Zulip Patrick Massot (Mar 20 2018 at 22:19):

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

view this post on Zulip Patrick Massot (Mar 20 2018 at 22:19):

You can give us Lean 4 now :wink:

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

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

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

view this post on Zulip Moses Schönfinkel (Mar 20 2018 at 22:31):

list had better be a monad

view this post on Zulip Patrick Massot (Mar 20 2018 at 22:31):

And the IO monad that is used by leanpkg

view this post on Zulip Patrick Massot (Mar 20 2018 at 22:31):

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

view this post on Zulip Patrick Massot (Mar 20 2018 at 22:32):

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

view this post on Zulip Moses Schönfinkel (Mar 20 2018 at 22:32):

option had better be a monad

view this post on Zulip Simon Hudon (Mar 20 2018 at 22:32):

There's also state and option I believe

view this post on Zulip Moses Schönfinkel (Mar 20 2018 at 22:32):

let's try #print instances monad

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

view this post on Zulip Sebastian Ullrich (Mar 21 2018 at 09:01):

I meant instances outside of core

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

view this post on Zulip Kevin Buzzard (Mar 21 2018 at 10:02):

I guess I use the tactic monad...

view this post on Zulip Patrick Massot (Mar 21 2018 at 10:03):

Sure, but this one is not broken

view this post on Zulip Kevin Buzzard (Mar 21 2018 at 10:03):

...and the occasional list...

view this post on Zulip Patrick Massot (Mar 21 2018 at 10:06):

also not broken

view this post on Zulip Mario Carneiro (Mar 21 2018 at 10:08):

computation, roption, pfun, seq, wseq, filter

view this post on Zulip Patrick Massot (Mar 21 2018 at 10:08):

Are these names of monads in mathlib?

view this post on Zulip Patrick Massot (Mar 21 2018 at 10:08):

Is mathlib currently broken?

view this post on Zulip Mario Carneiro (Mar 21 2018 at 10:09):

probably, haven't had time to check

view this post on Zulip Mario Carneiro (Mar 21 2018 at 10:09):

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

view this post on Zulip Mario Carneiro (Mar 21 2018 at 22:35):

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

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

view this post on Zulip Sebastian Ullrich (Mar 21 2018 at 23:03):

No, definitely not. Thanks for noticing.

view this post on Zulip Sebastian Ullrich (Mar 21 2018 at 23:03):

We should have some noticing tool for that :)

view this post on Zulip Kevin Buzzard (Mar 21 2018 at 23:05):

Looks like you do :-)

view this post on Zulip Sebastian Ullrich (Mar 21 2018 at 23:25):

@Mario Carneiro fixed

view this post on Zulip 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: May 14 2021 at 04:22 UTC