On 7/28/12 4:59 AM, Conor McBride wrote:
It's a bit of a tangent, but the context I have in mind is that all the polynomials are Foldable, Traversable and (the much neglected) HalfZippable (the idea and the name I learned from Roland Backhouse).
class Functor f => HalfZippable f where halfZip :: f a -> f b -> Maybe (f (a, b))
which is a zip that can abort in case of shape mismatch. If a functor is both Foldable and HalfZippable, then its (least) fixpoint has a decidable equality (you try to zip each node together, and if you succeed, you foldMap the equality test over the paired children), and moreover, its free monad (chucking in a representation of "free variables") has a unification algorithm.
Indeed. Though it's worth noting that in unification-fd[1] I recently switched from that exact type to the more powerful: class Traversable f => Unifiable f where zipMatch :: f a -> f a -> Maybe (f (Either a (a, a))) The benefit of this latter type is that it allows the instance to declare success for unification sub-problems--- which is necessary for things like unification of feature-structures. The downside is that, since you only get one type for the solved subproblems, you lose the ability to distinguish the type variables a and b (not that it matters for unification). [1] http://hackage.haskell.org/packages/archive/unification-fd/0.8.0/doc/html/Co... -- Live well, ~wren