f_algebra.cppm File Reference

Initial F-algebras and terminal F-coalgebras. More...

#include <concepts>
#include <cstddef>
#include <functional>
#include <tuple>
#include <type_traits>
#include <utility>
import dedekind.category:morphism;

Include dependency graph for f_algebra.cppm:

Classes
struct	dedekind::category::detail_f_algebra::component_orders< Op >
	The component orders of a product order, where Op is one. More...
struct	dedekind::category::detail_f_algebra::component_orders< ProductLeq< LA, LB > >
struct	dedekind::category::BetaReduction
	The β-reduction algebra: a leaf is its own normal form; a node is reduce_β over its reduced legs. reduce_β is a dependent call resolved by ADL against the node type, so a law lives next to its node: the composition unit law above is the canonical exhibit, and further node laws add their own overloads beside their vocabulary. No node carries an is-this-kind tag; dispatch is on the node type. More...
struct	dedekind::category::LawAlgebra< Op >
	The law algebra: a leaf is its declared profile, a node the law engine on its legs' profiles (:posetal, arrow_node); any other node certifies nothing (sound). The second algebra for the same cata: BetaReduction lands in a normal form (a free algebra, so it decides equality), LawAlgebra in a finite domain of profiles (an abstract interpretation, so it certifies, sound, not complete). More...

Namespaces
namespace	dedekind::category

Concepts
concept	dedekind::category::IsInitialFAlgebra
	Carrier A is the initial F-algebra for endofunctor F with structure map α.
concept	dedekind::category::IsTerminalFCoalgebra
	Carrier A is the terminal F-coalgebra for endofunctor F with structure map α.
concept	dedekind::category::IsTermNode
	A node of the term functor: a type that exposes its legs.
concept	dedekind::category::Steers
	An algebra that steers the fold at T (Mendler style): it recurses into the legs it chooses by cata itself, instead of the strict fold.
concept	dedekind::category::detail_f_algebra::HasComponentOrders
	Op is a product order with component orders to descend into.

Functions
template<IsArrow F, IsArrow G>
constexpr auto	dedekind::category::legs (const Compose< F, G > &c)
	The legs of a composite: the arrows it composes.
template<typename β, typename T> requires Steers<β, T> || IsTermNode<T> || std::invocable<const β&, const T&>
constexpr auto	dedekind::category::cata (const β &alg, const T &t)
	cata ⦇β⦈ — the catamorphism (fold): the unique F-algebra homomorphism from the initial algebra (the term itself, μF) into an algebra (B, β).
template<typename β, typename T, std::size_t... I> requires IsTermNode<T> && std::invocable< const β&, const T&, decltype(cata(std::declval<const β&>(), std::get<I>(legs(std::declval<const T&>()))))...>
constexpr auto	dedekind::category::detail_f_algebra::fold_legs (const β &alg, const T &t, std::index_sequence< I... >)
template<IsArrow T>
constexpr auto	dedekind::category::cata (const T &t)
	cata(t): the term rewritten to its normal form under the β-reduction algebra. simplify is cata. The IsArrow gate keeps a bare product out of the term universe.
reduce_β for a Compose node — the canonical β exhibit
reduce_β is the β (F-algebra structure map, i.e. the one-step β-reduction) that cata applies after folding a node's legs. This overload set is the canonical exhibit: the reducer's first law, the monoid law of composition, co-located with the cata engine. The identity is the unit (id∘f = f = f∘id), so an Identity in a reduced leg is dropped. Dispatch is structural on Identity<T> in the reduced leg (no is-identity tag): the overloads pattern-match the leg types, and partial ordering picks the Identity ones over the generic IsArrow one. The first parameter is the Compose node as a type-tag for β dispatch (which constructor is this?); its own legs are unused — cata passes the already-reduced legs rf / rg, which is what β combines. Found by ADL, so a partition MAY instead scatter its node's reduce_β next to that node's vocabulary; the composition law lives here as the reference instance.
template<IsArrow F, IsArrow G, IsArrow RF, IsArrow RG>
constexpr auto	dedekind::category::reduce_β (const Compose< F, G > &, const RF &rf, const RG &rg)
template<IsArrow F, IsArrow G, typename T, IsArrow RG>
constexpr RG	dedekind::category::reduce_β (const Compose< F, G > &, const Identity< T > &, const RG &rg)
template<IsArrow F, IsArrow G, IsArrow RF, typename T>
constexpr RF	dedekind::category::reduce_β (const Compose< F, G > &, const RF &rf, const Identity< T > &)
template<IsArrow F, IsArrow G, typename T, typename U>
constexpr Identity< T >	dedekind::category::reduce_β (const Compose< F, G > &, const Identity< T > &i, const Identity< U > &)
template<typename F, typename G, typename RF, typename RG>
constexpr auto	dedekind::category::reduce_β (const Pairing< F, G > &, const RF &rf, const RG &rg)
	A pairing (copairing) rebuilt from its reduced legs: inert.
template<typename F, typename G, typename RF, typename RG>
constexpr auto	dedekind::category::reduce_β (const Copairing< F, G > &, const RF &rf, const RG &rg)

Variables
template<typename F, typename A, typename α>
constexpr bool	dedekind::category::is_initial_f_algebra_v = false
	Opt-in trait: does carrier A witness the initial F-algebra universal property for endofunctor F with structure map α?
