Skip to content

Arrow Theories (panproto mirror)

TypeclassTheory records for the arrow typeclasses: ThCategory_, ThArrow, ThArrowChoice, ThArrowApply, ThArrowLoop, ThArrowZero, and ThArrowPlus.

theories

Panproto theories mirroring the arrow typeclass tower.

Each Hughes-style arrow typeclass corresponds to a panproto theory that declares the operations and laws the typeclass requires:

  • ThCategory_: composition and identity, with the three category laws.
  • ThArrow: adds arr and first, with the seven Hughes arrow laws.
  • ThArrowChoice, ThArrowApply, ThArrowLoop, ThArrowZero, ThArrowPlus: the additional operations and laws of each extension.

The bridges in quivers.monadic.bridges correspond to panproto theory morphisms ThMonad → ThArrowApply (Kleisli construction) and back (ArrowMonad construction); the round-trip composition is the identity on the appropriate theory image.

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.

The theory constants are documented on the arrows overview.