Stream: Coq devs & plugin devs

Topic: Discrimination trees & typeclass search


view this post on Zulip Janno (Jun 17 2020 at 15:28):

Sorry I didn't have a specific example prepared for the call. Here's a file that illustrates quite nicely what I was referring to: https://gist.github.com/Janno/a9bd105f427954438f930d9ccd30683d

view this post on Zulip Janno (Jun 17 2020 at 15:32):

If you run the file (8.11 should it do just fine) you'll see that the apply call in the first module will try all instances, even though it should be clear statically that none of the instances for addition can possibly work. The second module manually stratifies the Simplify class and now we don't seem to be wasting any time on impossible unification checks.

view this post on Zulip Janno (Jun 17 2020 at 15:34):

The example is stupid and possibly even contrived but I have real code (not yet public but it hopefully will be at some point) that has seen enormous speedups from this technique. The unification algorithm used by type class search is extremely bad when it comes to unification problems that come up when canonical structures are used and so in one instance we sped up proofs by 25% simply by adding a new layer of typeclasses like I do in the gist. 25% is a lot for such a simple change.

view this post on Zulip Janno (Jun 17 2020 at 15:40):

Oh, hold on a second I forgot to add the crucial instance. Don't be surprised, right now the example proves nothing :D

view this post on Zulip Janno (Jun 17 2020 at 15:41):

Never mind, I used :> which registers the right instance automatically

view this post on Zulip Janno (Jun 17 2020 at 15:44):

@Matthieu Sozeau is this behaviour expected? Is there a way for users to avoid writing these sub-classes manually?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:01):

this is very suspicious indeed, the dnet returns everything including stuff that shouldn't match

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:02):

oh my

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:03):

I think this is because pattern expansion is not stable under evar unfolding

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:04):

ah no

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:05):

it's just the algorithm for dnets which is funny

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:05):

if it sees a constant that is transparent, it claims it could be anything so virtually everything matches

view this post on Zulip Gaëtan Gilbert (Jun 17 2020 at 16:06):

(* doesn't even try SimplifyAdd at all and even if it did it would fail immediately without trying all the instances of SimplifyAdd *)

this is a priority issue, if the mult instance is at priority 2 instead of 1 it tries addition, fails, then tries mult

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:06):

so here Simplify (mul X Y) matches anything of the form Simplify _

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:06):

instead of Simplify (mul _ _)

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:06):

I guess this makes sense, somehow

view this post on Zulip Janno (Jun 17 2020 at 16:07):

this is a priority issue, if the mult instance is at priority 2 instead of 1 it tries addition, fails, then tries mult

Interesting. I suppose the instance generated by :> has the "wrong" priority for my demonstration.

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:07):

we need to allow arbitrary δ unfolding

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:07):

typeclass matching is higher-order is the bottom line I believe?

view this post on Zulip Janno (Jun 17 2020 at 16:08):

we need to allow arbitrary δ unfolding

How about a flag? Something like Hint Mode for delta unfolding? I think Typeclasses Opaque helps here but I might have messed up my experiment.

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:08):

it should help indeed

view this post on Zulip Janno (Jun 17 2020 at 16:09):

This will speed up iris and similar typeclass-driven developments immensely

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:09):

or more probably break a lot of stuff

view this post on Zulip Janno (Jun 17 2020 at 16:09):

Sorry, Typeclasses Opaque does not help here as far as I can tell

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:10):

hm, we have several transparency tables in the hintdb

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:10):

the dnet is probably looking at the wrong one

view this post on Zulip Janno (Jun 17 2020 at 16:17):

I think a lot of people would be extremely grateful if this could be fixed :)

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:17):

fixed with respect to what specification, that's the usual problem :/

view this post on Zulip Janno (Jun 17 2020 at 16:19):

Well, if Nat.add is Typeclass Opaque then none of the instances for it should be tried in my example. Is that possible?

view this post on Zulip Janno (Jun 17 2020 at 16:19):

In fact, wouldn't it already be the case that, if we have Typeclass Opaque Nat.add then all of the instances would fail even if they were applicable after reduction of Nat.add?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:22):

The problem is mul, not add

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:23):

but I see your point

view this post on Zulip Janno (Jun 17 2020 at 16:23):

Oh, right, sorry. Okay, assume all constants were made Typeclasses Opaque, even mul. It's a big ask of the user but it would still be an improvement. Could we have the "right", i.e. fast behavior then?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:24):

