by Conor on November 25, 2007.
Tagged as: Lunches.
This is another episode of ‘stuff I learned while implementing Epigram which might be interesting even if you’re not implementing Epigram’. It’s an approach to unification based on an idea in my thesis. The idea is to work over a context, containing ‘holes’ and ‘lets’.
For this post, let’s take contexts to be exactly a sequence of holes and lets, inductively defined thus:
Let us take Γ-terms to be some first-order syntax, built from variables declared in Γ and a fixed signature of constructors. A context Γ induces an equivalence =Γ= on its terms by the structural and equivalence closure of its lets. We say Γ ≤ Δ if Δ defines all Γ’s variables and s =Γ= t implies s =Δ= t. Let this preorder induce an equivalence on contexts ≡
We say that Δ is a Γ-unifier of Γ-terms s and t if Γ ≤ Δ and s =Δ= t. Given such a Γ, s, and t, our first-order unification procedure should deliver a minimal Γ-unifier of s and t.
We’ll need one more tool. We say (Θ, Ψ) pivots Δ about t if Θ;Ψ is a permutation of Δ with Θ the shortest such that t is a Θ-term. That is, Θ is just the bit of Γ on which t actually depends. It’s easy to compute these things: pivot(Δ,{},t,{}) pivots Ψ about t, where
pivot({},Θ,t,Ψ) = (Θ, Ψ)
pivot(Δ;x d,Θ,t,Ψ) = pivot(Δ,x d;Θ,t,Ψ) if x occurs in Θ or t
pivot(Δ;x d,Θ,t,Ψ) = pivot(Δ,Θ,t,x d;Ψ) otherwise
We’ll need to pivot in order to maintain the scope invariants in the formation of contexts.
Now we can present unification relationally. Firstly, unification for sequences of equations.
Γ []→ Γ
Γ [s=t, Q]→ Θ :- Γ s=t-> Δ ∧ Δ [Q]→ Θ
Next, unification for individual equations. Firstly, rigid-rigid problems just split.
Γ c(s1,..,sn)=c(t1,..,tn)→ Δ :-
Γ [s1=t1,..,sn=tn]→ Δ
Variable-variable problems either solve or expand whichever variable is the more local. I’ll leave out the symmetric cases.
Γ;x?;Δ x=y→ Γ;y=x;Δ :- y in Γ
Γ;x=s;Δ x=y→ Θ;x=s;Δ :- y in Γ ∧ Γ y=s→ Θ
What if we have a variable and a constructor? If the variable is defined…
Γ;x=s;Δ x=x*c(t1,..,tn)→ Θ :- Γ;x=s;Δ s=c(t1,..,tn)→ Θ
…we can eliminate it from the problem. I write x*blah for blah not containing x. Meanwhile, if the variable is a hole, we may be able to fill it, but we must shift everything our term depends on leftwards, so that the new definition of x is properly scoped. That’s just what pivoting does!
Γ;x?;Δ x=c(t1,..,tn)→ Γ;Θ;x=c(t1,..,tn);Ψ :-
pivot(x?;Δ,{},c(t1,..,tn),{}) = (Θ, x?;Ψ)
Why bother? Well, you might be interested in maintaining dependency invariants within the variables involved in your problems. Unification might just be one process involved in some richer problem-solving domain, where tracking dependency is important. That’s certainly the Epigram situation: we have other stuff besides holes and lets in our contexts. But as we’ll see next time, this approach pays off even if you’re just in the Hindley-Milner situation. If you want to start thinking about it, try to imagine how you might enrich our current notion of context so that it becomes the control structure for a type checker…
PS I have the code for the above, but I’ll post it later. Drop me a line if you’d like to see it sooner.