kleisli.cppm File Reference

The Kleisli Partition (The Extension Systems). More...

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

Include dependency graph for kleisli.cppm:

Classes
struct	dedekind::category::unit_witness< maybe_functor< T >, T >
struct	dedekind::category::unit_witness< tuple_functor< T >, T >
struct	dedekind::category::counit_witness< tuple_functor< T >, T >
struct	dedekind::category::is_kleisli_triple< Functor >
	Trait: Functor's unit and bind satisfy the Kleisli-triple laws (Manes): \(\eta(x)^* f = f(x)\), \(m^* \eta = m\) and \((m^* f)^* g = m^* (x \mapsto f(x)^* g)\). A certificate, primary false, declared where a container's bind keeps them by construction. More...
struct	dedekind::category::is_cokleisli_triple< Functor >
	Trait: the co-Kleisli-triple laws, the duals, for Functor's counit and extend. More...
struct	dedekind::category::is_kleisli_triple< maybe_functor< T > >
struct	dedekind::category::is_kleisli_triple< tuple_functor< T > >
struct	dedekind::category::is_cokleisli_triple< tuple_functor< T > >
struct	dedekind::category::is_frobenius_monad< Functor >
	Trait: Functor's multiplication and comultiplication satisfy the Frobenius law (Street, "Frobenius monads and pseudomonoids", 2004): \(T\mu \circ \delta T = \delta \circ \mu = \mu T \circ T\delta\). A certificate, primary false. Being a monad and a comonad is not enough: on streams (the diagonal monad, the suffix comonad) \(\delta \circ \mu\) reads \(s_{i+j}(i+j)\) where \(T\mu \circ \delta T\) reads \(s_{i+j}(j)\). More...
struct	dedekind::category::is_frobenius_monad< tuple_functor< T > >
struct	dedekind::category::kleisli_probe_arrow< A, B >
	An arrow A → B the triple concepts probe bind and extend with: only its type is read, never its value. In this namespace, not a detail one, so argument-dependent lookup finds the >>= and <<= defined below. More...
struct	dedekind::category::functor_of< MA >
	The functor whose values a container is: Maybe a value of maybe_functor , the one-tuple of tuple_functor . Kleisli extension reads its action on arrows, \(\mu \circ T(f)\). More...
struct	dedekind::category::functor_of< Maybe< A > >
struct	dedekind::category::functor_of< std::tuple< A > >
struct	dedekind::category::detail_kleisli::StepAt< Step, A, X, TA >
	The step at one element, a Kleisli arrow \(A \to T(A)\). More...
struct	dedekind::category::detail_kleisli::Extending< Step >
	A fold step on \(T(A)\): the step at the element, by κ. More...
struct	dedekind::category::detail_kleisli::Halved
	A witness's step that may fail: half of an even count. More...
struct	dedekind::category::_kleisli_arrow_witness_380::toy_partial_realize

Namespaces
namespace	dedekind::category
namespace	dedekind::category::detail_kleisli

Concepts
concept	dedekind::category::IsKleisliTriple
	A Kleisli triple ⟨T, η, (−)*⟩ (Manes), the monad in its extension form: the unit and bind, their laws certified by is_kleisli_triple.
concept	dedekind::category::IsCoKleisliTriple
	A co-Kleisli triple ⟨W, ε, (−)†⟩, the comonad in its extension form: the counit and extend, their laws certified by is_cokleisli_triple.
concept	dedekind::category::IsFrobenius
	A Frobenius monad (Street): a Kleisli and a co-Kleisli triple on one functor whose μ and δ satisfy the Frobenius law, certified by is_frobenius_monad.
concept	dedekind::category::detail_kleisli::IsKleisliStep
	A step from A and an element into TA, the monad on A.
concept	dedekind::category::HasKleisliBindOperators
	A monadic carrier MA supports Kleisli bind, >>=, with a Kleisli arrow F; >> composes arrows and nothing else.
concept	dedekind::category::HasComonadicExtendOperators
	A comonadic carrier WA supports comonadic extend, <<=, with a co-Kleisli arrow F.
concept	dedekind::category::HasArrowDereferenceOperator
	Syntactic check: m.operator->() compiles for M.
concept	dedekind::category::IsKleisliDeref
	M exposes operator-> and the carrier site has declared it as Kleisli dereference / comonadic extract (Mac Lane CWM §VI; Wadler 1992).
concept	dedekind::category::IsKleisliArrow
	An arrow declared to live in the Kleisli category indexed by the monad tag M (constrained by IsDefaultMonadTag).

Typedefs
template<typename MA>
using	dedekind::category::functor_of_t = typename functor_of<std::remove_cvref_t<MA>>::type

Functions
template<typename MA, IsArrow F> requires requires { typename functor_of_t<MA>; } && std::same_as<Dom<F>, typename functor_of_t<MA>::Σ_cat::Species>
constexpr auto	dedekind::category::detail_kleisli::lifted (const MA &ma, F f)
	\(T(f)\) applied to ma: the arrow f, from the value's element, under T's action, at the value.
