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

[Brian Hulley]

Karl Crary wrote:
> Hi Brian,
> 
> Basically you're observing that a qualified GADT package includes an 
> instance declaration, so unpacking it amounts to a using declaration.  
> Accordingly, the "Problem" clause of your code would need to be treated 
> as a using declaration, and it would be rejected for introducing 
> overlapping instances.

Hi Karl,

Thanks for pointing out that the compiler could just reject this clause: perhaps this would be an acceptable penalty to pay for the advantages of having scoped instances. However there are situations where it would not be so clear what the compiler should do eg:

    bar :: forall a. G a -> (a, Int)
    bar (Problem x) = (x + x, 1 + 2)
    bar (Ok _)      = ((), 0)

In the expression (x + x, 1 + 2), what instance should the compiler use for (1 + 2)? Since (bar) is polymorphic, the compiler, when compiling (bar), has no way of knowing whether or not the match against (Problem x) is going to introduce a Num Int dictionary.

Of course this could be rejected on the grounds that the match *may* introduce an overlapping instance, or we could restrict (a) so that it may not be instantiated to Int eg:

    bar :: forall a. (NotEqual Int a) => G a -> (a, Int)

where NotEqual is a built-in predicate, though this has the unfortunate effect of leaking information about the implementation into the function's type.

For example we might choose to accept the following implementation, with no restrictions on the instantiation of (a), since evaluation of the rhs expression does not involve conflicting dictionaries (assuming that we already have a top-level binding of (three) to the integer 3 so that no dictionary is needed in the evaluation of the second component of the pair):

    bar' (Problem x) = (x + x, three)

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

I'm not quite sure if I've understood what you mean here: GHC does support qualified existentials and in fact it is a common idiom to wrap a dictionary in a datatype together with a value, to simulate the effect of using an interface in a standard object oriented language e.g. for widgets:

    class Widget w where
       drawWidget :: w -> Canvas -> IO ()

    data WrappedWidget where
       Wrap :: forall w. (Widget w) => w -> WrappedWidget

    draw :: WrappedWidget -> Canvas -> IO ()
    draw (Wrap w) c = drawWidget w c

Although arguably it might be better practice to pass a simple record of functions instead of a qualified existential in such cases.

> 
> 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.  A better way to do GADTs would be to introduce a 
> "datakind" mechanism, and use algebraic data kinds as the indices for a 
> GADT.  You can get a picture of what this would look like from my 1999 
> paper "Flexible Type Analysis" with Stephanie Weirich.  (That paper 
> didn't have the tie-in with datatypes, which was invented later.)

Thanks for the reference, which looks to be very interesting for issues related to typed compilation in general not just typeclasses. Also it's useful that you suggest that GADTs may be at fault rather than typeclasses per se since it indicates that perhaps the best way to proceed is simply to ignore GADTs for the moment rather than letting the problems their current design introduces block progress towards an implementation that would allow other uses of typeclasses in a modular setting.

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

Such a mechanism would also be useful in its own right, for example to allow a limited form of dependently-typed programming with indices as described in [1] (which references the paper you co-authored above).

Cheers, Brian.

[1] "A formulation of Dependent ML with explicit equality proofs" by Daniel R. Licata and Robert Harper, Dec 2005, CMU-CS-05-178.