Skip to content

Arrow Typeclass Hierarchy

The Hughes-style arrow hierarchy: Category_, Arrow, ArrowChoice, ArrowApply, ArrowLoop, ArrowZero, and ArrowPlus.

typeclasses

Hughes-style arrow typeclass interfaces.

Each abstract typeclass declares the operations an arrow instance must provide. Concrete instances (Function, VRel, Stochastic, Kleisli(M), Cokleisli(W), LinearMap) live in quivers.arrows.instances.

References

Category_

Bases: ABC

A category of computations.

Provides identity at every object plus binary composition. The underscore disambiguates from quivers.dsl.ast_nodes.CategoryDecl and quivers.stochastic.categories.Category which use the same word in different senses.

Laws:

  • compose(id, f) = f (left identity)
  • compose(f, id) = f (right identity)
  • compose(compose(f, g), h) = compose(f, compose(g, h)) (associativity)

id_arr abstractmethod 

id_arr(A: SetObject) -> Morphism

id_A : A ⇝ A.

Source code in src/quivers/arrows/typeclasses.py 
38
39
40
@abstractmethod
def id_arr(self, A: SetObject) -> Morphism:
    """``id_A : A ⇝ A``."""

compose abstractmethod 

compose(f: Morphism, g: Morphism) -> Morphism

f : A ⇝ B, g : B ⇝ C ⊢ g ∘ f : A ⇝ C.

Source code in src/quivers/arrows/typeclasses.py 
42
43
44
@abstractmethod
def compose(self, f: Morphism, g: Morphism) -> Morphism:
    """``f : A ⇝ B, g : B ⇝ C  ⊢  g ∘ f : A ⇝ C``."""

Arrow

Bases: Category_, ABC

An arrow: Category_ with arr and first.

Adds:

  • arr — lift a pure morphism into the arrow.
  • first — apply on the left of a pair, threading a context.

Defaults derivable from these and compose: second f = swap >>> first f >>> swap; f *** g = first f >>> second g (the parallel-product combinator); f &&& g = arr (\x. (x, x)) >>> (f *** g).

Hughes 2000 §3 lists the seven arrow laws.

arr abstractmethod 

arr(A: SetObject, B: SetObject, f: Morphism) -> Morphism

Lift a pure morphism: arr(f) : A ⇝ B from f : A → B.

Source code in src/quivers/arrows/typeclasses.py 
63
64
65
@abstractmethod
def arr(self, A: SetObject, B: SetObject, f: Morphism) -> Morphism:
    """Lift a pure morphism: ``arr(f) : A ⇝ B`` from ``f : A → B``."""

first abstractmethod 

first(f: Morphism, C: SetObject) -> Morphism

f : A ⇝ B ⊢ first(f, C) : (A ⊗ C) ⇝ (B ⊗ C).

Source code in src/quivers/arrows/typeclasses.py 
67
68
69
@abstractmethod
def first(self, f: Morphism, C: SetObject) -> Morphism:
    """``f : A ⇝ B  ⊢  first(f, C) : (A ⊗ C) ⇝ (B ⊗ C)``."""

ArrowChoice

Bases: Arrow, ABC

An arrow with sum-elimination: left and (derivably) right.

Adds:

  • left_arr — apply on the left of a coproduct.

Derived: right_arr, +++, |||.

left_arr abstractmethod 

left_arr(f: Morphism, C: SetObject) -> Morphism

f : A ⇝ B ⊢ left(f, C) : (A + C) ⇝ (B + C).

Source code in src/quivers/arrows/typeclasses.py 
82
83
84
@abstractmethod
def left_arr(self, f: Morphism, C: SetObject) -> Morphism:
    """``f : A ⇝ B  ⊢  left(f, C) : (A + C) ⇝ (B + C)``."""

ArrowApply

Bases: Arrow, ABC

An arrow that can apply arrow-valued data: app.

ArrowApply instances are equivalent in expressive power to quivers.monadic.typeclasses.Monad; the bridges in quivers.monadic.bridges realise the conversion in both directions.

app abstractmethod 

app(A: SetObject, B: SetObject) -> Morphism

app : Hom(A, B) ⊗ A ⇝ B.

Hom(A, B) is the internal hom of the arrow's underlying symmetric monoidal closed structure.

Source code in src/quivers/arrows/typeclasses.py 
 96
 97
 98
 99
100
101
102
@abstractmethod
def app(self, A: SetObject, B: SetObject) -> Morphism:
    """``app : Hom(A, B) ⊗ A ⇝ B``.

    ``Hom(A, B)`` is the internal hom of the arrow's underlying
    symmetric monoidal closed structure.
    """

ArrowLoop

Bases: Arrow, ABC

An arrow with feedback: loop.

Encodes traced symmetric monoidal structure on the arrow category.

For an arrow f : (A ⊗ C) ⇝ (B ⊗ C), loop(f) : A ⇝ B closes the loop on C. In Function, this is the least-fixed-point operator; in VRel, it is the iterative trace; in Stochastic and Kern, it is the cartesian / sampled trace.

The chart-fold parser combinator of quivers.dsl.ast_nodes.ExprChartFold is denotationally an loop_arr invocation on the appropriate arrow.

loop_arr abstractmethod 

loop_arr(f: Morphism, C: SetObject) -> Morphism

f : (A ⊗ C) ⇝ (B ⊗ C) ⊢ loop(f) : A ⇝ B.

