the MPTC Dilemma (please solve)

[Claus Reinke]

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

I've already answered the last question. as for polymorphism, all this
requires is for a graph type parameterized by an edge and vertex
type (just as the SML solution, which got full marks in this category,
requires instantiations of the edge and vertex types in the graph structure). 
I already gave an example of a graph instantiated with (Int,Int) edges 
and Int vertices. see below for a translation of the ATC paper examples
 
>> 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)? 

it suffers as little as the previous variant. and it was meant to be a special
form, showing that the full generality of ATs as a separate type class 
extension is not required to solve that paper's issue. and the translation 
from type functions to FDs or ATs is entirely syntactic, I think, so it 
would be nice to have in Haskell', as long as at least one of the two is 
included.

> Would
> 
>   instance Graph Int
>     -- methods left undefined
> 
> be a type error here?

yes, of course. instances still have to be instances of classes. in variation
A, the type error would be in the instance head, in variation B, it would
be in the method types (although it could backpropagate to the head).

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

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

you're free to your own opinions, of course!-)

it is, however, probably as close as we can come within current Haskell,
and the shifting of Edge/Vertex to the right of the '=>' is a purely syntactic
transformation, even if it is a nice one.

and as you can see from the implementation below (I had to move the 
class methods out of the class to circumvent GHC's current typing problem, 
so no method implementations, only the types), it is sufficient to address the 
problem in that survey paper, and accounting for graphs with specific types 
is no problem (direct translation from ATC paper examples):

    *Main> :t \e->src e (undefined::NbmGraph)
    \e->src e (undefined::NbmGraph) :: GE2 -> GV2
    *Main> :t \e->src e (undefined::AdjGraph)
    \e->src e (undefined::AdjGraph) :: GE1 -> GV1

cheers,
claus

{-# OPTIONS_GHC -fglasgow-exts #-}

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 Graph g
-- these should be class methods of Graph..
src, tgt :: (Edge g e,Vertex g v,Graph g) => e -> g -> v
src = undefined
tgt = undefined

-- adjacency matrix
data G1 e v = G1 [[v]]
data GV1 = GV1 Int
data GE1 = GE1 GV1 GV1
type AdjGraph = G1 GE1 GV1  -- type associations

instance Graph AdjGraph

-- neighbor map
data FiniteMap a b
data G2 e v = G2 (FiniteMap v v) 
data GV2 = GV2 Int
data GE2 = GE2 GV2 GV2
type NbmGraph = G2 GE2 GV2  -- type associations

instance Graph NbmGraph