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

[oleg at okmij.org]

Type classes are the approach to constrain type variables, to bound
polymorphism and limit the set of types the variables can be
instantiated with. If we have two type variables to constrain,
multi-parameter type classes are the natural answer then. Let's take
this solution and see where it leads to.

Here is the original type class
> class XyConv a where
>   toXy :: a b -> [Xy b]

and the problematic instance
> data CircAppr a b = CircAppr a b b -- number of points, rotation angle, radius
>     deriving (Show)
>
> instance Integral a => XyConv (CircAppr a) where
>   toXy (CircAppr divns ang rad) =
>       let dAng = 2 * pi / (fromIntegral divns) in
>       let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in
>       map (\a -> am2xy a rad) angles

To be more explicit, the type class declaration has the form

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

with the type variable 'b' universally quantified without any
constraints. That means the user of (toXy x) is free to choose any type
for 'b' whatsoever. Obviously that can't be true for 
(toXy (CircAppr x y)) since we can't instantiate pi to any type. It
has to be a Floating type. Hence we have to constrain b. As I said, the
obvious solution is to make it a parameter of the type class.

We get the first solution:

> class XYConv1 a b where
>     toXy1 :: a b -> [Xy b]
>
> instance (Floating b, Integral a) => XYConv1 (CircAppr a) b where
>   toXy1 (CircAppr divns ang rad) =
>       let dAng = 2 * pi / (fromIntegral divns) in
>       let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in
>       map (\a -> am2xy a rad) angles

The type class declaration proclaims that only certain combinations of
'a' and 'b' are admitted to the class XYConv1. In particular, 'a' is
(CircAppr a) and 'b' is Floating. 

This reminds us of collections (with Int keys, for simplicity)

> class Coll c where
>   empty :: c b
>   insert :: Int -> b -> c b -> c b
>
> instance Coll M.IntMap where
>   empty  = M.empty
>   insert = M.insert

The Coll declaration assumes that a collection is suitable for elements of
any type. Later on one notices that if elements are Bools,
they can be stuffed quite efficiently into an Integer. If we wish to
add ad hoc, efficient collections to the framework, we have to
restrict the element type as well:

> class Coll1 c b where
>   empty1 :: c
>   insert1 :: Int -> b -> c -> c

Coll1 is deficient since there is no way to specify the type
of elements for the empty collection. When the type checker sees
'empty1', how can it figure out which instance for Coll1 (with the
same c but different element types) to choose?
We can help the type-checker by declaring (by adding the functional
dependency c -> b) that for each collection
type c, there can be only one instance of Coll1. In other words, the
collection type determines the element type.

Exactly the same principle works for XYConv.

> class XYConv2 a b | a -> b where
>     toXy2 :: a -> [Xy b]
>
> instance (Floating b, Integral a) => XYConv2 (CircAppr a b) b where
>   toXy2 (CircAppr divns ang rad) =
>       let dAng = 2 * pi / (fromIntegral divns) in
>       let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in
>       map (\a -> am2xy a rad) angles

The third step is to move to associated types. At this stage you can
consider them just as a different syntax of writing functional
dependencies:

> class XYConv3 a where
>     type XYT a :: *
>     toXy3 :: a -> [Xy (XYT a)]
>
> instance (Floating b, Integral a) => XYConv3 (CircAppr a b) where
>   type XYT (CircAppr a b) = b
>   toXy3 (CircAppr divns ang rad) =
>       let dAng = 2 * pi / (fromIntegral divns) in
>       let angles = map ((+ ang) . (* dAng) . fromIntegral) [0..divns] in
>       map (\a -> am2xy a rad) angles

The step from XYConv2 to XYConv3 is mechanical. The class XYConv3
assumes that for each convertible 'a' there is one and only Xy type
'b' to which it can be converted. This was the case for (CircAppr a
b). It may not be the case in general. But we can say that for each
convertible 'a' there is a _class_ of Xy types 'b' to which they may be
converted. This final step brings Tillmann Rendel's solution.