[mercury-users] semidet vs unique updating

[Mark Brown]

On 17-Oct-2001, Michael Day <mikeday at bigpond.net.au> wrote:
> 
> > You are reading more into the mode declaration than is there.  The mode
> > declaration says nothing about whether the queue has been modified.  In
> > fact it says nothing whatever about the relationship between the first and
> > third arguments -- this declaration would be perfectly consistent with a
> > clause that ignores the first argument and returns (unique) constant
> > values for the other two.
> 
> Very true, it doesn't say the queue is modified.
> 
> > What the declaration _does_ say about the first argument is that there
> > is only one reference to it at the point of call, and that there is
> > nowhere that needs that reference after the call.  In particular, it
> > implies the reference will not be needed on backtracking.  Making the
> > call semidet would unfortunately contradict this.
> 
> Right,
> 
> :- mode di :: unique >> dead.
> :- mode mdi :: mostly_unique >> mostly_dead.
> 
> now suppose the existence of a "could_be_dead" inst. The meaning of this
> fictitious inst is that the variable cannot be referred to if the call
> succeeds, just like the dead and mostly_dead insts. However the variable
> can still be referenced if the call fails, just like mostly_dead. However
> rather than copying it surreptitiously from a trail or whatever, the
> compiler just uses the original variable.

So you are asking for something with the same meaning as mostly_dead,
but with a better implementation?  I think the Right Thing To Do is to
use mostly_dead and let the compiler choose the best implementation it
is capable of.  In grades with trailing, optimizations like destructive
update could involve surreptitious use of the trail.  In other grades,
such optimizations may only be applied if the compiler can prove they
are safe, as Nancy said.

If you want to hand-code destructive updates of your queue without using
a trail, or you hope a future implementation will do it for you, your
best bet is to use det code and unique modes.  So my advice to anyone
writing an ADT like this would be to use the det interface:

	:- pred get_det(queue(T)::di, maybe(T)::uo, queue(T)::uo) is det.

But since your aim was to minimise the change to the original interface,
a better implementation for you could be written in terms of the above:

	:- pred get(queue(T)::mdi, T::muo, queue(T)::muo) is semidet.
	get(Q0, T, Q) :-
		not_empty(Q0, Q1),
		unsafe_promise_unique(Q1, Q2),
		get_det(Q2, yes(T), Q).

You will also need to add the following:

	% This has two arguments to work around the fact that "ui" modes
	% are not implemented.
	:- pred not_empty(queue(T)::mdi, queue(T)::muo) is semidet.
	not_empty(Q, Q) :-
		...

Note that a "promise" is required because uniqueness is stronger than
mostly-uniqueness, so the compiler needs the constraint on calling
get_det to be weakened.  Since we can see that no failure can happen
after the promise is made (assuming not_empty is correct), we know that 
the promise is not a lie, so no bad karma results.

Perhaps this will help solve your problem?

Cheers,
Mark.

--------------------------------------------------------------------------
mercury-users mailing list
post:  mercury-users at cs.mu.oz.au
administrative address: owner-mercury-users at cs.mu.oz.au
unsubscribe: Address: mercury-users-request at cs.mu.oz.au Message: unsubscribe
subscribe:   Address: mercury-users-request at cs.mu.oz.au Message: subscribe
--------------------------------------------------------------------------