Towards Generic Higher-Order Unification Implementations in Haskell
summary
Claims a reusable Haskell library approach that uses Free Foil and a separate signature for parameterised metavariables to produce a limited Second‑Order Abstract Syntax and to run unification algorithms over it. The prototype implements second‑order matching (no fresh meta generation), a preliminary test corpus of untyped higher‑order problems, and plans to generalize Huet preunification and Miller pattern unification; scalability and performance tuning remain unresolved.
AI-written summary · about
chapters (10)
- 0:00Introduction
- 1:50Higher-order unification
- 3:15Reusing implementations
- 5:22Generic first-order inspiration
- 6:25Second-order syntax
- 8:39Intrinsically scoped syntax
- 10:25Second-order matching
- 11:51Current results
- 12:55Improvements and scalability
- 14:33Q&A
related talks
27mHaskell equations, thirty-eight years later
16mSyntax-Generic Operations, Reflectively Reified (Extended Abstract)
41mIntroduction to the Unison programming language
01h 14mBeyond Free Monads
57mApplied category theory and abstract algebra
36mGoing Higher
16mDigging for Fold: Synthesis-Aided API Discovery for Haskell
42mFunctional interpreters and you