Help Using Functional Dependencies

Question

I have a question about functional dependencies. My understanding was that, for example, if I write class Graph gab | g -> a, g -> b class Graph gab | g -> a, g -> b , then any particular g can be associated with only one type of a and b . Indeed, trying to declare two instances 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 gab | 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 gab => Subgraph gab | g -> a, g -> b where extVertices :: g -> [b] data Subgraph1 g where Subgraph1 :: Graph gab => g -> [b] -> Subgraph1 g instance Graph gab => Graph (Subgraph1 g) ab where vertices (Subgraph1 g _) = vertices g edges (Subgraph1 g _) = edges g src (Subgraph1 g _) = src g dst (Subgraph1 g _) = dst g 

If I rework Subgraph1 , adding a and b parameters to the type signature, then everything will work.

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

Answer 1

Do not use funds, they are too strong. Use related 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 

It looks a bit more readable. Edge g - type of edges g , etc.

Please note that I translated your code mechanically without understanding what Subgraph1 does. Why do you need GADT here, and what does the second argument to the data constructor mean? It is not used anywhere.