[m-dev.] Mostly unique

[Fergus Henderson]

On 07-Dec-1998, Peter Schachte <pets at cs.mu.OZ.AU> wrote:
> Is there a difference between mostly unique input and unique input?

Yes.  

Mostly unique input is defined as

	:- mode mui :: mostly_unique -> mostly_unique.

whereas unique input is defined as

	:- mode ui :: unique -> unique.

If the argument has initial inst `unique', as is the case for `ui' modes,
then there are guaranteed to be no references to it on backtracking.
One consequence of this is that a semidet procedure whose argument
has mode `ui' is allowed to clobber that argument before failing.

	:- mode clobber(di) is det.

	/* this is perfectly legal */
	:- mode p1(ui) is semidet.
	p1(X) :-
		clobber(X),
		fail.

	/* this one has a unique mode error */
	:- mode p2(mui) is semidet.
	p1(X) :-
		clobber(X),
		fail.

Likewise, if the argument has final inst `unique', as it the case for `ui'
modes, then there are guaranteed to be no references to it on backtracking,
so a procedure that comes after this one is allowed to clobber it without
trailing.

	:- mode p1(di, out) is nondet.
	:- mode q1(ui, out) is semidet.		% `ui' and `semidet'
	:- mode r(di, uo) is det.

	/* this one is legal */
	p1(X, W) :-
		q1(X, Y),
		r(X, Z),	/* may clobber X */
		W = f(Y, Z).

	:- mode p2(di, out) is nondet.
	:- mode q2(mui, out) is nondet.		% `mui' and `nondet'

	/* this one has a unique mode error */
	p2(X, W) :-
		q2(X, Y),
		r(X, Z),	/* mode error here */
		W = f(Y, Z).

> As far as I can see, a promise not to copy a pointer to any part of a
> term should not depend on how many solutions that predicate has, so I
> would argue there isn't a difference.  The problem with multiple
> solutions comes up when one wants to destructively modify something,
> which requires both deadness and uniqueness.

`unique' promises deadness on backtracking, as well as uniqueness.
This means that `ui' allows destructive update in some cases
where `mui' wouldn't.

> This then raises the question: is there a useful difference between
> the unique and mostly unique insts?  I'm not as sure about this, but I
> don't see this difference either.  If there isn't a meaningful
> difference, I think it would be a good thing to remove that
> distinction from the language.

Well, there is a meaningful difference.  Whether or not it is useful
is another question.

Removing the distinction would be a non-trivial exercise,
since the distinction derives directly from the distinct
definitions of `unique' and `mostly_unique'.
How would you suggest going about it?

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "Binaries may die
WWW: <http://www.cs.mu.oz.au/~fjh>  |   but source code lives forever"
PGP: finger fjh at 128.250.37.3        |     -- leaked Microsoft memo.