Monad ↔ Arrow Bridges¶
Kleisli and ArrowMonad, together with the kleisli and
arrow_monad helpers that connect the two typeclass hierarchies.
bridges
¶
Bridges between the monad and arrow typeclass towers.
Three canonical conversions:
kleisli— given aMonadinstancem, produce aKleisli(m)arrow whose hom fromAtoBis the V-Rel morphism setHom(A, m(B)).arrow_monad— given anArrowApplyinstancea, produce aMonadwhose underlying functor isArrowMonad(a)(α) = a(1, α).cokleisli— comonadic dual ofkleisli.
Each bridge is realised at the value level as concrete morphism
constructions: compose is Kleisli composition (fmap-then-join),
first is the monad's strength applied to the second-factor
input, app is the canonical evaluator over the function-space
encoding [A → B]. The bridge round-trip arrow_monad ∘ kleisli
is the identity on monad theories (Hughes 2000, Theorem 3.1).
Kleisli
didactic-model
¶
Bases: Model
The Kleisli arrow of a monad.
Hom from A to B is the set of morphisms A → m(B) in
V-Rel. Composition is Kleisli composition (fmap, then join);
identity is Monad.pure. first is realised via the
canonical monad strength; app evaluates a function-space
embedding through the monad's Monad.apply.
monad is held opaquely so the typeclass-ABC reference
survives in-process identity through with_ without panproto
schema validation; the field does not round-trip through JSON.
| ATTRIBUTE | DESCRIPTION |
|---|---|
monad |
The underlying monad instance.
TYPE:
|
compose
¶
Kleisli composition f ; g = join ∘ fmap(g) ∘ f.
f : A → m(B), g : B → m(C) ⊢ g ∘_K f : A → m(C).
Source code in src/quivers/monadic/bridges.py
first
¶
first(f) : (A × C) → m(B × C) via the monad's strength.
Realised as (f × id_C) ; strength_m(B, C).
Source code in src/quivers/monadic/bridges.py
app
¶
app : m([A → B]) × m(A) → m(B) via the monad's apply.
Routes through the Applicative-level apply, which every Monad has by inclusion.
Source code in src/quivers/monadic/bridges.py
ArrowMonad
didactic-model
¶
Bases: Model
The monad induced by an ArrowApply arrow.
Hughes 2000 §4: any ArrowApply arrow a gives a monad
ArrowMonad(a)(α) = a(1, α), where 1 is the monoidal unit.
Realised concretely:
fmap_obj(A) = A(the underlying carrier coincides with the target type of the arrow's hom from the unit);pure(A)is the arrow'sarr(id_A);join(A)is the arrow'sappmorphism on the unit-anchored arrow values.
arrow is held opaquely.
| ATTRIBUTE | DESCRIPTION |
|---|---|
arrow |
The underlying arrow.
TYPE:
|
fmap
¶
fmap(f) : ArrowMonad(a)(A) → ArrowMonad(a)(B).
Realised as arr(f) on the underlying arrow.
pure
¶
apply
¶
apply : ArrowMonad(a)([A → B]) ⊗ ArrowMonad(a)(A) → ArrowMonad(a)(B).
Routes through the underlying arrow's ArrowApply.app.
join
¶
join : ArrowMonad(a)(ArrowMonad(a)(A)) → ArrowMonad(a)(A).
ArrowMonad's fmap_obj is identity, so join is also identity.
lift_a2
¶
lift_a2(f) : a(A) × a(B) → a(C), derived via arr(f).
CoKleisli
didactic-model
¶
Bases: Model
The CoKleisli category of a comonad.
Hom from A to B is the set of morphisms W(A) → B.
Composition is the comonadic CoKleisli composition
f =>> g = g ∘ W(f) ∘ δ_A; identity is the counit ε_A.
CoKleisli is registered as Category_ rather than
Arrow because the arrow first derivation requires
a comonadic costrength W(A × C) → W(A) × C, which is not
canonical for an arbitrary comonad. When the underlying comonad
supplies a costrength(A, C) method, that morphism composes
with parallel(f, ε_C ∘ W(π_2)) to realise first as the
full Arrow primitive; the helper first_via_costrength
constructs that morphism given an explicit costrength.
comonad is held opaquely so the typeclass-ABC reference
survives in-process identity without panproto schema validation.
| ATTRIBUTE | DESCRIPTION |
|---|---|
comonad |
The underlying comonad instance.
TYPE:
|
first_via_costrength
¶
Realise first(f) given an explicit comonad costrength.
costrength : W(A × C) → W(A) × C is the comonad-specific
morphism (analogous to the monad strength). With it,
first(f, C) = costrength ; (f × id_C) is a valid CoKleisli
arrow W(A × C) ⇝ B × C.
| PARAMETER | DESCRIPTION |
|---|---|
f
|
A CoKleisli arrow
TYPE:
|
C
|
The fixed second-factor object.
TYPE:
|
costrength
|
The comonad's costrength
TYPE:
|
Source code in src/quivers/monadic/bridges.py
kleisli
¶
arrow_monad
¶
arrow_monad(arrow: ArrowApply) -> ArrowMonad
Wrap an ArrowApply arrow as a Monad.
| PARAMETER | DESCRIPTION |
|---|---|
arrow
|
The arrow whose
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
ArrowMonad
|
The monad of |
Source code in src/quivers/monadic/bridges.py
cokleisli
¶
Wrap a Comonad as a CoKleisli category.
The result is registered as Category_ (always) but not
Arrow; promoting to an Arrow requires the user-supplied
costrength routed through CoKleisli.first_via_costrength.
| PARAMETER | DESCRIPTION |
|---|---|
comonad
|
The comonad whose CoKleisli category is built.
TYPE:
|
| RETURNS | DESCRIPTION |
|---|---|
CoKleisli
|
The CoKleisli category of |