dedekind::category::detail_arrows Namespace Reference

The endomorphisms of T that have a storage class, as three coproducts, each an arrow by case analysis and a coproduct by construction (the Jlt paper, Listing 2). More...

Classes
struct	At
	The visitor that applies the active arrow to x. More...

Functions
constexpr void	refuse_deep_composite ()
	The refusal of a composite of composites: not a constant expression, so the compile-time evaluation that reaches it fails, and at run time the end of the program, since Rule 1 admits no throw.
template<typename T, typename Op>
constexpr bool	is_identity_tag (const Morphisms< T, Op > &m)
	Whether a morphism is the identity, read off its tags, so that composing asks no == of the carrier.

Detailed Description

The endomorphisms of T that have a storage class, as three coproducts, each an arrow by case analysis and a coproduct by construction (the Jlt paper, Listing 2).

cartesian__Arrows_As_Coproducts

• Sections<T, Op>: the identity, or a section of the operation. Closed under composition by the rewrites id >> s = s and s >> s' = s'' (associativity): a monoid.
• Morphisms<T, Op>: a section, or a morphism over a function pointer, which every stateless arrow on T becomes through call<F{}, T>. Two pointers compose to a closure, so this is not closed: it composes into Arrows.
• Arrows<T, Op>: a Morphisms, or the composite of two. Composition is restricted to one level, since a composite of composites has no alternative of fixed size to land in: it is refused, at compile time by failing the constant evaluation, at run time by ending the program. Within the restriction it is a partial monoid, its composition defined to one level, not a monoid, so no monoid is certified on it; the identity is its unit, decidably so: the unit has one representation, and equality is case by case, pointers and elements, so the laws can be checked, which an erased closure would not allow. Composition normalises: the identity is absorbed and two sections merge, so that the laws hold on representations, which is what equality reads.

Function Documentation

is_identity_tag()

template<typename T, typename Op>

bool dedekind::category::detail_arrows::is_identity_tag ( const Morphisms< T, Op > & m )

constexpr

Whether a morphism is the identity, read off its tags, so that composing asks no == of the carrier.

Parameters

m	the morphism.