Dependent Type Theory Implementation of a Graph

Question

In Haskell you find graphs defined like this:

data Graph a = GNode a (Graph a)

Or this:

data Graph a = Empty | Vertex a | Overlay (Graph a) (Graph a) | Connect (Graph a) (Graph a)

class Graph g where
  type Vertex g
  empty   :: g
  vertex  :: Vertex g -> g
  overlay :: g -> g -> g
  connect :: g -> g -> g

Or this:

type Graph = Table [Vertex]
type Table a = Array Vertex a
type Bounds = (Vertex, Vertex)
type Edge = (Vertex, Vertex)
type Vertex = Int

I am wondering why it is not implemented more like this (this is JavaScript):

class Graph {
  constructor() {
    this.nodes = []
    this.edges = []
  }
}

Or perhaps in Haskell-ish:

data Graph = Graph
  { nodes :: [Node]
  , edges :: [Edge]
  }

For example, in this Graph in Coq, it looks more like the JavaScript version (though I don't understand the Structure in Coq):

Structure Graph := {
  V :> nat ; (* The number of vertices. So the vertices are numbers 0, 1, ..., V-1. *)
  E :> nat -> nat -> Prop ; (* The edge relation *)
  E_decidable : forall x y : nat, ({E x y} + {~ E x y}) ;
  E_irreflexive : all x : V, ~ E x x ;
  E_symmetric : all x : V, all y : V, (E x y -> E y x)
}.

Finally, here seems to be a complete Coq graph definition:

Inductive Graph : V_set -> A_set -> Set :=
  | G_empty : Graph V_empty A_empty
  | G_vertex :
      forall (v : V_set) (a : A_set) (d : Graph v a) (x : Vertex),
      ~ v x -> Graph (V_union (V_single x) v) a
  | G_edge :
      forall (v : V_set) (a : A_set) (d : Graph v a) (x y : Vertex),
      v x ->
      v y ->
      x <> y ->
      ~ a (A_ends x y) -> ~ a (A_ends y x) -> Graph v (A_union (E_set x y) a)
  | G_eq :
      forall (v v' : V_set) (a a' : A_set),
      v = v' -> a = a' -> Graph v a -> Graph v' a'.

My question is, what a proper definition of a graph is in Dependent Type Theory in formal type theory notation. Mathematically $G = (V, E)$, but in Coq and Haskell, things are a lot more functional/recursive. It seems weird that Haskell is defining it sometimes as a recursive structure. Wondering how to model this using the abstract type theory notation (using dependent types) and recursion if necessary, to get a better sense of realistic data structures in dependent type theory, and how to parse the formal notation. The types of graphs I am thinking about are directed, cyclic, and finite, non-hypergraphs.

Answer 1

So, there are two different things you are talking about.

1. The definition of a graph
2. The encoding of a graph

A Graph is always defined as a set of vertices and edges. This tells us what vertices are in the graph, and for any pair of vertices, whether there is an edge between them.

However, this definition is purely mathematical. A set isn't a "thing" that you can store in memory. So we need an encoding of a graph, so that the abstract mathematical set operations can be mapped onto concrete algorithmic operations.

Once you're talking about encoding, there are many different ways to implement a graph, all of which will give you something that is (in a sense) equivalent to the mathematical definition. But, there are practical trade-offs with different encodings:

• What operations are fast?
• What operations are easy to implement?
• How much memory does the graph take?
• How easy is it to use the graph in different settings.

In JavaScript, all types are dynamic, so it's easy to just say "A graph is a list of nodes and a list of edges", because the language doesn't ever require that you formally specify what a node or an edge looks like. It doesn't care, and if you make a mistake, it will just crash at runtime.

Notice that your JavaScript version of a graph doesn't actually specify how nodes and edges are represented. What does an edge look like? If you insert an edge as a 2-element array, but try to access it as an object, you will have a runtime error.

Haskell and Coq's definitions try to solve this issue with type safety. They have a formal definition of the different forms a Graph can take, so that you always know at compile-time which operations on it are valid or not.

Let's look at the versions and their tradeoffs:

data Graph a = Empty | Vertex a | Overlay (Graph a) (Graph a) | Connect (Graph a) (Graph a)

This version is interesting, because it is an inductive definition of a graph, that allows you to implement graph operations easily as recursive functions. So you know that a graph is always empty, a single vertex, the overlay of two graphs, or the connection of two graphs, and you can safely pattern match on these 4 cases.

class Graph g where
  type Vertex g
  empty   :: g
  vertex  :: Vertex g -> g
  overlay :: g -> g -> g
  connect :: g -> g -> g

This isn't actually an implementation of a graph, but instead is an interface for a graph. It says what operations are available on a graph, but not how they're implemented. Users could provide their own Graph instances, and can write code that is generic over which Graph implementation is used. This helps bring back some of the flexibility that we had in JavaScript but lost when adding types.

type Graph = Table [Vertex]
type Table a = Array Vertex a

This is a classic "Adjacency List" implementation of a graph: we store the outgoing edges for each vertex. It is space efficient, and allows for quick BFS and DFS, but is slower for checking the existence of an edge, or deleting an edge.

Structure Graph := {
  V :> nat ; (* The number of vertices. So the vertices are numbers 0, 1, ..., V-1. *)
  E :> nat -> nat -> Prop ; (* The edge relation *)
  E_decidable : forall x y : nat, ({E x y} + {~ E x y}) ;
  E_irreflexive : all x : V, ~ E x x ;
  E_symmetric : all x : V, all y : V, (E x y -> E y x)
}.

This is an interesting representation. First, it's similar to a typeclass, in that it's abstract: it works for any types $V$ and $E$ so long as they can be coerced into numbers and edge-lookup functions. This isn't saying "this is how you can represent a graph", it's saying "here's an interface for graph representations".

Second, because we are in a dependently typed setting, we want to encode some properties of the graph, so that we can't create ill-formed graphs. We can then use these properties when proving things about graphs later on. Here, there are three properties that we require all graphs to have:

1. The encoding must be irreflexive i.e. there are no self edges
2. The encoding must be symmetric i.e. any time there's an edge u->v, there's also an edge v->u
3. The edge relation is decidable i.e. we can take

The third condition is important because Coq is a total language. It doesn't allow for any non-terminating code, so we need to prove that our edge lookup actually halts.

Finally, there's the Coq graph definition:

Inductive Graph : V_set -> A_set -> Set :=
  | G_empty : Graph V_empty A_empty
  | G_vertex :
      forall (v : V_set) (a : A_set) (d : Graph v a) (x : Vertex),
      ~ v x -> Graph (V_union (V_single x) v) a
  | G_edge :
      forall (v : V_set) (a : A_set) (d : Graph v a) (x y : Vertex),
      v x ->
      v y ->
      x <> y ->
      ~ a (A_ends x y) -> ~ a (A_ends y x) -> Graph v (A_union (E_set x y) a)
  | G_eq :
      forall (v v' : V_set) (a a' : A_set),
      v = v' -> a = a' -> Graph v a -> Graph v' a'.

This version provides a concrete implementation, that (I think) fulfills the interface you gave. In particular, it says we can build a graph in 4 ways:

1. A graph can be empty
2. We can add a vertex to a graph
3. We can add an edge to a graph
4. We can map an equality over a graph

The beauty of this implementation is that the vertex and edge sets are stored at the type level. This is the magic of dependent types: the type of the graph depends on the values it contains. So, when adding an edge, the type system ensures that we can't possibly add an edge between two vertices that aren't in our vertex sets.

Secondly, this implementation is inductive, similar to the Haskell one, so writing proofs about this graph by induction will be easy.