jozefg/higher-order-unification

A small implementation of higher-order unification

{
  "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"
}

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.