chain.cppm File Reference

Dedekind's chain as a range: the unfold of a seed by a coalgebra, the chain of a step guarded by an end, the arrow mapped along it, the bounded chain [lo, hi], and the default chain of a carrier with the NNO's step (the Jlt paper's Figure 2 and Listing 3, #981). The NNO itself, its step and Lambek's destructor Prior, are :nno's; the folds over a chain are :total's concat and :action's fold. More...

#include <algorithm>
#include <concepts>
#include <cstddef>
#include <functional>
#include <iterator>
#include <optional>
#include <ranges>
#include <type_traits>
#include <utility>
import dedekind.category:nno;

Include dependency graph for chain.cppm:

Classes
struct	dedekind::category::is_integer_chain< T >
	Whether a carrier is an integer chain: the integral types, and the carriers that register themselves (sets' cardinals, a bignum). More...
class	dedekind::category::unfold_view< S, Coalg >
class	dedekind::category::unfold_view< S, Coalg >::iterator
	A position of the walk: the element, the next state, live. More...
struct	dedekind::category::StepCoalgebra< X, Step >
	The coalgebra of a partial step \(X \to 1 + X\): the element, and the step as the next state, while the step has a value. Turns Prior, lower_cover or cover into a lens. More...
struct	dedekind::category::Until< End, Step >
	The chain in arrows (the Jlt paper, Listing 3). Three arrows make it: an end, a predicate on the states; a step, an endo; a seed, a point. until(end, step) is the guard, after the Haskell Prelude's until, the partial step \(N \to 1 + N\) a cartesian category builds as \(\langle end, 1\rangle ; dist ; (! + step)\). chain(out) is the anamorphism as an arrow \(N \to N^*\), so a seed composed into it, x >> chain(out), is its chain. ns >> f is the functor's action, f mapped over the elements, the coalgebra's emitted leg post-composed, \((1 + f \times 1) \circ out\), and map id is the chain itself, decided at the type. A fold over the composite is a hylomorphism: nothing between the seed and the fold is built. More...
struct	dedekind::category::Unfold< S, Coalg >
	The anamorphism of a coalgebra as an arrow from the seeds: x >> unfold<S>(c) is unfold(x, c). More...
struct	dedekind::category::Mapped< S, Coalg, F >
	The functor's action on a coalgebra: f on the emitted leg. More...
struct	dedekind::category::detail_chain_arrows::IsZero
struct	dedekind::category::Below< C >
	The coalgebra of the bounded chain [lo, hi]: over the state \(1 + C\), since past hi is no element, and the cover of a saturating top is nothing. More...
class	dedekind::category::chain_view< C >
struct	dedekind::category::detail_chain::SliceStep< C, F >
	The step of a chain restricted by value to [lo, hi): f of the element and its cover, while the element is below hi. More...
struct	dedekind::category::Slice< C >
	The chain of C restricted by value to [lo, hi): the elements from lo up to hi, hi excluded, as pandas' .loc reads a slice. For any carrier with the covering step, std::byte among them. More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsIntegerChain
	A chain with integer arithmetic: a discrete total order, locally finite (every bounded interval is finite), so a distributive lattice under min and max, with the NNO's step and the arithmetic operators as a shape. Finite on a machine word, unbounded for a bignum. Not a ring: int's overflow is undefined and a cardinal may saturate at \(\aleph_0\); the ring is IsRing's to claim.
concept	dedekind::category::IsCountWord
	A word of the counts: an integer chain whose arithmetic wraps at its cyclic order, the unsigned integers but bool, and none narrower than int, whose products promote to a signed int that may overflow. std::size_t is the default throughout.
concept	dedekind::category::IsFiniteChainSequence
	A sequence on finite chains: an arrow out of the counts, read along a chain of them (the Jlt paper's Figure 2, its vertical arrows). The chain is finite by its descent and ordered by its step, so the sequence needs no set concept; its laws, a period or an order kept or reversed, are laws of the composite chain >> f, and the folds read them (#1133).

Typedefs
template<std::regular X, std::semiregular Step>
using	dedekind::category::chain_t = unfold_view<X, StepCoalgebra<X, Step>>
	The chain of x under a partial step: what the step reaches from x, the step of it, then the step of that, until the step has nothing (Dedekind's chain of the step of x, [4]). With Prior it is \(n - 1, \ldots, 0\), the n elements below n, n itself excluded: the Jlt paper's Figure 2, after Lambek.
template<IsCountWord N, IsFiniteChainSequence F>
using	dedekind::category::FiniteChainSequence
	The finite sequence as a value, n >> chain<N>() >> f: the chain of n read by f, never built. A fold over it is the list as its fold, the Church encoding (#1133).

Functions
template<std::regular S, std::semiregular Coalg>
constexpr unfold_view< S, Coalg >	dedekind::category::unfold (S seed, Coalg step)
	The unfold of seed by step.
template<std::regular X, std::semiregular Step>
constexpr chain_t< X, Step >	dedekind::category::chain (X x, Step step)
template<IsArrow End, IsArrow Step>
constexpr Until< End, Step >	dedekind::category::until (End end, Step step)
	The guard.
template<std::regular S, std::semiregular Coalg>
constexpr Unfold< S, Coalg >	dedekind::category::unfold (Coalg c)
	The anamorphism, as an arrow.
template<IsArrow Step> requires std::regular<Dom<Step>> && std::semiregular<Step>
constexpr Unfold< Dom< Step >, StepCoalgebra< Dom< Step >, Step > >	dedekind::category::chain (Step step)
	The chain of a partial step, as an arrow from the seeds: x >> chain(out) is chain(x, out).
template<std::regular S, std::semiregular Coalg, IsArrow F> requires std::same_as<Dom<F>, typename unfold_view<S, Coalg>::element_type>
constexpr unfold_view< S, Mapped< S, Coalg, F > >	dedekind::category::operator>> (const unfold_view< S, Coalg > &v, F f)
	ns >> f: f mapped over the walk, as a walk.
template<std::regular S, std::semiregular Coalg, IsArrow F> requires std::same_as<Dom<F>, typename unfold_view<S, Coalg>::element_type> && IsIdentityArrow<F>
constexpr unfold_view< S, Coalg >	dedekind::category::operator>> (const unfold_view< S, Coalg > &v, F)
	The functor's unit law, decided at the type: map id is the walk itself.
template<HasNNOStep C> requires std::totally_ordered<C>
constexpr Slice< C >	dedekind::category::slice (C lo, C hi)
template<HasNNOStep C, IsArrow F> requires std::totally_ordered<C> && std::same_as<Dom<F>, C>
constexpr unfold_view< std::optional< C >, detail_chain::SliceStep< C, F > >	dedekind::category::operator>> (const Slice< C > &s, F f)
	An arrow along a restricted chain: f(lo), ..., f(hi - 1), a range never built.
template<HasNNOStep N> requires std::regular<N>
constexpr auto	dedekind::category::chain ()
	The default chain of a carrier with the NNO's step, the one its certificate supplies: n >> chain<N>() is what Prior<N> reaches from n, n - 1, ..., 0 (the Jlt paper's Listing 3).

Variables
constexpr auto	dedekind::category::detail_chain_arrows::ns = 3u >> chain(until(IsZero{}, Predecessor<unsigned>{}))

Detailed Description

Dedekind's chain as a range: the unfold of a seed by a coalgebra, the chain of a step guarded by an end, the arrow mapped along it, the bounded chain [lo, hi], and the default chain of a carrier with the NNO's step (the Jlt paper's Figure 2 and Listing 3, #981). The NNO itself, its step and Lambek's destructor Prior, are :nno's; the folds over a chain are :total's concat and :action's fold.

@partition :chain

Copyright

2026 The Dedekind Authors Licensed under the Apache License, Version 2.0.