[Haskell-cafe] Associative Commutative Unification
John D. Ramsdell
ramsdell0 at gmail.com
Tue Jul 8 08:24:45 EDT 2008
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
>
More information about the Haskell-Cafe
mailing list