Zulip Chat Archive

Stream: general

Topic: unusable arguments


Reid Barton (Apr 28 2020 at 10:59):

From #2502:

instance forget₂ (F : Π {α}, d α  c α) [parent_projection @F] : has_forget₂ (bundled d) (bundled c) :=
{ forget₂ :=
  { obj := λ X, X, F X.2,
    map := λ X Y f, f } }

Unless I am very confused, I'm pretty sure this is not usable as an instance because F could never be inferred (bundled doesn't mention it implicitly). Wasn't there some discussion about a linter for cases like this?

Gabriel Ebner (Apr 28 2020 at 11:10):

It can be inferred using an instance for parent_projection.

Scott Morrison (Apr 28 2020 at 11:15):

I think you're right, Reid, this should be a def, not an instance.

Reid Barton (Apr 28 2020 at 11:20):

It makes me wonder whether, in the context of #2502, parent_projection plays any role at all

Reid Barton (Apr 28 2020 at 11:30):

Gabriel, I don't understand. I see that we could infer F from the instance or the instance from F (by instance search), but how can either of them be determined by anything on the right side of the :?

Gabriel Ebner (Apr 28 2020 at 11:42):

I hope I understand how this is supposed to be used. Say you want to solve ?m_1 : has_forget₂ (bundled group) (bundled monoid), then Lean will apply the instance forget₂ and you get a new goal ?m_2 : @parent_projection monoid group ?m_3, which is then presumably solved using the instance Group.category_theory.bundled_hom.parent_projection : parent_projection group.to_monoid.

Gabriel Ebner (Apr 28 2020 at 11:44):

I think it would be a bit clearer if the type arguments in parent_projection were explicit and the functor was explicily marked as an out_param.

Mario Carneiro (Apr 28 2020 at 11:47):

Couldn't the functor be a field of parent_projection?

Reid Barton (Apr 28 2020 at 11:47):

I thought that the instance could only be used if F was an out_param.

Gabriel Ebner (Apr 28 2020 at 11:48):

If the functor is a field you'd need to reduce them afterwards to get acceptable terms.

Gabriel Ebner (Apr 28 2020 at 11:48):

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

Mario Carneiro (Apr 28 2020 at 11:48):

no more than usual, I think

Mario Carneiro (Apr 28 2020 at 11:49):

With this setup it seems that parent_projection doesn't carry any information at all

Reid Barton (Apr 28 2020 at 12:07):

Gabriel Ebner said:

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

Oh wow, that seems super crazy to me (but then I am used to the sensible world of Haskell)

Reid Barton (Apr 28 2020 at 12:10):

I feel like this is variable declaration all over again, where ALGOL 60 solved the problem properly and subsequently every dynamic language in the world decided it had a better idea how to do it.

Gabriel Ebner (Apr 28 2020 at 12:16):

I guess it explains some of our performance problems. Unfortunately the powers that be have decided to keep this Prolog-like search in Lean 4. AFAICT the only real application of this "feature" are the transitive instances for has_coe such as coe_trans. And Lean 4 isn't getting rid of coe_trans either, so we'll have to live with the coe_coe simp lemma hack. :disappointed:

Reid Barton (Apr 28 2020 at 12:39):

Well, I'd prefer an efficient, predictable, and dumb procedure over what we have in Lean 3. The dumb part is not a requirement :upside_down: We'll see how well the Lean 4 approach works when we start using it.

Kevin Buzzard (Apr 28 2020 at 12:42):

Gabriel Ebner said:

Unfortunately the powers that be have decided to keep this Prolog-like search in Lean 4.

Maybe it's time for a fork!

Reid Barton (Apr 28 2020 at 12:45):

Lean 4.0.0-beta-1-c-alpha?

Reid Barton (Apr 28 2020 at 13:27):

I wanted to believe that instance search doesn't really work the way Gabriel said, but it does. Here is a simplified example.

class is_good {α β : Type} (F : α  β)

instance : is_good nat.succ := ⟨⟩

class has_forget (α β : Type) :=
(forget : α  β)

instance I {α β : Type} (F : α  β) [is_good F] : has_forget α β :=
F

#reduce (show has_forget  , by apply_instance)   -- {forget := nat.succ}

Reid Barton (May 19 2020 at 14:50):

Gabriel Ebner said:

out_param is only necessary at the interface between type-class search and the rest of Lean. Inside type-class search, everything is an out-param.

