Introduction to type-safe graphs
Tags: functional
Published: 2020-10-10 08:51:34

---
title: Introduction to type-safe graphs
published: true
description: A way to make assertions about signal-flow diagrams and state machines at compile time
tags: functional
cover_image: https://6lli539m39y3hpkelqsm3c2fg-wpengine.netdna-ssl.com/wp-content/uploads/2013/11/image2.jpg
---

As developers, we work with graphs all the time.  For front-end developers, what a user sees at any time can be thought of as nodes of a graph, and the transitions between nodes are edges.  For anyone working with signal processing, individual processing units are nodes and their connections are edges.

Often times, parts of these graphs are deterministic.  For example, in a state machine, there are certain properties that stay the same throughout the whole lifecycle of an application. In strongly-typed languages, these properties can be asserted at compile-time using typelevel graph constraints.  In this article, I'd like to briefly show what typelevel graph constraints and manipulations are, how to use them, and how they help in the real world.

## Typelevel graphs in the real world

We'll start with a real-world example.  Using Firefox, copy-and paste the following code into [klank.dev](https://klank.dev). Before running it, make sure you have headphones plugged in, as the example will use your microphone.

```haskell
module Klank.Dev where

import Prelude
import Data.List (List(..))
import Data.NonEmpty ((:|))
import Data.Symbol (SProxy(..))
import Data.Tuple (Tuple(..))
import Data.Typelevel.Num (D1)
import FRP.Behavior (Behavior)
import FRP.Behavior.Audio (AudioUnit, g'add, g'bandpass, g'delay, g'gain, gain, graph, microphone, runInBrowser, speaker)
import Record.Extra (SLProxy(..), SNil)
import Type.Data.Graph (type (:/))
import Math(pi, sin)

scene :: Number -> Behavior (AudioUnit D1)
scene t = pure
        ( speaker
            ( ( graph
                  { aggregators:
                      { out: Tuple g'add (SLProxy :: SLProxy ("combine" :/ SNil))
                      , combine: Tuple g'add (SLProxy :: SLProxy ("gain" :/ "mic" :/ SNil))
                      , gain: Tuple (g'gain 0.9) (SLProxy :: SLProxy ("del" :/ SNil))
                      }
                  , processors:
                      { del: Tuple (g'delay (0.7 + 0.5 * sin (0.3 * t * pi))) (SProxy :: SProxy "filt")
                      , filt: Tuple (g'bandpass 1000.0 1.0) (SProxy :: SProxy "combine")
                      }
                  , generators:
                      { mic: microphone
                      }
                  }
              )
                :| Nil
            )
        )

enableMicrophone = true

main = runInBrowser scene
```

In this example, we create a signal-processing chain that modulates the voice by a time-variant delay, creating an alternating speed-up and slow-down effect.

The example above creates a graph that looks like this:

![Graph](https://dev-to-uploads.s3.amazonaws.com/i/kvw45qdoy88rr1qj9wfe.png)

Reading the code, you can see that `combine` consumes `mic` and `gain`, that `gain` consumes `del`, etc.  Representing a graph this called an **adjacency list**.

To see why this is type-safe, you can try changing some of the symbols above.

- After `gain`, change `(SLProxy :: SLProxy ("del" :/ SNil))` to `(SLProxy :: SLProxy ("delll" :/ SNil))`.
- After `combine`, change `(SLProxy :: SLProxy ("gain" :/ "mic" :/ SNil))` to `(SLProxy :: SLProxy SNil)`.

Both will result in compilation errors:

- The first one uses a node `delll` that does not exist.
- The second one disconnects the graph, as `combine` no longer has any input and thus forms a separate subgraph with `out`.

Catching this sort of mistake at compile-time instead of runtime can save _hours_ of signal processing debugging, especially as graphs get more complicated.

So how does the compiler know that `filt` is a node in the graph, that the graph is connected, that there are no orphan nodes, etc?  This is where type-safe graphs come in.  They can be used to build state-machines, signal-processing chains like the one above, or anything where you need to make assertions about a graph's properties.

## Typelevel graphs in theory

Under the hood, [klank.dev](https://klank.dev) uses [`purescript-typelevel-graph`](https://github.com/mikesol/purescript-typelevel-graph) to guarantee the type safety of its audio graph.  Let's look at two small examples from [`purescript-typelevel-graph`](https://github.com/mikesol/purescript-typelevel-graph) to see how assertions about a graph can catch errors at compile time. We'll also look at one example of graph manipulation.

### Connectivity

The following type class asserts that a graph is connected.

```haskell
testConnected1 :: BProxy True
testConnected1 =
  BProxy ::
    forall b.
    IsConnected ( a :: (SLProxy ("a" :/ SNil)), b :: (SLProxy ("a" :/ SNil)) ) b =>
    BProxy b
```

Here, `a` loops to itself and `b` is connected to `a`. If you change `b` to be connected to only itself, the compilation will fail.  To make it succeed, you'd have to use `BProxy False`, which is the equivalent of declaring that the graph is disconnected.

```haskell
testConnected1 :: BProxy False
testConnected1 =
  BProxy ::
    forall b.
    IsConnected ( a :: (SLProxy ("a" :/ SNil)), b :: (SLProxy ("b" :/ SNil)) ) b =>
    BProxy b
```

### Unique terminus

It's often the case in signal processing graphs that you will want a unique terminal state, ie sound coming from a speaker or electricity going to a light switch.  This can be accomplished with the `HasUniqueTerminus` typeclass.

```haskell
hasUniqueTerminus2 :: BProxy True
hasUniqueTerminus2 =
  BProxy ::
    forall b.
    HasUniqueTerminus
      ( "q" :: SLProxy ("a" :/ "r" :/ SNil)
      , "a" :: SLProxy SNil
      , "f" :: SLProxy ("r" :/ "p" :/ SNil)
      )
      b =>
    BProxy b
```

Here, `a` is a unique terminus in the graph, so the `BProxy` is `True`.

### Flipping the direction of a graph

The native representation of edge direction in [`purescript-typelevel-graph`](https://github.com/mikesol/purescript-typelevel-graph) is outgoing edges, meaning that the `SList` after each node shows a list of _outgoing_ edges.  However, in [`purescript-audio-behaviors`](https://github.com/mikesol/purescript-audio-behaviors), the edge list is _incoming_. To flip the direction of a graph, one can use the `FlipDirection` typeclass.

```
flipDirection ::
  RProxy
    ( "q" :: SLProxy SNil
    , "a" :: SLProxy ("f" :/ "q" :/ SNil)
    , "f" :: SLProxy SNil
    , "r" :: SLProxy ("q" :/ SNil)
    , "p" :: SLProxy ("f" :/ SNil)
    )
flipDirection =
  RProxy ::
    forall (r :: # Type).
    FlipDirection
      ( "q" :: SLProxy ("a" :/ "r" :/ SNil)
      , "a" :: SLProxy SNil
      , "f" :: SLProxy ("a" :/ "p" :/ SNil)
      , "r" :: SLProxy SNil
      , "p" :: SLProxy SNil
      )
      r =>
    RProxy r
```

All of these functions are part of the test suite of [`purescript-typelevel-graph`](https://github.com/mikesol/purescript-typelevel-graph).

## Conclusion

Type-level programming can sometimes feel pretty abstract, but in the case of [klank.dev](https://klank.dev), typelevel programming allows me to catch a lot of gnarly signal-flow bugs at compile time.  I hope this article has given you intuition about the type of assertions you can make about graphs at compile time in a strongly-typed functional language (ie PureScript, Haskell, Typescript).