[TYPES] A show-stopping problem for modular type classes?

[Stefan Monnier]

> It strikes me that in GHC you might well have the same problem with the 
> "Ok" constructor.  A qualified existential package also includes an 
> instance declaration, and unpacking it too amounts to a using 
> declaration.  That ought not be a problem because it's an instance for 
> an abstract type, so it cannot overlap any existing instances.  But, my 
> understanding is that internally GHC does not really support abstract 
> types, so that might not help.

Actually, since GHC uses a variant of System F internally, it should
have no trouble supporting real abstract types.

> By the way, I think that this issue exposes a design flaw in GADTs.
> GADTs provide a convenient way to do dynamic type analysis by
> integrating type representations into the datatype mechanism.  But, I
> think it's a mistake for GADTs to use actual types for those type
> representations.  Conceptually, the indices for a GADT are data, not
> sets of terms.

I presume you're talking about GHC's GADTs.  As it turns out, they
are not specifically indexed by types of kind * (aka Ω), instead they
can be indexed by type expressions of pretty much any kind.

> A better way to do GADTs would be to introduce a "datakind" mechanism,
> and use algebraic data kinds as the indices for a GADT.

If GHC had datakinds, then its GADTs would support them as well.
I.e. you're talking about a design flaw of GHC/Haskell rather than its
GADTs which just happen to inherit it.

> The relevance to modular type classes is this:  If the index for a GADT
> were an algebraic data kind, rather than an actual type, there would be
> no temptation to try to attach an instance to that index.

Why would you think so?  Going back to the "type classes as SML modules"
point of view, it's like saying you wouldn't want modules parameterized
by types of other kinds than Ω.  It didn't take long for type classes to
be generalized to constructor classes, so I can't see any reason why
people wouldn't want to have classes over types of other kinds than
Ω and Ω→Ω.

> The "Problem"  constructor would be ill-kinded.  Obviously,
> introducing a datakind  mechanism and supporting machinery would be
> a much more substantial fix  than simply checking for overlapping
> instances when unpacking a GADT, and it also might break existing
> code.  But I do think it would be a better design looking forward.

Sadly, I don't think it would be a fix at all.  It might be a good new
feature, tho.


        Stefan