[m-dev.] discussion about the implementation of compact type representations

[Zoltan Somogyi]

On Mon, 30 Oct 2017 12:42:02 +1100, Michael Day <mikeday at yeslogic.com> wrote:

> > Attached is a set of proposals that I would like your opinions on.
> > Which parts do you agree with and which parts do you disagree with?
> > Do you have a better idea for any component?
> 
> Sounds sensible to me, although I'm curious about why types with user 
> defined equality can't be no-tag types.

Consider a type such as

:- type t1
   --->  f(t2) where unification is u1, comparison is c1.

If we consider t1 to be a notag type, then we will treat values of type t1
the same way as values of type t2. The semantics of the language say
that the code for unify for t1 has to be

unify_t1(X, Y) :- u1(X, Y).

while treating it as a notag type would require it to be

unify_t1(X, Y) :- unify_t2(X, Y).

It can't be both. And the same for compare_t1.

Of course, there is nothing prohibiting us from inventing a new kind of type,
a sort-of notag-lite or diet-notag, saying that types such as t1 (one
function symbol of arity 1, and user-defined compare and/or unify) belong to it,
and storing values of type t1 the same way we store values of type t2. However,
the conversion from t1 to t2 would be significantly different, because deconstructing
a value of a type with user-defined equality is an operation that takes place
in a committed choice context. In this case, that means the deconstruction
won't be det; it will be cc_multi.

To see why, consider a set implemented as a binary search tree, with a type such as

:- type set(T)
   ---> set(bst(T)).

A value of type set(T) represents a given set. When you unwrap it, you know
you will get a binary search tree whose elements are the elements of that set,
but you *don't* know which of the many possible BSTs that could possibly
represent that set you will get. Executing the unwrapping commits you to
exactly one of those possibilities, and the code doing the unwrapping
does *not* get to choose which one.

Such code is significantly harder to get right than code that does not involve
committed choice. This is one reason why user defined unify and compare preds
are relatively rare. We have in the past tried out specifying unification and comparison
predicates for some of the set types in the standard library, but (for reasons that
I can't remember right now) we never committed them.

I therefore don't think there is any urgency in trying to optimize the representation
of such types.

Zoltan.