monad puzzle

Stream: mathlib4

[Patrick Massot]

Warning: there is no question in this post, this is only for fun. For people who like monads and know Mathlib, consider the following code:

import Lean
import Mathlib

open Lean

def foo : Nat → Option Nat
| 0 => some 0
| _ => none

def bar (n : Nat) : MetaM (Option Nat) := do
  return ← foo n

Removing the import Mathlib line will make it fail. Challenge: without using Lean, guess what is the minimal file to import to make it work again.

[Patrick Massot]

If this is too difficult you can then try using Lean.

[Patrick Massot]

answer

Tactic.NormNum.Basic

[Patrick Massot]

@Mario Carneiro may enjoy this puzzle for instance.

[Patrick Massot]

Bonus question: without running it, #eval bar 1 in your head.

[Patrick Massot]

answer

failed

[Mario Carneiro]

answer

it looks like a type error, in that foo n is an Option Nat but you are using <- with it to make a MetaM

So whether this works depends on whether there is a monadLift instance

and my guess is that mathlib somewhere decides that there is such a monad lift instance for any Alternative m

so the answer to the bonus question is probably failed

and the minimal file will be something in Mathlib.Control if we're lucky and in some random number theory file if we are unlucky

[Mario Carneiro]

..oof, it looks like my code is the one at fault

[Patrick Massot]

I guess you should have put all your messages behind spoiler tags. But you can now look at the answers.

[Patrick Massot]

I would say this is a minor foot gun.

[Mario Carneiro]

yeah, that code should have been a local instance

[Mario Carneiro]

although TBH it's not unreasonable as a global instance, it's just poorly placed

[Patrick Massot]

I was not expecting the answer to the bonus question when writing code in my teaching library.

[Mario Carneiro]

I think the footgun here is distributed across two features, both individually reasonable:

• Option A -> M A should be a coercion / monad lift instance when M is an alternative monad
• A -> Option A should be a coercion via some

[Mario Carneiro]

the result is that when you have M (Option A) there isn't a lot lean can do to help detect errors when you send none the wrong direction

[Mario Carneiro]

since depending on the context both pure none and failure are reasonable answers

[Patrick Massot]

I was not expecting the first one. When I want this behavior I write let some x := y | throwError ….

[Mario Carneiro]

I think that behavior is also related to the sentiment of "Option should not be a monad"

[Mario Carneiro]

i.e. Option is just for data and if you want control flow you should use OptionM

[Mario Carneiro]

Actually, the original issue comes up in general when you have M A and want M (M A)

[Mario Carneiro]

but at least pure isn't a coercion (anymore...) so there is less damage

[Patrick Massot]

Note that I don’t have strong feelings here. The main point of this thread is still the game at the beginning.

[Damiano Testa]

Btw, this seems to be the same thing that confused me as well.

[Jovan Gerbscheid]

Patrick Massot said:

I was not expecting the first one. When I want this behavior I write let some x := y | throwError ….

I agree with this, and I'm generally not a fan of the Alternative instance of MetaM. I think it is better to give names to errors instead of having it throw "failure" through the alternative instance.

[Thomas Murrills]

It took a little while for me to learn that seeing just failed at the tactic level likely meant some guard failing in MetaM.

But guards are useful. I'd be curious to know how often the Alternative MetaM instance is used. If it's too useful to abandon, it'd be nice for the instance to throw some information about the MetaM state instead of the string failed—or at the very least for it to express the fact that this was specifically a MetaM failure.

[Thomas Murrills]

(As an example of its use: the failed you see from a failed solve_by_elim is from the MetaM Alternative instance!)

[Jovan Gerbscheid]

I don't really see the need for guard condition in MetaM, when you can just write unless condition do throwError "failed". The latter forces the user to give an error message that will most likely be more useful than "failed".

[Jovan Gerbscheid]

In the case of solve_by_elim, wouldn't it be nicer if it said something more specific, like "solve_by_elim failed to close the goal" or something like that?

[Thomas Murrills]

Definitely! I merely meant to show that it's not uncommon to see it used. (Though, as it happens, solve_by_elim is implemented in terms of something that takes in an arbitrary monad with an Alternative instance—this part might actually be unusual.)

[Thomas Murrills]

Though, firstM also depends on an Alternative instance, and that's pretty useful—as is failing while checking many conditions in try/catch blocks, where the error simply won't propagate up to the user.

[Thomas Murrills]

I agree that it's a bad error message, but I'd be reluctant to give up all of the functionality built on Alternative in MetaM. I wonder if there's a way to prevent it from bubbling to the surface somehow while allowing internal use.