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

[Brian Hulley]

Simon Peyton-Jones wrote:
> 
> The ability to have a data constructor capture a constraint
> of a *non-existential* type variable is newish in GHC.  I added it
> for several reasons.  Firstly, it is more uniform.  It's great to be
> able to say "You can give a constructor any old type, with
> arbitrary constraints".  Secondly, it's useful,  You can have,
> the constructor for (Set a) capturing the (Ord a) constraint, eg
>    data Set a where
>       S :: forall a. Ord a => [a]
> so that union can have type union :: Set a -> Set a -> Set a.
> (Empty set is another matter!)  Incidentally, the union function
> then illustrates Brian's point beautifully:
> 	union (S xs) (S ys) = S (merge xs ys)
> The Ord constraint needed by merge can be satisfied from either
> the (S xs) or the (S ys) -- and they'd better be the same Ord implementation!
> 

Actually even if we go back to plain Haskell 98 and consider the original types for the functions in Data.Set we can see that none of the types would be sufficient to describe the parameter requirements in a modular setting:

    data Set a = Set [a] -- example implementation

    insert :: Ord a => a -> Set a -> Set a

    union  :: Ord a => Set a -> Set a -> Set a

The problem is, for these type signatures to be correct in the sense that they would force the programmer to supply arguments that would lead to the expected results, it is essential that there can only ever be one global Ord instance per type, whereas in a modular setting it would be all too easy to construct sets in one module (or different modules) and then attempt to take the union in a third module i.e. using 3 different Ord_A dictionaries.

In contrast, suppose we had a dependently typed language:

    type OrdDict a = { less : a -> a -> Bool }

    data Set : (a : *) -> (d : OrdDict a) -> * = List a

    insert : (a : *) -> (d : OrdDict a) -> a -> Set a d -> Set a d

    union : (a : *) -> (d : OrdDict a) -> Set a d -> Set a d -> Set a d

The types above would ensure that (union) can only be passed sets created using the same dictionary.

This suggests to me that instead of regarding typeclasses as a kind of automatic way of applying functors or selecting modules, we should perhaps instead regard typeclasses as a special syntactic sugar for the use of dependent types in the restricted setting where whenever type T depends on (v : V), V determines (v).

In the example above, translated back into Haskell, (OrdDict _A) determines it's inhabitant (d_A) hence we are allowed to say that (Set a d) depends only on (a) and (OrdDict a), hence the (d) parameter is redundant, hence dependent types are not needed.

>From this angle it is then easy to see that far from regarding the global nature of Haskell typeclass instances as a minor inconvenience to be circumvented by lexical scoping or some other mechanism, it is in fact the central core of the concept itself!

Perhaps the way forward is simply to take the idea of starting from ML rather than Haskell, begun in the MTC paper, further, and not expect to be able to write Haskell-style programs in ML. For example the above considerations may lead us to reject qualified polymorphism via the translation into HS semantics but keep the idea of being able to generate canonical modules for a given signature, leading to a more modest, but still useful, extension.

Brian.