Zulip Chat Archive

Stream: general

Topic: could meta be a monad


view this post on Zulip Johan Commelin (Oct 14 2018 at 23:38):

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?

view this post on Zulip Simon Hudon (Oct 15 2018 at 02:30):

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

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:26):

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

view this post on Zulip Scott Morrison (Oct 15 2018 at 04:28):

I think you're conflating meta and tactic here.

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:33):

No, I really meant meta.

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:34):

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...

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:34):

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

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:35):

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

view this post on Zulip Simon Hudon (Oct 15 2018 at 04:38):

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

view this post on Zulip Simon Hudon (Oct 15 2018 at 04:39):

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.

view this post on Zulip Simon Hudon (Oct 15 2018 at 04:39):

What gain do you think it would give us?

view this post on Zulip Johan Commelin (Oct 15 2018 at 04:42):

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

view this post on Zulip Simon Hudon (Oct 15 2018 at 04:46):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 05:03):

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

view this post on Zulip Mario Carneiro (Oct 15 2018 at 05:04):

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

view this post on Zulip Gabriel Ebner (Oct 15 2018 at 07:48):

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.

view this post on Zulip Johan Commelin (Oct 15 2018 at 07:53):

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

view this post on Zulip Reid Barton (Oct 19 2018 at 14:20):

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.

view this post on Zulip Reid Barton (Oct 19 2018 at 14:23):

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


Last updated: May 18 2021 at 16:25 UTC