lawcheck

Property-based algebraic law testing for Python. Ready-made Hypothesis law suites for semigroups, monoids, commutative structures, groups, abelian groups, semirings, functors, applicatives, monads, equivalence relations (Eq), and total orders (Ord), with a pluggable equality oracle.

The problem

Algebraic laws (associativity, identity, functor composition, monad associativity) are easy to state but hard to test systematically. You want Hypothesis to search for counterexamples, not to write the laws yourself every time.

The bigger problem: what does "equal" mean for your type?

For int it's obvious. For IO[A], Task, async wrappers, or any effectful type, two logically equal values are often physically distinct objects. Python's == is wrong or absent. The cats-effect Scala library confronted this exactly and introduced a formal Eq type-class hierarchy. lawcheck asks you to supply eq explicitly so the meaning of "equal" is always unambiguous.

Install

pip install lawcheck

Sole runtime dependency: hypothesis.

Usage

Layer 1: pure primitives (no Hypothesis, deterministic)

import operator
from lawcheck import holds_associative, assert_associative

# Check one triple
holds_associative(operator.add, 1, 2, 3, eq=operator.eq)  # True
holds_associative(operator.sub, 1, 2, 3, eq=operator.eq)  # False

# Assert or raise with a precise message
assert_associative(operator.sub, 1, 2, 3, eq=operator.eq)
# AssertionError: Associativity violated: (op(1, 2)) op 3 = -4, but 1 op (op(2, 3)) = 2

Layer 2: Hypothesis runners (search for counterexamples)

import operator
from hypothesis import strategies as st
from lawcheck import verify_monoid, verify_commutative, verify_semigroup

# Passes for int addition (associative, left and right identity at 0, commutative)
verify_monoid(operator.add, 0, strategy=st.integers(), eq=operator.eq)
verify_commutative(operator.add, strategy=st.integers(), eq=operator.eq)

# Finds a counterexample for subtraction
verify_semigroup(operator.sub, strategy=st.integers(), eq=operator.eq)
# Raises with Hypothesis's shrunk minimal counterexample

Group, abelian group, and semiring laws

import operator
from hypothesis import strategies as st
from lawcheck import verify_group, verify_abelian_group, verify_semiring

# Group: monoid laws + left and right inverse
verify_group(operator.add, 0, operator.neg, strategy=st.integers(), eq=operator.eq)

# Abelian group: group laws + commutativity (reuses verify_commutative)
verify_abelian_group(
    operator.add, 0, operator.neg, strategy=st.integers(), eq=operator.eq
)

# Semiring: additive commutative monoid + multiplicative monoid +
# distributivity + annihilation by zero
verify_semiring(
    operator.add, operator.mul, 0, 1, strategy=st.integers(), eq=operator.eq
)

# The non-negative integers are a monoid under addition but not a group:
# no function N -> N can satisfy the inverse laws, so the inverse check fails
verify_group(
    operator.add,
    0,
    lambda x: 0,
    strategy=st.integers(min_value=0, max_value=100),
    eq=operator.eq,
)
# Raises: Left inverse violated

Functor, applicative, and monad laws

from lawcheck import verify_functor, verify_applicative, verify_monad

# fmap: (f: A -> B, fa: F[A]) -> F[B]
verify_functor(
    my_fmap,
    f=lambda x: x * 2,
    g=lambda x: x + 1,
    strategy=my_strategy,
    eq=my_eq,
)

# pure: A -> F[A];  ap: (F[A -> B], F[A]) -> F[B]
verify_applicative(
    my_pure,
    my_ap,
    lambda x: x * 2,
    value_strategy=st.integers(),
    functor_strategy=my_fa_strategy,
    ap_strategy=my_fn_strategy,
    eq=my_eq,
)

verify_monad(
    ret=my_return,
    bind=my_bind,
    f_arrow=lambda x: my_return(x + 1),
    g_arrow=lambda x: my_return(x * 2),
    strategy=st.integers(),
    monad_strategy=my_monad_strategy,
    eq=my_eq,
)

Eq and Ord laws

import operator
from hypothesis import strategies as st
from lawcheck import verify_eq, verify_order

# Eq: reflexivity, symmetry, transitivity of an equality predicate
verify_eq(operator.eq, strategy=st.integers())

# A broken relation (equal if within 1) is reflexive and symmetric but not
# transitive, so verify_eq finds a counterexample:
verify_eq(lambda a, b: abs(a - b) <= 1, strategy=st.integers(min_value=0, max_value=10))
# Raises: Eq transitivity violated

# Ord: reflexivity, antisymmetry (up to eq), transitivity, totality of a <=
verify_order(operator.le, strategy=st.integers(), eq=operator.eq)

# Divisibility is only a partial order; 2 and 3 are incomparable, so totality fails:
verify_order(lambda a, b: b % a == 0, strategy=st.integers(min_value=2, max_value=12), eq=operator.eq)
# Raises: Order totality violated

Pluggable equality oracle

from lawcheck import normalized_eq, lifted_eq, value_eq

# Compare after normalization (e.g. abs value, canonical form)
abs_eq = normalized_eq(abs)

# Unwrap a container and compare inner values
box_eq = lifted_eq(lambda b: b.value, operator.eq)

# Plain == (correct for ints, strings, lists)
value_eq(1, 1)  # True

Laws implemented

The eq parameter is required everywhere

lawcheck has no default for eq. Where ergonomics would tempt a default, there is an explicit second function instead (e.g., value_eq for plain types). This is by design: the cats-effect equality-oracle problem is real, and baking in == would silently produce wrong answers for effects, async types, and custom containers.

See docs/architecture.md for the full design rationale.

Contributing

See CONTRIBUTING.md and CODE_OF_CONDUCT.md.

License

MIT. See LICENSE.