T vs. by exact T

Stream: new members

[Jason Reed]

Naively, I would have assumed by exact T would be interchangeable with T for any term T.

However, searching around in Lean Std, I find things like "NB: Postponement through by exact is the entire point of this macro" and I notice in the definition of TreeMap.ofArray, the cmp argument is default (cmp : α → α → Ordering := by exact compare), which appears to be a deliberate choice. I also found this archived zulip thread discussing "by-exact postponement" somewhat.

More concretely, I see in examples like

class Klass (α : Type) where
  meth : α

open Klass

instance : Klass String where
  meth := "foo"


structure Foo.{u} (α : Type u) (wit : α) where

def good1 : Foo String (         meth) := Foo.mk (wit :=          meth)

def good2 : Foo String (by exact meth) := Foo.mk (wit :=          meth)

def bad_1 : Foo String (by exact meth) := Foo.mk (wit := by exact meth)

def bad_2 : Foo String (         meth) := Foo.mk (wit := by exact meth)

the goods typecheck and the bads have "typeclass instance is stuck" errors, and

import Std.Data.TreeMap

def Label := String deriving BEq, Ord

def good : Std.TreeMap Label (Array Nat) := (Std.TreeMap.ofArray
  #[ ("name", #[  ]) ] (compare))

def bad : Std.TreeMap Label (Array Nat) := (Std.TreeMap.ofArray
  #[ ("name", #[  ]) ] (by exact compare))

leads to actual type mismatch errors. This is coming from an example @Rob Simmons showed me that led to this after I tried minimizing it.

I dimly perceive that by exact is somehow reordering some steps of elaboration; is this summarized or documented in more detail somewhere that I should be looking?

[Aaron Liu]

by delays elaboration of the tactic as much as possible, so that when you see the tactic state there won't be random metavariables there. As a side effect, if you want to delay elaboration of a particular term then by exact works pretty well.

[Jason Reed]

Can you drill into why

class Klass (α : Type) where
  meth : α

open Klass

instance : Klass String where
  meth := "foo"

structure Foo.{u} (α : Type u) (wit : α) where

def bad := (Foo.mk (wit := by exact meth) : Foo String meth)

doesn't work, then? Is the type ascription simply too "late" in elaboration to propagate the String into the required type of exact meth? I see the expected type if I replace by exact meth with by sorry as a free metavariable.

[Aaron Liu]

Can you pinpoint what you need explained?

[Jason Reed]

Sorry, I hit 'enter' instead of 'shift-enter' there

[Jason Reed]

If the answer is it tries to delay it "as much as possible" but, given the design of elaboration, what I'm asking for is more than what is possible, then I'd be totally satisfied.

[Aaron Liu]

I'm guessing the expected type isn't taken into account when elaborating an application with the (arg := val) syntax

[Jason Reed]

Ok, I think I find that satisfying enough as an explanation as well.

[Jason Reed]

I worry a bit there is still a repeatable footgun lurking here, e.g.

import Std.Data.TreeMap

def Label := String deriving BEq, Ord

-- This is a type mismatch, because the invisible 'by exact compare'
-- can't instantiate Compare where the type variable is a metavariable
def bad : Std.TreeMap Label (Array Nat) := (Std.TreeMap.ofArray
  #[ ("name", #[  ]) ])

-- But making the default argument explicit fixes it
def good : Std.TreeMap Label (Array Nat) := (Std.TreeMap.ofArray
  #[ ("name", #[  ]) ] compare)

for end users who never actually said by exact, because the default cmp argument of Std.TreeMap for example (and there are some other examples in Std and Mathlib that I found just grepping around) causes it to appear

[Jason Reed]

(This in fact just came up because @Rob Simmons encountered this problem in the wild and we were both puzzled by it for a bit)

[Kyle Miller]

Aaron Liu said:

I'm guessing the expected type isn't taken into account when elaborating an application with the (arg := val) syntax

It's still taken into account.

Expected type propagation only happens at the first explicit argument, and Foo.mk has no explicit arguments.

[Kyle Miller]

Jason Reed said:

I notice in the definition of TreeMap.ofArray, the cmp argument is default (cmp : α → α → Ordering := by exact compare), which appears to be a deliberate choice.

The reason here is that := compare doesn't work, since there's no Ord instance passed to Std.TreeMap.ofArray, which compare needs.

Jason Reed said:

Can you drill into why

I'm not sure exactly why the first works and the second doesn't:

def good : Foo String meth := Foo.mk (wit := meth)
def bad : Foo String meth := Foo.mk (wit := by exact meth)

I'm guessing it's something to do with by exact meth immediately creating a synthetic opaque metavariable ?m.2, which can't unify with meth, so Foo String meth can't unify with Foo ?m.1 ?m.2, so α is still unknown by the time by exact meth is forced to evaluate.

[Kyle Miller]

Oh, yeah, that's why. If we add a unification hint to allow partial unification of Foo, then it goes through.

unif_hint (α α' : Type u) (wit : α) (wit' : α') where
  α =?= α'
  ⊢ Foo α wit =?= Foo α' wit'

def now_good : Foo String meth := Foo.mk (wit := by exact meth)

[Jason Reed]

Interesting! Thanks for the explanation. I'll have to read up on unif_hint then.

[Kyle Miller]

Maybe you don't need to read too much about it, but it's good to know about!

Here's what you need to know: this tells unification to try doing the unifications above the ⊢ if the one after ⊢ is currently failing.

[Jason Reed]

I am someone who has done proof assistant implementation in the past, in addition to being a normal Lean user who wants to do math in Lean, so gnarly details about unification mechanisms are interesting :)

[Kyle Miller]

I'm pretty sure my unification hint is a bad one (what's above the turnstile should cause what's below to be a defeq), but at least it helps prove the hypothesis.

https://github.com/leanprover/lean4/blob/e2e36087e1ff1c29043ded4949862d5da7a8cf4a/src/Lean/Meta/ExprDefEq.lean#L1862 is when they're applied, for reference.

[Rob Simmons]

To make concrete what @Jason Reed called a "repeatable footgun" and which I keep running into, this is basically the situation I'm finding myself in:

import Std.Data.TreeMap
inductive Typ where | Int : Typ | Str : Typ
def Schema := Std.TreeMap String Typ
def Example : Schema :=
  Std.TreeMap.ofArray #[
    ("Name", Typ.Str),
    ("Age", Typ.Int)
  ]

It's super unmotivated that this doesn't work! But it seems like (and I think the FP in Lean book is backing me up here) the right solution wasn't discussed here, and it's that the cosmetic Schema definition should be an abbrev instead:

import Std.Data.TreeMap
inductive Typ where | Int : Typ | Str : Typ
abbrev Schema := Std.TreeMap String Typ
def Example : Schema :=
  Std.TreeMap.ofArray #[
    ("Name", Typ.Str),
    ("Age", Typ.Int)
  ]

@Jason Reed , how much do you remember the problems that led Twelf to have an #abbrev decl? Because I wonder if it's similar. How possible might it be to detect this footgun and error/warn the user about it, pointing them towards abbrev instead of def?

[Kyle Miller]

I might want to upgrade this from "footgun" to "elaboration bug" (or "library bug" due to missing language features).

It's either from functions like Std.TreeMap.ofArray using this := by exact compare auto-param scheme, which isn't friendly for unification due to the kinds of metavariables tactic goals use (synthetic opaque) or its from the way the expected type is propagated, or both.

[Kyle Miller]

(@Paul Reichert Maybe you want to take a look at this? I can see why the library uses auto-params, since it means you can pass a cmp argument, which is more convenient than using Ord instances, but on the flip side since it's a tactic it seems like it's not really possible to solve for by unification.)

[Kyle Miller]

@Rob Simmons A workaround, rather than using an abbrev Schema (correct me if I'm wrong, but I believe that's where you intended to add abbrev), you can use a (cmp := _) named argument to disable the auto-param and let it be solved for by unification.

import Std.Data.TreeMap
inductive Typ where | Int : Typ | Str : Typ
def Schema := Std.TreeMap String Typ
def Example : Schema :=
  Std.TreeMap.ofArray (cmp := _) #[
    ("Name", Typ.Str),
    ("Age", Typ.Int)
  ]

[Rob Simmons]

@Kyle Miller yes whoops put the abbrev in the wrong place in the "this works" example (I've now edited it)

[Rob Simmons]

For the purpose of my example abbrev clearly seems like the "introduces fewer unusual concepts" solution, but it's useful to know about the cmp := _ method of, in effect, re-ordering arguments.

[Rob Simmons]

I guess Ord... or, something else... is the approach I'd expect to see here — seems like you could cause some pretty severe shenagians by forming a tree with one compare function and then looking up in it with another compare function oh, I think I'm understanding what the dependent types are doing here a bit better now — seems like that won't work

[Kyle Miller]

Rob Simmons said:

in effect, re-ordering arguments.

This isn't what's going on here to be clear. I can equally have written

  Std.TreeMap.ofArray #[
    ("Name", Typ.Str),
    ("Age", Typ.Int)
  ] _

The point is that since I'm specifying the argument myself as _, it's the kind of metavariable that can be solved for by unification. The by exact compare creates a metavariable that's "synthetic opaque" and can't be solved for by unification. You can check that

  Std.TreeMap.ofArray #[
    ("Name", Typ.Str),
    ("Age", Typ.Int)
  ] (by exact compare)

