Sequence

The one lazy iteration protocol: pull-based sequences with natural names.

A Sequence is a pull producer: a thunk that, when forced with (()), yields one Step – either SDone (exhausted) or SMore(x, rest), the next element x paired with the thunk producing the remainder. Nothing is materialized up front; each (()) advances the stream by one element. A transformer (map, filter, take, …) wraps a producer in a new producer that pulls, reshapes, and re-yields; a consumer (fold, sum, to_list, …) drives the producer to exhaustion and folds the elements into a value.

Type

type Step(a) = SDone | SMore(a, (Unit) -> Step(a))
Seq(a)       = (Unit) -> Step(a)          -- read `Seq(a)` in the prose as this

The step continuation is ordinary data, not an effect, so every combinator is a total pure function over Step. That is the whole reason this substrate exists: an earlier push design routed elements through a shared Emit effect, and a single Emit(a) label per scope made element-type changes, heterogeneous zip, and mixing two element types in one function unrepresentable. On pull Step the element type is a plain type parameter, so map : Seq(a) -> Seq(b) type-changes freely, zip : (Seq(a), Seq(b)) -> Seq((a, b)) is genuinely heterogeneous, and a consumer’s per-element function may perform any ambient effect (it runs directly, with no handler closing the row over it). Every combinator below exercises one of those, and the correctness corpus in tests/cases/run pins them on both backends.

Effect-polymorphic consumers

for_each’s function argument runs in the ambient row: for_each(s, \(x) -> println(x)) threads IO straight out with no annotation, because the driver is a plain recursion and installs no handler. This is the effectful-mapper case the push substrate could not express.

Naming and the import idiom

The combinators keep their natural names (map, filter, take, zip, …), which collide with the prelude’s eager List surface. That is why this module is opt-in and NOT opened by the prelude: the flat namespace has no shadowing, so the documented idiom is a qualified import at the use site:

import Sequence as Seq          -- qualified: Seq.map, Seq.filter, Seq.take
Seq.to_list(Seq.filter(Seq.map(Seq.range(1, 100), \(x) -> x * x), even))

A selective import Sequence (unfold, iterate) also works for names that do not clash with the prelude.

Fusion status (baseline: unfused)

A pull pipeline is correct and constant-space per stage, but on the current optimizer it is NOT yet fused: each transformer stage allocates one SMore cons and one step thunk per element, so a k-stage pipeline over n elements allocates ~2kn heap cells (PRISM_ALLOC_STATS counts them; the algebraic-effect EOp counter reads zero here because a pull sequence performs no effects). The tests/perf_gate.rs pull-allocation cases pin those current numbers as the baseline; a dedicated stream-fusion pass (Coutts-style stream/unstream with case-of-case) is the separate work that ratchets them toward O(1). For contrast, the eager Data.List surface already fuses to ~1 cell per element with FBIP reuse recycling the uniquely-owned spine, so it is the faster tier today when strict, non-incremental traversal is acceptable; pull Sequence earns its keep on laziness (early exit through take/find, infinite producers) rather than on allocation, until fusion lands.

Types

Step

type Step(a) = SDone | SMore(a, (Unit) -> Step(a))

Functions and Values

empty

empty : forall a. () -> (Unit) -> Sequence.Step(a)

The empty sequence: yields nothing.

singleton

singleton : forall a. (a) -> (Unit) -> Sequence.Step(a)

The one-element sequence yielding x.

range

range : (Int, Int) -> (Unit) -> Sequence.Step(Int)

The ascending integers in [lo, hi). Self-recursive: the continuation is the next range, so no element is built until pulled.

from_list

from_list : forall a. (List(a)) -> (Unit) -> Sequence.Step(a)

The container boundary in: the elements of list xs, in order.

iterate

iterate : forall a. (a, (a) -> a) -> (Unit) -> Sequence.Step(a)

The infinite sequence x, f(x), f(f(x)), .... Bound it with take.

repeat

repeat : forall a. (a) -> (Unit) -> Sequence.Step(a)

The infinite sequence of x repeated. Bound it with take.

unfold

unfold : forall a b. (a, (a) -> Option((b, a))) -> (Unit) -> Sequence.Step(b)

