The imminent departure of Doctor No reminds me to think about orange things a little.
As some of you may know, Buddy Holly subcategorizes the unsolved definitions in the proof state as
- crying, with no value nor any way ever to get one, for things have gone wrong: these are brown
- waiting, with no value yet, but a definite solution strategy which may yet work: these are yellow
- hoping, with no value yet, nor any particular process intended to deliver one: these are orange
All holes wish they could have a value and go green. The brown ladies know this will never happen for them, and they also know that it’s your fault. The yellow ladies just wait for the solution strategy (these days, that’s you) to do its stuff. But the orange ladies should show a bit more independence. Let’s think about why and how later. For now, let’s ask ‘Who are these orange ladies anyway?’.
The most obvious place they come from is implicit syntax. An implicit syntax scheme is given by the grammar
Scheme ::= !Type | (x : Scheme)→Scheme | {x : Type}→Scheme
and there’s a forgetful map |-| from Schemes to types which drops ! and turns {} into () everywhere. If we have a high-level function f with scheme σ, and corresponding fimp : |σ|, how should we elaborate a call f s1 .. sn, inferring its type? Let me write this task as a problem which might decorate a yellow variable of type Thing (being a type-term pair)
wait Thing ← [fimp for σ] s1 .. sn
then show how to refine it by giving stuff to stuff in the context, and a value if we’re lucky enough to be done.
wait Thing ← [s for !S]
[] = (S, s) : Thing
wait Thing ← [f for !(x:S)→T] s ss
[wait x [] = ? : S ← s [check]] = ? : Thing ← [f x for !T] ss
wait Thing ← [f for (x:σ)→τ] s ss
[wait x [] = ? : |σ| ← s [to σ]] = ? : Thing ← [f x for τ] ss
wait Thing ← [f for (x:σ)→τ]
[wait Tt [x : |σ|] = ? : Thing ← [f x for τ]]
= ((x : |σ|)→Tt x fst, λx→Tt x snd): Thing
wait Thing ← [f for {x:S}→τ] {s} ss
[wait x [] : S ← s [check]] = ? : Thing ← [f x for τ] ss
wait Thing ← [f for {x:S}→τ] ss
[hope x [] : S] = ? : Thing ← [f x for τ] ss
So, orange holes can stand for implicit arguments. Partially applied functions need to be η-expanded as far as their schemes indicate, in order to insert their missing arguments. While I’m on the subject of higher-order stuff, let me see if I can manage the insertion of implicit lambdas in higher-order schemes.
wait T ← s [to !T]
[] = ? : T ← s [check]
wait (x:|σ|)→|T| ← (λx→t) [to (x:σ)→τ]
[x : |σ|; x implements x:σ] = ? : |τ| ← t [to τ]
wait (x:|σ|)→|T| ← e [to (x:σ)→τ] ExTerm e
[x : |σ|; x implements x:|σ|] = ? : |τ| ← e x [to τ]
wait (x:S)→|τ| ← (λ{x}→t) [to {x : S}→τ]
[x : S; x implements x:!S] = ? : |τ| ← t [to τ]
wait (x:S)→|τ| ← t [to {x : S}→τ] otherwise
[x : S] = ? : |τ| ← t [to τ]
Each explicitly bound symbol is given a scheme and an implementation. Now we can write a bit of general-purpose elaboration. Firstly, inference for (possibly nullary) applications of implemented functions, invoking our scheme elaborator:
wait Thing ← f ss [infer] fimp implements f:σ
[] = ? : Thing ← [fimp for σ] ss
Secondly, a bit of a typechecker:
wait (x:S)→T ← λx→t [check]
[λ x : S; x implements x:!S] = ? : T ← t
wait T ← e [check] ExTerm e
[wait Ss [] = ? : Thing ← e [infer]; hope Q [] = ? : Prf (Ss fst = T)]
= coe (Ss fst) T Q (Ss snd) : T
Note here that the constraint on change of direction is expressed in orange! Old-fashioned implementations call some unification algorithm which is basically a conversion check with haemhorroids: it solves metavariables when it sees suitable equations and says ‘no’ when conversion cannot thus be made to succeed. Often, if unification fails because some helpful hint hasn’t shown up yet, typechecking breaks when it shouldn’t. Check your system:
For metavariables x, y in Nat, try unfying
(x, 3) = (0, x + y)
(3, x) = (x + y, 0)
Epigram 1 and Agda 2 have some cunning technology for storing unification constraints until they can be solved (or repudiated). For Epigram 2, it’s just more orange. Why? Epigram 2’s propositional equality is extensional for functions, and that means we can faithfully represent unification problems under binders as ∀-quantified equations, and then discharge those binders. Think about how to say that two Π-types are equal, for example. In the usual overly intensional type systems, knowing that domains coincide and that ranges coincide pointwise does not allow us to derive equality of two Π-types, but for us, that’s exactly the definition!
So there we have it: both implicit arguments and typing constraints give rise to orange things. Unification is not special: it’s one part of proof search.