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

[Fergus Henderson]

David Glen JEFFERY, you wrote:
> 
> > Can you have preds which are polymorphic on types 
> > [...] 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.

OK.  But that might not be trivial to implement.  If you want to
implement this by transforming it all to use higher-order terms,
allowing that may require some work, because currently the way we
handle the quantification of type variables in higher-order types
implies that all higher-order terms are monomorphic. 

Consider

	:- pred p(pred(T)).

There are two possible meanings for this, depending on the scope of `T'.
Using `all [<type-variable>] <type>' to denote universal type quantification,
this could mean either

	`p' has type `all [T] pred(pred(T))'.
	(Here `p' is polymorphic, but its argument is monomorphic.)

or

	`p' has type `pred(all [T] pred(T))'.
	(Here `p' is monomorphic, but its argument is polymorphic.)

Currently we assume the former, and don't provide any way of saying the
latter. 

Note that Haskell has a similar restriction.  The reason is that if you
allow nested quantifiers anywhere, then type inference reportedly
becomes undecidable.

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

I don't agree that there should be only two builtin classes.
It's easy to imagine types which you might want to be comparable but for
which you don't want to allow arg or functor; you may want to allow
things to be compared, but want to truly hide the representation.
It would be better to have a separate class, say `decomposable', for
arg and functor.

But I think the basic idea of having everything be instances of
unifiable, comparable, and decomposable except where explicitly
declared as `limited'.

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

There are other cases where this distinction may be useful.
For example, a Prolog-style `=..' would require its argument to be
composable (for one mode) or decomposable (for the other mode).
It's quite possible to imagine examples where you want something to be
decomposable but not composable or vice versa.

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

Currently we do allow typeinfos to be returned:  you just have to wrap
them up in a `univ'.  `univ' is a bit like a special case of
existential types.  You can think of `univ' as an abbreviation for
`(some [T] T)'.  For type classes, it would be nice to generalize this:
you want to be able to have a type `(some [T where comparable(T)] T )'
or something like that -- a type which is unknown until runtime, but
which is known to be an instance of a particular class.  Using
`univ_to_type', e.g.

	MyUniv = make_univ(...),
	univ_to_type(MyUniv, Unifiable),
	( Unifiable = Unifiable ->
		...
	;	
		...
	)

doesn't work.  In that example the type of `Unifyiable' is T, an
uninstantiated type variable.  Currently we conceptually instantiate all
such type variables to a single nameless type (whose type-info is
represented by a null pointer) -- although adding type classes may
require us to rethink our current approach to uninstantiated type variables:
it might be better to just disallow them.  Anyway, currently the call to
`univ_to_type' will always fail, because there are no objects of this
nameless type. 

What you want here is perhaps some kind of `univ_to_type_class'... 
as usual, the devil is in the details.

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