[m-dev.] [reuse] fixes of some naughty bugs

[Fergus Henderson]

On 12-Mar-2001, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> On Sun, Mar 11, 2001 at 04:55:10AM +1100, Fergus Henderson wrote:
> > On 11-Mar-2001, Peter Schachte <schachte at cs.mu.OZ.AU> wrote:
> > > is it fair to call a predicate pure if it
> > > destructively modifies a term in a way that leaves it equal to what it
> > > originally was, but may create new aliases?
> > 
> > So long as the aliasing respects the mode declaration,
> > I'd say yes.
> > 
> > > This is semantically pure, but
> > > operationally impure.  Would I be wrong not to declare it impure?
> > 
> > No.
> 
> My concern is that this may inhibit some optimizations we'd like to perform,

You mean that it would inhibit compiler optimizations.
That may be true, but the alternative would inhibit optimizations
by the user in procedures implemented using impure/foreign code,
e.g. as is done in the implementation of lazy__force.

> and require the compiler to be more careful.  For example,
> 
> 	X = f(Y,Z), p(X), q(Y).
> 
> If p/1 is allowed to destructively modify X in an equivalence-preserving
> way, then q/1 may be called with different copy of Y depending on in which
> order the first two goals are executed.  Reordering is no longer quite as
> safe.  Of course, there's no logical difference, but there is an operational
> difference.

Sure there's an operational difference, but that's what the
--(no-)reorder-conj option is for.

> I'm a bit concerned about doing this kind of thing on a type with a
> user-defined equivalence predicate.  Suppose you have a set type:
> 
> 	type set(T) ---> set(sorted :: bool, elements :: list(T))
> 		where equality is set_equal.

The fact that the compiler allows such declarations is an outstanding bug.
Allowing named fields in types with user-defined equality, and
treating those fields as functions, breaks referential transparency.

> Where set_equal/2 checks the sorted flags of its arguments, sorts any lists
> that aren't yet sorted, and destructively sets the sorted flag and replaces
> the list with its sorted version.  This is equivalence-preserving.  Now if I
> write
> 
> 	Elts = Set^elements, Set = Set2, Flag = Set^sorted, ...
> 
> I may wind up with an unsorted list Elts, but a Flag that says it is sorted.

With field names as functions, this is indeed very confusing --
it breaks referential transparency.  You should not be allowed to write that.

If field names are allowed in types with user-defined equality
(and I'm not sure that this is actually a good idea),
they should be predicates, not functions.  So you should have to write

	elements(Set, Elts), Set = Set2, sorted(Set, Flag)
or
	Set = set(_, Elts), Set = Set2, Set = set(Flag, _)

Yes, this may result in `Flag' being `yes' but `Elts' being unsorted.
If you want to avoid that you need to extract both `Flag' and `Elts'
in a single unification:

	Set = set(Flag, Elts), Set = Set2

That may come as a surprise.  But the same could happen in pure Mercury code,
without any destructive update, if set/2 was a function rather than a
constructor.  For example:

	:- type myset(T) ---> mkset(list(T)).

	:- func set(bool, list(T)) = myset(T).
	:- mode set(out, out) = in is nondet.
	set(IsSorted, List) = mkset(SortedList) :-
		sorted(SortedList),
		( IsSorted = yes, List = SortedList
		; IsSorted = no, list__perm(SortedList, List)
		).

	sorted(L) :- list__sort(L, L).

Given that this can happen with functions anyway, is it so much worse
to allow it to happen with constructors too?  I think your example
is a good example of exactly the kind of thing I'd like to use
user-defined equality types for, so I would certainly like to permit
those kinds of value-preserving but representation-changing destructive
updates.

I agree that there is some potential for confusion.  One thing that we
could do to reduce that is to prohibit types with user-defined equality
from having more than one functor or more than one argument, i.e. require
them all to be no-tag types.  As a matter of programming style, that is
probably good programming practice anyway.  We could go one or two steps
further and have the compiler issue a warning if this practice is not
followed or even make it mandatory.  Then you'd have to write your
example type as something like this

 	:- type set(T) ---> set(set_rep(T)) where equality is set_equal.
 	:- type set_rep(T) ---> set_rep(sorted :: bool, elements :: list(T))

and your example use of it would become either

	Set = set(set_rep(_, Elts)), Set = Set2,
	Set = set(set_rep(Flag, _))

or (preferably)

	Set = set(SetRep1), Elts = SetRep1^elements, Set = Set2,
	Set = set(SetRep2), Flag = SetRep2^sorted, ...

Either way you write it, it's clearer that the representation might be
different each time (a lot clearer with the second way).

> > why do you say it is "operationally impure"?
> > What do you mean by "operationally impure"?
> 
> I couldn't think of a better name for it.  I mean an operation that does
> something that would ordinarily be completely forbidden (it certainly
> couldn't be done in pure Mercury code), but it does it in a careful way so
> that it's logically ok.  It's guilty, but it gets off on a technicality.
> I'm being deliberately vague, because I'm not sure what properties that are
> ordinarly enjoyed by pure Mercury code, but not necessarily by foreign code,
> might be interesting.

OK, I understand what you mean.
I guess "operationally impure" is not a bad term for it.
At least I can't think of a better one ;-)

> > When I say that something is pure, I mean that it has
> > a declarative semantics, and that its operational
> > semantics is sound w.r.t. that declarative semantics.
> 
> That definition doesn't let you talk about extralogical operational
> characteristics.  Mercury's mode system lets you talk about aliasing in a
> restricted way; anything more you might want to be able to say, your
> definition of purity can't address.

Yes, I would classify such matters as mode-correctness issues
rather than purity issues.

> > > Suppose two ground terms
> > > have different types but identical representations (the same size and bit
> > > pattern).  I can't see why it wouldn't be correct for them to cohabitate.
> > > Does the Mercury language forbid it?
> > 
> > No, so long as they don't have unique modes.
> 
> Not to be pedantic, but I think you mean so long as they don't have unique
> insts at that point in the program.  Right?

Right.

> I take this to mean that a
> foreign proc whose mode requires certain arguments to be unique is
> considered buggy if it aliases them.  So Nancy's conservative strategy for
> handling foreign code could be loosened up for uniquely moded foreign code?

Right.

> Am I right that there is no way to write a foreign predicate that has both
> unique and non-unique modes without writing two copies of the code?

Well, you need two copies of the `pragma import' or `pragma foreign_proc'
declaration.  But the code itself can be defined once in a subroutine
(defined either externally or using `pragma foreign_code').

It would not be difficult to change the syntax to allow a single
`pragma import' or `pragma foreign_proc' declaration to define
multiple modes of a given procedure.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
                                    |  of excellence is a lethal habit"
WWW: <http://www.cs.mu.oz.au/~fjh>  |     -- the last words of T. S. Garp.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------