Unification, comparison

[Raphael Collet]

Filip Konvička wrote:
> Since the constraint store is monotonic, I thought that the equality 
> constraints (or even the equality test results) were cached in some way. 

No, they're not.  And such a cache is hard to maintain, since the 
garbage collector moves data around (and thus references change).

> I was not sure about the equality test, but I thought it that was clear 
> for unification (I did have the idea of one of the variables 
> "disappearing", which - as it seems - actually is the case only if the 
> variable is free).
> 
> If making one of the variables being unified point to the other data 
> structure is difficult, why not have a cache of *variables* that have 
> been explicitly unified/tested for equality? (This may be stupid, but I 
> wonder what would be the performance with such modification...)

In Mozart's implementation, bound variables immediately disappear from 
memory!  Only unbound variables have an explicit representation. 
Therefore in your example, no representation of a variable is involved 
in the unification T1=T2.  It's only comparing data structures.

In practice, your optimization will not pay off, except in rare cases. 
First, most programs simply never use such unifications.  Note that 
pattern matching does not use unification either.  And even when you 
unify two records A and B, you often write you program such that one of 
both identifiers is no longer used.  Therefore one of both data 
structures will be garbage collected.

Actually, there are two types of structural data for which unicity is 
ensured in memory: atoms and record arities.  Comparison is therefore 
simply reference comparison for those.  The efficiency of record arity 
comparison pays off in unification, of course...

Feel free to send more ideas!

Cheers,
raph