elaboration and unification

Stream: general

[Paul van Wamelen]

Can someone suggest a good reference for learning more about what exactly is meant by 'elaboration' and 'unification'? I have a vague feel for what they are but would like to learn more.

[Kevin Buzzard]

My very vague understanding of what's going on here is that in principle elaboration and unification are just the study of filling in certain kinds of blanks. For example when you apply some theorem of the form a = b to a goal of f x = 37 the elaborator figures out that a is going to be f x and b is going to be 37. However the issue is that sometimes the elaborator has to solve a gigantic logic problem, and how it solves it is very system specific, so now I have to start talking about Lean and because I'm just going from experience rather than reading the C++ code or meta Lean code (neither of which I understand) things will now start to get hazier.

Lean has this attribute system, where you can just stick a "tag" like simp or no_lint docstring or irreducible or even a tag which you made up yourself, onto a definition or theorem. These tags don't change the definition or theorem in any way, but they change the way various internal systems treat the definition or theorem. For example tagging a theorem with simp makes the simplifier aware of it. There are several tags which you can attach to things which change the way Lean elaborates them, for example elab_as_eliminator or elab_simple, and these slightly change the way the (presumably rather complicated) elaborator works when it's trying to fill in all the {} and _ gaps in the term which it's trying to complete. We've seen examples recently where elaboration can fail for all sorts of obscure reasons, and then someone like Mario or Reid or one of the other people who _do_ know what's going on comes along and suggests a very minor tweak and all of a sudden things are working again.

[Paul van Wamelen]

Isn't "figures out that a is going to be f x and b is going to be 37" unification? And elaboration is basically filling in underscores and other stuff that the user didn't supply explicitly?
Are there some settings or traces that can show me what elaboration does?

[Mario Carneiro]

Elaboration is the whole proof script -> proof process, which includes unification, type class inference, and running tactics

[Mario Carneiro]

unification is specifically "A : T needs to have type T' here so T = T' and therefore this and that metavariable can be assigned"

[Heather Macbeth]

Bumping an old thread: What is the best source for learning how elaboration works? For simplicity, let's restrict to contexts in which no typeclasses are involved -- but there are still lambdas, structures, implicit arguments, etc:

import Mathlib

theorem Real.pow_two_pos_of_ne_zero : ∀ {a : ℝ}, a ≠ 0 → 0 < a ^ 2 :=
  @_root_.pow_two_pos_of_ne_zero ℝ _ _
theorem Real.sub_eq_zero : ∀ {a b : ℝ}, a - b = 0 ↔ a = b :=
  @_root_.sub_eq_zero ℝ _

structure Point where
  x : ℝ
  y : ℝ

def f (p : Point) : ℝ := (p.x - p.y) ^ 2

example {p : Point} (hp : p.x ≠ p.y) : f p > 0 :=
  -- how does this proof term get typechecked
  -- (and how are the implicit arguments determined?)
  Real.pow_two_pos_of_ne_zero fun h ↦ hp (Iff.mp Real.sub_eq_zero h)

[Heather Macbeth]

If there's a resource which is about Coq, Haskell, Isabelle, or some simplified teaching language, I think that would be fine for me -- I would like to learn the general principles, not necessarily literally how it is done in Lean.

[Kyle Miller]

In the future it should be the Lean reference manual, but for now I'm not sure. (Yesterday I wrote an explanation of a different elaboration example, in case that's helpful.)

[Heather Macbeth]

By the way, I'm aware of the article Elaboration in Dependent Type Theory which is about Lean 2 -- how far is this from Lean 3/4?

[Kyle Miller]

I'm not sure, but skimming through, (1) for defeq only similarity might be that there's unification, and all the details are probably different, including higher-order unification, which is much much simpler now and (2) now elaboration can postpone many problems until later until more information comes in.

[Heather Macbeth]

OK, so quite far :)

[Kyle Miller]

Here's a slightly simplified explanation of your example:

