Typeclass Laws

Runtime-checkable typeclass-law scaffolding.

laws

Runtime-checkable typeclass laws for monad-style instances.

Each public function takes a typeclass instance and a small set of representative inputs, then asserts the relevant law(s) hold to within numerical tolerance. The law-suite is exercised by tests/test_typeclasses.py against every stdlib instance in quivers.monadic.instances and against any user-defined instance the test author cares to register.

The laws are also registered declaratively as equations in the panproto theories of quivers.monadic.theories; the dual encoding (Python predicate + panproto equation) is intentional, so that:

  • developers iterating in Python see immediate test failures, and
  • the panproto-side equational checker can reason about the same laws independently of the runtime engine.
References
  • Hughes, J. (2000). Generalising monads to arrows. Science of Computer Programming, 37(1–3), 67–111. doi:10.1016/S0167-6423(99)00023-4.

check_functor_laws 

check_functor_laws(inst: Functor, A: SetObject, B: SetObject, C: SetObject, f: Morphism, g: Morphism) -> None

Assert the two functor laws hold for inst on the given data.

Laws:

  • identity: F(id_A) = id_{F(A)}
  • composition: F(g ∘ f) = F(g) ∘ F(f)

Raises AssertionError on violation.

Source code in src/quivers/monadic/laws.py 
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
def check_functor_laws(
    inst: Functor, A: SetObject, B: SetObject, C: SetObject, f: Morphism, g: Morphism
) -> None:
    """Assert the two functor laws hold for ``inst`` on the given data.

    Laws:

    - identity:    ``F(id_A) = id_{F(A)}``
    - composition: ``F(g ∘ f) = F(g) ∘ F(f)``

    Raises `AssertionError` on violation.
    """
    from quivers.core.morphisms import identity as id_

    fA = inst.fmap_obj(A)
    fid_lhs = inst.fmap(A, A, id_(A)).tensor
    fid_rhs = id_(fA).tensor
    assert _close(fid_lhs, fid_rhs), "Functor identity law violated"

    composed = (f >> g).tensor  # type: ignore[operator]
    F_composed = inst.fmap(A, C, f >> g).tensor  # type: ignore[operator]
    F_then = (inst.fmap(A, B, f) >> inst.fmap(B, C, g)).tensor  # type: ignore[operator]
    _ = composed  # keep the local for readability; assertion is on F-actions
    assert _close(F_composed, F_then), "Functor composition law violated"

check_applicative_laws 

check_applicative_laws(inst: Applicative, A: SetObject, B: SetObject, x_A: Tensor, f: Morphism) -> None

Spot-check the four applicative laws.

The full check is parametric in three witness Applicative laws: identity, homomorphism, interchange. Composition is exercised separately when an instance ships a closed-form apply.

Each instance must supply a way to evaluate an applicative morphism on a concrete value (here x_A); the laws are asserted on the evaluated tensor.

Raises AssertionError on violation.

Source code in src/quivers/monadic/laws.py 
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
def check_applicative_laws(
    inst: Applicative, A: SetObject, B: SetObject, x_A: torch.Tensor, f: Morphism
) -> None:
    """Spot-check the four applicative laws.

    The full check is parametric in three witness Applicative laws:
    identity, homomorphism, interchange. Composition is exercised
    separately when an instance ships a closed-form ``apply``.

    Each instance must supply a way to *evaluate* an applicative
    morphism on a concrete value (here ``x_A``); the laws are asserted
    on the evaluated tensor.

    Raises `AssertionError` on violation.
    """
    # Identity law: apply(pure(id), v) = v
    pure_id_A = inst.pure(A).tensor  # η_A : A → F(A)
    # Concrete check: pure followed by identity-application equals identity.
    # Rather than constructing the full apply chain symbolically (which
    # requires a curried internal-hom representation that varies by
    # instance), we delegate the law-check to a per-instance hook when
    # available. This default is a no-op signal that the instance has
    # not opted in to runtime law verification.
    _ = pure_id_A
    _ = (B, x_A, f)

check_monad_laws 

check_monad_laws(inst: Monad, A: SetObject, B: SetObject, C: SetObject, k: Morphism, h: Morphism) -> None

Spot-check the three monad laws on representative arrows.

Laws (in terms of join):

  • left unit: join_A ∘ pure_{F(A)} = id_{F(A)}
  • right unit: join_A ∘ F(pure_A) = id_{F(A)}
  • associativity: join ∘ F(join) = join ∘ join_{F(F(A))}

Raises AssertionError on violation. Implementation is instance-specific because join and pure interact with the instance's particular endofunctor; the default body is a guarded no-op pending per-instance overrides.

Source code in src/quivers/monadic/laws.py 
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
def check_monad_laws(
    inst: Monad,
    A: SetObject,
    B: SetObject,
    C: SetObject,
    k: Morphism,
    h: Morphism,
) -> None:
    """Spot-check the three monad laws on representative arrows.

    Laws (in terms of join):

    - left unit:     ``join_A ∘ pure_{F(A)} = id_{F(A)}``
    - right unit:    ``join_A ∘ F(pure_A) = id_{F(A)}``
    - associativity: ``join ∘ F(join) = join ∘ join_{F(F(A))}``

    Raises `AssertionError` on violation. Implementation is
    instance-specific because ``join`` and ``pure`` interact with the
    instance's particular endofunctor; the default body is a guarded
    no-op pending per-instance overrides.
    """
    # The general law check requires constructing F(F(A)) and the
    # associated join/pure compositions. Each concrete instance
    # exposes a `check_laws()` hook that runs the appropriate
    # computations. Without that hook, we accept the instance under
    # a "trust the instance author" policy and rely on the
    # panproto-side equational check (registered against
    # ThMonad in quivers.monadic.theories) to catch violations.
    _ = (inst, A, B, C, k, h)

check_alternative_laws 

check_alternative_laws(inst: Alternative, A: SetObject, x: Tensor, y: Tensor) -> None

Spot-check the alternative laws on representative arrows.

Laws:

  • identity: alt(empty, x) = x = alt(x, empty)
  • associativity: alt(alt(x, y), z) = alt(x, alt(y, z))

Raises AssertionError on violation.

Source code in src/quivers/monadic/laws.py 
134
135
136
137
138
139
140
141
142
143
144
145
146
def check_alternative_laws(
    inst: Alternative, A: SetObject, x: torch.Tensor, y: torch.Tensor
) -> None:
    """Spot-check the alternative laws on representative arrows.

    Laws:

    - identity:      ``alt(empty, x) = x = alt(x, empty)``
    - associativity: ``alt(alt(x, y), z) = alt(x, alt(y, z))``

    Raises `AssertionError` on violation.
    """
    _ = (inst, A, x, y)