[mercury-users] typeclass constraint on type definition... wrong

[Fergus Henderson]

This email elaborates a little more on an old thread...

I just realized another important reason why Richard is right about
this, in addition to the software engineering and elegance arguments
that Richard explained.

On 28-May-1999, Richard A. O'Keefe <ok at atlas.otago.ac.nz> wrote:
> Now, for a priority queue, you really *really* want this:
> 
>     Ord k => data PQ k v = <whatever>
> 
>     new_pq   :: PQ k v
>     add_pq   :: PQ k v -> k -> v -> PQ k v
>     empty_pq :: PQ k v -> Bool
>     remin_pq :: PQ k v -> ((k,v), PQ k v)
>     merge_pq :: PQ k v -> PQ k v -> PQ k v
> 
> The constraint that k belong to the Ord type class is not
> an "accidental" property of some of the *functions*, it's
> a fundamental property of the priority queue *type*.

Yes.  In particular, this constraint might be well required for
computing even _equality_ on the type.  In Mercury, equality is
certainly considered a fundamental property of the type.  If a type has
a non-standard equality, then that must be stated as part of the type
definition: the user must specify a user-defined equality predicate
which the compiler will use whenever any two values of that type are
unified.

	:- type pq(K, V)
		---> <whatever>
		where equality is equal_pq.

For such a declaration to be legal, equal_pq/2 must have a type which
is sufficiently general to allow it to unify any two values of type pq(K, V).
If equal_pq has a type class constraint, e.g.

	:- pred equal_pq(pq(K,V), pq(K,V)) <= ord(K).

then with the current rules, the above definition of type pq/2 would result
in a type error.  If we want to allow user-defined equality predicates
which make use of type class constraints (which we clearly do, since for
some types the most natural way of implementing equality would be by
calling some type class methods), then we need to change the rules somehow.
And the obvious solution is to allow type class constraints on type
definitions.

If type class constraints were allowed on data definitions,
then you could write e.g.

	:- type pq(K, V) <= ord(K)
		---> <whatever>
		where equality is equal_pq.

and unlike the previous definition, this one would not be illegal, because
the constraint on equal_pq is now no less general than the constraint
on the type, so equal_pq can safely be used to test equality between any
two values of that type.

-- 
Fergus Henderson <fjh at cs.mu.oz.au>  |  "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh>  |  of excellence is a lethal habit"
PGP: finger fjh at 128.250.37.3        |     -- 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
--------------------------------------------------------------------------