[m-dev.] Typeclasses and constructor classes.

[David Glen JEFFERY]

On 20-Sep-2000, Ralph Becket <rbeck at microsoft.com> wrote:
> > 
> > :- instance sequence(list, T).
> 
> This looks a mite dodgy to me - in Mercury list/0 and list/1
> would be separate types, yet this syntax would be ambiguous.

Yes, `list' could refer either to the type list/0 or it could be the
constructor of list/0. However, for each argument to the type class, we
will know its `kind', which you can think of as telling what the
arity (including 0) of a type constructor is.

Well, it is really more complicated than that. A kind is something like:

:- type kind ---> t ; (kind -> kind).

(where `t' means `type'... you will find that most of the literature uses `*')

The `list' type constructor has kind `t -> t'. ie. it is a function from
types to types. Similarly, the `map' type constructor has kind `t -> t -> t'.

Much more fancy kinds are possible, though (and turn out to be pretty handy).
Basically, once you have allowed type constructors of kind other than `t'
in type classes, you have to let them leek out everywhere.

For example, given the class:

:- typeclass c(L::(t->t), T::(t)) where [
	func empty = L(T)
	% etc.
].
(where I've invented a syntax to annotate kinds to hopefully make things
clearer)

it becomes natural to want to be able to have these inside other structures:

:- type foo(L::(t->t), T::(t)) ---> foo(int, map(float, L(T))).

Now the type constructor `foo' has kind `(t -> t) -> t -> t'

Of course, you could now want to construct a pretty hairy constructor class:

:- typeclass c(F::((t -> t) -> t -> t)) where [
	func f(foo(A, B)) = F(A, B).
].

Even with such fancy kinds, kind inference remains decidable (and 
quite feasible), so there isn't any need to require explicit annotations
(although perhaps we should allow it... see below).

> Perhaps a better syntax is
> 
> :- typeclass sequence(S/1) where [
> 	func map(func(T) = U, S(T)) = S(U),
> 	...
> ].

Integers aren't enough to express all of the kinds that you need to.
Perhaps we should allow it as syntactic sugar.(?)
Anyhow, as kind inference is feasible you shouldn't have to explicitly
annotate it. 

FYI, there is one situation where you might want an explicit
annotation, though: a class with no methods. eg. 

:- typeclass c(A,B) where [].

In this case, Haskell would just assign A and B the kind `t' (or `*'). We
may like to provide a syntax to explicitly declare the kind for situations
like this. Then again, you can always just provide a dummy method that
restricts the kind to what you want... and this possibly isn't likely to happen
often enough to warrant an explicit syntax.

> > I'm sure that sent off alarm bells in a few people's heads. The instance
> > I've written above wouldn't be accepted according to Mercury's current
> > rules
> > for ensuring that instances do not overlap. (ie. top level type
> > constructors
> > must be bound).
> 
> With the above scheme, the problem disappears for some types (e.g. list/1).

In some sense, this is true. You have effectively of encoded the functional
dependency by saying that the `T' belongs to `list'. This isn't as powerful
as functional dependencies, though. (Functional dependencies are really
pretty yummy). Actually, what you have described here reminds me of Hudak &
Chen's parametric type classes. I can dig up a reference if you want...

> > (We are making quite a bit of use of type classes in HAL, particularly
> > as a way of modelling constraint solvers (a `plug and play' interface).
> > I've got this sneaking suspicion that very, very soon we are going to
> > realise that we need constructor classes to do what we're trying to
> > do... in which case I will probably wind up doing the implementation
> > anyway, both in HAL and in our target language Mercury).
> 
> If it doesn't look likely, is there any chance of handing this over
> to someone who is willing and able?  I'd like to start porting the
> Edison library, but that is pretty much impossible with typeclasses as
> they stand.

Indeed, although I doubt it'll come to that.


dgj
-- 
David Jeffery (dgj at cs.mu.oz.au) | If your thesis is utterly vacuous
PhD student,                    | Use first-order predicate calculus.
Dept. of Comp. Sci. & Soft. Eng.|     With sufficient formality
The University of Melbourne     |     The sheerist banality
Australia                       | Will be hailed by the critics: "Miraculous!"
                                |     -- Anon.
--------------------------------------------------------------------------
mercury-developers mailing list
Post messages to:       mercury-developers at cs.mu.oz.au
Administrative Queries: owner-mercury-developers at cs.mu.oz.au
Subscriptions:          mercury-developers-request at cs.mu.oz.au
--------------------------------------------------------------------------