[TYPES] Complexity of row unification

[Francois Pottier]

Dear Henning,

On Sun, Feb 13, 2005 at 03:34:25AM +0000, Henning Makholm wrote:

> In the absence of such distribution it is straightforward to bound a
> pedestrian implementation of the unification algorithm by
> O(nm²*alpha(n)), where n is the size of the original equation set and
> m is the number of different labels it mentions.

This sounds about right. I don't have a proof that this is indeed an
upper bound, but I do know it is a lower bound, i.e. the standard row
unification algorithm does exhibit this behavior in the worst case.

> Unless I'm much mistaken, just a tiny bit of ingenuity will get it down to
> O(nm*alpha(n)),

Sounds plausible, although my own attempts, which involved sorting
labels, brought up an additional log(m) factor, I think.

I did not publish anything about this because I hoped to also deal with
distribution of type constructors over rows. As you mention, this made the
problem more difficult, and I did not come up with a good algorithm.

> but neither of these bounds seem to be mentioned even in
> passing at the places where I've tried looking for them.

Indeed, the literature says nothing about the complexity of row unification.
I have published a paper about the complexity of solving nonstructural
subtyping constraints that involve rows (in LICS'03).

-- 
François Pottier
Francois.Pottier at inria.fr
http://pauillac.inria.fr/~fpottier/