8
$\begingroup$

In dependent-types, Miller pattern unification is used to solve a decidable fragment of higher-order unification. This allows dependently-typed languages to contain metavariables or implicit arguments.

There are many papers which describe, given a unification problem in the pattern fragment, how to find a solution if one exists. Examples include are (Gundry-McBride), (Abel-Pientka), and the original Miller paper.

What I'm wondering is, given a dependently typed program containing metavariables (or implicit arguments), how does one go about generating the problems that are passed to the unification solver?

|cite|improve this question
$\endgroup$
  • $\begingroup$ Have you looked at Norell's thesis? cse.chalmers.se/~ulfn/papers/thesis.pdf $\endgroup$ – adamse Feb 24 '16 at 8:09
  • $\begingroup$ The basic idea is that you do bidirectional type checking, but unify with metas instead of using case. $\endgroup$ – fread2281 Feb 24 '16 at 11:26
  • $\begingroup$ @adamse I have, though I'll admit, I had quite a hard time understanding it and seeing where the actual constraints are generated. $\endgroup$ – jmite Feb 24 '16 at 17:12
  • 2
    $\begingroup$ eb.host.cs.st-andrews.ac.uk/drafts/impldtp.pdf describes the elaboration of Idris and may have some of what you want, section 4 in particular $\endgroup$ – Edwin Brady Feb 26 '16 at 7:50
  • 1
    $\begingroup$ For implicits you need to be able to deal with holes aka meta variables in certification tems t of a judgement G |- t : A. In the worst case you end up in the inhabitation problem. en.wikipedia.org/wiki/Type_inhabitation $\endgroup$ – Mostowski Collapse Mar 14 '16 at 8:49
8
$\begingroup$

There's a nice idiom, which is explained more in chapter 22 of Types and Programming Languages (it's used for polymorphism rather than dependent types, but the idea is the same). The idiom is as follows:

A type checking system can be turned into a type inference system by making the rules linear and adding constraints.

I'll use the application rule as an example. The checking rule in dependent types is this:

$$\frac{\Gamma \vdash t:\Pi x:A.B\quad \Gamma\vdash u:A}{\Gamma\vdash t\ u: B[u/x]} $$

Linearizing this rule requires re-naming the 2 occurrences of $A$, such that we obtain:

$$\frac{\Gamma \vdash t:\Pi x:A_1.B\quad \Gamma\vdash u:A_2}{\Gamma\vdash t\ u: B[u/x]} $$

But this isn't correct anymore! We need to add the constraint $A_1\simeq A_2$:

$$\frac{\Gamma \vdash t:\Pi x:A_1.B\quad \Gamma\vdash u:A_2}{\Gamma\vdash t\ u: B[u/x]}\quad A_1\simeq A_2 $$

Note that $\simeq$ denotes equivalence modulo your conversion relation ($\beta\eta$, typically), just like for the conversion rule, but it is now a unification constraint, since you may have meta-variables in your terms.

In the course of type checking, you'll accumulate constraints like these, to potentially solve them all at once at the end (or earlier for efficiency reasons).

Now things can get trickier, because the type of $t$ itself could be a metavariable in context! A more generally applicable rule would therefore be

$$\frac{\Gamma \vdash t:C\quad \Gamma\vdash u:A_2}{\Gamma\vdash t\ u: B[u/x]}\ C\simeq \Pi x:A_1.B,\ A_1\simeq A_2 $$

Or alternatively, keeping the previous rule and adding the rule

$$\frac{}{\Gamma_1, x:C, \Gamma_2 \vdash x: A} C\simeq A $$

at variable lookup time.

Another useful remark is that in the checking system, the conversion rule only needs to be applied right before applications, and possibly once at the very end of the derivation. Since this rules correspond to a unification constraint in the inference system, this tells you where to place the constraints.

|cite|improve this answer
$\endgroup$
  • $\begingroup$ This is very helpful. Do you know of any reference that describes a full system for this? In particular, I'm having trouble generating constraints for lambda-expressions, dealing with the free variables from Pi-types. $\endgroup$ – jmite Feb 25 '16 at 1:37
  • 1
    $\begingroup$ We have a paper on arXiv that gives the nitty gritty details. You'd probably be most interested in section 3.5, though I'm afraid it's not as didactic as I'd like. $\endgroup$ – cody Feb 26 '16 at 16:11
  • $\begingroup$ @j4nbur53: that's correct, you indeed need to solve such a constraint in general. Most of the time though, getting the type of $t$ as a $\Pi$-type is rather easy, and the corresponding $B(x)$ comes as a consequence. This idea is implicit in the notion of bi-directional type-checking. $\endgroup$ – cody Mar 3 '16 at 15:32
  • $\begingroup$ I do in fact mean $B(x)$, since that is what you're looking for (getting $B(u)$ is trivial from there). I'm not sure what you mean by "(=)/2 introduction". In the first link, the system with constraints is linear. $\endgroup$ – cody Mar 3 '16 at 20:14
  • $\begingroup$ In the paper, we assume anything, including $t$, can be a meta-variable. In this case, and in the absence of additional constraints on $t$, we consider that the problem is underconstrained and give an error message (as would Coq). I would argue that this is the correct behavior. Of course, if the type of $t$ in this situation is, say, the witness of a type class inhabitation, then you will want a specialized routine for searching for such an inhabitant. $\endgroup$ – cody Mar 3 '16 at 20:30
4
$\begingroup$

If you model the lambda terms via deBruijn indexes and the meta variables via Prolog variables, you could build a Prolog constraint solver. Here is an example that works already quite well, the basic constraints that were used are as follows:

% shift(+Indexed, +Nat, +Nat, -Indexed)
% subst(+Indexed, +Nat, +Indexed, -Indexed)
% reduce(+Indexed, +Indexed, -Indexed)
https://gist.github.com/jburse/0ccd12698bfa24ce5c36#file-implicit2-p

The whole machinery also assumes that we strive for normal forms, in that we beta reduce in a certain order. There is an interaction between the normalizer and how new constraints above are generated. Since reducing a redex might require reevaluation of the normalization.

The constraint solver already implements a couple of cross constraint simplifications, without these simplifications and only constraint delay, the constraint solver would be too dumb and not practically usuable. We are still planning to add one or two more simplifications. A trove for simplifications is the following paper:

Residual Theory in λ-calculus
A Formal Development, Gerard Huet, 1998
http://pauillac.inria.fr/~huet/PUBLIC/residuals.pdf

In the paper one finds also the original inductive definitions of the constraints that we were using. See the following sections:
2.2 Lifting
2.3 Substitution
3.1 One-step β-reduction

Warning: The deBruijn terms help us in equality of normal terms, we do not need any step for alfa conversion. But we use a non-leveled dependent type, so for example there is no distinction between types and kinds under the hood. This makes the whole venture especially simple, on the other hand this is non-standard.

Bye

|cite|improve this answer
$\endgroup$
  • $\begingroup$ So you do not use Prolog's unification for your metas represented as Prolog's variables, and do your own constraint solving instead? $\endgroup$ – Saizan Feb 24 '16 at 10:55

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.