Skip to content
vic

jozefg/higher-order-unification

A small implementation of higher-order unification

jozefg/higher-order-unification.json
{
"createdAt": "2017-08-05T10:23:05Z",
"defaultBranch": "master",
"description": "A small implementation of higher-order unification",
"fullName": "jozefg/higher-order-unification",
"homepage": null,
"language": "Haskell",
"name": "higher-order-unification",
"pushedAt": "2017-08-06T10:17:19Z",
"stargazersCount": 192,
"topics": [],
"updatedAt": "2025-11-05T02:20:26Z",
"url": "https://github.com/jozefg/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 explanation.md.

An example of how higher-order unification might be used may be found in src/Client.hs which provides a simple type-inference/checking algorithm for a dependently typed language with Type : Type.