[mercury-users] Uniqueness modes etc

[Ralph Becket]

Dr Mark H Phillips, Thursday,  8 January 2004:
> 
> 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.

The correct solution is to make your "state" an abstract type.  For
example:

:- module f.
:- interface.
:- import_module int, bool.

:- type f_state.			% An abstract type.

:- func new_f_state(int) = f_state.	% Initialise an f_state.

:- pred changing_f(bool, bool, f_state, f_state).
:- mode changing_f(in,   out,  di,      uo     ) is det.

:- implementation.

:- type f_state == int.			% An f_state is actually an int.

new_f_state(I) = I.

changing_f(A, B, I0, I) :-
	A = not (B && I `mod` 2),	% Or whatever...
	I = I0 `div` 2.

Now a user of module f can create an f_state, but cannot examine it and
can only manipulate it by calling changing_f/4.

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

No, it's a show-stopping semantics problem.  A purely declarative
program should not be able to observe any side effects of its operation.
nb_references break this rule.

> 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's a design decision.  For instance, the latter arrangement would
make it impossible to accidentally use a mutvar from one store to access
a different store.

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