8
$\begingroup$

How do the implicit arguments work in proof assistants such as Agda or Coq? Specifically, how are the blanks filled in? What kind of resolution algorithm is used?

Are there any papers written about implicit arguments?

$\endgroup$
7
  • 4
    $\begingroup$ Take a look at Ulf Norell's thesis "Towards a practical programming language based on dependent type theory" and github.com/AndrasKovacs/elaboration-zoo $\endgroup$ Feb 15, 2022 at 8:22
  • 1
    $\begingroup$ Two other papers of interest: "Higher-Order Dynamic Pattern Unification for Dependent Types and Records" and "A tutorial implementation of dynamic pattern unification". Ulf Norell's thesis discusses the insertion of meta variables, which can then be solved via unification. $\endgroup$ Feb 15, 2022 at 10:01
  • $\begingroup$ @AlberttenNapel The tutorial is way too hard. Are these the only sources to dynamic pattern unification? $\endgroup$
    – Cheery
    Feb 16, 2022 at 16:03
  • $\begingroup$ The implementation from github.com/AndrasKovacs/elaboration-zoo is the simplest one I know. $\endgroup$ Feb 17, 2022 at 7:40
  • $\begingroup$ @AlberttenNapel I found this through citations, and it seems conceptually simplest of them all. lopezjuan.com/en/event/2020/licentiate $\endgroup$
    – Cheery
    Feb 18, 2022 at 19:32

1 Answer 1

2
$\begingroup$

I don’t think there is any detailed paper description of this for Coq, however there is one for Matita which as far as I know is quite close to how Coq does things.

Unification is taken as a black box there, if you want to open that box, the best I know of in the Coq ecosystem is UniCoq and its accompanying paper. Again, it is not what actually happens in the internals of Coq, but it should be close enough to satisfy some curiosity.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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