Zulip Chat Archive
Stream: new members
Topic: Replacing ℤ with a type argument breaks type class synthesis
Eric Wieser (Jul 03 2020 at 14:13):
Hi all,
I had some type class defined over (A : ℤ → Type u), but decided I wanted to be able to restrict it to (A : ℕ → Type u). To avoid losing the generality of the original statement, I changed the declaration to {ι : Type u} (A : ι → Type u). Unfortunately, this appears to break lean's ability to "synthesize type class instances".
The change in question can be seen at https://github.com/pygae/lean-ga/pull/6/files. The file is self-contained, and I've added comments to the lines causing me trouble. The file builds with no errors prior to this change.
I think the problem is something to do with my type class becoming a Pi-type, which prevents inference of its fields?
Reid Barton (Jul 03 2020 at 14:15):
The has_coe instance looks useless, btw
Reid Barton (Jul 03 2020 at 14:16):
(I mean instance has_coe (r s : ι) (h: r = s) : has_coe (A r) (A s), in case there are others)
Eric Wieser (Jul 03 2020 at 14:17):
It probably is - I was trying to solve a problem in another file where I couldn't equate terms of types A r and A (r + 0)
Reid Barton (Jul 03 2020 at 14:18):
There's no way to supply h.
Reid Barton (Jul 03 2020 at 14:18):
Anyways, I'm surprised if this worked before.
Eric Wieser (Jul 03 2020 at 14:19):
I suspect it just silently did nothing useful and I wasn't relying on it
Eric Wieser (Jul 03 2020 at 14:19):
But at any rate, after this change I now get complaints from lean
Reid Barton (Jul 03 2020 at 14:19):
I meant the file in general
Reid Barton (Jul 03 2020 at 14:19):
The fields of graded_module_components don't make good instances
Eric Wieser (Jul 03 2020 at 14:20):
Really I was trying to use graded_module_components as a shorthand for specifying all the properties over and over again
Reid Barton (Jul 03 2020 at 14:20):
I think this doesn't work.
Eric Wieser (Jul 03 2020 at 14:21):
I assume your statement is a judgement on the attribute [instance] lines below
Eric Wieser (Jul 03 2020 at 14:21):
Which actually worked perfectly until I replaced ℤ with ι
Reid Barton (Jul 03 2020 at 14:21):
For example, you're adding a rule for add_comm_group that matches literally anything applied to anything
Reid Barton (Jul 03 2020 at 14:22):
It may work so far in your small file
Eric Wieser (Jul 03 2020 at 14:23):
I suppose the number of "anything"s it matches grew immensely upon replacing ℤ...
Eric Wieser (Jul 03 2020 at 14:23):
But won't it only match things for which local instances of graded_module_components exist?
Reid Barton (Jul 03 2020 at 14:23):
It will match anything and then go look for instances of graded_module_components
Reid Barton (Jul 03 2020 at 14:24):
It can't see the future.
Jalex Stark (Jul 03 2020 at 14:24):
(Reid is talking about the typeclass inference algorithm)
Reid Barton (Jul 03 2020 at 14:24):
Eric Wieser said:
I suppose the number of "anything"s it matches grew immensely upon replacing
ℤ...
Yes, with the change now all the instances match anything applied to anything.
Reid Barton (Jul 03 2020 at 14:24):
Because anything could be 0.
Reid Barton (Jul 03 2020 at 14:26):
We do have instances like this but where the type isn't changing.
Eric Wieser (Jul 03 2020 at 14:26):
Could you point me to the builtin ones?
Reid Barton (Jul 03 2020 at 14:26):
Builtin what?
Reid Barton (Jul 03 2020 at 14:27):
I mean, imagine instead of A 0 or A r you just have A.
Eric Wieser (Jul 03 2020 at 14:27):
Sorry, wrong word - when you say "We do have", I'm asking for the names of those ones
Reid Barton (Jul 03 2020 at 14:27):
That seems more okay.
Reid Barton (Jul 03 2020 at 14:27):
You could also set_option trace.class_instances true and try to figure out why it didn't apply the instances you expected.
Reid Barton (Jul 03 2020 at 14:28):
I don't know if they have names. I think there are some in the category theory library.
Reid Barton (Jul 03 2020 at 14:28):
Also extends on a class creates them automatically I think.
Utensil Song (Jul 03 2020 at 14:29):
Reid Barton said:
We do have instances like this but where the type isn't changing.
I don't get the part "where the type isn't changing".
Reid Barton (Jul 03 2020 at 14:29):
An instance that says: In order to get an instance of C for a type, you need an instance of D for the same type.
Utensil Song (Jul 03 2020 at 14:30):
Ah, that makes sense in the context of category theory.
Utensil Song (Jul 03 2020 at 14:32):
Reid Barton said:
(I mean
instance has_coe (r s : ι) (h: r = s) : has_coe (A r) (A s), in case there are others)
@Eric Wieser What were you trying to have with this? I don't get it.
Eric Wieser (Jul 03 2020 at 14:33):
I was trying to have a coercion from A (r + 0) to A r if I had a local trivial proof that r = r + 0
Utensil Song (Jul 03 2020 at 14:33):
That seems to be not a coercion
Utensil Song (Jul 03 2020 at 14:34):
They're just equal
Eric Wieser (Jul 03 2020 at 14:36):
Well, the lean type system doesn't allow me to make statements arp0 = ar if ar : A r and arp0 : A (r + 0).
It was an attempt at doing something like @Kevin Buzzard's canonical_map in https://gist.githubusercontent.com/kbuzzard/f5ee35457c5d257ceec58c66d7da0c38/raw/e7eefed8190b436f4b6f34ee3895931e43859997/cdga.lean, and looking for alternate spellings
Reid Barton (Jul 03 2020 at 14:37):
Are you sure it was r + 0 and not 0 + r?
Eric Wieser (Jul 03 2020 at 14:40):
No, I'm probably misremembering the details
Eric Wieser (Jul 03 2020 at 14:41):
That was a problem that I only got halfway through investigating before running into the titular issue of this thread.
Eric Wieser (Jul 03 2020 at 14:41):
Unfortunately, set_option trace.class_instances true is not giving me anythiing I can easily sift though
Eric Wieser (Jul 03 2020 at 14:56):
Perhaps I should instead be asking the question "Is attempting to bundle type classes together like this sensible?"
Scott Morrison (Jul 04 2020 at 05:13):
An example of an instance which matches "anything" (and hence is probably a bad idea) is
which allows typeclass inference to prove an isomorphism is an epimorphism.
Scott Morrison (Jul 04 2020 at 05:14):
(the combination of "inference" and "prove" in that sentence may be a bad sign...)
Reid Barton (Jul 04 2020 at 12:53):
But here again the thing (no longer a type) f doesn't change.
Last updated: Dec 20 2023 at 11:08 UTC