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

[David Glen JEFFERY]

The epic type class discussion continues...

Fergus Henderson wrote:
> Well, we could spend a lot of time debating the syntax...

Yes... we should argue about that some time too... but not now.

> what about type checking and type inference?

Type checking isn't too bad. For each pred, whenever there is a call to
something from a class interface, we check that the appropriate variables
belong to the appropriate classes (including following the class hierarchy
upwards where necessary).

Inference is a little hairier --- not because it is any harder to implement, but
because there is a choice to make regarding _when_ you use instance declarations
to reduce the inferred type class constraint set to a smaller set. 

There is almost no change to the current type inference algorithm.  Basically,
as you infer the types, you also gather a set of class constraints. We don't
even need to check that the constraints are consistent (since a type may be
in many classes). Like I said, this set of class constraints can often be
reduced because of redundancies and the class hierarchy. It probably doesn't
matter a whole lot which way we choose to do that --- having a larger context
(ie. set of class contraints) means that there are more dictionaries to pass,
but we probably aren't too concerned about how it performs without type
declarations anyway.

> Can you have preds with multiple modes?

Yes.

> Must every class method have `T' somewhere in its type signature?

Yes.

> Can you have preds which are polymorphic on types other than `T',

No. `T' must be in every signature.

> or in addition to `T'?

Yes. For example, the following should be quite valid:

    :- type_class foo(T) where
        pred bar(T::in, X::in, map(T, X)::out) is det.

> As for declaring things to be non-unifiable/non-comparable,
> given that unify/2 and compare/3 can be implemented using arg and functor,
> you'd better make such things non-arg-able and non-functor-able too.
> Oh, and what about type_to_univ and univ_to_type -- should univ
> be unifiable?
> 
> Well, that's a nice little can of worms there...

Hmmm. Yes it is. I would say that arg and functor should just have type class
restrictions added to say that their arguments must be comparable. 

    eg.  :- pred arg(T::in, int::in, univ::out) <= comparable(T) is semidet.

I'm really not sure about univ, though. Thoughts, anyone?

Anyhow, I think that for the moment, we can probably leave this issue to
the side a little. We can still have a type class system in which unification
and comparison are allowed on all types. ie. unify/2 and compare/3 have no
type class context.

I think, however, that what I favour is to have two builtin classes: unifiable
and comparable. Everything is assumed to belong to them, except where the
type is abstract and an explicit declaration is made to the contrary. 
    eg. 

    :- interface.

    :- type non_canonical_set(T).
    :- nonunifiable(non_canonical_set(T)).
        .
        .
        .
    :- implementation.
        .
        .
        .

One nasty thing is that, in some modes, unification will not be needed for some
preds, but it will be needed for others. Should we allow contexts to be added
on a mode-by-mode basis? I think not, but it may be useful.

> Hmmm, so the type-infos are always input to the procedure, even for output
> arguments, or for a function's return value... that does seem a bit limiting.

Well... surely this is just the same as how we handle polymorphic output args
at the moment --- the typeinfo is always input (and with type classes, if there
is a type class constraint on the type variable, then the appropriate dictionary
is passed as well). Am I missing something, or did I just word it badly?


love and cuddles,
dgj
-- 



This .sig deliberately left blank