Can the type of valid graphs be encoded in Dhall?

Question

I'd like to represent a wiki (a set of documents comprising a directed graph) in Dhall. These documents will be rendered to HTML, and I'd like to prevent broken links from ever being generated. As I see it, this could be accomplished either by making invalid graphs (graphs with links to non-existent nodes) unrepresentable through the type system or by writing a function to return a list of errors in any possible graph (e.g. "In possible graph X, Node A contains a link to a non-existent Node B").

A naive adjacency list representation might look something like this:

let Node : Type = {
    id: Text,
    neighbors: List Text
}
let Graph : Type = List Node
let example : Graph = [
    { id = "a", neighbors = ["b"] }
]
in example

As this example makes evident, this type admits values that do not correspond to valid graphs (there is no node with an id of "b", but the node with id "a" stipulates a neighbor with id "b"). Moreover, it is not possible to generate a list of these issues by folding over the neighbors of each Node, because Dhall does not support string comparison by design.

Is there any representation that would allow for either the computation of a list of broken links or the exclusion of broken links through the type system?

UPDATE: I've just discovered that Naturals are comparable in Dhall. So I suppose a function could be written to identify any invalid edges ("broken links") and duplicate uses of an identifier if the identifiers were Naturals.

The original question, though, of whether a Graph type can be defined, remains.

Annemarie

Represent the graph as a list of edges instead. The nodes can be inferred from the existing edges. Each edge would consist of a source node and a destination node, but to accommodate disconnected nodes, the destination can be optional. – Foible

Answer 1

Yes, you can model a type-safe, directed, possibly-cyclic, graph in Dhall, like this:

let List/map =
      https://prelude.dhall-lang.org/v14.0.0/List/map sha256:dd845ffb4568d40327f2a817eb42d1c6138b929ca758d50bc33112ef3c885680

let Graph
    : Type
    =     forall (Graph : Type)
      ->  forall  ( MakeGraph
                  :     forall (Node : Type)
                    ->  Node
                    ->  (Node -> { id : Text, neighbors : List Node })
                    ->  Graph
                  )
      ->  Graph

let MakeGraph
    :     forall (Node : Type)
      ->  Node
      ->  (Node -> { id : Text, neighbors : List Node })
      ->  Graph
    =     \(Node : Type)
      ->  \(current : Node)
      ->  \(step : Node -> { id : Text, neighbors : List Node })
      ->  \(Graph : Type)
      ->  \ ( MakeGraph
            :     forall (Node : Type)
              ->  Node
              ->  (Node -> { id : Text, neighbors : List Node })
              ->  Graph
            )
      ->  MakeGraph Node current step

let -- Get `Text` label for the current node of a Graph
    id
    : Graph -> Text
    =     \(graph : Graph)
      ->  graph
            Text
            (     \(Node : Type)
              ->  \(current : Node)
              ->  \(step : Node -> { id : Text, neighbors : List Node })
              ->  (step current).id
            )

let -- Get all neighbors of the current node
    neighbors
    : Graph -> List Graph
    =     \(graph : Graph)
      ->  graph
            (List Graph)
            (     \(Node : Type)
              ->  \(current : Node)
              ->  \(step : Node -> { id : Text, neighbors : List Node })
              ->  let neighborNodes
                      : List Node
                      = (step current).neighbors

                  let nodeToGraph
                      : Node -> Graph
                      =     \(node : Node)
                        ->  \(Graph : Type)
                        ->  \ ( MakeGraph
                              :     forall (Node : Type)
                                ->  forall (current : Node)
                                ->  forall  ( step
                                            :     Node
                                              ->  { id : Text
                                                  , neighbors : List Node
                                                  }
                                            )
                                ->  Graph
                              )
                        ->  MakeGraph Node node step

                  in  List/map Node Graph nodeToGraph neighborNodes
            )

let {- Example node type for a graph with three nodes

           For your Wiki, replace this with a type with one alternative per document
        -}
    Node =
      < Node0 | Node1 | Node2 >

let {- Example graph with the following nodes and edges between them:

                       Node0 ↔ Node1
                         ↓
                       Node2
                         ↺

           The starting node is Node0
        -}
    example
    : Graph
    = let step =
                \(node : Node)
            ->  merge
                  { Node0 = { id = "0", neighbors = [ Node.Node1, Node.Node2 ] }
                  , Node1 = { id = "1", neighbors = [ Node.Node0 ] }
                  , Node2 = { id = "2", neighbors = [ Node.Node2 ] }
                  }
                  node

      in  MakeGraph Node Node.Node0 step

in  assert : List/map Graph Text id (neighbors example) === [ "1", "2" ]

This representation guarantees the absence of broken edges.

I also turned this answer into a package you can use:

• https://github.com/Gabriel439/graph

Edit: Here are relevant resources and additional explanation that can help illuminate what is going on:

First, start from the following Haskell type for a tree:

data Tree a = Node { id :: a, neighbors :: [ Tree a ] }

You can think of this type as a lazy and potentially infinite data structure representing what you would get if you just kept visiting neighbors.

