[Agda-dev] A new unifier for case splitting

[Jesper Cockx]

Dear all,

For some time now, I've been working on implementing a new unification
algorithm to be used by Agda's case splitting algorithm. I originally
started working on this because of issues
https://github.com/agda/agda/issues/1406,
https://github.com/agda/agda/issues/1408,
https://github.com/agda/agda/issues/1427, and
https://github.com/agda/agda/issues/1435. You may also remember my
presentation at AIM XXI (see
http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Main.AIMXXI). My
implementation has changed a lot since then, but the basic theory is still
the same.

I'm writing this mail because I've come to a point where I think it makes
sense to integrate my work into the main Agda repository. You can find the
current status of the new unifier at
https://github.com/jespercockx/agda/tree/unification.

The basic idea of the new unifier is to manipulate an explicit unification
state, consisting of a telescope of free variables, a telescope of
equations, and left- and right-hand sides of each equation. The algorithm
itself consists of two components: a strategy for suggesting which
unification rule to apply where, and the unifier trying all these
suggestions in turn until one succeeds. At each step, the current
substitution is updated, resulting in the final substitution once the
unification succeeds. Please don't hesitate to ask me if you want to know
more about the theory. You can also (hopefully) expect a paper about it in
the next few months.

In addition to fixing the issue with injective type constructors, my
unifier also handles eta rules for records in a better way than the current
unifier. Because can perform on-demand eta expansion of record variables,
it solves most problems with the eager eta-expansion of implicit record
patterns. This is related to issues https://github.com/agda/agda/issues/473,
https://github.com/agda/agda/issues/635,
https://github.com/agda/agda/issues/1603,
https://github.com/agda/agda/issues/1608, and
https://github.com/agda/agda/issues/1613. In order to make Agda handle dot
patterns more robustly (see https://github.com/agda/agda/issues/1608), I
also had to add a check that checks whether the dot patterns written by the
user are compatible with the dot patterns computed by the unifier. This is
done by the function checkLeftoverDotPatterns in TypeChecking/Rules/LHS.hs.

There is a small number of test cases that still fail with my new unifier,
I would appreciate your feedback on these:
- There are a few testcases that shouldn't work but are currently accepted,
these are Issue292.agda, Issue1427.agda, and Issue1435.agda (only
D-elim-c₁-helper doesn't work, the rest does).
- A number of testcases require the solution of metavariables during
unification, these are IndexInference.agda, Issue199.agda, Issue314.agda,
Issue501.agda, and SizedBTree.agda (only old-style sized types fail). In my
opinion, the case splitting algorithm should never instantiate
metavariables, since this results in non-unique solutions that depend on
the order of the constructors (see https://github.com/agda/agda/issues/1653).
However, if I get outvoted on this matter, it should be easy enough to add.
- SetDetection.agda: The second example in this testcase needs a better way
to generalize datatype indices when --without-K is enabled, i.e. the
"reverse unification rules" I talked about at AIM XXI. This is still work
in progress, but the current version seems to do the job well enough in
most cases.
- Issue473-1606.agda: This needs a modification of my
checkLeftoverDotPatterns function to handle 'with' clauses. Since I'm not
familiar with the implementation of 'with', I was hoping Andreas (or
someone else) could give me a hint here.

I haven't put much effort yet in optimizing the unifier, so I expect that
it may be slower than the current unifier in some cases. On the other hand,
it should handle code with deeply-nested records more efficiently because
of the on-demand eta expansion. On the standard library, my unifier
actually performs a tiny bit faster, but the result isn't really
significant (less than 1 sec). I'm very interested to see how it performs
on other people's code bases.

Implementation-wise, this is quite a large patch (~1500 insertions and
~1600 deletions). At the moment, I have just smashed everything in one big
commit, but I could try to extract some logical sub-commits from it if
there is demand for that.

I would appreciate your feedback on my work, and I'd be glad to answer any
questions about the theory or the implementation.

Cheers,
Jesper
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda-dev/attachments/20151211/13c4156c/attachment.html