[mercury-users] Uniqueness modes etc

[Fergus Henderson]

On 08-Jan-2004, Dr Mark H Phillips <mark at austrics.com.au> wrote:
> On Tue, 2004-01-06 at 19:01, Zoltan Somogyi wrote:
> > On 06-Jan-2004, Dr Mark H Phillips <mark at austrics.com.au> wrote:
> > > The question is: how does one implement a generic
> > > computation, that itself takes a generic state-changing computation
> > > as a parameter, and yet keep the state-changing details hidden from
> > > the generic computation?
> > 
> > If by "state-changing details" you mean the details of how the state
> > changes work, it can be done trivially: give the generic computation
> > a signature like this:
> > 
> > :- pred generic(..., pred(T, T)::in(pred(di, uo) is det), T::di, T::uo) is det.
> > 
> > That is, you pass in the state-change predicate and an initial state, and
> > get back the final state. Since the state is of a polymorphic type, generic
> > can't look inside it.
> 
> Okay, so what you're saying (I think) is that by using a generic
> (polymorphic) parameter T, we can guarantee that "generic", the pred,
> can not make use of any structure that is actually passed in as T.

Right.

> By the way, should those T's actually be T0, T1, T2 and T3?

No.  They need to be all be same type T, so that "generic"
can pass the supplied state to the supplied state-change predicate,
e.g.

	generic(..., P, !S) :- ..., P(!S), ..., P(!S), ...

or equivalently

	generic(..., P, S0, S) :- ..., P(S0, S1), ..., P(S1, S).

If we instead tried to declare generic with type

	:- pred generic(..., pred(T0, T1), T2, T3).

as you suggest, and then implement it as shown above,
then we would get several type errors.
S0 is the second-last argument of "generic" and also gets passed
to the first argument of P, so we must have T3=T0.
Similarlly, because S1 gets passed to both the first and second arguments of P,
we must have T0=T1.  And because S gets passed the second argument of P
and is also the last argument of "generic", we must have T1=T2.
So all four of these type variables have to be identical.

> And what is it, in Mercury, which makes a parameter have polymorphic type?

A parameter has a polymorphic type if its declared type is (or contains)
a type variable.  A type variable is an identifier starting with a
capital letter.

If there is no declaration, then the compiler will infer a polymorphic
type if the procedure uses the variable in a way that does not depend
on its type.

> So what you've illustrated above is that, by using polymorphism, a
> generic pred can guarantee that it will only work with state in a
> generic way.  (Though it is still possible for it to stuff up the
> order of state transitions.)  But what if I want a stronger 
> guarantee: that a given state-changing computation can _never_
> have the details of its state changing played with inappropriately.

I don't understand what you're getting at here.
What kind of inappropriate manipulations are you trying to prevent?

> > If by "state-changing details" you mean you don't want generic to know
> > even that some state is being changed, then you can use mutvar, but I would
> > strongly advise against this if the first approach is feasible.
> 
> How can the use of mutvar hide the fact that state is changing?  I
> thought you still needed to pass the store in and out?

I think Zoltan may have accidentally confused the store.mutvar(T)
type in the standard library with the nb_reference(T) in
extras/references/nb_reference.m.

> Why do you strongly advise against this approach?  What are the
> negatives?

The disadvantages of the nb_reference approach are that it uses impure
code.  This destroys the declarative semantics, makes the code more
difficult to reason about, inhibits compiler optimization, and in Mercury
requires any code which uses it to be explicitly annotated as "impure".

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