[m-dev.] type classes --- thoughts?

[Tyson Richard DOWD]

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

I think you should use 70-75 character width lines, since they tend to
quote better ;-).

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

Haskell (or at least Hugs) allows you to define a type that `derives
Eq', which means it defines equality using standard syntactic equality.
If all `:- type' definitions were treated in this way, and another
definition, say `:- sort' (*) defined types without this equality, you could
have both normal, syntactic unification, and user-defined unification.

Now, whether you want user-defined unification predicates is a little
harder to decide - but in the context of a language with type-classes,
their meaning is a little better defined - we simply assume that
anything in class `unifiable' has `=' defined on it, which is usually
the builtin unifier, but can be something else. 

Because the typeclass system defines a source-to-source transformation
(although it might not be implemented quite that way), the meaning of
the program is well defined, and reasonably clear.

In the compiler, however, we do some abstract interpretation of
unifications, so it needs to know whether an `=' is builtin unify, or
user-defined. But this would seem to be known relatively easily, in fact
it may have already been transformed away - it's either known, or the
type is polymorphic, and it must be called at runtime.

(*) we need more synonyms for `type' in English, wouldn't you agree?
`:- sort' isn't a great name, so I'm open to suggestions.

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

This is what the `:- sort' defintion provides, although via a different
mechanism. `:- sort' could be augmented with `derives unifiable' or
`derives comparable' or both, and could be considered a more basic
construct than `:- type' which is just shorthand.

Just an idea...

-- 
       Tyson Dowd           # "Well, let's just say, 'if your VCR is
                            #  still blinking 12:00, you don't
     trd at cs.mu.oz.au        #  want Linux'". 
http://www.cs.mu.oz.au/~trd #  --Bruce Perens, Debian's Fearless Leader