M06C02: Law-Guided Design – Identity & Associativity Checks with Hypothesis¶
Progression Note¶
Module 6 shifts from pure data modelling to effect-aware composition.
We now treat failure and absence as first-class effects that propagate automatically through pipelines — eliminating nested conditionals forever.
| Module | Focus | Key Outcomes |
|---|---|---|
| 5 | Algebraic Data Modelling | ADTs, exhaustive pattern matching, total functions, refined types |
| 6 | Monadic Flows as Composable Pipelines | bind/and_then, Reader/State-like patterns, error-typed flows |
| 7 | Effect Boundaries & Resource Safety | Dependency injection, boundaries, testing, evolution |
Core question
How do you use property-based testing with Hypothesis to machine-check that your and_then (and map) implementations satisfy the monad/functor laws — giving you high, mechanically verified confidence that arbitrarily long pipelines will behave exactly as the equational reasoning predicts?
Property-based testing with Hypothesis turns the algebraic laws from “nice theory” into executable specifications that run in CI and fail fast if anyone ever regresses the core abstractions.
Audience: Engineers who already write and_then chains and now want mechanical confidence (not hope) that their compositions are safe to refactor forever.
Outcome 1. You will have a reusable, DRY test suite that machine-checks monad/functor laws for Result and Option. 2. You will see exactly how a broken implementation fails the properties (and shrinks to a minimal counterexample). 3. You will internalise why these laws are the only thing standing between “works on happy path” and “works under all possible compositions”.
Why Laws Matter – One Sentence Each¶
- Left identity: Wrapping a value and immediately unwrapping is a no-op → you can safely insert
Ok(x)orSome(x)anywhere without changing meaning. - Right identity: Feeding the identity function (
Ok/Some) does nothing → you can refactor by extracting sub-pipelines without fear. - Associativity: Parentheses don’t matter → you can regroup chains freely during refactoring; the code stays correct even when the structure changes dramatically.
Violate any of these and your pipeline may work today but break silently tomorrow when someone adds a step or changes grouping.
1. Laws & Invariants (machine-checked in CI)¶
| Law | Formal Statement | Why it matters in practice |
|---|---|---|
| Monad Left Identity | Ok(x).and_then(f) == f(x) |
Safe to lift plain values into the monad |
| Monad Right Identity | m.and_then(Ok) == m / m.and_then(Some) == m |
Safe to extract sub-pipelines |
| Monad Associativity | m.and_then(f).and_then(g) == m.and_then(lambda x: f(x).and_then(g)) |
Refactor grouping without changing semantics |
| Functor Identity | m.map(id) == m |
Mapping identity does nothing |
| Functor Composition | m.map(f).map(g) == m.map(lambda x: g(f(x))) |
Order of mapping is predictable |
| Result Bifunctor Identity | m.map_err(id) == m |
Error mapping identity is no-op |
| Result Bifunctor Composition | m.map_err(f).map_err(g) == m.map_err(lambda e: g(f(e))) |
Error transformation composes correctly |
| Short-circuit | Err(e).and_then(any) == Err(e) / NoneVal().and_then(any) == NoneVal() |
Forgotten propagation paths impossible |
All laws are verified with Hypothesis in CI. A single failing example breaks the build.
2. Strategies – Shrinkable, Deterministic Function Families (tests/strategies.py)¶
from __future__ import annotations
from typing import Callable
from hypothesis import strategies as st
from funcpipe_rag.result.types import Ok, Err, Some, NoneVal, Result, Option
def st_values() -> st.SearchStrategy[int]:
return st.integers(-20, 20)
def st_errors() -> st.SearchStrategy[str]:
return st.text(min_size=0, max_size=8)
def st_result() -> st.SearchStrategy[Result[int, str]]:
return st.one_of(
st.builds(Ok, st_values()),
st.builds(Err, st_errors()),
)
def st_option() -> st.SearchStrategy[Option[int]]:
return st.one_of(
st.builds(Some, st_values()),
st.just(NoneVal()),
)
@st.composite
def st_func_to_result(draw) -> Callable[[int], Result[int, str]]:
ok_val = draw(st_values())
err_val = draw(st_errors())
threshold = draw(st.integers(-10, 10))
def f(x: int) -> Result[int, str]:
return Ok(ok_val if x >= threshold else x * 2) if x % 2 == 0 else Err(err_val)
return f
@st.composite
def st_func_to_option(draw) -> Callable[[int], Option[int]]:
some_val = draw(st_values())
threshold = draw(st.integers(-10, 10))
def f(x: int) -> Option[int]:
return (
Some(some_val if x >= threshold else x + 1)
if (x % 3) != 0
else NoneVal()
)
return f
These families are deliberately rich (both branches hit frequently) yet shrink beautifully.
3. Law Templates (tests/law_templates.py – completely DRY)¶
from __future__ import annotations
from typing import TypeVar, Callable
from funcpipe_rag.result.types import Result, Option, Some
A = TypeVar("A")
B = TypeVar("B")
C = TypeVar("C")
E = TypeVar("E")
# ====================== Result monad laws ======================
def result_monad_left_identity(
pure: Callable[[A], Result[A, E]],
x: A,
f: Callable[[A], Result[B, E]],
) -> None:
assert pure(x).and_then(f) == f(x)
def result_monad_right_identity(
m: Result[A, E],
pure: Callable[[A], Result[A, E]],
) -> None:
assert m.and_then(pure) == m
def result_monad_associativity(
m: Result[A, E],
f: Callable[[A], Result[B, E]],
g: Callable[[B], Result[C, E]],
) -> None:
left = m.and_then(f).and_then(g)
right = m.and_then(lambda x: f(x).and_then(g))
assert left == right
# ====================== Option monad laws ======================
def option_monad_left_identity(
pure: Callable[[A], Some[A]],
x: A,
f: Callable[[A], Option[B]],
) -> None:
assert pure(x).and_then(f) == f(x)
def option_monad_right_identity(
m: Option[A],
pure: Callable[[A], Some[A]],
) -> None:
assert m.and_then(pure) == m
def option_monad_associativity(
m: Option[A],
f: Callable[[A], Option[B]],
g: Callable[[B], Option[C]],
) -> None:
left = m.and_then(f).and_then(g)
right = m.and_then(lambda x: f(x).and_then(g))
assert left == right
4. Property-Based Proofs (tests/test_monad_laws.py)¶
from hypothesis import given, settings
from hypothesis import strategies as st
from tests.strategies import (
st_result,
st_option,
st_func_to_result,
st_func_to_option,
st_errors,
)
from tests.law_templates import (
result_monad_left_identity,
result_monad_right_identity,
result_monad_associativity,
option_monad_left_identity,
option_monad_right_identity,
option_monad_associativity,
)
from funcpipe_rag.result.types import Ok, Err, Some, NoneVal
# Reproducible, fast, CI-friendly profile
settings.register_profile("ci", max_examples=500, derandomize=True, deadline=None)
settings.load_profile("ci")
# ====================== Result ======================
@given(x=st.integers(-20,20), f=st_func_to_result())
def test_result_left_identity(x, f):
result_monad_left_identity(Ok, x, f)
@given(m=st_result())
def test_result_right_identity(m):
result_monad_right_identity(m, Ok)
@given(m=st_result(), f=st_func_to_result(), g=st_func_to_result())
def test_result_associativity(m, f, g):
result_monad_associativity(m, f, g)
@given(m=st_result())
def test_result_functor_identity(m):
assert m.map(lambda x: x) == m
@given(m=st_result(), a=st.integers(-10,10), b=st.integers(-10,10))
def test_result_functor_composition(m, a, b):
f = lambda x: x + a
g = lambda x: x * b
assert m.map(f).map(g) == m.map(lambda x: g(f(x)))
@given(m=st_result())
def test_result_bifunctor_identity(m):
assert m.map_err(lambda e: e) == m
@given(m=st_result(), prefix=st.text(max_size=4), suffix=st.text(max_size=4))
def test_result_bifunctor_composition(m, prefix, suffix):
f = lambda e: prefix + e
g = lambda e: e + suffix
assert m.map_err(f).map_err(g) == m.map_err(lambda e: g(f(e)))
@given(e=st_errors())
def test_result_short_circuit(e):
assert Err(e).and_then(lambda _: Ok(999)) == Err(e)
# ====================== Option ======================
@given(x=st.integers(-20,20), f=st_func_to_option())
def test_option_left_identity(x, f):
option_monad_left_identity(Some, x, f)
@given(o=st_option())
def test_option_right_identity(o):
option_monad_right_identity(o, Some)
@given(o=st_option(), f=st_func_to_option(), g=st_func_to_option())
def test_option_associativity(o, f, g):
option_monad_associativity(o, f, g)
@given(o=st_option())
def test_option_functor_identity(o):
assert o.map(lambda x: x) == o
@given(o=st_option(), a=st.integers(-10,10), b=st.integers(-10,10))
def test_option_functor_composition(o, a, b):
f = lambda x: x + a
g = lambda x: x * b
assert o.map(f).map(g) == o.map(lambda x: g(f(x)))
def test_option_short_circuit():
assert NoneVal().and_then(lambda _: Some(999)) == NoneVal()
All tests pass with the correct ADT implementation.
If you deliberately break Err.and_then to return Ok(0) instead of self, the right-identity test fails with the minimal counterexample Err('') in < 0.1 s.
5. Gotchas & Best Practices¶
- Domain restriction: Always bound integers/text you feed into functions; unbounded strategies generate values that trigger slow paths or overflow.
- Floating-point values: Never use
==on floats in laws; usemath.iscloseor stick to exact domains (int, str). - Vacuous laws: If your function strategy is too weak (e.g. always returns
Ok(42)), associativity becomes trivially true. Use rich predicates that hit both branches. - Performance: The
"ci"profile above is deterministic and fast enough for CI (≈ 3–4 seconds total).
6. Anti-Patterns & Immediate Fixes¶
| Anti-Pattern | Symptom | Fix |
|---|---|---|
| Only unit tests for laws | Misses subtle corner cases | Use Hypothesis properties |
| Random lambdas in tests | Flaky shrinks, non-reproducible | Deterministic function families |
| Ignoring a failing law | “It works in my case” | Fix the implementation – laws are non-negotiable |
| Duplicated law checks | Test rot | DRY templates + shared strategies |
7. Pre-Core Quiz¶
- Left identity guarantees…? → You can safely lift plain values
- Right identity guarantees…? → You can safely extract sub-pipelines
- Associativity guarantees…? → Grouping/refactoring never changes meaning
- Hypothesis gives you…? → Minimal counterexamples when a law breaks
- Why not just unit tests? → They miss the infinite corner cases laws protect against
8. Post-Core Exercise¶
- Deliberately break
Err.and_thento returnOk(0)instead ofself. Run the suite and observe which law fails first and the shrunk counterexample. - Add a new combinator
result_bimap(f_ok, f_err)and prove it satisfies the expected bifunctor laws. - Write a property that proves
result_sequence([Ok(x) for x in xs]) == Ok(list(xs))and short-circuits on the firstErr. - Implement the same laws for a tiny custom monad of your own (e.g. a
Logger[str, A]Writer) and get the suite green.
Next: M06C03 – Validation Applicative – Accumulating Errors Instead of Fail-Fast
You now have mechanical verification that your core abstractions satisfy the algebraic laws — meaning every pipeline you write for the rest of the project is extremely unlikely to break under composition or refactoring, because the laws have been checked over thousands of generated examples.