the MPTC Dilemma (please solve)

[Roman Leshchinskiy]

On Mon, 20 Mar 2006, Claus Reinke wrote:

> variant A: I never understood why parameters of a class declaration
>               are limited to variables. the instance parameters just have
>               to match the class parameters, so let's assume we didn't
>               have that variables-only restriction.
>
>               class Graph (g e v) where
>                   src :: e -> g e v -> v
>                   tgt :: e -> g e v -> v
>
>               we associate edge and node types with a graph type by
>               making them parameters, and extract them by matching.

If I understand correctly, this requires all graphs to be polymorphic in 
the types of edges and vertices. Thus, you cannot (easily) define a graph 
which provides, say, only boolean edges. Moreover, doesn't this require 
higher-order matching?

> variant B: I've often wanted type destructors as well as constructors.
>               would there be any problem with that?
>
>               type Edge (g e v) = e
>               type Vertex (g e v) = v
>
>               class Graph g where
>                   src :: Edge g -> g -> Vertex g
>                   tgt :: Edge g  -> g -> Vertex g

This suffers from the same problems as the previous variant. It also looks 
a lot like a special form of associated types. Could the AT framework be 
extended to support a similar form of type synonyms (in effect, partial 
type functions outside of classes)? Would

   instance Graph Int
     -- methods left undefined

be a type error here?

> variant C: the point the paper makes is not so much about the number
>               of class parameters, but that the associations for concepts
>               should not need to be repeated for every combined concept.
>               and, indeed, they need not be
>
>               class Edge g e | g -> e
>               instance Edge (g e v) e
>               class Vertex g v | g -> v
>               instance Vertex (g e v) v
>
>               class (Edge g e,Vertex g v) => Graph g where
>                   src :: e -> g -> v
>                   tgt :: e -> g -> v
>
>               (this assumes scoped type variables; also, current GHC,
>                contrary to its documentation, does not permit entirely 
> FD-determined variables in superclass contexts)

What are the types of src and tgt here? Is it

   src, tgt :: (Edge g e, Vertex g v, Graph g) => e -> g -> v

This does not seem to be a real improvement to me and, in fact, seems 
quite counterintuitive.

Roman