[mercury-users] Uniqueness modes etc

[Fergus Henderson]

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

Yes.

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

In that case, use an abstract data type.

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

	:- type bits.

	:- func make_bits(int::in) = (bits::uo) is det.

	:- pred next(bool::in, bool::out, bits::di, bits::uo) is det.

	:- implementation.
	:- import_module require.

	:- type bits ---> bits(int).

	make_bits(I0) = bits(I) :-
		(if I0 >= 0 then copy(I0, I)
		else error("make_bits: negative argument")).

	next(B, FB, bits(I0), bits(I)) :-
		NextBit = (if I0 `mod` 2 = 1 then yes else no),
		FB = not(B `and` NextBit),
		I = I0 `div` 2.

	:- end_module bit_sequence.

Only code in the bit_sequence module can mess with the internal
details of the "bits" abstract data type.

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

Well, nb_reference is impure.  But there's generally no need to use
nb_reference; you can use store.mutvar instead.

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

Either way will work, and there is probably no significant efficiency
difference, so it's just a matter of programming style.  As for which
style leads to more maintainable code, that depends on the details of
your application, but in most cases I think I would be include to use
a single store.

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