[Haskell-cafe] ANN: unification-fd 0.6.0

wren ng thornton wren at freegeek.org
Fri Feb 17 19:05:58 CET 2012 

--------------------------------------------
-- unification-fd 0.6.0
--------------------------------------------

The unification-fd package offers generic functions for single-sorted 
first-order structural unification (think Prolog programming or 
Hindley--Milner type inference)[1][2]. I've had this laying around for a 
few years, so I figured I might as well publish it.

An effort has been made to try to make this 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 supported[3]:

     Rank2Types
     MultiParamTypeClasses
     FunctionalDependencies -- Alas, necessary for type inference
     FlexibleContexts       -- Necessary for practical use of MPTCs
     FlexibleInstances      -- Necessary for practical use of MPTCs
     UndecidableInstances   -- For Show instances due to two-level types


--------------------------------------------
-- Changes (since 0.5.0)
--------------------------------------------

* The kind of variables has been changed from *->* to *. Thus, the 
definition of MutVar is now exactly the free monad generated by t on v:

     data MutTerm v t
         = MutVar  !v
         | MutTerm !(t (MutTerm v t))

This is a major API-breaking change, however it only affects the type 
level, and should only affect you if you're using the functions 
class-polymorphically or if you've defined your own variable types.


--------------------------------------------
-- Description
--------------------------------------------

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).

* Their implementation uses path compression, which we retain. Though we 
modify the compression algorithm in order to make sharing observable.

* In addition, we perform aggressive opportunistic observable sharing, a 
potentially novel method of introducing even more sharing than is 
provided by the monadic bindings. Basically, we make it so that we can 
use the observable sharing provided by the previous optimization as much 
as possible (without introducing any new variables).

* And we remove the notoriously expensive occurs-check, replacing it 
with visited-sets (which detect cyclic terms more lazily and without the 
asymptotic overhead of the occurs-check). A variant of unification which 
retains the occurs-check is also provided, in case you really need to 
fail fast for some reason.

* Finally, a highly experimental branch of the API performs *weighted* 
path compression, which is asymptotically optimal. Unfortunately, the 
current implementation is quite a bit uglier than the unweighted 
version, and I haven't had a chance to perform benchmarks to see how the 
constant factors compare. Hence moving it to an experimental branch.

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
--------------------------------------------

[1] At present it does not appear amenable for higher-rank structural 
unification (a la HMF, MLF, or other System F type systems). The Dyna 
code from which this package was based had such features, though the 
previous implementation doesn't fit with the simplified model of 
unification used in this package. It's on my todo list, and if you have 
any suggestions, feel free to contact me.

[2] At present it is only suitable for single-sorted (aka untyped) 
unification, a la Prolog. In the future I aim to support multi-sorted 
(aka typed) unification, however doing so is complicated by the fact 
that it can lead to the loss of MGUs; so it will likely be offered as an 
alternative to the single-sorted variant, similar to how the weighted 
path-compression is currently offered as an alternative.

[3] With the exception of fundeps which are notoriously difficult to 
implement. However, they are supported by Hugs and GHC 6.6, so I don't 
feel bad about requiring it. Once the API stabilizes a bit more I plan 
to release a unification-tf package which uses type families instead, 
for those who feel type families are easier to implement or use. There 
have been a couple requests for unification-tf, so I've bumped it up on 
my todo list.


--------------------------------------------
-- References
--------------------------------------------

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.
     <http://www.cs.uu.nl/research/techreps/repo/CS-2008/2008-027.pdf>

Oleg Kiselyov, Chung-chieh Shan, Daniel P. Friedman, and
     Amr Sabry (2005) /Backtracking, Interleaving, and/
     /Terminating Monad Transformers/, ICFP.
     <http://www.cs.rutgers.edu/~ccshan/logicprog/LogicT-icfp2005.pdf>

Tim Sheard (2001) /Generic Unification via Two-Level Types/
     /and Paramterized Modules/, Functional Pearl, ICFP.
     <http://web.cecs.pdx.edu/~sheard/papers/generic.ps>

Tim Sheard & 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.
     <http://web.cecs.pdx.edu/~sheard/papers/JfpPearl.ps>

Wouter Swierstra (2008) /Data types a la carte/, Functional
     Pearl. JFP 18: 423--436.
     <http://www.cs.ru.nl/~wouters/Publications/DataTypesALaCarte.pdf>


--------------------------------------------
-- Links
--------------------------------------------

Homepage:
     http://code.haskell.org/~wren/

Hackage:
     http://hackage.haskell.org/package/unification-fd

Darcs:
     http://community.haskell.org/~wren/unification-fd

Haddock (Darcs version):
 
http://community.haskell.org/~wren/unification-fd/dist/doc/html/unification-fd

-- 
Live well,
~wren

More information about the Haskell-Cafe mailing list