dedekind::sequences::IsSequence Concept Reference

The fundamental mapping from a Domain Set to a Value Type. More...

Concept definition

template<typename Seq>
concept dedekind::sequences::IsSequence =  IsNet<Seq> && IsCountablyIndexedFamily<Seq> && requires {
  
  typename Seq::Codomain;
  typename Seq::Domain;
} && requires(const Seq s) {
  requires IsSpecies<typename Seq::Domain>;
  
  
  
  
  
  
  
  
  requires dedekind::sets::IsRingIntegral<typename Seq::Domain>;
}

Detailed Description

The fundamental mapping from a Domain Set to a Value Type.

net__IsSequence_vs_stdlib_388

IsSequence anchors bidirectionally to the C++ standard library via two complementary surfaces.

(available today)

FinitePath<T> already exposes begin() / end() returning iterators that satisfy the std::input_iterator concept (cf.\ sequences:path), so FinitePath<T> is a std::ranges::input_range out of the box. The reverse direction is provided by the from_range factory in sequences:path, which lifts any std::ranges::input_range into a FinitePath<T>. In symbols:

FinitePath<T> => std::ranges::input_range

std::ranges::input_range<R> => FinitePath<value_t> = from_range(r)

This is the anchor that makes FinitePath<T> values flow into std::ranges algorithms such as transform and for_each, as well as range adaptors such as std::views::filter, and into iterator-based reductions such as std::accumulate — without a bespoke adapter. Other IsFiniteSequence carriers acquire the same range surface by additionally exposing begin() / end() (the concept does not require it; FinitePath provides it).

(C++23, future once libc++ ships

<generator>)

The C++23 std::generator<T> coroutine (P2502R2, <generator>) is the natural pull-model dual: a coroutine that yields T values in order. Semantically it is a sequence with domain \(\mathbb{N}\) (or a finite prefix) and codomain T, isomorphic to IsFiniteSequence / IsSequence over std::size_t. An adapter once libc++ ships <generator>:

template <typename Seq> requires IsFiniteSequence<Seq>
std::generator<typename Seq::Codomain> as_std_generator(Seq s) {
  for (std::size_t i = 0; i < s.size(); ++i) co_yield s.at(i);
}

Documented rather than implemented to avoid a toolchain-version dependency in the main source. Until libc++ ships it, the iterator/range anchor above covers the same use cases.

On_Pull_vs_Push

IsSequence is a pull model (consumer asks for index i, receives s.at(i)) and admits a directed-set domain via the IsNet refinement (cf. Munkres / Kelley nets). Standard iterators and std::generator are both pull-style too, but with domain implicitly \(\mathbb{N}\). The library's IsNet generalises the standard view to non-totally-ordered index sets; the iterator/range and coroutine anchors specialise to the \(\mathbb{N}\)-indexed case.

A natural worked example: the primitive-element enumeration \(\mathbb{F}_q^{\times} = \{\alpha^0, \alpha^1, \ldots, \alpha^{q-2}\}\) presents cleanly as both std::ranges::input_range (today, via FinitePath) and std::generator<F> (future, via the adapter sketched above).

net__IsSequence_categorical_anchors

Beyond the standard-library and topology-textbook anchors above, IsSequence sits at a categorical sweet-spot that several upstream concepts already reify in this codebase. Naming them here so the conceptual basis is explicit:

• F-coalgebra structure. An enumeration is, categorically, a coalgebra \(\alpha : X \to 1 + T \times X\) for the list/stream functor \(F(X) = 1 + T \times X\) — the unfold step that enables enumeration. The concept IsFCoalgebra is shipped in dedekind.category:functor (see category/functor.cppm). IsSequence does NOT enforce this coalgebraic shape structurally (the concept body asks for IsNet refinement, a countably-indexed family, and Codomain/Domain typedefs — not for a coalgebra morphism); it names the categorical reading the concept captures. Inhabitants like Path<T> in sequences/path.cppm are coalgebras for this functor by construction; arbitrary user-supplied IsSequence inhabitants carry the categorical interpretation as the engineer's reading, not as a type-system-enforced witness.
• Stream-comonad structure on the result. Terminal F-coalgebras of the list functor are automatically comonads (Pierce TAPL §5; Lambek's lemma corollary). In this codebase Path<T> reifies the terminal F-coalgebra and additionally satisfies IsStreamComonad (see sequences/path.cppm), giving head / tail / duplicate on the resulting sequence. This is structure on the output of an enumeration, not what enables it.
• NNO universal property. The \(\mathbb{N}\)-indexed case of IsSequence — i.e. when Domain is the carrier of the Natural Numbers Object (Lawvere–ETCS Axiom 9; IsNNO in dedekind.category , see category/nno.cppm ) — is what licenses primitive recursion: given a seed \(a_0\) and a step \(\sigma\), the universal property delivers a unique map \(f : \mathbb{N} \to T\) with \(f(0) = a_0\) and \(f(n+1) = \sigma(f(n))\). This is why NNO-indexed sequences (rather than arbitrary directed-set-indexed nets) suffice for bounded enumeration / take operations.
• Terminal-F-coalgebra reading. The universal-property anchor for Path<T> is named in the :f_algebra partition's title ("Initial F-algebras @b and @b terminal @b F-coalgebras", see category/f_algebra.cppm) and exposed there via the is_terminal_f_coalgebra_v opt-in trait (sibling to is_initial_f_algebra_v ). The opt-in defaults to false; the engineer registering a witness carries the universal-property obligation per the :f_algebra discipline.

In short: IsSequence is the natural gate for enumeration (take / limit -style operations) because the categorical structure the concept names — an NNO-indexed morphism, naturally read as a coalgebra for the stream functor — is what makes "first @c n elements" well-defined. The structural type-system check is the refinement of IsNet plus the typedef obligations named in the concept body; the F-coalgebra / stream-comonad / NNO apparatus above is the categorical reading the concept captures, enforced by canonical inhabitants like Path<T> rather than by the concept itself. The carrier-side companion IsCountableSet (defined immediately below) is the friendly user-facing predicate that asks "does my carrier produce a canonical @c IsSequence ?" The duality with the F-algebra side of argmax (sec:lp-centrepiece in paper.tex ) is the categorical reading: fold for argmax , unfold for take .