type classes --- thoughts?

[David Glen JEFFERY]

Hi,

I've been giving some thought to adding type classes (a la Haskell) to Mercury.
I thought I'd see what you guys think of it.

Basically, I want to allow declarations of the form:

	:- type_class foo(T) where
		pred a(T::out) is det,
		pred b(T::in, T::in, T::out) is det,
		pred c(T::in, T::in, T::out) is semidet,
		func d = T::out is det.
	% These can contain pred, mode and func decls.

This declares a class `foo', and says that if T is to be in the class, then a/1,
b/3, c/3 and d/0 must be defined for it.

For now, only single parameter type classes will be allowed. In the future, I 
think we should either add multi-parameter classes, or constructor classes with
parameters --- more on this later.

For a type to be considered a member of a class, a type_class_instance 
declaration is required, indicating how the type satisfies the interface
specification given in the type_class decl.

:- type_class_instance(foo, bar) where
	a/3 == init/3,
	b/3 == add/3,
	etc.
	% These probably shouldn't be required _if_ the class preds and
	% funcs are already available.

type_class and type_class_instance declarations can be exported from if they
are in the interface, or hidden if they are in the implementation just as
preds, funcs and types are.

Then, whenever a pred of func definition is given, any type variables can
be constrained to belong to a particular class, so preds/funcs from the
interface of the class may be used on the variable.

I'm not entirely sure of a good syntax for this... probably something
like:

:- pred blahblah(something::in, X::out) is det, where foo(X).
or
:- pred blahblah(something::in, X::out) is det <= foo(X).
or
:- pred (foo(X)) => blahblah(something::in, X::out) is det.

This indicates that the variable with type `X' in the pred blahblah/2 belongs to
class foo.

It should also be possible to make type_class declarations for derived classes:

	:- type_class (foo(T), other_foo(T)) => baz(T) where
		...stuff in terms of the foo and other_foo thingies...
	:- end_class.
This indicates that for T to be in class baz, it must also be in foo and
other_foo.

Similarly, we should allow derived instances, like:

	:- type_class_instance (foo(T)) => foo(list(T)) where
		...stuff explaining how to implement the foo interface for
		list(T) using the foo interface on T...
	:- end_class.
This says that if T is in foo, then so is list(T).

Overlapping instance declarations will be disallowed, eg.
	:- type_class_instance(foo, list(T)) where
		writeln/3 == output_list/3...
	:- type_class_instance(foo, list(char)) where
		writeln/3 == output_char_list_as_string/3
	would be illegal. I think that this is a good idea since adding
	an instance declaration really shouldn't alter the behaviour of a
	well-typed program.

BTW, what do you think about having default definitions in a class declaration?
	eg.
		:- type_class blah... where
			foobar(...),
			default(not_foobar(...)).	%better syntax, surely ?
		ie. a class may provide a definition that an instance may
		override.
	I don't think default definitions are a great idea, because once again
	adding to an instance decl can alter the behaviour of a well-typed
	program (once again). In this case, though, its probably not so bad.

One important point which applies to type classes for logic programs in
general is the restriction of equality (unification) to a certain typeclass.
(cf. Haskell's `Eq' class).  We really can't take the same approach as
Haskell/Gofer here, since we can't require the user to provide equality
predicates for all types which are allowed to be compared. (For one thing , it
would be really nasty if we allowed unification to mean anything other than what
it currently does). It even seems crazy for require the user to declare which
types _may_ be unified. 

A better solution is probably to allow the programmer to declare which types may
_not_ be unified. (Eg. the programmer may be using a non-canonical set
representation). Any type not declared to non-unifiable (and which doesn't
have a non-unifiable type as an argument) would be considered to be part of
the `eq' or `unifiable' class.

Hmmm, the same should probably go for `comparable' types (ie. let the
programmer disallow the calling of `>=' etc. for certain types).

As far as implementation goes, a field should probably be added to the
type-info which contains a `dictionary' of methods for each type class that
a type belongs to. (The dictionary is basically an array of code pointers for
each pred/func in the interface of a typeclass).

When calling a pred/func which has a typeclass constraint in its declaration, 
the appropriate dictionary is placed as an extra argument to the pred, much
in the same way as type-infos become extra arguments.

Well... any thoughts would be appreciated.


love and cuddles,
dgj
-- 



This .sig deliberately left blank