[mercury-users] Uniqueness modes etc

[Dr Mark H Phillips]

On Thu, 2004-01-08 at 13:25, Fergus Henderson wrote:
> > > :- pred generic(..., pred(T, T)::in(pred(di, uo) is det), T::di, T::uo) is det.

[snip]

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

Okay thanks.  I was misreading T to be a parameter rather than a
parameter type.

> > 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 it is much like Haskell say, except that variables must begin with a
capital letter.

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

Consider the following imperative process.  A non-negative integer i,
representing a sequence of booleans, is successively shifted to the
right by one, and the least significant bit extracted at each step
in the process.  At each process step a function is yielded: given
a boolean b, we return (please excuse the pseudo Haskell code)

  f_i b = not (b && (i `mod` 2))

and of course we then update the state according to

  i becomes i `div` 2

Now suppose we want to "package up" this process for use by some other
part of the program.  Ie we want a function which will take a starting
point integer i, and will return something which provides the above
process.  We could just return a pred of the form:

  :- pred changingf(bool, bool, int, int)
  :- mode changingf(in, out, di, uo) is det.

with

  changingf(F_i, B, I, Idash) :-
    F_i = not (B && (I `mod` 2)),   % not sure of Mercury syntax here
    Idash = I `div` 2.              % or here

and require the user of changingf to put the initial integer in and
thread the state changes manually as the process evolves.  But there
is nothing stopping the user "messing" with the process.  Eg, inbetween
calls to changingf, they could multiply the current I variable by 4.

What if we want to ensure that a user is _only_ allowed to use the
process in the intended way.  This is the kind of inappropriate
manipulations I am trying to prevent.  Using mutvar and store would stop
this I think.

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

Is this only a temporary difficulty.  Ie will the compiler be able to
handle this in a pure way down the track, or does this approach
fundamentally require an impure implementation?

A different question... if you have several different states evolving,
is it better to have a single store evolving and several mutvars
refering to separate parts of that store (ie the store acts as a sort
of program heap containing separate bits of allocated memory) or is
it better for each mutvar to have its own store, each evolving
separately?

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