[mercury-users] Modular data-abstraction and mostly unique modes.

[Peter Schachte]

On Wed, 7 Jan 1998, Fergus Henderson wrote:

> Well, instantiation information and uniqueness are different, but they
> are very closely linked -- so closely as to be pretty much
> inextricable, I think.  For example, if a variable is not uniquely
> referenced, then you cannot be sure that it is free -- because it may
> have been bound via one of the other references.
> 
> If anyone has ideas about how to improve on the current design,
> please share them!

Here's a general idea, with no specific proposal.

I think it might be easier to think about modes if you separated the
`required' from the `enforced' information about a predicate.  In the case
of instantiatedness, you'd specify which (parts of) which arguments are
required to be instantiated, plus what the instantiation dependencies are. 
For example, for append, you'd want to say that on successful termination,
the tail of the third list is ground iff the tails of the first two are, and
the elements of the third list are ground iff the heads of the first two
are.  You might want to also require that the tails of the first or third
argument are ground on call.  By ``tails of a list being ground'' I mean
that the ``spine'' of the list is all bound, but the heads of the list
needn't be.  Thus to compute the instantiation state of variables after a
call, you simply conjoin the state before the call with the `enforced' part
of the mode of the called predicate.  This works because variables can only
become more instantiated due to a call.  You can also easily check if the
variables in the call satisfy the `required' part of the mode. 

Uniqueness works the other way:  variables can only become less unique due
to a call, so the `enforced' information you want about that is actually
negative, in a way.  Probably the best thing would be to have possible
sharing information plus required uniqueness.  Unfortunately, this would be
much more verbose information.

For the distinction between mostly and all {dead,unique}, you'd really want
to know the determinacy of the calling context.  And of course, each mode
has a ``best'' determinacy it is capable of (eg, if a det proc is called in
a semidet context the result is semidet).  So again we have `required' and
`enforced' information. 

Coming up with a syntax for all this is another matter entirely.


-Peter Schachte			| When choosing between two evils, I always
pets at cs.mu.OZ.AU		| like to try the one I've never tried before.
http://www.cs.mu.oz.au/~pets/	| -- Mae West 
PGP key available on request	|