[Agda] Sharing --- Q-combinators

[wren ng thornton]

On 10/10/12 10:42 AM, Wolfram Kahl wrote:> On the code sprint page of the
AIM that just finished, I read:
>
>   |  Sharing (call by need)
>   |      UN, NP, NAD, DG, AA, MT
>   | [...]
>   | * Day 7: If you check syntactic equality before unification, you
>   |   actually gain surprisingly much. (Saves maybe 10% in the std. library
>   |   typechecking time). We 've identified that De Bruijn indices are
messing
>   |   up sharing. Annoying! What can we do? Maybe explicit substitutions;
>   |   Maybe keep track of closed terms (so substituting in a closed term is
>   |   a noop and keeps sharing). We are going to run more experiments.
>
> Have you heard of John Harrison's Q-combinators?
> They are about sharing at the Haskell (originally ML) run-time level,
> but could still be relevant for some aspects of this --- using them would
> at least make substitution on closed terms keep sharing.

I hadn't heard of Q-combinators before (reference?), but you can see a
similar idea in use in the unification-fd[1] package. In that package I
make aggressive use of observable sharing in order to maintain the sharing
inherent in unification.

The trick I use is a bit different from Wolfram's description of
Q-combinators though. For my approach, I first ensure that we can observe
when we're trying to unify bound variables which are already unified (so
success is immediate). And second, the unification process will
reconstruct terms (both in the bindings, and in the term returned from
unification) in order to maximize the sharing induced by successful
unification (subject to not introducing any new variables). For example,
if we have:

    x |-> f(a,b)
    y |-> f(c,d)

and we run into the unification problem:

    z <- x =:= y

assuming it succeeds, we'll end up with:

    x |-> f(a',b')
    y |-> x
    z = x

where

    a' <- a =:= c
    b' <- b =:= d

Thus, the technique ensures both that we preserve sharing and that we can
observe that fact in subsequent unifications (via the first step).


The unification-fd package is only targeted at first-order unification
problems, but you could probably adapt the technique to apply to
higher-order unification as well. I'm rather busy of late, but I'd be
willing/interested to help work out the details of such a scheme.


[1] http://hackage.haskell.org/package/unification-fd

-- 
Live well,
~wren