Data.Graph

Directed graphs over an ordered node type, with the deterministic algorithms the compiler relies on internally, mirrored into Prism.

A graph is an adjacency Map(k, List(k)) from a node to its successor list (the same “a set is a Map(k, Unit)” idiom Data.Set uses, so no new wired type is needed). Every traversal visits nodes and successors in ascending Ord(k) order, so output is a pure function of the edge set, never of insertion order or hashing. The strongly-connected-components pass is Tarjan’s, returning components callee-first (each component after the ones it points to) with each component’s members in ascending order, matching the compiler’s own SCC. Opt-in: not in Base.

Functions and Values

graph_empty

graph_empty : forall a b. Map(a, List(a), b)

The empty graph.

graph_successors

graph_successors : forall a b. (Map(b, List(b), a), b) -> List(b)

The successors of u in ascending order (empty if u has no out-edges).

graph_successors(graph_from_edges([(1, 3), (1, 2), (1, 2)]), 1)

[2, 3]

graph_add_node

graph_add_node : forall a b. (Map(b, List(b), a), b) -> Map(b, List(b), a)

Add u as a node with no new edges (a no-op if already present).

graph_add_edge

graph_add_edge : forall a b. (Map(b, List(b), a), b, b) -> Map(b, List(b), a)

Add the directed edge u -> v, keeping each successor list sorted and duplicate-free so iteration stays deterministic.

graph_from_edges

graph_from_edges : forall a b. (List((b, b))) -> Map(b, List(b), a)

Build a graph from a list of directed (from, to) edges.

graph_nodes

graph_nodes : forall a b. (Map(b, List(b), a)) -> List(b)

Every node, in ascending order: the sources plus everything pointed at, so a sink that only ever appears as a successor still shows up.

graph_nodes(graph_from_edges([(3, 1), (1, 2)]))

[1, 2, 3]

graph_reverse

graph_reverse : forall a b c. (Map(c, List(c), a)) -> Map(c, List(c), b)

The reverse graph: every edge u -> v becomes v -> u. Nodes are preserved, so an isolated node survives.

graph_successors(graph_reverse(graph_from_edges([(1, 2), (3, 2)])), 2)

[1, 3]

graph_dfs

graph_dfs : forall a b. (Map(b, List(b), a), b) -> List(b)

Depth-first preorder from start: start, then its successors’ subtrees, successors taken in ascending order. Each node appears once.

(graph_dfs(g, 1), graph_bfs(g, 1))

([1, 2, 4, 3], [1, 2, 3, 4])

graph_bfs

graph_bfs : forall a b. (Map(b, List(b), a), b) -> List(b)

Breadth-first order from start, successors taken in ascending order. Each node appears once.

graph_reachable

graph_reachable : forall a b. (Map(b, List(b), a), b) -> List(b)

The nodes reachable from start (including start), in ascending order.

graph_transitive_closure

graph_transitive_closure : forall a b c. (Map(c, List(c), a)) -> Map(c, List(c), b)

The transitive closure: an edge u -> v for every v reachable from u via at least one step (so u -> u only when u lies on a cycle).

graph_successors(graph_transitive_closure(graph_from_edges([(1, 2), (2, 3)])), 1)

[2, 3]

graph_topo_sort

graph_topo_sort : forall a b. (Map(b, List(b), a)) -> List(b)

Topological order: a node before every node it points to. Deterministic via a depth-first postorder over nodes in ascending order, reversed. A graph with a cycle still yields a total order, but not a valid topo sort (a cycle admits none); pair it with graph_scc when cycles are possible.

graph_topo_sort(graph_from_edges([(1, 2), (1, 3), (2, 3)]))

[1, 2, 3]

graph_scc

graph_scc : forall a b. (Map(b, List(b), a)) -> List(List(b))

Tarjan’s strongly-connected components, returned callee-first: a component comes after every component reachable from it, and each component’s members are in ascending order. A node with no self-loop is its own singleton component. This mirrors the compiler’s own SCC ordering exactly.

graph_scc(graph_from_edges([(1, 2), (2, 1), (2, 3)]))

[[3], [1, 2]]