[mercury-users] semidet vs unique updating

[Mark Brown]

On 19-Oct-2001, Mark Brown <dougl at cs.mu.OZ.AU> wrote:
> 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.
> 

Unfortunately, I'm going to have to take this back.  The promise *is* a
lie, because failure may occur after the exit from get/3 --- it is not
enough to verify that no failure occurs in the rest of the goal, we also
need to ensure that calls to get are not backtracked over from the outside.
For example, the following goal could cause problems:

	get(Q0, T1, Q1), get(Q1, T2, Q)

If the first call succeeds then the queue may be destructively updated,
but if the second call then fails we will backtrack over the first call
without undoing the destructive update.

I should have listened to my own advice and let the compiler choose the
best implementation.  :(

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