• We encounter the application Real.pow_two_pos_of_ne_zero fun h ↦ hp (Iff.mp Real.sub_eq_zero h) with expected type f p > 0. We see it has function Real.pow_two_pos_of_ne_zero and positional argument list [fun h ↦ hp (Iff.mp Real.sub_eq_zero h)].
  • We see that the function is a constant. We resolve the constant, getting that it is the theorem Real.pow_two_pos_of_ne_zero whose type is ∀ {a : ℝ}, a ≠ 0 → 0 < a ^ 2. Set expression e to this theorem.
  • We begin processing the parameters to the function one at a time.
    • Parameter {a : ℝ}. This is implicit. We create a fresh metavariable ?a and update e to be e ?a.
    • Parameter (_ : a ≠ 0). This is explicit.
      • Since it is the first explicit parameter, we try using the expected type to propagate type information. We try unifying 0 < ?a ^ 2 =?= f p > 0. This causes > to unfold to 0 < f p, and then this reduces to ?a ^ 2 =?= f p. This causes f to unfold, reducing to ?a ^ 2 =?= (p.x - p.y) ^ 2. This reduces to ?a =?= p.x - p.y, and we ultimately get a solution ?a := p.x - p.y.
      • Now substituting ?a for a in the parameter's type, we know the type of the argument needs to be p.x - p.y ≠ 0.
      • We consume the next positional argument, which is fun h ↦ hp (Iff.mp Real.sub_eq_zero h) and elaborate it with expected type p.x - p.y ≠ 0.
        • The fun elaborator expects the expected type to be a pi type. This causes the expected type to unfold to p.x - p.y = 0 -> False.
        • We create a local variable h of type p.x - p.y = 0 and elaborate hp (Iff.mp Real.sub_eq_zero h) with expected type False. Skipping these details... this happens, yielding an expression e'. We then abstract h out of e' and create a function expression fun h : p.x - p.y = 0 => e' (where this e' here is referring to the bvar h instead of the fvar h). Call this function expression arg.
      • With the positional argument elaborated as some expression arg, we update e to be e arg.
    • There are no more parameters.
  • Now we finalize the application. The result is the value of e, which is @Real.pow_two_pos_of_ne_zero (p.x - p.y) arg.

[Heather Macbeth]

This is really helpful. Thank you, Kyle!

[Heather Macbeth]

I would still be very happy to receive recommendations for "general reading", if anyone has them. I've started reading the Elaboration in Dependent Type Theory article and this is also useful so far.

[Heather Macbeth]

By the way, what part of the lean4 codebase handles this? I'm pretty sure reading this code is above my paygrade, but even so I would like to take a look.

[Edward van de Meent]

Kyle Miller said:

Here's a slightly simplified explanation of your example:

that's very insightful. i'd love to be able to read more details about what kind of problems can or need to be postponed when...

[Kyle Miller]

The most pervasive one is typeclass instances. It tries to synthesize immediately, but if it's able to blame a failure on metavariables, it'll put it into a work list for later.

Another is by notation. If the expected type has metavariables, it again puts itself onto a work list for later.

[Kyle Miller]

if c then a else b notation postpones if c's type is a(n application of a) metavariable.

[Kyle Miller]

Custom elaborators can decide to postpone if they decide there isn't enough information to continue yet. Eventually they'll be forced to decide to continue anyway (like what by does) or throw an error (like what @[elab_as_elim] does).

[Yaël Dillies]

Thanks Kyle. Here goes an apology to all the times I've called Lean names for being too slow :snail:

[Daniel Weber]

You can also enable tracing for elaboration (set_option trace.Elab true doesn't work, but enabling trace.Elab.app and trace.Elab.step seems to work ok), and for unification (set_option trace.Meta.isDefEq true) to get an idea of what's going on in specific instances

[Craig McLaughlin]

Heather Macbeth said:

I would still be very happy to receive recommendations for "general reading", if anyone has them. I've started reading the Elaboration in Dependent Type Theory article and this is also useful so far.

For general reading, I can recommend Adam Gundry's PhD dissertation on "Type Inference, Haskell and Dependent Types" and available on his website. I like his presentation because it starts simply: unification for a Hindley-Milner type system (just lambdas, variables and let-generalisation), makes a connection to elaboration and builds incrementally to the dependently typed setting. For his reconstruction of HM type inference alone, I am often returning to the relevant chapters.

I would also be interested in additional resources on the topic. I can't recall any other relatively self-contained account of elaboration, type inference, and unification.

[Heather Macbeth]

Thank you! I'll check it out.