I guess so, assuming we sort out the reason why we have so many transparent states in the database

view this post on Zulip Janno (Jun 17 2020 at 16:26):

So which transparent state is the dnet using?

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:26):

good question, I am trying to understand

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:26):

in the meantime, I've found the option I mentioned before

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:26):

it's Typeclasses Filtered Unification

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:27):

which does something very similar to first-order unification on goals

view this post on Zulip Janno (Jun 17 2020 at 16:27):

Right, not a very memorable name.. I thought that one had some sort of drawback that made it either ineffective or unusable. I'll try to find out which.

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:28):

honestly I don't understand why our auto-like tactics have such a complex implementation

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:28):

the simplest one is eauto, which apart from being broken, is straightforward

view this post on Zulip Janno (Jun 17 2020 at 16:30):

this option seems to be a global thing that affects all typeclasses.. that's going to make it impossible to activate in most developments, I think

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:33):

Can you confirm that setting Typeclasses Opaque of Nat.mul solves the problem though?

view this post on Zulip Janno (Jun 17 2020 at 16:37):

No, it does not currently solve the problem as far as I can tell

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:37):

(ah, it seems you need to set both add and mul opaque, but then it does work)

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:38):

the discrimination is cut of both for the pattern and the term being matched, so if you want that two constants don't match both must be set opaque

view this post on Zulip Janno (Jun 17 2020 at 16:39):

Indeed, interesting. So my request was already fulfilled.. now one just needs to find every single constant used anywhere ever to make everything faster :D

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:40):

we can add a command to turn everything opaque though

view this post on Zulip Janno (Jun 17 2020 at 16:42):

For a single type class? that would be great!

view this post on Zulip Pierre-Marie Pédrot (Jun 17 2020 at 16:43):

yes, we have access to the global so should be fine

view this post on Zulip Janno (Jun 17 2020 at 17:04):

I wonder if a better alternative would be Typeclasses Default Opaque/Transparent <class> (the latter being the current default I guess?)

view this post on Zulip Janno (Jun 17 2020 at 17:05):

That way one could still make certain constants transparent later?

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 18:43):

Be careful that making everything Opaque will make some things not match syntactically because of implicit arguments in many cases.

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 18:45):

Indeed the Filtered Unification is a bit drastic, but it gives the most control on which patterns trigger which hint (you get to give the syntactic pattern yourself)

view this post on Zulip Matthieu Sozeau (Jun 17 2020 at 18:51):

You can already do Hint Constants/Variables Opaque : typeclass_instances, at your own risk :)

view this post on Zulip Janno (Jun 17 2020 at 19:59):

You can already do Hint Constants/Variables Opaque : typeclass_instances, at your own risk :)

Interesting! What does Hint Variables do? Is it for existential variables?

view this post on Zulip Janno (Jun 17 2020 at 20:01):

Be careful that making everything Opaque will make some things not match syntactically because of implicit arguments in many cases.

Do you have an example for this? I would only be declaring the head constants opaque so if those match the parameters would still be unified (if possible), right?

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 07:57):

Yes, it's more in cases like setoid rewriting where if you make e.g. "relation" opaque you won't get unifications with "A -> A -> Prop". In general type aliases are one case where this breaks.

view this post on Zulip Matthieu Sozeau (Jun 18 2020 at 07:57):

Hint Variables is about section/goal variables

view this post on Zulip Janno (Jun 19 2020 at 09:32):

Here's my experience report: I set Hint Constant Opaque for the various databases we use for TC-guided proof search. I had to add various exceptions by making them Hint Transparent again. Some of those, I think, would be unnecessary if tactic unification wasn't so crazy but the rest is well-motivated.
Finding out which constants are blockers is a pain but I used the following recipe: Set Typeclassses Debug Verbosity 2, look for the failing instance and copy the part that says cannot unify X and Y. Use Hint resolve eq_refl : your_db, then assert (X = Y) and finally alternate between Fail typeclasses eauto with your_db and various incantations of cbn and unfold until eauto no longer fails. Then convert your reduction tactics into new Hint Transparent exceptions.
We got a 30% reduction in ltac execution time from this. Not bad for an afternoon's work.

view this post on Zulip Janno (Jun 19 2020 at 09:33):

The number of instances considered by typeclass search went down by a factor of 5!


Last updated: Oct 16 2021 at 03:02 UTC