Adam Gundry and Conor McBride
A higher-order unification algorithm is an essential component of a dependently typed programming language implementation, and understanding its capabilities is important if dependently typed programmers are to become productive. Miller showed that, for simply typed λ-terms in the pattern fragment (where metavariables are applied to spines of distinct bound variables), unification is decidable and most general unifiers exist. We describe an algorithm for pattern unification in a full-spectrum dependent type theory with dependent pairs (Σ-types). The algorithm exploits heterogeneous equality and a novel concept of 'twin' free variables to handle dependency. Moreover, it supports dynamic management of constraints, postponing equations that fall outside the pattern fragment in case other equations make them simpler. We aim to make sense both to language implementors and users, and to this end present our algorithm as a Haskell program.
Latest version: A tutorial implementation of dynamic pattern unification (PDF), updated 10th July 2012, rejected from POPL 2013
darcs get https://personal.cis.strath.ac.uk/adam.gundry/pattern-unify/
or download the source tarball
Up to Adam Gundry's home page