The generator producer: yield x for each Some((x, seed')) that step returns from the running seed, stopping at None. Every finite producer is a special case; on pull Step a generator is just a fold over the seed, needing no coroutine or handler.

map

map : forall a b. ((Unit) -> Sequence.Step(a), (a) -> b) -> (Unit) -> Sequence.Step(b)

Apply f to every element. Type-changing: Seq(a) -> Seq(b).

filter

filter : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> (Unit) -> Sequence.Step(a)

Keep only the elements satisfying p.

filter_map

filter_map : forall a b. ((Unit) -> Sequence.Step(a), (a) -> Option(b)) -> (Unit) -> Sequence.Step(b)

Map and filter in one pass: yield y for each f(x) == Some(y), dropping the Nones.

append

append : forall a. ((Unit) -> Sequence.Step(a), (Unit) -> Sequence.Step(a)) -> (Unit) -> Sequence.Step(a)

Concatenate two sequences: all of s, then all of t.

flat_map

flat_map : forall a b. ((Unit) -> Sequence.Step(a), (a) -> (Unit) -> Sequence.Step(b)) -> (Unit) -> Sequence.Step(b)

For each element x, splice in the sequence f(x).

take

take : forall a. ((Unit) -> Sequence.Step(a), Int) -> (Unit) -> Sequence.Step(a)

The first n elements, stopping the producer once the budget is spent.

drop

drop : forall a. ((Unit) -> Sequence.Step(a), Int) -> (Unit) -> Sequence.Step(a)

Skip the first n elements, yielding the rest.

take_while

take_while : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> (Unit) -> Sequence.Step(a)

The longest prefix whose elements satisfy p; stops at the first failure.

drop_while

drop_while : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> (Unit) -> Sequence.Step(a)

Drop the longest prefix satisfying p, yielding the rest.

dedup

dedup : forall e1 a. ((Unit) -> Sequence.Step(Int) ! {e1}) -> (a) -> Sequence.Step(Int) ! {e1}

Drop consecutive duplicates, keeping the first of each run (needs Eq(a)). Left unsigned so the Eq(a) constraint is inferred from ==.

enumerate

enumerate : forall a. ((Unit) -> Sequence.Step(a)) -> (Unit) -> Sequence.Step((Int, a))

Pair each element with its zero-based index, yielding (i, x).

scan

scan : forall a b. ((Unit) -> Sequence.Step(a), b, (b, a) -> b) -> (Unit) -> Sequence.Step(b)

The running left-fold, streamed: yield z, then each successive accumulator.

interleave

interleave : forall a. ((Unit) -> Sequence.Step(a), (Unit) -> Sequence.Step(a)) -> (Unit) -> Sequence.Step(a)

Alternate elements of s and t (s0, t0, s1, t1, ...); when one runs out, yield the whole remainder of the other. Streamed, no materialization.

zip

zip : forall a b. ((Unit) -> Sequence.Step(a), (Unit) -> Sequence.Step(b)) -> (Unit) -> Sequence.Step((a, b))

Pair two sequences element-wise, stopping at the shorter. Genuinely heterogeneous: Seq(a) and Seq(b) yield Seq((a, b)).

zip_with

zip_with : forall a b c. ((Unit) -> Sequence.Step(a), (Unit) -> Sequence.Step(b), (a, b) -> c) -> (Unit) -> Sequence.Step(c)

Combine two sequences element-wise with f, stopping when either runs out. Heterogeneous in both operand types.

chunk

chunk : forall a. ((Unit) -> Sequence.Step(a), Int) -> (Unit) -> Sequence.Step(List(a))

Group elements into consecutive lists of length n (the final chunk may be shorter). Pulls one group at a time, holding only the current group.

window

window : forall a. ((Unit) -> Sequence.Step(a), Int) -> (Unit) -> Sequence.Step(List(a))

Every contiguous length-n sliding window, in order. Fewer than n elements yields nothing. Holds one window (n elements) at a time.

fold

fold : forall a b. ((Unit) -> Sequence.Step(b), a, (a, b) -> a) -> a

Left-fold the sequence with f from initial accumulator z.

for_each

for_each : forall e0 a. ((Unit) -> Sequence.Step(a), (a) -> Unit ! {e0}) -> Unit ! {e0}

Run f for its effects on each element, in order. Effect-polymorphic: f runs in the ambient row (no handler intervenes), so for_each(s, \(x) -> println(x)) threads IO out. The explicit {| e} row matters: unsigned, the self-recursion would infer f as pure and reject an effectful body.

sum

sum : ((Unit) -> Sequence.Step(Int)) -> Int

Sum a sequence of integers.

product

product : ((Unit) -> Sequence.Step(Int)) -> Int

Product of a sequence of integers.

count

count : forall a. ((Unit) -> Sequence.Step(a)) -> Int

The number of elements.

to_list

to_list : forall a. ((Unit) -> Sequence.Step(a)) -> List(a)

Collect the sequence into a list, in order. The container boundary out.

head

head : forall e0 a. ((Unit) -> Sequence.Step(a) ! {e0}) -> Option(a) ! {e0}

The first element, or None if the sequence is empty.

find

find : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> Option(a)

The first element satisfying p, or None; stops the producer at the match.

any

any : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> Bool

True when some element satisfies p; short-circuits.

all

all : forall a. ((Unit) -> Sequence.Step(a), (a) -> Bool) -> Bool

True when every element satisfies p; short-circuits on the first failure.

from_bytes

from_bytes : (Wire.Bytes) -> (Unit) -> Sequence.Step(Int)

The bytes of bs as a sequence of ints in 0..255, in order.

to_bytes

to_bytes : ((Unit) -> Sequence.Step(Int)) -> Wire.Bytes

Collect a sequence of ints (each masked to a byte) into a Bytes. The Bytes container boundary out.