# 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: May 14 2021 at 04:22 UTC