Towards Generic Higher-Order Unification Implementations in Haskell
We present work-in-progress on generic implementations of higher-order unification algorithms in Haskell. We rely on the Free Foil library for generic (in the style of data types à la carte) representation of syntax with binders. We extend Free Foil with parametrised metavariables to achieve a (limited) version of Second-Order Abstract Syntax, over which we then implement generalized versions of Huet’s preunification and Miller’s higher-order pattern unification algorithms. We also plan to work towards a dedicated benchmark suite to compare standalone unification algorithms. Our goal is to provide a library of sufficiently reusable and reasonably performant language-agnostic higher-order unification algorithms to assist development of systems such as dependently typed languages.