template<std::regular S, std::semiregular Coalg>
requires std::regular_invocable<const Coalg&, const S&> && requires(std::invoke_result_t<const Coalg&, const S&> y) { { y.has_value() } -> std::same_as<bool>; { y->first }; { y->second } -> std::convertible_to<S>; }
class dedekind::category::unfold_view< S, Coalg >
The anamorphism, and Dedekind's chain
The unfold of a seed by a coalgebra \(S \to 1 + A \times S\): nothing ends the walk, a pair yields an element and the next state. This is the list anamorphism, the lens \([\![(g, p)]\!]\) of Meijer, Fokkinga and Paterson [8], with p the coalgebra yielding nothing: the element where it does is the delimiter and is not emitted. Read against the Jlt paper's Figure 2 (#981): the chain of counts on top, generated by the step and delimited by its fixed point.
| Bananas | here | | the initial algebra of 1 + X | IsNNO, In | | out, by Lambek | Prior, lower_cover | | anamorphism, a lens | unfold; chain, Dedekind's | | catamorphism, a banana | std::ranges::fold_left, cata | | hylomorphism, an envelope | a fold over chain: nothing in between |
The lens here unfolds on the initial algebra: chain walks Lambek's inverse down from a seed and always ends, so Jlt's data-only posture holds by construction. Meijer et al.'s lens into the terminal coalgebra, codata, is a different arrow; it is kept out of the posture, not out of the library (IsTerminalFCoalgebra; #449). A fold over the chain is the Church-encoded finite sequence, the list as its fold (#1133).
A forward view, O(1) state: the element, its source state, the next state, and whether the walk is live. The coalgebra is a value (Rule 1: semiregular), and two positions of one walk compare by state, so the element need not be comparable.
- Template Parameters
-
| S | the state. |
| Coalg | the coalgebra, S to optional<pair<A, S>>. |
