[Haskell-cafe] Associative Commutative Unification

[John D. Ramsdell]

The Haskell typechecker contains a nice example of a unifier for
freely generated terms.  My focus is on equational unification, but
thanks anyway.

John

On Sun, Jul 6, 2008 at 10:38 PM, Don Stewart <dons at galois.com> wrote:
> ramsdell0:
>> I'd like to write an obviously correct implementation of a unifier, a
>> program that when given two terms, finds a substitution that makes the
>> two terms equal.  The phrase "obviously correct" is meant to imply
>> that the clarity of the code trumps efficiency.  As near as I can
>> tell, high performance unifiers are full of side-effects, and
>> achieving the same performance without side-effects in Haskell is
>> difficult or impossible.
>>
>> In contrast, it is easy to write obviously correct Hasklell
>> implementations of unifiers for freely generated term algebras.  One
>> can use Lawrence Paulson's code in ML for the Working Programmer as a
>> template or follow Martelli and Montanari's simple set of rules.
>>
>> My problem is one of my operators is multiplication, which is
>> associative and commutative.  These two properties make unification
>> much more difficult.  Mark Stickel described a complete unification
>> algorithm for this problem, but the task of translating his
>> description into an obviously correct Haskell program appears to be
>> difficult.  For example, the algorithm requires the generation of the
>> basis of solutions to linear homogeneous diophantine equations.  I
>> haven't located an algorithm for this part yet.
>>
>> If you have experience implemented equational unification in Haskell,
>> please share it.
>
> "Typing Haskell in Haskell" lives here,
>
>    http://hackage.haskell.org/cgi-bin/hackage-scripts/package/thih
>
> "a Haskell program that implements a Haskell typechecker, thus providing
> a mathematically rigorous specification in a notation that is familiar
> to Haskell users. We expect this program to fill a serious gap in
> current descriptions of Haskell, both as a starting point for
> discussions about existing features of the type system, and as a
> platform from which to explore new proposals"
>
> Might be useful as a starting point.
>
> -- Don
>