Copatterns & Coinduction

Most data in Verum is inductive: built by constructors, consumed by pattern matching. Lists are Nil | Cons(head, tail); you build them bottom-up, you destructure top-down.

Coinductive data is the opposite: built by observations, consumed one step at a time, potentially infinite. A Stream<Int> is not a finite list of integers — it is a promise to answer, for every natural number n, "what is the nth element?".

Verum's syntax for this is the cofix function modifier with a copattern body.

The basic shape

Inductive definition, for contrast:

type List<T> is Nil | Cons(head: T, tail: Heap<List<T>>);

fn range(lo: Int, hi: Int) -> List<Int> {
    if lo >= hi { List.Nil }
    else        { List.Cons(lo, Heap.new(range(lo + 1, hi))) }
}

Coinductive — a Stream<T> defined by its observations .head and .tail:

type Stream<T> is protocol {
    fn head(&self) -> T;
    fn tail(&self) -> Stream<T>;
};

cofix fn nats_from(n: Int) -> Stream<Int> {
    .head => n,
    .tail => nats_from(n + 1),
}

Each arm answers one observation. The whole value is the observation function: ask .head, get n; ask .tail, get the continuation.

The resulting stream is lazy — no work happens until an observation fires. nats_from(0).tail().tail().head() evaluates to 2 without constructing an infinite list.

Grammar

fn_keyword      = 'fn' , [ '*' ] ;
function_modifiers = [ 'pure' ] , [ meta_modifier ] , [ 'async' ]
                   , [ 'cofix' ] , [ 'unsafe' ] | epsilon ;

copattern_body  = '{' , copattern_arm , { ',' , copattern_arm } , [ ',' ] , '}' ;
copattern_arm   = '.' , identifier , '=>' , expression ;

The body is only valid on functions marked cofix. Each arm pairs an observation — a .name referring to a protocol method — with the expression to return when that observation fires.

Productivity

For a cofix fn to be well-defined, every observation must make progress — it must produce something before recursing. The productivity check is structural:

cofix fn ones() -> Stream<Int> {
    .head => 1,                 // progress: delivers 1
    .tail => ones(),            // tail-call into self, but .head was served
}

A definition that recurses in .head without a guarding constructor is meant to be rejected:

cofix fn bad() -> Stream<Int> {
    .head => bad().head(),       // no progress
    .tail => bad(),
}

This is the dual of induction's termination check: induction demands the input shrink; coinduction demands the output grow.

The productivity check cannot be what rejects it today

the productive definition and the unproductive one produce the same diagnostic, so the rejection is not the productivity check speaking.

cofix fn nats_from(n: Int) -> Stream<Int> { .head => n, .tail => ... }
  -> error: Type inference for expression kind 'copattern body'
            requires additional context.

cofix fn bad() -> Stream<Int> { .head => bad().head(), .tail => bad() }
  -> the identical error

A copattern body does not typecheck at all — the control fails exactly as the subject does — so a negative test on this page's bad() would pass for the wrong reason. check_cofix_productivity exists in the pipeline and is called; it is not reached, because inference stops first. The conformance spec 070_copattern_basic.vr carries @expect: pass and reports nine errors.

Coinductive protocols

The protocol a cofix function answers against is ordinary:

type Stream<T> is protocol {
    fn head(&self) -> T;
    fn tail(&self) -> Stream<T>;
};

type Conway is protocol {
    fn value(&self) -> Int;
    fn left(&self)  -> Conway;
    fn right(&self) -> Conway;
};

Any protocol whose methods return the same protocol (or another coinductive type) is admissible as a cofix target.

Worked example: Hamming numbers

The Hamming sequence (numbers of the form 2^i · 3^j · 5^k) is a textbook coinductive definition.

This example does not compile today

It is written the way the feature is meant to read, not the way it currently behaves. Two things are missing, both checked:

