[mercury-users] Uniqueness modes etc

[Fergus Henderson]

On 29-Dec-2003, Dr Mark H Phillips <mark at austrics.com.au> wrote:
> Thanks for your helpful response!
> 
> On Mon, 2003-12-29 at 08:44, Fergus Henderson wrote:
> > On 24-Dec-2003, Dr Mark H Phillips <mark at austrics.com.au> wrote:
> > >   :- pred r(int, int, int, int).
> > >   :- mode r(di, uo, in, out) is det.
> > 	r(X, Y, N, Fn) :- ....
> [snip]
> > 	X = X_0,
> > 	Y = X_0,
> > 	Q = (pred(N::in, Fn::out) is det :- r(X, Y, N, Fn))
> > 
> > > Now presumably q could be "applied" to several different n, producing
> > > in turn several different fn.  Now r is referentially transparent,
> > > but because q has uniqueness modifying behaviour hidden away inside
> > > the "currying", q acts as if it is referentially opaque.  Ie, on each
> > > application, x_0 may be modified, potentially giving rise to different
> > > q behaviour down the track.
> > 
> > Indeed, if code like this was allowed, that would be a problem.
> 
> But would it really be a problem?  This is what I am not sure about.

Yes, it would really be a problem.
Several problems, actually:
	- the meaning of "unique" insts would be violated
	- referential transparency would be lost
	- soundness would be lost

> It seems very similar to what DCG does.  If I am understanding DCG
> correctly, what it does is to hide a thread of state variables from the
> user.  If the compiler were to accept:
> 
>   Q = (pred(N::in, Fn::out) is det :- r(X_0, X_0, N, Fn))
> 
> it would be interpreted as: "each time Q is evaluated, feed in
> uniqueness variable X_0 which dies, then create a new uniqueness
> variable which we will also call X_0 (okay because the old X_0 is 
> dead), ready for feeding in next time Q is evaluated".

This is an operational semantics.  The problem is that this code would
have no declarative semantics, i.e. no meaning in predicate logic.
There is not even any (local) translation which you could apply
to give this code a declarative semantics.

The normal meaning of

	Q = (pred(N::in, Fn::out) is det :- r(X_0, X_0, N, Fn))

in logic would be

	(all [N, Fn] Q(N, Fn) <=> r(X_0, X_0, N, Fn))

but the operational semantics that you suggest is not sound
w.r.t. this declarative semantics.

> In this way a sequence of uniqueness state variables are destroyed
> and created, but this sequence is hidden from the user, much like
> what DCG does.  So if we allow DCG, why not this?

We allow DCGs for several reasons:

	- history: Prolog supports them

	- DCGs can be considered as mere syntactic sugar for
	  state variable threading.  That is, there is a
	  local syntactic transformation which translates
	  DCG clauses into ordinary clauses, which can then
	  be given a declarative semantics in the usual fashion.

	- it is also noteworthy you can define a declarative semantics
	  for DCGs directly, if non-DCG code which calls DCGs uses phrase/3.

> Are there theoretical problems that allowing Q would introduce, that
> DCG does not introduce? 

Yes, DCGs do not violate the meaning of "unique" insts,
and nor do the lose referential transparency or soundness.

> > If 
> > you _want_ this kind of behaviour, then I think the right way of modelling
> > it in Mercury would probably be to use a "mutvar" -- see the "store" module
> > in the Mercury standard library.
> 
> Thanks for the suggestion!  I've done a google search and read a few
> things which have given me a rough idea of the concept (I think!).
> 
> So using this approach I think what I would be doing is something
> like this:
> 
>   :- pred r(mutvar(int, S), int, int, S, S)
>   :- mode r(in, in, out, di, uo) is det.
>   r(X, N, Fn) --> ....
>   X_0 ....
>   Q = (pred(N::in, Fn::out, ::di, ::uo) --> r(X_0, N, Fn))

That's basically right.

> (I might have got some of the syntax a bit wrong.)

Yes, the declaration for `r' should have a `store(S)'
type class constraint,

	:- pred r(mutvar(int, S), int, int, S, S) <= store(S).
	:- mode r(in, in, out, di, uo) is det.

and there should not be a "::" in front of the "di" and "uo"
in the lambda expression:

	Q = (pred(N::in, Fn::out, di, uo) --> r(X_0, N, Fn))

> In this way I could then pass Q to some other procedure which
> has no knowledge of X_0.  All the procedure knows is that it
> can use Q to pass in an N and get out an Fn, and that behind
> the scenes (via DCG on a list of store variables) there are
> state changes happening, hence there is no guarantee that
> passing in the same N twice will give the same Fn each time.

Right.

> This approach seems good.  For example it would allow me to 
> write a generic, yet efficient, procedure which essentially 
> takes a sequence of integer permutations as input and 
> computes the result of applying these permutations to 0 a 
> certain number of times (10 times for example).
> 
> Let me explain what I mean.  Q is effectively a changing
> function taking an int to an int.  If each of these functions is
> one-to-one and onto (each representing a shuffling of the 
> integers) then each is a permutation on the set of integers.
> My procedure starts with 0 and applies Q to get the result
> of applying the first permutation.  It then takes this result
> and applies Q to it, effectively applying the second
> permutation.  It repeats this operation 10 times and returns
> the final result.
> 
> Because I "pass in" the sequence of integer permutations via
> a mechanism of uniqueness based mutation, there is the potential
> for this sequence to be generated in a very efficient fashion.
> In addition, because I am currying the mutvar, I am hiding the
> details of the mutation from my procedure, hence ensuring that
> my procedure is generic --- ie will work equally well with any
> sequence of integer permutations passed in this way.
> 
> However, this approach has its limitations (I think).  It is
> okay if my procedure only applies the first 10 permutations
> generated, but what if I want it to apply the first M 
> permutations where M is an input variable?  If I understand
> the DCG mechanism correctly, this won't work.  (Perhaps
> I am wrong about this??)

I don't see the problem.  You can achieve this sort of thing using
recursion and if-then-else:

	 apply_repeatedly(M, Q) -->
	 	(if { M = 0 } then
			{ true }
		else
			Q,
			apply_repeatedly(M - 1, Q)
		).

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
The University of Melbourne         |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------