Support for Traversals

[bwestergard]

@Gabriel439: Thank you again for writing this helpful Dhall snippet. I'm bringing my further questions here to make it easier for others to find them.

Would it be possible to implement common graph traversals for this type? For instance, mapping across each vertex in an arbitrary order, or in a topological order? I'd be happy to take this on myself if you could provide pointers to literature describing how best to do so.

[Gabriella439]

@bwestergard: Yes, it is possible to implement other graph operations. I updated the linked StackOverflow answer with some of the theory behind what is going on.

In general, I find it's easiest to first model things in Haskell using the following equivalent Haskell type:

{-# LANGUAGE ExistentialQuantification #-}

data Vertex a node = Vertex { label :: a, neighbors :: [node] }

data Graph a =
    forall node . Graph { start :: node, step :: node -> Vertex a node }

... and then implement operations on that and translate them back to Dhall.

For example, if you want to implement map to transform all labels in a Graph, the Haskell code for that would essentially be a Functor instance for Graph:

{-# LANGUAGE ExistentialQuantification #-}

module Test where

import Data.Bifunctor

data Vertex a node = Vertex { label :: a, neighbors :: [node] }

instance Bifunctor Vertex where
    first f (Vertex label nodes) = Vertex (f label) nodes

    second f (Vertex label nodes) = Vertex label (fmap f nodes)

data Graph a =
    forall node . Graph { start :: node, step :: node -> Vertex a node }

instance Functor Graph where
    fmap f (Graph start step) = Graph start step'
      where
        step' state = first f (step state)

... and translating that to Dhall, gives:

let Graph = ./Graph.dhall

let map
    : ∀(a : Type) → ∀(b : Type) → (a → b) → Graph a → Graph b
    =   λ(a : Type)
      → λ(b : Type)
      → λ(f : a → b)
      → λ(graph : Graph a)
      → λ(Graph : Type)
      → λ ( MakeGraph
          :   ∀(Vertex : Type)
            → Vertex
            → (Vertex → { label : b, neighbors : List Vertex })
            → Graph
          )
      → graph
          Graph
          (   λ(Vertex : Type)
            → λ(start : Vertex)
            → λ(step : Vertex → { label : a, neighbors : List Vertex })
            → let newStep =
                      λ(state : Vertex)
                    → let result = step state

                      in  { label = f result.label
                          , neighbors = result.neighbors
                          }

              in  MakeGraph Vertex start newStep
          )

in  map

There are still some non-obvious steps in that translation, though, and a lot of it is learning how to encode higher-level programming idioms in System F.

The general name for the trick of encoding data structures in System F is Boehm-Berarducci encoding, which originated in this paper:

• Automatic synthesis of typed Λ-programs on term algebras

The paper is a little terse, but if you follow it closely it spells out the general algorithm for translating data types into System F and also how to translate functions on those types, too.

I also wrote a post related to that paraphrasing what I had learned in my own words:

• Data is Code

... which also introduced a language called annah, which was one of the precursors to dhall.

However, in my experience the thing that really helped me better how to translate things was to "follow the types". For example, for the above map function there is essentially only one way to implement the function that will type-check and since Dhall's type system doesn't have any escape hatches you can essentially play type tetris until you arrive at the one and only implementation.

Doing that sort of "type tetris" repeatedly is how I got much more proficient at these sorts of translations.

[Gabriella439]

I forgot to also mention that a useful stepping stone to understanding Boehm-Berarducci encoding is to study Church encoding first, which is essentially the same algorithm, except for a language without explicit types

[bwestergard]

This is fascinating!

A follow up question: So I see now how map over labels can be written, and how the Graph type is cleverly derived from the recursive type in Haskell.

But can a useful fold be written? In other words, a function that applies a function to each vertex (i.e. each { label: Text, neighbor: List Vertex} record in the graph) once and accumulates a result? If this were possible, it would be trivial to convert between a value of your Graph type and the equivalent value of the type List Node in my Stackoverflow question.

My vague intuition is that such a fold function cannot be written for Graph because there is no way to exclude vertices that have already been "visited" in subsequent steps. For that, I suppose the System F equivalents of these inductive graph types would be required.

[Gabriella439]

@bwestergard: Probably the simplest solution that gives you what you want would be to change the start Vertex into a List Vertex or NonEmpty Vertex. My reasoning is that the current Graph representation does not let one reach any Vertex that is disconnected from the starting Vertex, but if you just store all possible vertices then the problem goes away and you get the ability to list all vertices for free.

[bwestergard]

@Gabriel439 That's actually what I started playing around with. It's a shame to have to write out a List with one instance of each alternative in the union type manually.

let Vertex = < Vertex0 | Vertex1 | Vertex2 >
let vertices : List Vertex = [ Vertex.Vertex0, Vertex.Vertex1, Vertex.Vertex2 ]

I can't really think of a good way to DRY this out any further. I suppose Dhall could be extended with some syntactic sugar like toList Vertex for union types with all empty alternatives, but this seems like a hack.

[Gabriella439]

@bwestergard: Yeah, I'm not aware of a way to make that simpler. It's probably too narrow a use case to add language support unless we require the same feature in other areas