2
$\begingroup$

Suppose, for example, we want to type-check the following term:

main
: ∀(b: Bool) -> (if b then Nat else Char)
= λb -> (match b { true: <A>; false: <B> } : ?R)

Where <A> and <B> stand for arbitrary terms, and match performs the dependent elimination on bools. As we traverse this term in a conventional bidirectional type-checker, we'll see typed holes in the following order:

<A> : (?R true)
<B> : (?R false)
?R  : Bool -> *

Then, since the return type of main is (if b then Nat else Char), and since the dependent pattern-match returns (?R b), we'll have the following equation:

(if b then Nat else Char) = (?R b)

This satisfies all the requisites of pattern unification, giving us the substitution:

?R = λb (if b then Nat else Char)

So far, so good; my question is: what happens next? With this new knowledge, we would be able to substitute ?R for the found unification, and re-type-check the entire program. But this would wasteful. If I understand correctly, smalltt, a high-performance type theory elaborator by András Kovács, has a mechanism where <A> : (?R true) and <B> : (?R false) are ~frozen~ suspended, and, as soon as we know ?R, we're able to immediately go back, and check <A> : Nat and <B> : Char, respectively.

My question is: how this situation is handled? Will the type-checker just fail on <A> : (?R true), or will it suspend these problems and revisit them later? And, if that's the case, how is that implemented in a way that is more efficient than "re-checking" the whole program once R is solved?

Note: this question is a mirror of this issue. I'll replicate the answer when available.

$\endgroup$

2 Answers 2

4
$\begingroup$

I believe there are two mechanisms at play here. The first and simplest is that usually unification/elaboration happens with a meta-context, containing meta-variables (solved and unsolved), which gets updated in an imperative fashion as type-checking progresses.

The second mechanism is called dynamic unification (often in full dynamic pattern unification, when restricting to the fragment of unification with most general unifiers). I'm not sure what exact references are the best, but a quick search gives A tutorial implementation of dynamic pattern unification by Gundry and McBride, and a JFP paper by Abel and Pientka. The idea of dynamic unification is that solving unification problems in order is often not enough, because they might not be in the right form right away. So what dynamic unification does is it tries to eagerly solve as much as is possible of a new unification problem, until it either succeeds, fails, or gets stuck. If it succeeds, great, it now learned a bunch of things, ie solved meta-variables to add in the meta-context. If it fails, an error is reported. But if it gets stuck, instead of throwing away the problem, it "freezes" it, keeps it to the side, and goes on with the type-checking. Whenever another unification problem is encountered and solved, old frozen problems are revived and attempted again with the new acquired knowledge (aka new solutions for meta-variables). You can do this in a smart way, by recording which metavariables were blocking a frozen problem, so that you only attempt to revive problems which have potentially been unstuck.

Let me try and detail how this plays in your example:

  1. a λ-abstraction is checked against a ∀-type, so we are left with checking the pattern-matching in a context b : Bool
  2. we switch to inference mode, inferring a type for the pattern-matching, to be compared with (if b then Nat else Char)
  3. we infer type Bool for b
  4. we check ?R against Bool -> *, adding a new meta-variable ?R : Bool -> * in our meta-context
  5. we check <A> against ?R true
  6. we check <B> against ?R false
  7. we infer the type ?R b for the whole pattern-matching, and compare it to if b then Nat else Char, as you notice this solves ?R to λ b. if b then Nat else Char
  8. this potentially triggers back unification problems that were frozen in steps 5 and 6
  9. we are done (although a type-checker at this point might report unsolved meta-variables/unification problems, if any remain)

What happens in steps 5 and 6 depends on the shape of <A> and <B>, but there are two typical behaviours. If <A> infers a type (for instance, if it is a variable), say <TA>, then the unification problem <TA> = ?R true will be triggered. If instead <A> merely checks, say it is λ x. <t>, we will create two new metavariables ?F and ?G, trigger the unification problem Π x : ?F. ?G = ?R true and continue checking <t> : ?G in a context extended by x : ?F (not sure there is a good argument to choose the order in which to perform these two operations).

In both cases, the problem involving ?R true is a tricky one until ?R has been solved in step 7 (for instance, Π x : ?F. ?G = ?R true is not in the pattern fragment). So it is likely that delayed unification would kick in. If the unification problem does not fall into the solvable fragment, it will get frozen, and resumed after ?R is solved, where it now simplifies to the easier … = Nat. Thus, if you erroneously put a function for <A>, this error will be noticed in step 8, when the problem Π x : ?F. ?G = ?R true simplifies to Π x : ?F. ?G = Nat, which is not solvable.

$\endgroup$
6
  • $\begingroup$ To clarify, ?T and ?F should be just placeholders for arbitrary terms; in making them metavars, I accidentally made the question confusing. Basically, I was just trying to ask what would happen when the checker reaches, say, check (λx. x) :: (?R b). Should it throw (because (?R b) can't be forced into a Pi), or should it "suspend" (not freeze) that problem until later. From your answer, I now understand it is indeed suspended, and "revisiting" it is often implemented efficiently (say, keeping dependency graphs), which is exactly what I wanted to know! $\endgroup$
    – MaiaVictor
    Commented Feb 28 at 19:58
  • $\begingroup$ Note: I've edited the original question to clear up this confusion, in a way that shouldn't require you to edit your answer. Thank you! $\endgroup$
    – MaiaVictor
    Commented Feb 28 at 20:06
  • 1
    $\begingroup$ @MaiaVictor: You should just edit the question, without the visible "Edit" remarks. This is not reddit. Then Meven can change the answer if needed. At least that's how I understand the SE policies, a moderator can perhaps clarify. $\endgroup$ Commented Feb 28 at 21:20
  • 1
    $\begingroup$ I've adapted my answer to your edit. $\endgroup$ Commented Feb 29 at 10:21
  • 1
    $\begingroup$ I didn't mean to give you additional work, so I apologize. Your answer was very helpful. Thank you. $\endgroup$
    – MaiaVictor
    Commented Feb 29 at 19:20
1
$\begingroup$

Meven's answer is excellent, I would just like to make a theoretical remark that is too long for a comment.

Speaking meta-theoretically, a metavariable $\Gamma \vdash M : A$ can be thought of as an additional primitive symbol, adjoint to whatever signature our type theory has. A solution $\Gamma \vdash M \equiv t : A$ can similarly be thought of as an additional judgemental equality rule that is added to whatever rules our type theory has.

If a judgement can be derived without using the equation $M \equiv t$ then it can also be derived when the equation is adjoint as a rule (whatever is proved remains proved when more axioms become available). The practical consequence is that if a type-checker managed to type-check something involving $M$ before it knew $M \equiv t$, then whatever it did is still valid when $M \equiv t$ appears.

If I may go on rattling a little longer, one should wonder why it is ok to adjoin new rules to a type theory. If we derive something using a metavariable $M$ and an equation $M \equiv t$, how do we know that we could derive it without? The answer again is a suitable meta-theorem which says that substitution is admissible: a derivation $\mathcal{D}[M, M \equiv t]$ can be transformed to a one not relying on $M$ and $M \equiv t$, namely $\mathcal{D}[t, t \equiv t]$ obtained by a substitution which replaces $M$ with $t$ (provided that $M$ does not appear in $t$, which is why there are occurs-checks in real life), and applications of the rule $M \equiv t$ with reflexivity $t \equiv t$.

$\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.