Comments on The Alien Tongue: recursive types, unification, sharing

Ok, I've implemented Huet's algorithm, and...

2011-02-04T17:48:15.868-08:00

Ok, I've implemented Huet's algorithm, and -- fingers crossed -- it appears to work, and to correctly handle infinite types. The fledgling self-hosted Irken types in 11s now, so the performance is also looking good. The extra scrutiny was good, I found a few subtle problems that are now fixed.

Found an excellent reference for this, that gives ...

2011-02-03T12:17:07.265-08:00

Found an excellent reference for this, that gives Huet's quai-linear algorithm, *and* handles 'infinite unification'. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.64.8967

So Huet's algorithm, along with path compression, runs in 'quasi-linear' time which is O(nα(n)), where α is the inverse of Ackerman's function. Never thought I'd see a real-world appearance of Ack.

Quoth Remy: "In order to obtain maximum shari...

2011-02-02T18:47:58.908-08:00

Quoth Remy: "In order to obtain maximum sharing, non-variable terms should never be copied. Hence, rule Decompose requires that one of the two terms to be decomposed is a small term—which is the one used to preserve sharing."

I think this means to always leave a tvar attached to a term. That variable acts like a rendezvous for all the identical uses of that type - including recursive ones.