• copattern bodies still fail inference, the same diagnostic as the warning above — so hamming() does not typecheck;
• merge3 and map_stream are declared nowhere in core/, and .take(10) is not available here: the Stream<T> protocol on this page declares .head and .tail and nothing else. ``` grep -rlE '\b(merge3|map_stream)\b' core/ --include='*.vr' | wc -l # 0 grep -n 'fn take' core/async/stream.vr # :211, :216

  
  The word boundaries earn their place: without them the first command
  answers **1**, on `fn test_map_stream()` in `core/async/stream.vr` —
  a test whose name merely contains the string.
  
  The second command is the reason the call reads as though it should
  work: `core.async.stream` does have a `take`, on a different,
  asynchronous `Stream`.

Read it as the shape of the definition. The .head/.tail walk in the section above is the part you can write today.

// does not compile — see the caution above. `merge3`, `map_stream` and
// `.take` are not declared for this `Stream`, and copattern bodies do
// not yet infer. This is the shape of the definition, not a snippet to
// paste.
cofix fn hamming() -> Stream<Int> {
    .head => 1,
    .tail => merge3(
        map_stream(|n| n * 2, hamming()),
        map_stream(|n| n * 3, hamming()),
        map_stream(|n| n * 5, hamming()),
    ),
}

fn main() {
    let first_ten: List<Int> = hamming().take(10).collect();
    // [1, 2, 3, 4, 5, 6, 8, 9, 10, 12]
    print(first_ten);
}

Combinators: take, zip, map_stream

A coinductive library looks familiar:

cofix fn map_stream<A, B>(f: fn(A) -> B, s: Stream<A>) -> Stream<B> {
    .head => f(s.head()),
    .tail => map_stream(f, s.tail()),
}

cofix fn zip<A, B>(a: Stream<A>, b: Stream<B>) -> Stream<(A, B)> {
    .head => (a.head(), b.head()),
    .tail => zip(a.tail(), b.tail()),
}

fn take<T>(s: Stream<T>, n: Int) -> List<T> {
    if n == 0 { List.new() }
    else      { List.prepend(s.head(), take(s.tail(), n - 1)) }
}

take is ordinary (inductive): it peels a finite prefix off the stream. You consume a coinductive value with inductive recursion and produce it with coinductive recursion — the two never mix on the same side of the definition.

Bisimulation proofs

To prove two streams equal you need bisimulation: agreement on .head, and a bisimulation on the two .tails. The verifier implements it — verum_smt::coinductive::CoinductiveChecker discharges stream equality through Z3 — but it is reachable only from Rust today. There is no surface tactic: bisimulation appears nowhere in grammar/verum.ebnf, and the block below is rejected with expected proof step (have, show, suffices, let, obtain, …).

The shape the surface syntax is meant to take:

// not yet supported: `bisimulation` is not a surface tactic — see above
theorem nat_plus_zero(n: Int)
    ensures nats_from(n) == map_stream(|x| x + 0, nats_from(n))
{
    proof by bisimulation {
        head_step => by omega,
        tail_step => by induction,
    }
}

See verification/cubical-hott for path equalities between coinductive values and the cubical tactic.

cofix and async

cofix composes with async. An async-coinductive function produces a Stream whose observations perform I/O:

async cofix fn readings() -> AsyncStream<Reading>
    using [SensorBus]
{
    .head => bus.read().await,
    .tail => readings(),
}

Each observation performs a bus read; the stream is infinite until the underlying bus fails.

Relationship with generators (fn*)

Generators (fn*) are the imperative counterpart. A generator uses yield to produce values step by step, but its shape is a function whose control returns to the caller at each yield point. A cofix definition is data: an object answering observations on demand.

Feature	fn* generator	cofix stream
Shape	imperative with yield	observational
Required protocol	Iterator	user-defined
Natural result	Iterator<T>	coinductive type
Bisimulation proofs	indirect	direct via cofix
Composes with async	yes	yes

Use generators for control-flow-heavy producers; use cofix for data-flow-heavy infinite values.

See also

• Patterns — for inductive destructuring.
• Functions → generators.
• Proof DSL — bisimulation tactic.
• verification/cubical-hott.