[bitc-dev] Type Classes, Mutability, and Monomorphism

[Mark P Jones]

| That being said, I propose that we should stick to the "set 
| of n-ary relations" view, if only to finish this whole 
| exercise in bounded time.

I agree with this.  However, for the record, I should probably
add that I still don't agree with the following:

| If a type class
| 
|   TC 'a 'b
| 
| is viewed as a constraint-induced subtype of ('a , 'b) (the 
| constraint being the existence of an n-ary relation), then a 
| credible meaning can be assigned to TC as a type.

A type represents a set of values.  If we impose constraints on
values, then we obtain a subtype, as in the following examples:

   Positive  = { x \in Int | x >= 0 }
   Odd       = { x \in Int | x mod 2 = 0 }
   Printable = { c \in Char | c >= ' ' && c <= '~' }
   Multiples = { (x,y) \in (Int, Int) | \exists n. x = n * m }

The first two are subtypes of Int, the third is a subtype of Char,
while the fourth example is a subtype of (Int, Int).

Type classes do a similar thing, but at the `next level', which is
to say that a type class represents a set of types.  If we impose
constraints on the types that we include, then we obtain a subclass,
as in the following examples:

   Num = { Int, Integer, Float, Double, Rational }

   Eq  = { Int, Bool, Char } union { a list | a \in Eq }
                             union ( (a, b) | a \in Eq, b \in Eq }

   Collect = { (a, a list) | a \in Eq }
                      union { (a, a SearchTree) | a \in Ord }
                      union ...

The first two here are type classes (if you prefer, subclasses of *,
which is the Haskell name for the set/class/kind of all types), while
the second is a binary relation on types (a subclass of (*, *) if you
prefer).

In essence, we have the same concept at two different levels: classes
are sets of types, while types are sets of values.

All the best,
Mark