Semantics of pattern unification

We propose a notion of syntax with metavariables that generalises Miller’s decidable pattern fragment of second-order unification for simply typed λ -calculus. Using categorical semantics, we show that, under some conditions, a generalisation of Miller’s unification algorithm applies. To illustrate our semantic analysis, we implemented our generic unification algorithm in Agda. The syntax with metavariables given as input of the algorithm is specified by a notion of signature generalising binding signatures, covering a wide range of examples, including ordered λ -calculus and (intrinsic) polymorphic syntax such as System F. Although we do not explicitly handle equations, we also tackle simply typed λ -calculus modulo β - and η -equations (Miller’s original setting) by working on the syntax of normal forms.