Expr.mdata

Stream: lean4

[Dan Velleman]

Can someone explain what Expr.mdata is for? Here's a silly example:

elab "traceGoal" : tactic => do
  let g ← getMainTarget
  dbg_trace g

example (p q : Prop) (h : p ∧ q) : p → q := by
  traceGoal
  have h2 : q := h.right
  traceGoal

The two calls to traceGoal reveal that initially, the goal is _uniq.45324 -> _uniq.45325, but after the use of have it is [mdata noImplicitLambda:1 _uniq.45324 -> _uniq.45325]. What happened?

The reason for my interest is that I want to write tactics that decide what to do based on the form of the goal. If the goal has the form Expr.mdata m e d, then I guess I need to look inside e to see what the form of the goal is. It is easy enough to do that using something like this:

def stripMData (e : Expr) : Expr :=
  match e with
    | Expr.mdata _ e _ => stripMData e
    | _ => e

But is that a good idea? If I remove all of the mdata to get at the underlying expression, am I going to get myself in trouble somehow? I'm reluctant to throw away the mdata without knowing what it is.

[Alex Keizer]

I'm not sure what mdata is, but have you had a look at whnf? It stands for weak head normal form and if you want to match on expressions you probably want to normalise them first. I suspect whnf might get rid of the mdata for you.

[Alexander Bentkamp]

If whnf doesn't do it, there is also Expr.consumeMData.

[Jannis Limperg]

mdata is a mechanism for attaching arbitrary metadata to expressions. It's used for a number of things (e.g. better pretty-printing if I recall correctly), but it should never be semantically relevant, so you can remove it if you need to. If you construct an expression that's derived from an existing expression, it may be nice to preserve mdata, but my impression is that Lean itself doesn't do this consistently.

[Dan Velleman]

I'm still unclear on when it is necessary to call consumeMData. For example, here's the definition of Expr.getAppFn:

def getAppFn : Expr -> Expr
  | app f _ => getAppFn f
  | e             => e

Why isn't it:

def getAppFn : Expr -> Expr
  | app f _ => getAppFn (consumeMData f)
  | e            => e

How do we know f doesn't have mdata associated with it?

[Jannis Limperg]

I agree that your definition would likely be better for most purposes. Maybe the Lean devs would even consider this a bug, or maybe they use this function in ways that are supposed to be sensitive to mdata. Other functions have primed versions which ignore mdata, e.g. isAppOfArity'.

[Gabriel Ebner]

Maybe we need a "what are mdata used for" document, because these are quite mysterious (and also very well hidden). Some prominent applications:

1. show X from y is encoded as .mdata (KVMap.empty.setBool `let_fun true) (.app (.lam _ X (.var 0) y). Here mdata is used to create a "custom expression constructor", if you will.
2. Tags like noindex or @& are stored as annotations.
3. You can annotate an expression with pretty-printing options using mdata. Check out Expr.setPPExplicit and co.

My general feeling is: only strip mdata if you're beta-reducing as well.

[Alex Keizer]

I just wanted to add a note that I just spent some time being very confused why getAppFn was returning an expression like Foo x y, where I was expecting it to give me Foo. Turns out, my original expression actually had some mdata [mdata _inaccessible:1 Foo _uniq.17084 _uniq.17086]. What is the danger of stripping this mdata in getAppFn?

[Scott Morrison]

Because then the mdata would not be there for the people who need it. Unfortunately the mdata design requires everyone to participate in transporting it along, unless you are certain you are the only consumer of the Exprs you are processing.

[Kyle Miller]

std has docs#Lean.Expr.getAppFn' and docs#Lean.Expr.getAppArgs' if you know you want to ignore metadata

[Kyle Miller]

I use metadata in the implementation mathlib's congruence quotations partly to make sure that when you do getAppFn you don't accidentally separate a certain function (cHole) from its arguments. Normally it's impossible to tell where one function application ends and the next begins (they're all Expr.apps after all), but mdata is one way to insert delimiters.