Victor Lopez Juan, Computer Science and Engineering
Practical Unification for Dependent Type Checking
When using popular dependently-typed languages such as Agda, Idris or
Coq to write a proof or a program, some function arguments can be
omitted, both to decrease code size and to improve readability. Type
checking such a program involves inferring a combination of these
implicit arguments that makes the program type-correct.
Victor Lopez Juan belongs to the Logic and Types division of Computer Science and Engineering.
Finding such a combination of implicit arguments entails solving a higher-order unification problem.
higher-order unification is undecidable, our aim is to infer the
omitted arguments for as many programs as possible with a reasonable use
of computational resources. The extent to which
these goals are achieved affect how usable a dependently-typed proof assistant or programming language is in practice.
approaches to higher-order unification are in some cases too
inflexible, postponing unification of terms until their types have been
unified (Coq, Idris). In other cases they are too optimistic, which
sometimes leads to ill-typed terms that break internal invariants
In order to increase the flexibility of our unifier
without sacrificing soundness, we use the twin types technique by Gundry
and McBride. We simplify their approach so that it can be used within
an existing type
theory without changes to the syntax of terms. We
also extend it so that it can handle more classes of constraints. We
show that the resulting solutions are correct and unique.
we implement the resulting unification algorithm on an existing type
checker prototype for a smaller variant of the Agda language, developed
by Mazzoli and Abel. We make a suitable choice of internal term
representation, and use few, if any, example-specific optimizations. We
obtain a type-checker which avoids ill-typed solutions, and is also able
to handle some challenging examples in time and memory comparable to
the existing Agda implementation.
Matthieu Sozeau, researcher at the National Institute for Research in Computer Science and Control (INRIA), France.
Link to publication
02 October, 2020, 10:00
02 October, 2020, 12:00