dedekind::category::IsRetractableArrow Concept Reference

A monic arrow that ships with a structurally-known retract, a partial inverse retract(f) : Cod<F> → Maybe<Dom<F>>, discoverable via ADL on F. More...

Concept definition

template<typename F>
concept dedekind::category::IsRetractableArrow =  IsMonicArrow<F> && requires(F f, const Cod<F>& y) {
  { retract(f)(y) } -> std::same_as<Maybe<Dom<F>>>;
}

Detailed Description

A monic arrow that ships with a structurally-known retract, a partial inverse retract(f) : Cod<F> → Maybe<Dom<F>>, discoverable via ADL on F.

The retract is the operational gate for a decidability path on image(f, S) that's strictly more general than IsIsomorphism (which requires a total inverse): for a monic F that admits a partial inverse, the image membership

y ∈ image(F, S)

reduces to

let mx = retract(f)(y); mx.has_value() && S(*mx)

which is decidable whenever the retract itself is decidable. The canonical project use case is the embed_* family of carrier- lattice embeddings, each of which is monic and admits a natural partial inverse (e.g. embed_𝔹_ℕ has retract Cardinality → std::optional<bool>; embed_uint_ℕ has retract Cardinality → std::optional<unsigned> that fires on the finite-representable range).

Concept shape

The concept requires that retract(f) is invocable on Cod<F> const& and returns a Maybe -shaped value (Maybe<T> = std::optional<T>, supporting has_value() and operator*). Generalising to the project's broader IsPotential surface (which also admits Partial<T> / TernaryResult<T> as Maybe-likes) is a deliberate follow-up; for retracts specifically, the binary has/has-not distinction std::optional carries is what the image-overload needs, and tighter shapes than that aren't load-bearing today.

Relation to IsIsomorphism

Mathematically, an isomorphism has a total inverse, so a retract for it is available by construction (wrap inverse(f) in always-Some). We wire that up: IsMonicArrow accepts isos (in :morphism) and the IsoRetract blanket retract above serves every IsIsomorphism, so IsIsomorphism ⟹ IsRetractableArrow with no manual opt-in. A sound iso yields a sound retract, so this trades the (never audited) requirement to hand-register a retract for a derivation that cannot drift from inverse. Dispatch still branches on iso where a tighter iso path exists: the DSL image(iso, Set) overload (#657, in :sets:expressions) and the ImageChi iso specialisation both take precedence over the retract path (guarded !IsIsomorphism), so an iso uses its own path and only monic-but-not-iso arrows take the retract route. The point is to avoid divergent parallel paths, not to guard a developer against a mathematically-sound derived retract.

Opt-in semantics

A monic-but-not-iso retract is user-declared via the retract(f) ADL hook; there the user owns the correctness obligation (the hook genuinely partially-inverts F). The iso case needs no such hook.