Higher-Order Dynamic Pattern Unification for Dependent Types and Records

摘要

Abstract. While higher-order pattern unification for the An-calculus is decidable and unique unifiers exists, we face several challenges in practice: 1) the pattern fragment itself is too restrictive for many applications; this is typically addressed by solving sub-problems which satisfy the pattern restriction eagerly but delay solving sub-problems which are non-patterns until we have accumulated more information. This leads to a dynamic pattern unification algorithm. 2) Many systems implement λ~(II∑) calculus and hence the known pattern unification algorithms for λ~(II) are too restrictive.rnIn this paper, we present a constraint-based unification algorithm for λ~(II∑)-calculus which solves a richer class of patterns than currently possible; in particular it takes into account type isomorphisms to translate unification problems containing ∑-types into problems only involving II-types. We prove correctness of our algorithm and discuss its application.