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

[Peter Schachte]

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

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.

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.

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

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

> > But whether even that is ok or not is also unclear.  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?  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?

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?  This
seems like an important omission in Mercury's unique mode system.  I'm sure
lots of foreign code does not require its arguments to be unique on entry,
but does preserve any preexisting uniqueness.  We can infer the "preserves
but does not require uniqueness" property for Mercury code, but not for
foreign code (well, actually we could, but that's a whole new analysis
problem that would have to be addressed separately for each foreign
language).

-- 
Peter Schachte <schachte at cs.mu.OZ.AU>  What we cannot speak about we must
http://www.cs.mu.oz.au/~schachte/      pass over in silence.
Phone:  +61 3 8344 9166                    -- Wittgenstein 
Fax:    +61 3 9348 1184                
--------------------------------------------------------------------------
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
--------------------------------------------------------------------------