template<typename F, typename A, typename α>
constexpr bool	dedekind::category::is_terminal_f_coalgebra_v = false
	Opt-in trait: does carrier A witness the terminal F-coalgebra universal property for endofunctor F with structure map α?

Detailed Description

Initial F-algebras and terminal F-coalgebras.

@partition :f_algebra

Copyright

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

f_algebra__FAlg_Universal_Property

Pierce §5 introduces F-algebras and F-coalgebras immediately after functors and before natural transformations because they are the load-bearing concept that grounds recursive types and the universal property of recursion. This project's :functor partition already carries the structural-shape concepts:

IsFAlgebra<Carrier, Structure, Functor> — structure map F → A.

IsFCoalgebra<Carrier, Structure, Functor> — structure map A → F .

What was missing — and what this partition adds — is the universal-property layer:

Initial F-algebra: an F-algebra (A, α) is initial if for every other F-algebra (B, β) there exists a unique morphism h : A → B with h ∘ α = β ∘ F(h). That unique morphism is the catamorphism (fold).

Terminal F-coalgebra: dually; the unique morphism is the anamorphism (unfold).

Data first, codata kept open

The Jlt posture is data only: initial algebras in Set, codata out of scope as values (the Jlt paper's Rule 3). The restriction lives in the posture (the rules, jlt-lint, the listings), not here: this partition keeps both halves of the dual, IsInitialFAlgebra and IsTerminalFCoalgebra, so that codata (Trsk, later) is registered beside the data side and needs no rewrite of it. Jlt's recursion pair stays on the initial algebra: cata out of \(\mu F\), and unfold of Lambek's inverse \(\mathit{prior} = \mathit{in}^{-1}\) on \(\mu F\) itself (:chain), which always ends; an anamorphism into \(\nu F\) is a different arrow and keeps a different name.

See also

#449 (the NNO and the list functor registered, after #1115 and #1007), #1133 (Figure 2's hylomorphism as the finite sequence).

f_algebra__Bridge_to_NNO

The :nno partition reifies Lawvere's NNO universal property as the (z, s) shape — pedagogically the more recognisable form for a working mathematician. The textbook reading of NNO is that it is the initial F-algebra for F(X) = 1 + X (the "Maybe" endofunctor; Pierce §5.4, Mac Lane III–VI). This partition exposes that reading as a separate concept; the two universal properties are operationally equivalent — the (z, s) pair induces the structure map [z, s] : 1 + N → N via coproduct copairing on the standard injections inl : 1 → 1 + N and inr : N → 1 + N.

The 1 in 1 + N is the terminal object of the ambient category — concretely, the category::One = std::monostate reified in the :limit partition (which carries IsTerminalObject<One> as a static_assert). The categorical pattern IsInitialFAlgebra is itself one level up from the IsInitialObject reification in :limit (which pins category::Zero = std::nullptr_t as the initial in Set): the F-Alg category has its own initial object (μF, in), and IsInitialFAlgebra is the engineer's honesty obligation that a particular (A, α) is that initial object. See f_algebra_test.cpp for the static_assert witnesses linking the two layers.

f_algebra__Honesty_Obligation

As with :nno, C++ concepts cannot quantify over the universal property's uniqueness clause. The structural shape ( IsFAlgebra / IsFCoalgebra in :functor) is what the type system can pin; the universal-property concepts here are opt-in traits that carriers must explicitly register via is_initial_f_algebra_v / is_terminal_f_coalgebra_v. The trait is the engineer's honesty obligation: declaring it asserts that the carrier truly satisfies the universal property, and the paper's ethical register applies (Wadler 2015, NSPE Code of Ethics). An identical opt-in pattern is used by algebra:initial_ring (PR #451) for ℤ as the initial ring.

f_algebra__Categorical_Duality

The dual pair carries the recursion ↔ corecursion split structurally — no catamorphism without an anamorphism. Both halves land in this partition as concepts; the operational discharge of the fold is cata below ( ana / hylo are still to come).

| side               | UP                  | unique morphism |
|--------------------|---------------------|-----------------|
| initial (μF, in)   | initial in F-Alg    | cata (fold)     |
| terminal (νF, out) | terminal in F-Coalg | ana  (unfold)   |

Note

"An algebra over an endofunctor F is just a structure map @c F(A) @c → @c A; what makes some particular algebra @b interesting is that other algebras factor through it uniquely." — paraphrase of Pierce 1991, §5.

See also

Pierce, B.C. (1991) "Basic Category Theory for Computer Scientists" §5.

Mac Lane, S. (1971) "Categories for the Working Mathematician" III–VI.

Meijer, E., Fokkinga, M., Paterson, R. (1991) "Functional Programming with Bananas, Lenses, Envelopes and Barbed Wire" (FPCA).

dedekind.algebra:universal (IsAlgebra<T, Ops...>) for the universal-algebra (A, F) reading of the same notion. Per the textbook isomorphism Alg(Σ) ≅ F_Σ-Alg (Pierce §2.2), every IsAlgebra<T, Ops...> there corresponds to an F-algebra here for the polynomial endofunctor F_Σ generated by the signature Σ = (Ops...). The two partitions name the same structural fragment from the universal-algebra and category-theoretic traditions respectively.