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?
$\begingroup$
$\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$– Albert ten NapelFeb 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$– Albert ten NapelFeb 15, 2022 at 10:01
-
$\begingroup$ @AlberttenNapel The tutorial is way too hard. Are these the only sources to dynamic pattern unification? $\endgroup$– CheeryFeb 16, 2022 at 16:03
-
$\begingroup$ The implementation from github.com/AndrasKovacs/elaboration-zoo is the simplest one I know. $\endgroup$– Albert ten NapelFeb 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$– CheeryFeb 18, 2022 at 19:32
|
Show 2 more comments
1 Answer
$\begingroup$
$\endgroup$
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.
answered Feb 23, 2022 at 9:54