dedekind::sequences::IsStreamComonad Concept Reference

\emph{Operational} duck-typed check that W carries the Uustalu–Vene stream-comonad shape on an infinite sequence \(\mathbb{N} \to A\). The concept body checks the two primitive legs — ε (head w.at(0)) and δ (tails(w)) — only; the third leg extend (w <<= f) is the derived \(\mathrm{map}\,f \circ \delta\) and is certified separately by the IsCoKleisliTriple witness (pinned beside the IsStreamComonad<Path<int>> assertion below), not re-checked here. More...

Concept definition

template<typename W>
concept dedekind::sequences::IsStreamComonad = 
    IsSequence<W> && !dedekind::sets::IsFinite<typename W::cardinality_type> &&
    requires(const W& w, std::size_t n) {
      { w.at(0) } -> std::same_as<typename W::Codomain>;
      { tails(w).at(n) } -> std::same_as<W>;
    }

Detailed Description

\emph{Operational} duck-typed check that W carries the Uustalu–Vene stream-comonad shape on an infinite sequence \(\mathbb{N} \to A\). The concept body checks the two primitive legs — ε (head w.at(0)) and δ (tails(w)) — only; the third leg extend (w <<= f) is the derived \(\mathrm{map}\,f \circ \delta\) and is certified separately by the IsCoKleisliTriple witness (pinned beside the IsStreamComonad<Path<int>> assertion below), not re-checked here.

This is the extension presentation of the stream comonad (counit ε + coextension <<=), the dual of Manes' Kleisli-triple theorem. It is equivalent to — not weaker than — the comultiplication presentation \((W, \varepsilon, \delta)\) of dedekind::category::IsComonad: the two determine each other, with δ recovered as tails (s <<= std::identity{}). The pairing mirrors IsCyclic vs IsCyclicGroup.

Why the extension presentation rather than IsComonad directly: IsComonad refines IsEndofunctor (Σ_cat == Τ_cat), and no non-identity type-constructor in the library is an endofunctor — every reified functor maps Set<T> → Set<F<T>> (so maybe_functor and tuple_functor are IsShapedFunctor but not IsEndofunctor; the only IsComonad witness in the codebase is identity_functor). Path is no exception, so the co-Kleisli layer is the level on which the comonad is actually certified — see the path__Why_The_Kleisli_Layer_And_Not_IsComonad note on path_functor. The extend leg here is the derived \(\mathrm{map}\,f \circ \delta\), separately certified by the IsCoKleisliTriple witness pinned beside the IsStreamComonad<Path<int>> assertion below.

Finiteness is excluded on purpose: the comonad of infinite streams (with δ = tails) is a different beast from the non-empty-list comonad on finite carriers, so a FinitePath is honestly rejected.

The δ leg constrains tails(w) to be indexable with elements of type W (a stream of W tails), not merely well-formed — this pins the comultiplication shape \(W \Rightarrow W \circ W\) and rejects an unrelated ADL-found tails returning some other type.