conic-graphs

Vinyl-style extensible graphs.

A vinyl style extensible record is a hetrogenous list, using a type-level list to track the indicies. The constructors of Rec mirror the constructors of the list used to index them.

data Rec :: (u -> *) -> [u] -> * where
  RNil :: Rec f '[]
  (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)

We can apply the same method to the algebraic-graphs definition, albeit with four constructors instead of two.

data RGraph :: (u -> *) -> Graph u -> * where
  REmpty :: RGraph f 'Empty
  RVertex :: !(f r) -> RGraph f ('Vertex r)
  ROverlay :: !(RGraph f xs) -> !(RGraph f ys) -> RGraph f ('Overlay xs ys)
  RConnect :: !(RGraph f xs) -> !(RGraph f ys) -> RGraph f ('Connect xs ys)

Then each vertex of the RGraph may be of a different type, with the types tracked in the type level Graph.

type G = 'Connect ('Vertex Int) ('Vertex String)

myGraph :: RGraph Identity G
myGraph = RConnect (RVertex (Identity 5)) (RVertex (Identity "foo"))

Using fcf-graphs, we are able to perform type-level graph computations to match the operations at the term level.

edge :: f a -> f b -> RGraph f (Eval (Edge a b))
edge x y = RConnect (RVertex x) (RVertex y)

Including, collapsing RGraphs to vinyl Recs by computing the type level list of vertex types.

data VertexList :: Graph a -> Exp [a]

type instance Eval (VertexList 'Empty) = '[]

type instance Eval (VertexList ('Vertex x)) = '[x]

type instance Eval (VertexList ('Overlay x y)) = Eval (LiftM2 (++) (VertexList x) (VertexList y))

type instance Eval (VertexList ('Connect x y)) = Eval (LiftM2 (++) (VertexList x) (VertexList y))

vertexList :: RGraph f xs -> Rec f (Eval (VertexList xs))
vertexList REmpty = RNil
vertexList (RVertex x) = x :& RNil
vertexList (ROverlay x y) = rappend (vertexList x) (vertexList y)
vertexList (RConnect x y) = rappend (vertexList x) (vertexList y)

ghci> vertexList myGraph
{5, "foo"}

(Note, we use a different version of rappend that makes it more obvious to fcf that this is what we mean, defined in fcf-vinyl.