Source code in src/quivers/arrows/typeclasses.py 
121
122
123
@abstractmethod
def loop_arr(self, f: Morphism, C: SetObject) -> Morphism:
    """``f : (A ⊗ C) ⇝ (B ⊗ C)  ⊢  loop(f) : A ⇝ B``."""

ArrowZero

Bases: Arrow, ABC

An arrow with a designated bottom at every hom: zero_arr.

zero_arr abstractmethod 

zero_arr(A: SetObject, B: SetObject) -> Morphism

zero : A ⇝ B — the bottom element of Hom(A, B).

Source code in src/quivers/arrows/typeclasses.py 
129
130
131
@abstractmethod
def zero_arr(self, A: SetObject, B: SetObject) -> Morphism:
    """``zero : A ⇝ B`` — the bottom element of ``Hom(A, B)``."""

ArrowPlus

Bases: ArrowZero, ABC

An ArrowZero with pointwise alternative: alt_arr.

alt_arr plays the role of Alternative.alt lifted to the arrow category's hom-sets.

alt_arr abstractmethod 

alt_arr(A: SetObject, B: SetObject) -> Morphism

Hom(A, B) ⊗ Hom(A, B) ⇝ Hom(A, B).

Source code in src/quivers/arrows/typeclasses.py 
141
142
143
@abstractmethod
def alt_arr(self, A: SetObject, B: SetObject) -> Morphism:
    """``Hom(A, B) ⊗ Hom(A, B) ⇝ Hom(A, B)``."""

Package constants

The arrow typeclass theories of quivers.arrows, each a TypeclassTheory.

Hughes-style arrow hierarchy for compositional computation.

Arrows present effectful computation as a category of computations rather than as a sequence of binds. Following Hughes 2000, the hierarchy is:

Category_
├── Arrow
│   ├── ArrowChoice
│   ├── ArrowApply       — equivalent power to Monad via ArrowMonad
│   ├── ArrowLoop        — feedback / fixed points
│   └── ArrowZero
│       └── ArrowPlus

Each typeclass is an ABC declaring the operations an arrow instance must provide; default derivations are supplied where Hughes admits them. Concrete instances (Function, VRel, Stochastic, Kleisli(M), Cokleisli(W), LinearMap) live alongside in quivers.arrows.instances.

Bridges between the monad and arrow hierarchies live in quivers.monadic.bridges: every Monad gives a Kleisli arrow, every ArrowApply gives a Monad. The two presentations of effectful computation are interchangeable through these conversions.

References

ThCategory_ module-attribute 

ThCategory_ = TypeclassTheory(name='ThCategory_', sorts=('Object', 'Arr'), operations=('id_arr : Object → Arr', 'compose : Arr ⊗ Arr → Arr'), equations=('compose(id, f) = f', 'compose(f, id) = f', 'compose(compose(f, g), h) = compose(f, compose(g, h))'))

The theory of Category_.

ThArrow module-attribute 

ThArrow = TypeclassTheory(name='ThArrow', operations=('arr : (Object → Object) → Arr', 'first : Arr → Arr'), equations=('arr(id) = id_arr', 'arr(g ∘ f) = compose(arr(f), arr(g))', 'first(arr(f)) = arr(f × id)', 'compose(first(f), arr(id × g)) = compose(arr(id × g), first(f))', 'compose(first(f), arr(fst)) = compose(arr(fst), f)', 'first(first(f)) ≡ first(f) (assoc)', 'first(compose(f, g)) = compose(first(f), first(g))'), extends=('ThCategory_',))

The theory of Arrow.

ThArrowChoice module-attribute 

ThArrowChoice = TypeclassTheory(name='ThArrowChoice', operations=('left_arr : Arr → Arr',), equations=('left(arr(f)) = arr(left(f))', 'left(compose(f, g)) = compose(left(f), left(g))'), extends=('ThArrow',))

The theory of ArrowChoice.

ThArrowApply module-attribute 

ThArrowApply = TypeclassTheory(name='ThArrowApply', operations=('app : (Arr ⊗ Object) → Object',), equations=('compose(arr(λx. (arr(λy. (x, y)), z)), app) ≡ id',), extends=('ThArrow',))

The theory of ArrowApply.

ThArrowLoop module-attribute 

ThArrowLoop = TypeclassTheory(name='ThArrowLoop', operations=('loop_arr : Arr → Arr',), equations=('left tightening: loop(compose(arr(first(h)), f)) = compose(h, loop(f))', 'right tightening: loop(compose(f, arr(first(h)))) = compose(loop(f), h)', 'sliding: loop(compose(f, arr(id × k))) = loop(compose(arr(id × k), f))', 'vanishing: loop(arr(id)) = arr(id)', 'superposing: first(loop(f)) = loop(arr(assoc) ∘ first(f) ∘ arr(assoc⁻¹))'), extends=('ThArrow',))

The theory of ArrowLoop.

ThArrowZero module-attribute 

ThArrowZero = TypeclassTheory(name='ThArrowZero', operations=('zero_arr : Arr',), extends=('ThArrow',))

The theory of ArrowZero.

ThArrowPlus module-attribute 

ThArrowPlus = TypeclassTheory(name='ThArrowPlus', operations=('alt_arr : Arr ⊗ Arr → Arr',), equations=('alt(zero, f) = f', 'alt(f, zero) = f', 'alt(alt(f, g), h) = alt(f, alt(g, h))'), extends=('ThArrowZero',))

The theory of ArrowPlus.