Now, let's pretend that the above Tree representation actually is our Graph by just renaming the datatype to Graph:

data Graph a = Node { id :: a, neighbors :: [ Graph a ] }

... but even if we wanted to use this type we don't have a way to directly model that type in Dhall because the Dhall language does not provide built-in support for recursive data structures. So what do we do?

Fortunately, there actually is a way to embed recursive data structures and recursive functions in a non-recursive language like Dhall. In fact, there are two ways!

• F-algebras - Used to implement recursion
• F-coalgebras - Used to implement "corecursion"

The first thing I read that introduced me to this trick was the following draft post by Wadler:

• Recursive types for free!

... but I can summarize the basic idea using the following two Haskell types:

{-# LANGUAGE RankNTypes #-}

-- LFix is short for "Least fixed point"
newtype LFix f = LFix (forall x . (f x -> x) -> x)

... and:

{-# LANGUAGE ExistentialQuantification #-}

-- GFix is short for "Greatest fixed point"
data GFix f = forall x . GFix x (x -> f x)

The way that LFix and GFix work is that you can give them "one layer" of your desired recursive or "corecursive" type (i.e. the f) and they then give you something that is as powerful as the desired type without requiring language support for recursion or corecursion.

Let's use lists as an example. We can model "one layer" of a list using the following ListF type:

-- `ListF` is short for "List functor"
data ListF a next = Nil | Cons a next

Compare that definition to how we would normally define an OrdinaryList using an ordinary recursive datatype definition:

data OrdinaryList a = Nil | Cons a (OrdinaryList a)

The main difference is that ListF takes one extra type parameter (next), which we use as a placeholder for all recursive/corecursive occurrences of the type.

Now, equipped with ListF, we can define recursive and corecursive lists like this:

type List a = LFix (ListF a)

type CoList a = GFix (ListF a)

... where:

• List is a recursive list implemented without language support for recursion
• CoList is a corecursive list implemented without language support for corecursion

Both of these types are equivalent to ("isomorphic to") [], meaning that:

• You can convert reversibly back and forth between List and []
• You can convert reversibly back and forth between CoList and []

Let's prove that by defining those conversion functions!

fromList :: List a -> [a]
fromList (LFix f) = f adapt
  where
    adapt (Cons a next) = a : next
    adapt  Nil          = []

toList :: [a] -> List a
toList xs = LFix (\k -> foldr (\a x -> k (Cons a x)) (k Nil) xs)

fromCoList :: CoList a -> [a]
fromCoList (GFix start step) = loop start
  where
    loop state = case step state of
        Nil           -> []
        Cons a state' -> a : loop state'

toCoList :: [a] -> CoList a
toCoList xs = GFix xs step
  where
    step      []  = Nil
    step (y : ys) = Cons y ys

So the first step in implementing the Dhall type was to convert the recursive Graph type:

data Graph a = Node { id :: a, neighbors :: [ Graph a ] }

... to the equivalent co-recursive representation:

data GraphF a next = Node { id ::: a, neighbors :: [ next ] }

data GFix f = forall x . GFix x (x -> f x)

type Graph a = GFix (GraphF a)

... although to simplify the types a little bit I find it's easier to specialize GFix to the case where f = GraphF:

data GraphF a next = Node { id ::: a, neighbors :: [ next ] }

data Graph a = forall x . Graph x (x -> GraphF a x)

Haskell doesn't have anonymous records like Dhall, but if it did then we could simplify the type further by inlining the definition of GraphF:

data Graph a = forall x . MakeGraph x (x -> { id :: a, neighbors :: [ x ] })

Now this is starting to look like the Dhall type for a Graph, especially if we replace x with node:

data Graph a = forall node . MakeGraph node (node -> { id :: a, neighbors :: [ node ] })

However, there's still one last tricky part, which is how to translate the ExistentialQuantification from Haskell to Dhall. It turns out that you can always translate existential quantification to universal quantification (i.e. forall) using the following equivalence:

exists y . f y ≅ forall x . (forall y . f y -> x) -> x

I believe this is called "skolemization"

For more details, see:

• Wikipedia - Existential Quantification

... and that final trick gives you the Dhall type:

let Graph
    : Type
    =     forall (Graph : Type)
      ->  forall  ( MakeGraph
                  :     forall (Node : Type)
                    ->  Node
                    ->  (Node -> { id : Text, neighbors : List Node })
                    ->  Graph
                  )
      ->  Graph

... where forall (Graph : Type) plays the same role as forall x in the previous formula and forall (Node : Type) plays the same role as forall y in the previous formula.

Pereyra

Thank you so much for this answer, and for all of the hard work required to develop Dhall! Could you suggest any material newcomers to Dhall/System F could read to better understand what you've done here, what other possible graph representations there might be? I'd like to be able to extend what you've done here to write a function that can produce the adjacency list representation from any value of your Graph type through a depth first search. – Annemarie

@BjørnWestergard: You're welcome! I edited my answer to explain the theory behind it, including useful references – Pereyra