Streams — Brief ☧
Deep version → | Back to Datalog →
Q: How many descendants does Abraham have?
A: The promise in Genesis says "as numerous as the stars of heaven" — effectively without limit.
Q: If a computer had a list of all those descendants, it would need infinite memory. That is not possible. So how do we deal with collections that might be endless?
A: Instead of building the entire list up front, we use a stream — a sequence that computes its next element only when you ask for it. Think of it like a scroll that writes itself as you unroll it: you never need the whole thing in memory at once, only the part you are currently reading.
Q: Why does miniKanren specifically need streams?
A: Because a logic query can have infinitely many answers. Consider
appendowith all three arguments left unknown — it generates every possible way to split every possible list. That is an infinite space. A stream lets you pull answers out one at a time: "give me the next answer," then "give me the next," as many as you need.Q: That makes sense for a single source of answers. But what if a query has two branches — say from a
conde— and both branches produce infinite answers? How do you avoid getting stuck on the first branch forever?A: This is the fairness problem, and it echoes the Prolog vs miniKanren distinction. If you only pull from the first branch, the second branch starves — just like Scribe A who never reaches Isaiah. The solution is interleaving: alternate between the branches, pulling one answer from each in turn. This way both branches make progress.
Streams in One Picture
graph LR
G["Goal"] --> S1["Stream: answer 1, answer 2, answer 3, ..."]
S1 --> TAKE["take(3)"]
TAKE --> R["[answer 1, answer 2, answer 3]"]A goal produces a stream. You consume as many answers as you need with take.
Three Stream Operations
| Operation | What it does | Analogy |
|---|---|---|
mplus | Merge two streams by interleaving | Two prophets speaking in turns — each gets heard |
bind | Apply a goal to each answer in a stream | Each disciple receives a message and carries it onward |
take | Pull N values from a stream | "Show me N witnesses" — you decide when to stop |
These three operations form the engine underneath miniKanren. Every conde produces an mplus (merging branches). Every conjunction (combining two goals) produces a bind (feeding answers from one goal into the next). And run N is just take N.
Types of Streams
# Empty stream: no answers
empty_chirho = []
# Mature stream: answers are ready now
mature_chirho = [subst1_chirho, subst2_chirho, subst3_chirho]
# Immature stream: a computation that has been paused (a "thunk")
immature_chirho = lambda: expensive_computation_chirho()The immature stream is the key insight. By wrapping a computation in a function that has not been called yet (a thunk), miniKanren can pause one branch and switch to another. This is the mechanism behind interleaving: each branch is an immature stream, and the system alternates which one it forces to produce its next answer.
In algorithm terms, this is a form of lazy evaluation — the iteration does not happen until it is needed. A queue-like discipline ensures every branch eventually gets a turn.
For Hardware
On the FPGA, streams become the command ring buffer — and this mapping is worth understanding carefully, because it is one of the most elegant aspects of the hardware design.
- Each entry in the ring is a search state — a snapshot of all variable domains at a particular point in the search. In software, this is a substitution dictionary; in hardware, it is a set of bitmask values stored in HBM slots.
- The ring FSM (finite state machine) pulls one entry at a time from the consumer pointer, processes it (applying constraints via AND), and either writes results to the output buffer or enqueues new states back into the ring.
- New branches from
condeenqueue new entries at the back. When acondecreates two alternative branches, each branch becomes a new entry in the ring, positioned behind whatever entries are already waiting. - The ring IS the stream, materialized in hardware. There is no lazy evaluation, no thunks, no function closures. The ring buffer is a physical circular array in memory, with read and write pointers that advance independently. The interleaving that miniKanren achieves through careful thunk swapping in software happens naturally in hardware through the circular structure of the ring: entries from different branches are interleaved in the buffer, and the FSM processes them in order.
This means the FPGA does not need to implement lazy evaluation — it simply cycles through a physical queue of active search states, which naturally provides the interleaving that miniKanren needs for completeness. The ring buffer has a fixed capacity (1024 entries in the current design), which bounds the maximum number of active search branches — but for practical queries, this is more than sufficient.
Soli Deo Gloria