could meta be a monad

Stream: general

[Johan Commelin]

Something that popped into my head recently, and my curiosity makes me ask this question:
Could meta have been a monad?
In Haskell, there is the IO monad that marks functions "unsafe" (i.e., they can have side effects). I could imagine that meta could also be a monad that marks functions "unsafe" (i.e., they are meta). Would this work? What would be the pros and cons?

[Simon Hudon]

Do you mean tactic? It's already a monad.

[Johan Commelin]

No, I meant what I wrote. [Edit: misinterpreted Simon's answer.]

[Scott Morrison]

I think you're conflating meta and tactic here.

[Johan Commelin]

No, I really meant meta.

[Johan Commelin]

If I have a trusted piece of code, I could wrap it into the "meta" tactic, and it would no longer be trusted, etc, etc...

[Johan Commelin]

Or does @Simon Hudon mean that tactic is already a monad. I see. Yes, that I knew.

[Johan Commelin]

So I repeat my question: Could meta be a monad?

[Simon Hudon]

Ok so instead of having a keyword meta, you'd have a meta monad which would enable unbounded recursion and access to the prover's internals

[Simon Hudon]

I know that they want more parts of the tactics framework to be in pure code for Lean 4 but I don't know if everything can go there.

[Simon Hudon]

What gain do you think it would give us?

[Johan Commelin]

Like I said in my first post: just curiosity. I don't know anything about theoretical pros and cons.

[Simon Hudon]

I think at the moment, pure code doesn't allow unbounded recursion yet but that could be added too. I can't think of other reasons to not write all meta code as pure code

[Mario Carneiro]

I think the best analogue here is actually the io monad of lean

[Mario Carneiro]

it is non-meta, but you can do lots of external manipulation stuff and unbounded recursion

[Gabriel Ebner]

Could meta have been a monad?

Yes, instead of the meta keyword we could have a meta monad as follows:

def «meta» : Type u → Type u
| α := false → α

I think you can derive all features of the current meta in this monad, including undefined and general recursion. But I'm not sure how helpful it would be.

[Johan Commelin]

I'm not sure if it is helpful. But I do find it funny.

[Reid Barton]

Encoding a type of effect as a monad has various generic disadvantages, including:

• You need different syntaxes to form the application f x depending on whether each of f or x is a monadic value or an ordinary value (here: meta or not).
• You need to specify an order of effects, which forces you to linearize your program to a certain extent, whereas a pure program can have a tree structure.
• If you want to use a second monad as well (say the list monad), now you need to figure out some way to combine the second monad with your effect monad (using something like monad transformers perhaps).

In some contexts these points could be viewed as advantages, but the effect of nontermination is so mild that that doesn't apply here. For example, if x and y are possibly nonterminating computations, then computing x and then y is the same as computing y and then x.

[Reid Barton]

The only advantage of meta as a monad that I can think of is on the implementation side: Lean would no longer have to track the meta property. However, I think there would still be special cases required to reproduce the current behavior, e.g., meta inductive types have a relaxed syntax for recursion--Lean would have to make the constructors and/or recursors operate in the meta monad