# 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.