Is this something that could easily be "fixed" to behave more like a Haskell programmer (or at least a GHC developer :upside_down:) would expect, or do we think mathlib relies heavily on it? To be clear: the expected behavior is that when a instance search problem contains a metavariable, we never select an instance if it means assigning that metavariable. (But it's still fine to select an instance which has a variable where the search problem has a metavariable.)

Reid Barton (May 19 2020 at 14:51):

I think this is still compatible with "Prolog-like search" and backtracking; I'm not sure what Lean 4 does in this area but from my visit to MSR I have the impression that the plan was to do something like what I describe here.

Gabriel Ebner (May 19 2020 at 14:54):

I'm not exactly sure what you mean. Do you suggest that has_mem ?m (set ℕ) may not assign ?m? I think this would break lots of stuff. For example 42 ∈ A would no longer work if A : set ℝ.

Reid Barton (May 19 2020 at 14:54):

Sorry, what I say only applies in the absence of out_param.

Reid Barton (May 19 2020 at 14:55):

I'm not sure exactly what to say when there is out_param but I think it's roughly: allow assigning to a metavariable when that metavariable occurs in a position with out_param.

Reid Barton (May 19 2020 at 14:55):

∈ has

class has_mem (α : out_param $ Type u) (γ : Type v) := (mem : α  γ  Prop)

Gabriel Ebner (May 19 2020 at 14:55):

Can you maybe give an example?

Reid Barton (May 19 2020 at 14:57):

I think my previous message (from Apr 28) is an example: to apply the instance I we first have to solve is_good ?m_1 and we shouldn't be allowed to apply the instance for is_good nat.succ.

Gabriel Ebner (May 19 2020 at 14:57):

Ah, so does this question come from the "function expected" thread? Then I think the answer is "this will change in Lean 4".

Reid Barton (May 19 2020 at 14:57):

Yes.

Reid Barton (May 19 2020 at 14:57):

Can we change Lean 3 to what Lean 4 will do?

Reid Barton (May 19 2020 at 14:58):

And, the other question is will Lean 4 do more or less what I described above?

Gabriel Ebner (May 19 2020 at 14:58):

The Apr 28 example will not change. The only place where we make use of this feature is in transitive coercions. AFAICT Lean 4 will rely on transitive coercions implemented in this way even more heavily.

Reid Barton (May 19 2020 at 15:00):

I guess I can just test the Apr 28 example in current Lean 4.

Reid Barton (May 19 2020 at 15:03):

Indeed, it still seems to work :slight_frown:

Reid Barton (May 19 2020 at 15:07):

Well, with not so current Lean 4. I tried getting the latest version and building it, but the build instructions don't work for me:

rwbarton@operad:~/math/lean/lean4/build/release$ cmake ../..
-- The CXX compiler identification is GNU 7.5.0
-- The C compiler identification is GNU 7.5.0
-- Check for working CXX compiler: /usr/bin/c++
-- Check for working CXX compiler: /usr/bin/c++ -- works
-- Detecting CXX compiler ABI info
-- Detecting CXX compiler ABI info - done
-- Detecting CXX compile features
-- Detecting CXX compile features - done
-- Check for working C compiler: /usr/bin/cc
-- Check for working C compiler: /usr/bin/cc -- works
-- Detecting C compiler ABI info
-- Detecting C compiler ABI info - done
-- Detecting C compile features
-- Detecting C compile features - done
CMake Error at CMakeLists.txt:76 (add_custom_target):
  The target name "test" is reserved or not valid for certain CMake features,
  such as generator expressions, and may result in undefined behavior.


-- Configuring incomplete, errors occurred!
See also "/home/rwbarton/math/lean/lean4/build/release/CMakeFiles/CMakeOutput.log".

Reid Barton (May 19 2020 at 15:12):

@Sebastian Ullrich :point_up: is this a cmake version issue perhaps?

Sebastian Ullrich (May 19 2020 at 15:13):

@Reid Barton Huh, that's interesting. Which cmake version are you using?

Reid Barton (May 19 2020 at 15:13):

cmake version 3.10.2

Gabriel Ebner (May 19 2020 at 15:13):

@Reid Barton Note that Lean 3 type class synthesis also works if the type contains metavariables, it's just that the elaborator refuses to add a coercion. This should be fixable.

class foo (α : Type) := (x : )
instance fourty_two (α) : foo α := 42
example :  :=
begin
  have α : Type, tactic.swap,
  -- at this point α is still a metavariable
  exact foo.x α,
  --
  exact unit
end

Reid Barton (May 19 2020 at 15:14):

I also tried building a version from May 8 but I got a different error:

CMake Error at CMakeLists.txt:530 (if):
  if given arguments:

    "EQUAL" "0"

  Unknown arguments specified

Sebastian Ullrich (May 19 2020 at 15:14):

@Reid Barton It works on 3.16.5

Reid Barton (May 19 2020 at 15:16):

I'll see if Ubuntu has packaged some more recent version. But maybe it's easiest if you can just rename the target?

Reid Barton (May 19 2020 at 15:16):

Might hit that other error next though

Reid Barton (May 19 2020 at 15:17):

20.04 LTS has 3.16.3, maybe if I am feeling brave some day I can try upgrading to that.

Reid Barton (May 19 2020 at 15:21):

@Gabriel Ebner This example is unobjectionable because the instance claims to work for all types. If you change fourty_two to be about a specific type, then it fails (which is also correct). And this is good because it means there is always at most one value for x (assuming you don't write overlapping instances), but if you want to write an instance that fixes the same value of x for every type, then it works even when the type is unknown.

Sebastian Ullrich (May 19 2020 at 15:23):

@Reid Barton They changed this in 3.11.0 apparently. But you can try passing -Wno-dev to cmake ../..

Gabriel Ebner (May 19 2020 at 15:23):

@Reid Barton I am really dense today. Do you agree that fourty_two should work, or do you think it shouldn't?

Reid Barton (May 19 2020 at 15:24):

Your example should work.

Reid Barton (May 19 2020 at 15:25):

It should fail if you change fourty_two to be about a specific type (rather than an arbitrary α), and it does.

Reid Barton (May 19 2020 at 15:27):

Actually, in this setup with have α : Type, tactic.swap, it seems that instance search doesn't believe that α is a metavariable it could assign.

Reid Barton (May 19 2020 at 15:29):

@Sebastian Ullrich I got the same error, but I just renamed the test target locally and it seems to work fine for me for now.

Reid Barton (May 19 2020 at 15:29):

Of course you probably don't want to rename the target for other reasons, so I'm happy with this workaround for now.

Reid Barton (May 19 2020 at 15:33):

@Gabriel Ebner My main worry, which might be misplaced, is that if we have Lean look for a has_coe_to_fun instance too early, before we know anything about the actual type, it will commit to some nonsense instance.

Reid Barton (May 19 2020 at 15:37):

That is, the thing e we want to coerce is actually an equiv but we don't know this yet, and then instance selection chooses the instance for linear_fun or whatever, and then e gets type checked as a linear_fun.

Reid Barton (May 19 2020 at 15:37):

I'd rather fix this structurally by never letting instance selection refine a metavariable (unless directed to by out_param).

Reid Barton (May 19 2020 at 15:39):

The current implementation avoids this in the heavy-handed way of not even considering using a coercion until there are no metavariables, which has me worried that the problem I imagine is a real one.

Reid Barton (May 19 2020 at 15:42):

I guess a weaker sufficient property is "instance selection never refines a metavariable that existed beforehand", and I don't know whether this can fail.

Gabriel Ebner (May 19 2020 at 15:47):

Right now, type class synthesis just rejects all instances that contain metavariables, no matter whether they are introduced during TC search ("temporary metavariables") or are metavariables that existed before. I'll try weakening this check to "doesn't contain metavariables introduced during TC search", is that what you had in mind?

Reid Barton (May 19 2020 at 16:05):

I'm not sure what "instances that contain metavariables" means.
What I object to is the second (successful) step in the trace from the Apr 28 example:

[class_instances] (0) ?x_0 : has_forget   := @I ?x_1 ?x_2 ?x_3 ?x_4
[class_instances] (1) ?x_4 : @is_good   ?x_3 := nat.succ.is_good

Here nat.succ.is_good has type @is_good ℕ ℕ nat.succ. In order to apply this instance we need to assign ?x_3 := nat.succ; I claim we should never assign a metavariable in this way (except in the presence of out_param).
In general, a metavariable might be "owned" by something other than instance search and so it does not make sense for instance search to assign it. For example, it might be the type of an expression e in an application e x; we haven't elaborated e yet so we represent its type as a metavariable. In this case it is definitely not sensible for instance search to assign this metavariable (except in the presence of out_param, since this is its purpose).
Now, in the trace above, ?x_3 actually came from applying another instance, and so arguably it is "owned" by the instance search. This still seems dubious to me (and definitely breaks instance coherence), but it is better than assigning metavariables that existed prior to instance search. For example, if the type of ?x_0 contained a metavariable, it would definitely be wrong to assign it in the course of applying an instance.
It's possible that the behavior is already "instance selection never refines a metavariable that existed beforehand".

Gabriel Ebner (May 19 2020 at 16:08):

I don't like it either, but this required by how transitive coercions are encoded as type class resolution problems, which I don't like either. But for that reason it's very unlikely it will change in Lean 4.

Mario Carneiro (May 19 2020 at 17:33):

It sounds like Reid is not objecting to applying instances like coe_trans because these have a type like coe1 a b -> coe_t b c -> coe_t a c, and as long as both a and c are known then this can apply, because it's not assigning any existing metavariables, only creating a new one. (I would argue that this instance should have an out_param on b to flag that this new variable is okay, but that's another matter.) Reid's criterion means that the coe1 a ?b is now stuck, but coe_t ?b c can make progress because coe_t has an out_param on its first argument, and once it is done coe1 a b can fire.


Last updated: Dec 20 2023 at 11:08 UTC