[m-dev.] Herbrand types are canonical?

[Fergus Henderson]

On 15-Jan-2004, Ralph Becket <rafe at cs.mu.OZ.AU> wrote:
> Just a quick check: even though Herbrand types have their own
> unification and comparison predicates, they are nevertheless canonical
> types?

Herbrand types are a bit of a special case.

There is more than one representation for any given ground value,
so normally they would be considered a non-canonical type.
The representations can be different because they can have
different lengths of pointer chains.  I think this is true
even if you use Parma-style bindings, where there is at most one
level of dereferencing, because the same value can be represented
using either zero or one level of dereferencing.

But it would certainly be nicer to treat Herbrand types as canonical types.
Deconstruction unifications on Herbrand types should have determinism
semidet, not cc_nondet.  However, this implies that the code for
deconstruction must not be the same as for ordinary types; it must
check for the reserved functor which represents variables and dereference
any bound variable chains.  Likewise, other operations such as
dynamic deconstruction (std_util.deconstruct) must dereference any
bound variables.  Provided that all operations dereference bound variables,
it should be OK to treat them as canonical.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------