Skip to content

Recursive schemas

recursive ties a fixpoint: the builder it receives is given a placeholder standing for the schema being defined, and returns the body. The recursive reference must occur under a structural constructor (a list, tuple, set, dict, record, or object) so membership stays decidable; a non-contractive body is rejected when the validator is built.

A recursive JSON value

from valgebra import recursive, union

json_value = recursive(
    lambda j: union(None, bool, int, float, str, [j], {str: j}),
)
assert json_value.is_valid({"a": [1, "x", {"b": None}], "c": [True, 3.5]})
assert not json_value.is_valid({"a": object()})

A tree, then composed

A recursive schema is an ordinary validator and composes like any other:

from valgebra import recursive, Validator

tree = recursive(lambda t: {"value": int, "left?": t, "right?": t})
assert tree.is_valid({"value": 1, "left": {"value": 2}})

forest = Validator([tree])
assert forest.is_valid([{"value": 1}, {"value": 2, "right": {"value": 3}}])

A type alias is a fixpoint too

A PEP 695 alias that names itself is the standard typing spelling of a recursive schema, and it builds one. The alias is the binder: it is reached again while its own body is read, and the schema it builds is the schema the explicit call builds — the two are one set, and is_equivalent says so.

from valgebra import Validator, recursive, union

type Json = None | bool | int | float | str | list[Json] | dict[str, Json]

alias = Validator(Json)
assert alias.is_valid({"a": [1, "x", {"b": None}]})
assert alias.is_equivalent(
    recursive(lambda j: union(None, bool, int, float, str, [j], {str: j}))
)

Mutual recursion works the same way, since each alias binds its own fixpoint: type Branch = list[Leaf] beside type Leaf = int | Branch is two definitions naming each other. An alias that names itself outside a structural constructor — type Bad = int | Bad — is refused when the validator is built, for the reason the next section gives: it denotes no set a value settles.

The syntax is Python 3.12 and later. On 3.10 and 3.11, write the fixpoint with recursive.

Why classes need it

A class whose own type appears in a field is recursive in the same way, but a class definition has no place to tie the fixpoint. Compiling such a class directly is rejected with a message pointing here; model it with recursive instead:

from valgebra import recursive

# instead of a self-referential @dataclass Node, write the shape with recursive:
node = recursive(lambda n: {"value": int, "next?": n})
assert node.is_valid({"value": 1, "next": {"value": 2}})

Soundness guarantees

Recursion is bounded so it always terminates cleanly:

  • A value that contains itself is rejected with recursion_loop rather than looping forever (an object-identity guard).
  • A value nested past a fixed depth fails with recursion_limit rather than overflowing the native stack: 128 levels of unfolding, and 512 levels of descent in total, which is the bound a deep definition body reaches first (limits).
  • A non-contractive body — one whose recursive reference is not under a structural constructor — is rejected when the validator is built, not at validation time.
from valgebra import recursive, union

cyclic = []
cyclic.append(cyclic)
assert not recursive(lambda s: union(int, [s])).is_valid(cyclic)  # recursion_loop

Recursion in the decision procedure

Recursive schemas also take part in subtyping, equivalence, and emptiness. Equirecursive schemas compare at their greatest fixpoint — a coinductive comparison that assumes a goal already being proven on the current path — so a recursive schema is a subtype of itself and two structurally identical recursive schemas are equivalent, and a recursive schema with no base case is detected as uninhabited.

These are views of one definition, not separate definitions. Membership unfolds the definition against a finite value — a value is in the set when its finite unfolding matches. That is not a choice between fixpoints: values are finite, so each unfolding asks about strictly smaller values and the set is defined by that induction. Guardedness is what makes it well founded, which is why a non-contractive body is refused rather than resolved somehow. Inclusion uses the greatest fixpoint coinductively, which is the sound way to relate two such definitions without unfolding forever. On the finite values the two agree, so a subtype result never contradicts membership.

Emptiness asks the opposite question and takes the least fixpoint: a reference reached again while resolving it demands an infinite unfolding, and no finite value supplies one, so that occurrence is uninhabited. This is why a mandatory self-reference with no base case is empty — under the greatest fixpoint it would be inhabited by infinite trees, and valgebra validates finite Python values. Contractivity is what keeps the two consistent: over the finite values a guarded definition names one set, so what inclusion relates and what emptiness counts are the same set.

from valgebra import recursive, union, Validator

json_value = recursive(lambda j: union(None, bool, int, float, str, [j], {str: j}))
assert Validator(json_value).is_subtype_of(json_value)  # reflexive across the fixpoint
assert recursive(lambda t: {"value": int, "next": t}).is_empty()  # no base case
assert not recursive(
    lambda t: union(None, {"next": t})
).is_empty()  # a base case exists