Typeclass Theories (panproto mirror)

ThFunctor, ThApplicative, ThMonad, ThAlternative, ThMonadPlus, ThMonadTrans, ThFoldable, ThTraversable, panproto-theory record-stubs for each typeclass.

theories

Panproto theories mirroring the typeclass hierarchy.

For each typeclass in quivers.monadic.typeclasses, this module declares a corresponding panproto.Theory:

  • ThFunctor — sorts: Carrier, Hom; operation: fmap with the two functor laws as equations.
  • ThApplicative — extends ThFunctor with pure and apply and the four applicative laws.
  • ThMonad — extends ThApplicative with join (or equivalently bind) and the three monad laws.
  • ThAlternative, ThMonadPlus, ThMonadTrans, ThTraversable — likewise.

Class extension is realised as theory inclusion via panproto.colimit. Each typeclass instance in quivers.monadic.instances emits a panproto theory morphism whose existence panproto can verify (the operations are present, the equations hold).

The arrow tower in quivers.arrows.theories mirrors this construction for the Hughes-style arrow typeclasses.

Implementation note

This module currently declares the theories as Python data structures using a thin wrapper around panproto.define_theory. Some panproto API surface required for the full encoding (notably polymorphic-arity operations and equation-set composition under colimit) is in flux upstream; the wrapper falls back to a record-only representation when the panproto API is unavailable, so the typeclass framework remains usable without the panproto theory mirrors.