fails in the same way.

[Kyle Miller]

Rob Simmons said:

For the purpose of my example abbrev clearly seems like the "introduces fewer unusual concepts" solution

I'm finding the fact that abbrev works here to be somewhat mysterious. I'm guessing it's letting expected type propagation to solve for the cmp argument and then the auto-param doesn't get triggered... but I'm not sure, I'd have to check the elaboration code more carefully.

Named arguments are not an unusual concept, and you can switch between using positional and named arguments without changing anything about elaboration.

[Rob Simmons]

@Kyle Miller The rule that I'm gleaning from the linked "FP in lean" lesson is "you can't assume that def obeys the property of substitution/inlining, but abbrev has this property" — are there cases where abbrev definitions _don't_ obey substitution? I'd find that more surprising.

[Kyle Miller]

When typechecking/unifying, defs can be unfolded, and I think I'd expect it to be unfolded here when propagating the expected type.

[Kyle Miller]

That said, I don't see expected type propagation happening at all either for def or abbrev, according to the output of set_option trace.Elab.app.propagateExpectedType true.

[Rob Simmons]

interesting... still learning here, will keep the question "what does abbrev mean if it's not syntactic substitution/inlining" in my head as I learn

[Kyle Miller]

Sorry, I implicitly answered your question by not saying anything about abbrev. It creates a "reducible" definition, one that unfolds even at the most conservative transparency setting.

[Kyle Miller]

def creates a "semireducible" definition, which tends not to get unfolded by processes that match expressions, for example when finding instances that might apply for a given typeclass.

[Kyle Miller]

I still don't see any reason why abbrev should make this elaboration succeed...

It's very delicate whether it succeeds or not. For example, even this makes it succeed:

import Std.Data.TreeMap
inductive Typ where | Int : Typ | Str : Typ
def Schema := Std.TreeMap String Typ
def Example (a : Array (String × Typ)) : Schema :=
  (Std.TreeMap.ofArray a :)

This causes the by exact compare to evaluate before unifying types.

[Kyle Miller]

(lean4#9346 is an experiment in having auto-params elaborate in a way that lets these unifications go through)

[Paul Reichert]

Kyle Miller said:

(Paul Reichert Maybe you want to take a look at this? I can see why the library uses auto-params, since it means you can pass a cmp argument, which is more convenient than using Ord instances, but on the flip side since it's a tactic it seems like it's not really possible to solve for by unification.)

I fully agree that the situation at hand is confusing, but it's not clear to me how to improve it from the library's angle. Always requiring an Ord instance would be an option, although it would complicate other use cases that involve an ad-hoc comparison function. Let me hope for now that the experimental PR turns out to be promising ;)