unification-fd: Simple generic unification algorithms.

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Generic functions for single-sorted first-order structural unification (think of programming in Prolog, or of the metavariables in type inference).

[Skip to Readme]


Versions 0.5.0, 0.6.0, 0.7.0, 0.8.0, 0.8.1, 0.9.0, 0.10.0,, 0.11.0, 0.11.1, 0.11.1, 0.11.2
Change log CHANGELOG
Dependencies base (>=4.5 && <5), containers, logict (>=0.4 && <0.7.2), mtl (>=2.0) [details]
License BSD-3-Clause
Copyright Copyright (c) 2007--2021 wren gayle romano
Author wren gayle romano
Maintainer winterkoninkje@gmail.com
Category Algebra, Algorithms, Compilers/Interpreters, Language, Logic, Unification
Home page https://wrengr.org/software/hackage.html
Source repo head: git clone https://github.com/wrengr/unification-fd
Uploaded by WrenRomano at 2021-02-25T00:46:41Z




Maintainer's Corner

For package maintainers and hackage trustees

Readme for unification-fd-0.11.1

[back to package description]


Hackage version Build Status Dependencies

The unification-fd package offers generic functions for single-sorted first-order structural unification (think of programming in Prolog, or of the metavariables in type inference)12. The library is sufficient for implementing higher-rank type systems à la Peyton Jones, Vytiniotis, Weirich, Shields, but bear in mind that unification variables are the metavariables of type inference— not the type-variables.

Build Warnings/Errors

This is a simple package and should be easy to install; however, on older setups you may encounter some of the following warnings/errors. If during building you see some stray lines that look like this:

mkUsageInfo: internal name? t{tv a7XM}

Feel free to ignore them. They shouldn't cause any problems, even though they're unsightly. This should be fixed in newer versions of GHC. For more details, see:


If you get a bunch of type errors about there being no MonadLogic instance for StateT, this means that your copy of the logict library is not compiled against the same mtl that we're using. To fix this, update logict to use the same mtl.


An effort has been made to make the package as portable as possible. However, because it uses the ST monad and the mtl-2 package it can't be H98 nor H2010. However, it only uses the following common extensions which should be well supported3:


The unification API is generic in the type of the structures being unified and in the implementation of unification variables, following the two-level types pearl of Sheard (2001). This style mixes well with Swierstra (2008), though an implementation of the latter is not included in this package.

That is, all you have to do is define the functor whose fixed-point is the recursive type you're interested in:

-- The non-recursive structure of terms
data S a = ...

-- The recursive term type
type PureTerm = Fix S

And then provide an instance for Unifiable, where zipMatch performs one level of equality testing for terms and returns the one-level spine filled with pairs of subterms to be recursively checked (or Nothing if this level doesn't match).

class (Traversable t) => Unifiable t where
    zipMatch :: t a -> t b -> Maybe (t (a,b))

The choice of which variable implementation to use is defined by similarly simple classes Variable and BindingMonad. We store the variable bindings in a monad, for obvious reasons. In case it's not obvious, see Dijkstra et al. (2008) for benchmarks demonstrating the cost of naively applying bindings eagerly.

There are currently two implementations of variables provided: one based on STRefs, and another based on a state monad carrying an IntMap. The former has the benefit of O(1) access time, but the latter is plenty fast and has the benefit of supporting backtracking. Backtracking itself is provided by the logict package and is described in Kiselyov et al. (2005).

In addition to this modularity, unification-fd implements a number of optimizations over the algorithm presented in Sheard (2001)— which is also the algorithm presented in Cardelli (1987).

These optimizations pass a test suite for detecting obvious errors. If you find any bugs, do be sure to let me know. Also, if you happen to have a test suite or benchmark suite for unification on hand, I'd love to get a copy.

Notes and limitations


Luca Cardelli (1987)
Basic polymorphic typechecking. Science of Computer Programming, 8(2): 147–172.
Atze Dijkstra, Arie Middelkoop, S. Doaitse Swierstra (2008)
Efficient Functional Unification and Substitution. Technical Report UU-CS-2008-027, Utrecht University.
Simon Peyton Jones, Dimitrios Vytiniotis, Stephanie Weirich, Mark Shields (2007)
Practical type inference for arbitrary-rank types. JFP 17(1). The online version has some minor corrections/clarifications.
Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and Amr Sabry (2005)
Backtracking, Interleaving, and Terminating Monad Transformers. ICFP.
Tim Sheard (2001)
Generic Unification via Two-Level Types and Parameterized Modules, Functional Pearl. ICFP.
Tim Sheard and Emir Pasalic (2004)
Two-Level Types and Parameterized Modules. JFP 14(5): 547–587. This is an expanded version of Sheard (2001) with new examples.
Wouter Swierstra (2008)
Data types à la carte, Functional Pearl. JFP 18: 423–436.

At present the library does not appear amenable for implementing


At present it is only suitable for single-sorted (aka untyped)


With the exception of fundeps which are notoriously difficult