template<typename MA, typename F> requires requires(MA const& ma, F&& f) { μ(detail_kleisli::lifted(ma, std::forward<F>(f))); }
constexpr auto	dedekind::category::κ (MA const &ma, F f)
	κ (kappa): Kleisli bind (monadic extension).
template<typename WA, typename F> requires requires(WA const& wa, F&& f) { detail_kleisli::lifted(δ(wa), std::forward<F>(f)); }
constexpr auto	dedekind::category::σ (WA const &wa, F f)
	σ (sigma): Co-Kleisli extend (comonadic extension).
template<typename MonadTag, typename MA, typename F> requires IsDefaultMonadTag<MonadTag> && requires(MonadTag tag, MA const& ma, F&& f) { μ(tag, detail_kleisli::lifted(ma, std::forward<F>(f))); }
constexpr auto	dedekind::category::κ (MonadTag tag, MA const &ma, F f)
	κ with explicit monad-tag dispatch.
template<typename MonadTag, typename WA, typename F> requires IsDefaultMonadTag<MonadTag> && requires(MonadTag tag, WA const& wa, F&& f) { detail_kleisli::lifted(δ(tag, wa), std::forward<F>(f)); }
constexpr auto	dedekind::category::σ (MonadTag tag, WA const &wa, F f)
	σ with explicit monad-tag dispatch.
template<std::ranges::input_range R, typename TA, typename Step> requires detail_kleisli::IsKleisliStep<Step, TA, std::ranges::range_value_t<R>>
constexpr TA	dedekind::category::fold (R r, TA ta, Step step)
template<typename MA, typename F> requires requires(MA const& ma, F&& f) { { κ(ma, std::forward<F>(f)) }; }
constexpr auto	dedekind::category::operator>>= (MA const &ma, F f)
	operator>>= : Monadic bind (Kleisli arrow application).
template<typename WA, typename F> requires requires(WA const& wa, F&& f) { { σ(wa, std::forward<F>(f)) }; }
constexpr auto	dedekind::category::operator<<= (WA const &wa, F f)
	operator<<= : Comonadic extend (co-Kleisli arrow application).

Variables
template<typename M>
constexpr bool	dedekind::category::is_kleisli_deref_v = false
	is_kleisli_deref_v<M>: opt-in marker that the carrier's operator-> realises Kleisli dereference (for monadic carriers like Maybe<T>) or comonadic extract ε (for comonadic carriers like Identity<T>). Default false; specialise to true at the carrier site.
template<typename E, typename M>
constexpr bool	dedekind::category::is_kleisli_arrow_v = false
	User-declared "Kleisli arrow" witness (#380, step 1).
template<>
constexpr bool	dedekind::category::is_kleisli_arrow_v< _kleisli_arrow_witness_380::toy_partial_realize, maybe_monad_tag > = true

Detailed Description

The Kleisli Partition (The Extension Systems).

@partition :kleisli

kleisli__The_Kleisli_Unification

This partition defines the "Extension Systems" that serve as the functional engine for the Dedekind ontology. By focusing on the Kleisli Triple (for Monads) and the Co-Kleisli Triple (for Comonads), extension reads the functor's action on arrows, F(f), and needs no applicator of its own.

(Monadic Push)

A species provides a Kleisli system if it implements:

• η (Unit/Return): value injection into context.
• >>= (Bind) : The 'extension' operator, chaining computations within the context.

(Comonadic Pull)

A species provides a Co-Kleisli system if it implements:

• ε (Counit/Extract): value extraction from context.
• <<= (Extend) : The 'co-extension' operator, sampling the species into a new context.

kleisli__Notation_Mapping

Surface

Core monadic/comonadic symbols and their implementation names:

• η : unit/pure (concrete overloads defined in :natural)
• μ : join/flatten (concrete overloads defined in :natural)
• ε : counit/extract (concrete overloads defined in :natural)
• δ : comultiplication/duplicate (concrete overloads defined in :natural)
• κ : Kleisli extension (κ(ma, f)), exported in this partition
• σ : co-Kleisli extension (σ(wa, f)), exported in this partition

Operator and named aliases in this partition:

• ma >>= f is κ(ma, f) as an operator, κ(tag, ma, f) with a monad tag
• wa <<= f is σ(wa, f) as an operator, σ(tag, wa, f) with a monad tag
• fish aliases: ma >> f (Kleisli) and wa << f (co-Kleisli)

kleisli__The_Bootstrapping_Mechanism

Kleisli extension is μ ∘ T(f) and co-Kleisli extension W(f) ∘ δ: both read the functor's action on arrows, F(f), from :functor (#1114).

Copyright

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

Note

"Important though the general concepts and propositions may be with which the modern industrious passion for axiomatizing and generalizing has presented us, in algebra perhaps more than anywhere else, nevertheless I am convinced that the special problems in all their complexity constitute the stock and core of mathematics." – Hermann Weyl, The Classical Groups (1939)