[Haskell-cafe] rip in the class-abstraction continuum

[Tillmann Rendel]

Hi,

Christopher Howard wrote:
> class XyConv a where
>    toXy :: a b -> [Xy b]
>
> [...]
>
> I can get a quick fix by adding Floating to the context of the /class/
> definition:
>
> class XyConv a where
>    toXy :: Floating b => a b -> [Xy b]
>
> But what I really want is to put Floating in the context of the
> /instance/ declaration.

This is not easily possible. If you could just put the constraint into 
the instance, there would be a problem when youc all toXy in a 
polymorphic context, where a is not known. Example:

   class XyConv a where
     toXy :: a b -> [Xy b]

   shouldBeFine :: XyConv a => a String -> [Xy String]
   shouldBeFine = toXy

This code compiles fine, because the type of shouldBeFine is an instance 
of the type of toXy. The type checker figures out that here, b needs to 
be String, and since there is no class constraint visible anywhere that 
suggests a problem with b = String, the code is accepted.

The correctness of this reasoning relies on the fact that whatever 
instances you add in other parts of your program, they can never 
constrain b so that it cannot be String anymore. Such an instance would 
invalidate the above program, but that would be unfair: How would the 
type checker have known in advance whether or not you'll eventually 
write this constraining instance.

So this is why in Haskell, the type of a method in an instance 
declaration has to be as general as the declared type of that method in 
the corresponding class declaration.


Now, there is a way out using some of the more recent additions to the 
language: You can declare, in the class, that each instance can choose 
its own constraints for b. This is possible by combining constraint 
kinds and associated type families.

   {-# LANGUAGE ConstraintKinds, TypeFamilies #-}
   import GHC.Exts

The idea is to add a constraint type to the class declaration:

   class XyConv a where
     type C a :: * -> Constraint
     toXy :: C a b => a b -> [Xy b]

Now it is clear to the type checker that calling toXy requires that b 
satisfies a constraint that is only known when a is known, so the 
following is not accepted.

   noLongerAccepted :: XyConv a => a String -> [Xy String]
   noLongerAccepted = toXy

The type checker complains that it cannot deduce an instance of (C a 
[Char]) from (XyConv a). If you want to write this function, you have to 
explicitly state that the caller has to provide the (C a String) 
instance, whatever (C a) will be:

   haveToWriteThis :: (XyConv a, C a String) => a String -> [Xy String]
   haveToWriteThis = toXy

So with associated type families and constraint kinds, the class 
declaration can explicitly say that instances can require constraints. 
The type checker will then be aware of it, and require appropriate 
instances of as-yet-unknown classes to be available. I think this is 
extremely cool and powerful, but maybe more often than not, we don't 
actually need this power, and can provide a less generic but much 
simpler API.

   Tillmann