[mercury-users] Uniqueness modes etc

[Zoltan Somogyi]

On 08-Jan-2004, Dr Mark H Phillips <mark at austrics.com.au> wrote:
>   :- 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.

That is because changingf knows the type of the state to be an int.
If you hide the type of the state as I suggested, Mercury code can't
"mess with the process".

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

Not unless you hide the types of the mutvar and/or the store, at which
point using mutvars becomes unnecessary.

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

Using nb_references is fundamentally impure *semantically*, and nothing
an implementation can do can make it pure.

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

That depends on whether the states can ever interact. If yes, I would
probably use one state, if no, I would use separate states.

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