Towards Generic Higher-Order Unification Implementations in Haskell

Watch this 17-minute conference talk from WITS 2025 workshop where researchers from Innopolis University present their work-in-progress on implementing generic higher-order unification algorithms in Haskell. Learn how they extend the Free Foil library with parametrized metavariables to achieve a limited version of Second-Order Abstract Syntax, implementing generalized versions of Huet's preunification and Miller's higher-order pattern unification algorithms. The researchers discuss their plans to develop a dedicated benchmark suite for comparing standalone unification algorithms, with the ultimate goal of creating a library of reusable and performant language-agnostic higher-order unification algorithms to support the development of systems like dependently typed languages. This presentation was sponsored by ACM SIGPLAN and delivered at the WITS 2025 workshop on January 20, 2025.