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

[Fergus Henderson]

Zoltan Somogyi wrote:
> 
> This is a bad example of the use of the capability that Fergus is (I think)
> talking about, since it would be better to simply require programmers
> to call bintree_set:init or tree234_set:init. The reason it is better
> is because it avoid "control coupling" as defined by Steve McConnell,
> (see, writing 252 lecture notes is good for something ;-). Are there
> any better examples?

For a bunch of good examples, see Konstantin Laufer's paper
"Type classes and existential types".

I guess I'm arguing that if we're going to extend the type system, then
as well as type classes we should also support local type quantifiers
(both universal and existential) in data structures, e.g.

	:- type normal1(T) ---> foo(pred(T, int)).
	:- type normal2(T < comparable) ---> foo(T).  % uses type classes:
						      % T must be comparable

	% universal quantification
	:- type universal1 ---> foo(all [T < comparable] pred(T, int)).

	% existential quantification
	:- type existential1 ---> some [T]		foo(T, pred(T, int)).
	:- type existential2 ---> some [T < comparable] foo(T).
	:- type existential3 ---> some [T]		foo(T).

To implement existential types, you need to store a type_info field
in the struct for each existentially quantified type variable
(that's needed in case you pass the existentially typed value to
a polymorphic predicate).

Note the last example existential3 is not very useful, since you can't
do much with the value of type T.  The existential1 example is a bit
more useful, because you can do `X = foo(Y, P), P(Y, Z)'.  However,
with the existential3 example, I guess you _could_ use type_to_univ and
then univ_to_type to get at the value.  In fact that existential3
example is fairly similar in effect to

	:- type existential4 ---> foo(univ).

I suspect that the name `univ' may have been a bad choice, because even
though it is a "universal" type, it seems to be closer to existential
quantification rather than universal quantification.
Of course, existential quantification at the point of definition (construction)
corresponds to universal quantification at the point of use (deconstruction)
and vice versa, so the choice of which one to call universal and which
one to call existential is not entirely obvious.
Still, all the literature on "existential types" uses the same terminology
so the mismatch of that terminology with the name `univ' is unfortunate.
Hang on, I think we got the name `univ' because Cardelli called it
`Universal'?  If so, I guess the literature is inconsistent <sigh>.

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