Introduction to type-safe graphs

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. Before running it, make sure you have headphones plugged in, as the example will use your microphone.

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:

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 uses purescript-typelevel-graph to guarantee the type safety of its audio graph. Let's look at two small examples from 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.

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.

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.

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 is outgoing edges, meaning that the SList after each node shows a list of outgoing edges. However, in 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.

Conclusion

Type-level programming can sometimes feel pretty abstract, but in the case of 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).