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

[Lee Naish]

In message <Pine.GSO.3.95.980108103920.19930B-100000 at cat.cs.mu.OZ.AU>pets wrote:
>On Wed, 7 Jan 1998, Fergus Henderson wrote:
>
>> Well, instantiation information and uniqueness are different, but they
>> are very closely linked
>> 
>> 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. 

The enforced component is what is covered by my work on "declarative
modes".  See http://www.cs.mu.oz.au/~lee/papers/modes/ (plus more
recent work extending the mode language and implementing a mode checker).

>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.

Even the enforced mode dependencies can get a bit verbose if you include
all of them.  Eg, to use append in lots of modes you might want to say
that the last argument will be instantiated to a list iff the second
argument is, the first argument will always be instantiated to a list
and the multiset of elements in the last argument equals the multiset
union of the elements in the first two arguments (using multisets allows
us to infer uniqueness info; sets would not).  My mode checker accepts
the following syntax to express these dependencies:

:- mode append(X=list(T1), Y=list(T2), Z=list(T3)):
	Y <-> Z,	% Y is list(any) iff Z is list(any)
	([] -> X),	% X is list(any)
        T1 + T2 <==> T3.% multiset constraint on list elements

Although this seems somewhat verbose, it is much more concise than the
infinite set of Mercury modes which can be inferred from it:-).  For
common cases where not so many different modes are required, simpler
declarations (preferably with some syntactic sugars) suffice.  Also,
inferring declarations such as the one above are possible (a trivial
extension to what I have implemented, theoretically), though its likely
to be rather slow unless there is at least some help from the programmer.

This kind of "enforced" information plus some declarations for
"required" information could replace the Mercury mode declarations.
However, there are a couple of disadvantages.  First, the output insts
and uniqueness become implicit, losing possibly valuable documentation
and checks.  Second, the determinism info still has to go somewhere.

The more mode dependencies you throw together, the harder it is to attach
the determinism information in an orthogonal way.  I have toyed with
constraints which include determinism (or functional dependency) info.
For example, the constraint below could be added to the declaration for
append:
	X + Y ->> Z % Z is a function of X and Y
I guess I could come up with yet another arrow corresponding to semidet:
	Y + Z -?> X % X is a "partial function" of Y and Z
I'm not entirely happy with this kind of thing, partly because of the
divergence of declarative and procedural notions of determinism when you
can have multiple proofs of the same thing.  The Mercury determinism
system is more complicated than this also.

>For the distinction between mostly and all {dead,unique}, you'd really want
>to know the determinacy of the calling context.

To be more precise, the contexts from the times when the data structures were
created.

	lee