[mercury-users] Uniqueness modes etc
fjh at cs.mu.OZ.AU
Thu Jan 8 16:56:06 AEDT 2004
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.
> > > 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.
> 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.
:- 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.
:- 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
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
More information about the users