Well, as promised, I'm going to try to capture my thoughts
semi-coherently on this. Summary: type classes are merely classes with
a funny overload resolution mechanism. Constraints are just an idiom
trick on abstract class instantiation.

A class in C++/C#/Java may have methods that are overloaded on type.
This is nothing new, but for some reason it has been considered "not
tasteful" in the Haskell/O'Caml communities. I submit, first, that
there is no essential difference (from a taste perspective) between
the following three things:

  - Resolving an overloaded method call by consulting the available definitions
    in the current lexical context.
  - Resolving a desired type class instance by consulting the
available instances
    in the current lexical context.
  - Resolving a template specialization (as in C++) by consulting the available
    specializations in the current lexical context.

Each of these, fundamentally, is a matter of ad-hoc type-based
overload resolution. There seems to be no qualitative difference
between them, and no reason I can see to view any one as more tasteful
than any other.


Given this, I claim that:

 - A type class is merely an abstract, generic "interface" class in
the C# sense: (that is: one
  which has only virtual methods), and the fact that it is an
interface class is merely
  a matter of convention (see below).
- A type class instance is a total or partial specialization of that
generic (not sure C#
  supports this, so perhaps this should be taken in the style of C++
partial template
  specialization.
- A type class constraint merely expresses the requirement that a
suitable specialization
  must exist.
- Type class instance resolution is merely a variation on template
specialization selection.
- There is a little "magic" of type classes is a combination of
syntactic sugar and
  unambiguous resolution. The sugaring is the "lifting" of type class
methods into
  the namespace containing the type class declaration, and the unambiguous
  resolution devolves from a combination of specialization and
resolution discovery
  rules. This, coupled with the constant nature of the resulting
method bindings,
  lets us partially evaluate the dictionary/v-table away in most
cases, but that is
  merely a detail (albeit an important detail) of implementation.

  Note that all of this magic can be accounted for by parametric procedures.
- Finally, there is some "magic" in letting the type derivation mechanism drive
  the instantiation of these classes, and thereby enabling the dropping of
  locally satisfiable type class constraints.

This is, I think (I hope?), one way of synopsizing what Oliveira and
Martin are saying. Now let's play with it a bit.

It does not seem to me that there is any reason to restrict type
classes to virtual methods. For example, we might imagine defining a
hypothetical Eq type class as:

type class Eq 'a {
  // intentionally ignoring operator syntax issues here ...
  instantiated equals :: 'a x 'a -> bool;
  fn notEquals x y = ! equals x y;
}

By this pseudo-syntax, I mean to suggest that "equals" is a function
whose implementation must be supplied by some specialization of Eq 'a,
but that "notEquals" has a parametric implementation that is common to
*all* instantiations of Eq 'a. Note here that "notEquals" is *not* a
function that needs to appear in any dictionary or v-table; it is not
a virtual method. Eq 'a is a type in the sense that it defines a
(parametric) dictionary structure. In the terminology of C#/C++/Java,
Eq 'a is an abstract type; specialization (a.k.a instantiation) is
required.

Indeed, I see no reason why we should not have written this (ignoring
human factors) as:

abstract class Eq 'a {
  // intentionally ignoring operator syntax issues here ...
  virtual equals :: 'a x 'a -> bool; // abstract method
  fn notEquals x y = ! equals x y;
  virtual fn anotherNotEquals x y = ! equals x y; // inherited
}

def isEqual x y = equals x y;
> isEqual: Eq 'a => 'a -> 'a -> bool

and interpret the "Eq 'a" constraint to mean simply that some suitably
matching specialization of the Eq 'a class must be shown to exist.

A type class instance is an "object" in the sense of Scala: it is
simultaneously a definition of a type which is a partial or total
specialization of the type class and a unique singleton value of that
type. Given the concept of static methods, it seems largely a matter
of lexicography whether we consider this to be an instance of class Eq
'a, a subclass of class Eq 'a, or a specialization of class Eq 'a.
They are all, in some sense, different words for the same thing.

However, note that a type class instance is then a subclass (in the
sense that it inherits methods, virtual methods, and abstract virtual
method mandates) of its type class. There seems to be no inherent
reason to restrict the subclassing depth to one.

Now if all of this is the case, then we must ask whether we shouldn't
just allow fields in [type] class definitions. I don't see any
particular *use* for fields in a type class, but at the same time I
see no need to exclude them arbitrarily. It seems perfectly fine that
the absence of fields from type classes can merely be a matter of
convention. If they are permitted, and if we take the view that a type
class constraint merely expresses an instantiation requirement on an
abstract class, then we will have subsumed quite a number of things
into one concept (as Sandro noted earlier):

  structures
  unions (realized through subclassing)
  classes/objects (realized through subclassing)
  type classes (realized through abstract classes and instantiation
requirements)

Have I *finally* wrapped my head around the essentials of what
Oliveira and Martin have been saying?

If so, then I confess this is fairly embarassing. Here I have been
running around saying that OO did not seem like such a good idea in
hindsight, and that type classes seem better, when all I was actually
advocating was a different *idiom* of the same old OO ideas.
Appropriately biasing the selection of idioms is terribly important in
programming languages, and I don't mean to trivialize it, but what a
tragically funny gaffe this would all turn out to be if BitC is merely
C++ with type system that isn't irredeemably screwed and a new
abstract class idiom trick...

Oh. And it shouldn't go unsaid: Crap! I think the subtyping bullet has
finally caught up with me! :-)

But do I *finally* have my head around this properly?


shap
_______________________________________________
bitc-dev mailing list
[email protected]
http://www.coyotos.org/mailman/listinfo/bitc-dev

Reply via email to