Free Monads, Intrinsic Scoping, and Higher-Order Preunification
A novel approach to higher-order preunification based on the second-order abstract syntax of Fiore, data types à la carte of Swierstra, and intrinsic scoping of Bird and Patterson. Given an evaluation function and a few reasonable assumptions, we derive a higher-order preunification procedure for any object language generated freely from a bifunctor. Briefly demonstrates an application to type checking for Martin-Löf Type Theory.
Kudasov, N. (2025). "Free Monads, Intrinsic Scoping, and Higher-Order Preunification." In Trends in Functional Programming (TFP 2024), Springer, pp. 22–54. ISBN 978-3-031-74558-4.