A small implementation of higher-order unification
A simple, concise implementation of Huet's algorithm. Written because it's difficult to translate the simple prose explanations of algorithms often adopted by the unification community to a working piece of code. The code is documented fully in
An example of how higher-order unification might be used may be found in
src/Client.hswhich provides a simple type-inference/checking algorithm for a dependently typed language with
Type : Type.