[m-dev.] proposal: user-defined equality predicates

[Fergus Henderson]

Tyson Richard DOWD, you wrote:
> I'm concerned that it might not smoothly merge in with typeclasses. 
> Does it?

The proposed syntax for type classes (still fairly tentative) is
like this:

	:- type_class number(T) where [
		(:- func plus(T, T) = T),
		(:- mode plus(in, in) = out is det),
		(:- mode plus(in, out) = in is det),
		(:- mode plus(out, in) = in is det),
		(:- pred less_than(T::in, T::in) is semidet)
	].

or perhaps like this:

	:- type_class number(T) where [
		func(plus(T, T) = T),
		mode(plus(in, in) = out is det),
		mode(plus(in, out) = in is det),
		mode(plus(out, in) = in is det),
		pred(less_than(T::in, T::in) is semidet)
	].

Type class constraints are expressed using `<=', e.g.

	:- type_class number_with_zero(T) <= number(T) where [
		func(zero = T)
	].

	:- func sum(list(T)) = T <= number_with_zero(T).
	sum([]) = zero.
	sum([X|Xs]) = plus(X, sum(Xs)).

Type class instances look like this:

	:- instance number(int) where [
		func(plus/2)	  is (+),
		pred(less_than/2) is (<)
	].
	:- instance number_with_zero(int) where [
		func(zero/0)	  is int_zero
	].
	:- func int_zero = int.
	int_zero = 0.

The syntax for user-defined equality predicates does not conflict
with the syntax for type classes, because user-defined equality
predicates are specified in type definitions, whereas
type classes don't add any syntax to type definitions.
However, the syntax for user-defined equality predicates is analagous
to the syntax for instance declarations.

	:- type complex
		--->	polar(float, float)		% r, theta
		;	cartesian(float, float)		% x, y
		where	equality is complex_equals.

	:- pred complex_equals(complex::in, complex::in) is semidet.
	complex_equals(A, B) :- ...

I thought about changing the syntax to

		where	pred(=/2) is complex_equals.

but that would be wrong, since =/2 is really a builtin language construct,
not a predicate.  I think the syntax `where equality is ...' is ok
and is consistent with the anticipated syntax for type classes.

> >      :- type set(T) ---> set(list(T)).
> > 
> > In this example, the concrete representations `set([1,2])' and
> > `set([2,1])' would both represent the same abstract value, namely the
> > set containing the elements 1 and 2.
> 
> The `type(representation)' notation isn't really introduced clearly.

Ah, that notation is just `constructor(args)'.
Perhaps it would be clearer if I changed the example to

      :- type set(T) ---> set_as_unsorted_list(list(T)).

	In this example, the concrete representations
	`set_as_unsorted_list([1,2])' and `set_as_unsorted_list([2,1])'
	would both represent the same abstract value, namely the set
	containing the elements 1 and 2.

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