[m-dev.] for review: new predicates in map.m

[Peter Schachte]

Hi Fergus and all,

I think this is a very important topic, so I'm plucking it from
the far reaches of my mail file to respond to it.

On Tue, Oct 20, 1998 at 08:38:12PM +1000, Fergus Henderson wrote:

> I prefer the "conceptual equality" approach, but
> it does have some drawbacks: defining a user-defined equality
> for the `map' type is straight-forward, but that implies a need to
> promise representation-invariance for every operation which
> examines the representation, and explicitly coding all those
> promises may be tedious.

I don't understand what you mean.  The idea would be to effectively
have two types, an internal view and an external view, and effectly
cast between them by making the external view a single-constructor
type enclosing the internal view, right?  So most of the predicates in
the map module would need wrapper predicates (unwrapper predicates?)
that would do the casting both ways and call the existing predicates
to do the work.  So where do you need to make promises?  I agree that
writing all the wrapper predicates would be a nuissance, but perhaps
some syntactic sugar could be added to hide them.

> On the other hand, the alternative of not
> requiring such promises would be dangerous, because users might
> unknowingly define operations on an abstract type which expose
> the representation and which therefore break referential transparency.

Please explain.

> Zoltan suggested a third approach, namely disallowing equality
> for certain types.

I think the idea of a user-forbidden equality makes a lot of sense,
too.  You're basically saying that semantic equality is not the same
as representational equality, but you can't be bothered to implement a
semantic equality check.

> This is a bit problematical because checking
> this statically is difficult, since equality may be needed in
> some modes but not others, and we don't have mode-dependent type classes.

Don't you already have to handle this for pred types?  Isn't this just
a matter of not allowing modes for predicates and functions in which
equality must be checked?  I would think this would all work in the
current mode system if you considered =/2 to be almost just another
predicate.  Actually, =(in, out) and =(out, in) are always allowed,
and =(out,out) is never allowed (until alias tracking works), but
whether =(in,in) is allowed depends on the type.

> However, even if that problem were overcome, disallowing equality
> wouldn't solve the dilemma.  You still need to specify
> the semantics for equality, even if you don't let users
> call it

Agreed.  But you must have had some idea of semantic equality for that
in mind, or you wouldn't have forbidden equality checking.

> For example, since `map__keys' is declared `det',
> then for every X, Y such that X = Y we have
> 
> 	(map__keys(X, XKs), map__keys(Y, YKs)) => XKs = YKs
> 
> If map__keys is allowed to return different results for
> maps that are conceptually equal but not representationally
> equal

That's a bug.  But it would be a bug with "representational equality"
too, because whatever you may be telling Mercury, you know in your
heart of hearts that whether you draw the map as

        a -> 1		          b -> 2
        /    \		or        /    \   	
       []  b -> 2	       a -> 1  []

it's still the same map.

You may argue that if map__keys on the first returns [a,b] and for the
second returns [b,a], then you're in trouble with the semantic view of
equality, but you're ok with the representational view.  But that's
only because you're not taking the semantic view far enough.  The fact
is that semantically, map__keys returns a set of keys, and [a,b] and
[b,a] are the same set.  The problem here is that the code makes a
semantic conversion between a set and a sequence without
comment.  Adding map__sorted_keys is meant to get rid of that
conversion.

> > If you take the oposite view, then you have to make sure
> > that two maps unify iff the elements were added in the same order.
> 
> You need to ensure that two maps unify if the elements were added in
> the same order.  But the converse (if two maps unify then the
> elements were added in the same order) does not necessarily
> have to hold.

Ok, I think I see where we differ on this.  I think we can agree that
maps are an abstract type and should remain that way.  My view is that
unification of two terms has to mean /something/.  If you take the
representational view of eqality for an abstract type, you're poking a
hole in the abstraction, at least in this case.  You can start doing
experiments to see in what cases two maps that map all the same keys
to the same values unify.  Unification becomes two distinct
semi-decision procedures: if two maps don't unify, you know they were
not created the same way, if the do, you don't know whether or not
they were.  Also, if two maps unify you know they map the same keys to
the same values; if they don't unify, you don't know whether they do
or not.  In other words, representational unification of maps is
pretty much meaningless.

> Having the unsorted version is less justifiable, since it is
> hard to imagine a reasonable implementation of `map' for which `map__keys'
> would not return the elements in sorted order anyway -- especially
> if the equality on maps is conceptual equality rather than representational
> equality.  Dynamically resizing hash tables would probably need to sort
> the keys, just to ensure that map__keys returns the same results for
> hash tables with the same elements that happened to have different sizes

map__keys should return some representation of a set, it needn't be
represented as a sorted list.  A set represented as an unsorted list
would be the natural way for a hash table to return its keys.  This
works fine as long as you've defined equality for
sets-as-unsorted-lists.

-- 
Peter Schachte                | Any Idiot can face a crisis; it is this
mailto:pets at cs.mu.OZ.AU       | day-to-day living that wears you out.
http://www.cs.mu.oz.au/~pets/ |     -- Anton Chekhov 
PGP: finger pets at 128.250.37.3 |