The Brown PLT Blog

Diagramming Program Values by Spatial Refinement

Tags: Diagram, Programming Languages, Spatial, Tools, Visualization

Compilers can vectorize loops you never wrote. IDEs can finish functions before you do. Agents can refactor your codebase from a sentence. And yet, when you want to inspect the value your program just produced, you still use the REPL as if nothing has changed in fifty years: type a variable name, get text back, squint. Here is Python showing you a binary decision diagram:

Node(15, 'x1', Node(14, 'x2', Node(8, 'x3', TRUE, FALSE), Node(4, 'x3', FALSE, TRUE)), Node(3, 'x2', FALSE, TRUE))

That is, technically, the value you wanted to inspect. The way it is shown is also not super useful. Anyone who has ever debugged a BDD knows the move that comes next: you reach for paper and pen and draw the thing, because we reason about these data structures spatially. (They are called binary decision diagrams, after all.)

What you want to see (and what you might draw by hand) is something like this:

This diagram is useful because it embodies the spatial conventions we use when talking about BDDs: top-down variable layers, nodes grouped by variable, visually distinct high and low edges, and shared terminals. These conventions are how the data structure becomes readable.

So why not generate diagrams like this whenever we need them? Because the usual way is to write drawing code. Before the picture can tell you anything, you have to choose marks, compute positions, handle updates, and own a pile of rendering details. Some of that captures the BDD conventions that matter; much of it is scaffolding.

Here’s the thing: the language already gives us enough structure to draw a faithful diagram of the instance. To show you a value at the REPL, the runtime has to use mechanisms like introspection, printing, or serialization: ways of walking records, atoms, fields, and references. Turn records and atoms into nodes, fields and references into edges, and you get a diagram that preserves the value’s structure without asking the programmer to write drawing code. It may not be pretty, but it is faithful to the underlying value. The remaining diagramming work, then, is just of refinement. To abuse a line attributed to Michelangelo: David was already in the marble; the BDD was already in the value graph.

Spytial is a language built for this kind of diagramming of program values. It starts with the faithful value graph, then lets rules add the constraints that matter: same-variable nodes align, children sit below parents, high and low edges differ, implementation details disappear. Each rule makes the picture more like the diagram you wanted. Because the rules describe relationships rather than drawing steps, you are writing a specification, not a rendering pipeline.

The example below shows that process in stages: starting from the raw value structure, each stage adds more of the BDD convention until the diagram becomes recognizable.

@attribute(field="nid")
@hideAtom(selector="NoneType + int")

@align(selector="{x, y : Node | (x != y) and (x.v) = (y.v)}", direction="horizontal")

@orientation(selector="{x, y : Node | x->y in (lo + hi)}", directions=["below"])

@group(selector="{vr : str, y : Node | @:(vr) = @:(y.v)}", name="nodes")
@hideAtom(selector="str")

@atomColor(selector="{x: Node | @num:(x.nid) = 0}", value='red')
@atomColor(selector="{x: Node | @num:(x.nid) = 1}", value='blue')
@atomColor(selector="{x: Node | (@num:(x.nid) > 1)}", value='black')
@edgeColor(field="hi", value='green')
@edgeColor(field="lo", value='orange')
@orientation(selector="{x, y : Node | x->y in lo and (@num:(y.nid) > 1)}", directions=["left"])
@orientation(selector="{x, y : Node | x->y in hi and (@num:(y.nid) > 1)}", directions=["right"])

More precisely, a Spytial program denotes a set of acceptable 2D layouts, and each rule narrows that set by selecting the atoms and edges it constrains. A selector such as {x, y : Node | (x != y) and (x.v) = (y.v)} matches every pair of distinct nodes that test the same variable — on any BDD, not just this one. Because selectors describe structural patterns rather than rendering steps, rules are declarative and order-independent. There is no if, no callback, no rendering pipeline to maintain. You are writing a specification, not coding a visualizer.

By making spatial description a programming-languages problem, Spytial can do more than draw pictures. When rules conflict, the diagnostic can itself be spatial: Spytial isolates a minimal conflicting subset of constraints, relaxes it to produce a counterfactual diagram, and ties the offending elements back to the rules that caused the inconsistency. And because a specification describes a space of acceptable pictures rather than a single one, the same specifications can also run backward, enabling value construction through the diagram.

Spytial is designed to work across programming paradigms: we have integrated it with Python, Rust, and Pyret, and want to see it in your favorite language too. We think this recipe is what you need to cook up an integration, but reach out if you want help.

To learn more, read our upcoming PLDI paper or visit our getting-started guide for using Spytial.