[mercury-users] semidet vs unique updating

[Fergus Henderson]

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

Just using `mdi' and `muo' wouldn't suffice.  Firstly, it would allow
programs that shouldn't be allowed for the kind of untrailed conditional
destructive update that Michael day was looking for.  For example, the
following program should not be allowed, because it uses Q0 after the
call to queue__get(Q0, ...) has succeeded and then been backtracked over,
but if you use the mode `mdi, muo, muo' for queue__get, then it would
be allowed:

	:- mode make_queue(uo) is det.

	main -->
		{ make_queue(Q0) },
		(if { queue__get(Q0, X, Q1), X > 10 } then
			print(X), nl
		else
			print(Q0), nl
		).

Secondly, using `mdi' and `muo' would prevent untrailed destructive
update in subsequent parts of the program.  For example, the following
program would not be allowed:

	:- mode make_queue(uo) is det.
	:- mode update_queue(di, uo) is det.

	main -->
		{ make_queue(Q0) },
		(if { queue__get(Q0, X, Q1), X > 10 } then
			{ update(Q1, Q2) },
			print(Q2), nl
		else
			[]
		).

This would not be allowed because `Q1' would have inst
`mostly_unique' rather than `unique', so the call to
`update_queue(di, ...)' would be disallowed.

Instead of using `mdi' and `muo',
I think what is wanted is something like this:

	:- mode cdi == mostly_unique >> dead.

 	:- pred queue__get(queue(T)::cdi, T::uo, queue(T)::uo) is semidet.

The `mostly_unique' initial inst means that this is the only reference
for forward execution, but there might be additional references
on backtracking.  The `dead' final inst means that after the call
succeeds, there are no more references at all.

Unfortunately this is not quite enough, because in general you'd want to
use `cdi, uo' pairs, as in  and the problem would be that the current
mode checking algorithm would complain that the uo mode arguments have
inst `mostly_unique' rather than `unique' at the end of the call.

However, I think using `cdi == mostly_unique >> dead' and `uo' is
the right way to express what is wanted; I suspect that if the mode
checking algorithm was a bit more clever, it could keep track of which
mostly_unique objects were guaranteed to become unique at the end of
the call and thus be able to correctly handle cases like the
`cdi, uo, uo' mode of queue__get above.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  | "... it seems to me that 15 years of
The University of Melbourne         | email is plenty for one lifetime."
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- Prof. Donald E. Knuth
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------