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

[Peter Schachte]

On Mon, Mar 12, 2001 at 04:41:08PM +1100, Fergus Henderson wrote:
> > 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.

I can't see how the blame lies with the accessor functions.  Without them,
you can still write

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

and have the same problem.  The problem is the assumtion that structures are
not destructively modified.

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

This isn't quite the same, because reordering does not change the behavior.
You're just pointing out that nondet functions don't behave like functions,
right?  Though in this case it's a reverse mode, which is even less
surprising.  Ie, who is shocked that,

	X + _ = 4, _ + Y = 4, X + Y = Z

could wind up with Z != 4?

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

Agreed.  But maybe there needs to be some concept like impurity (only
without the stigma and without the ubiquitous declarations of impurity) to
indicate that it can happen.  This would inhibit reordering of accesses, and
perhaps inhibit some optimizations.  It would be a shame if the compiler
could never count on terms remaining fixed just so once in a great while we
could use some clever coding trick.

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

Better still, require non-canonical types (ie, types with user defined
equality) to be abstract.  Users have no business poking around inside,
anyway.  Then the implementor is the only one who can mess up, and hopefully
she will know better.

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

You can only do so if the properties you are interested in are covered by
the mode system.  The sort of thing we've been talking about isn't.

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

I think it would be better to make it equally easy to declare a foreign proc
input that does or doesn't need to be unique, and that does or doesn't have
uniqueness preserved.  If uniqueness is required, then all modes will expect
that argument to be unique on entry.  If uniqueness is preserved for an
argument, then the number of modes is doubled to include both a
starts-and-finishes-unique mode and a starts-and-finishes-nonunique mode for
that argument.  For outputs, the question is just whether they are unique.

Programmers tend to be lazy and only declare the modes they need, rather
than all the modes that make sense.  Failing to declare the
uniqueness-preserving modes of foreign code means a significant amount of
uniqueness information will be lost.  Since the code is identical, there's
no codespace cost of having all the combinations of modes (there are 2^n
where n is the number of uniqueness-preserved arguments).  I can't really
see implementors writing 1000 mode declarations for a 10 input argument
foreign pred that preserves uniqueness of all arguments.  Properly declaring
30 input arguments is even less likely, and 60 is right out.

I think it would also be worth thinking about making users specify whether
each foriegn pred or goal is pure, semipure or impure.

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