Search code examples
haskellfunctional-dependencies

help with use of functional dependencies


I have a question about functional dependencies. My understanding was that, for example, if I write class Graph g a b | g -> a, g -> b, then any specific g can be associated with only one type of a and b. Indeed, trying to declare two instance with the same g and different a and b does not work.

However, the compiler (ghc) seems unable to use the dependency in the following case,

class (Eq a, Eq b) => Graph g a b | g -> a, g -> b where
    edges :: g -> [b]
    src :: g -> b -> a
    dst :: g -> b -> a

    vertices :: g -> [a]
    vertices g = List.nub $ map (src g) (edges g) ++ map (dst g) (edges g)

class Graph g a b => Subgraph g a b | g -> a, g -> b where
    extVertices :: g -> [b]

data Subgraph1 g where
    Subgraph1 :: Graph g a b => g -> [b] -> Subgraph1 g

instance Graph g a b => Graph (Subgraph1 g) a b where
    vertices (Subgraph1 g _) = vertices g
    edges (Subgraph1 g _) = edges g
    src (Subgraph1 g _) = src g
    dst (Subgraph1 g _) = dst g

If I revise Subgraph1 by adding the parameters a and b to the type signature, then everything works out.

data Subgraph1 g a b where
    Subgraph1 :: Graph g a b => g -> [b] -> Subgraph1 g a b

Solution

  • Don't use fundeps, they are too much pain. Use associated types.

    class (Eq (Vertex g), Eq (Edge g)) => Graph g where
      type Edge   g :: *
      type Vertex g :: *
    
      edges :: g -> [Edge g]
      src   :: g -> Edge g -> Vertex g
      dst   :: g -> Edge g -> Vertex g
    
      vertices :: g -> [Vertex g]
      vertices g = nub $ map (src g) (edges g) ++ map (dst g) (edges g)
    
    class Graph g => Subgraph g where
      extVertices :: g -> [Edge g]
    
    data Subgraph1 g where
        Subgraph1 :: Graph g => g -> [Edge g] -> Subgraph1 g
    
    instance Graph g => Graph (Subgraph1 g) where
        type Edge (Subgraph1 g) = Edge g
        type Vertex (Subgraph1 g) = Vertex g
        vertices (Subgraph1 g _) = vertices g
        edges (Subgraph1 g _) = edges g
        src (Subgraph1 g _) = src g
        dst (Subgraph1 g _) = dst g
    

    This looks somewhat more readable. Edge g is the type of g's edges, etc.

    Note that I translated your code mechanically, without understanding what Subgraph1 does. Why do you need a GADT here, and what the second argument of the data constructor means? It is not used anywhere.