7
$\begingroup$

I gather, from practical experience and Zulip hearsay, that Coq has two unification algorithms, known as “tactic unification” and “evarconv”. However, I can't find any documentation on these from a web search.

I would like to know (with 3 and 4 being optional):

  1. In what situations are each of these unification algorithms used?
  2. What differences can we observe between the two algorithms?
  3. Are there any tricks to force one algorithm over the other as the situation may require?
  4. How do both algorithms compare to those of other dependently typed programming languages? I'm most familiar with Agda, but I think any comparison could help me understand the scope of unification in Coq.
$\endgroup$
4
  • 3
    $\begingroup$ Are you aware of doi.org/10.1145/2784731.2784751 and doi.org/10.1017/S0956796817000028 ? $\endgroup$ Apr 30 at 18:13
  • $\begingroup$ @AndrejBauer I don't think I was. Which unification algorithm(s) do they refer to? $\endgroup$
    – mudri
    May 1 at 9:54
  • $\begingroup$ I am not following too closely, but I think that's the new one that is implemented in the latest versions of Coq. If Pierre-Marie walks by he can tell for sure. $\endgroup$ May 1 at 10:01
  • $\begingroup$ I think that's the algorithm in the Unicoq Coq plugin. $\endgroup$ May 25 at 20:40

1 Answer 1

4
$\begingroup$

Blaisorblade is right, these papers are about a third algorithm, available via the UniCoq plugin, which is a cleaner, documented, and almost backward compatible, version of evarconv.ml. It is still slower, last time we checked (not algorithmically, it was due to simpler data structures IIRC) so we could not replace evarconv.ml with it.

I think we need Matthieu to know exactly the differences. From far away, also in time, unification.ml used Metas and not Evars (you still find that node in the internal syntax of terms). Metas are not assigned a type and don't track which bound variables are in scope. This is a funny beast for a type theoretic system. Indeed you can't possibly implement HO unification in a sound way with them. evarconv.ml is based on Evars, which do have a type and an explicit substitution to make reduction and instantiation commute. So evarconv.ml definitely makes more sense than unification.ml, but, coding style on the side, it has still a few downsides, in particular it may suspend/resume hard unification (sub) problems in unpredictable ways.

All SSReflect tactics use evarconv.ml since I can remember. Most of the vanilla tactics were progressively ported to evarconv.ml as well, with the notable exception of apply which is still "in progress" (there is a series of PRs called "unifall", not all merged).

I don't think you can compare unification in isolation. It is used inside elaboration (say, type inference). IIRC Agda has an algorithm based on accumulating (unification) constraints during typing, and then solving them in a "good" order. Lean used to have a similar approach (it is described in a paper) but that part of the system got rewritten. In Coq, pretyping.ml does solve unification problems via evarconv.ml eagerly, with some exceptions in which the problem is postponed (since it is too loosely constrained to hint to a single solution) and eventually resumed when made more constrained by some related Evar assignment or when the client forcibly asks for a solution, not necessarily the only one.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.