Foundations

This page records the theory valgebra rests on: what a schema means, why the combinators form a real Boolean algebra, and where the algebra decides relationships versus where it stays deliberately conservative. It is the reference behind the claims the rest of the docs make — "a closed, lawful lattice", "subtyping is set inclusion", "sound but deliberately conservative" — so each is backed rather than asserted. The soundness argument takes the next step: why an accept is never wrong, node by node.

Schemas denote sets; validation is membership

A schema denotes a set of Python values. Validating a value is deciding whether it is a member of that set — nothing is copied or coerced. This is the denotational view: the meaning of a schema is its value-set [[s]], and every other relationship is defined from it.

• Subtyping is set inclusion. s is a subtype of t exactly when [[s]] ⊆ [[t]].
• Equivalence is mutual inclusion. s and t are equivalent when [[s]] = [[t]] — they accept the same values, whatever their syntax.

Because meaning is a set, the connectives are the set operations, and they obey the set-algebra laws by construction rather than by convention.

A Boolean algebra of schemas

union, intersection, and complement are set union, intersection, and complement; anything is the top (every value) and nothing is the bottom (no value). Schemas under these operations form a Boolean lattice: a bounded, distributive, complemented lattice. Every Boolean-algebra law therefore holds — commutativity, associativity, idempotence, absorption, identities, distributivity, De Morgan, and double negation — and valgebra property-tests each against the membership relation rather than asserting it (see the algebra guide).

The laws hold of the schema a caller builds, not of a pass over it afterwards: union, intersection and complement produce the lattice normal form, so union(int, int) is Validator(int), a member written twice in either order is one member, and a schema beside its own complement folds to a bound. Absorption is the law construction does not apply: A | (A & B) is A only when A contains A & B, and containment is the decision procedure rather than a shape -- so the two are equivalent sets and two terms. repr shows that form and == compares it. The deprecated simplify method folds nothing construction has not already folded; the algebra guide says what remains of it.

Semantic (set-theoretic) subtyping

Treating types as sets of values, with full union, intersection, and negation and subtyping as inclusion, is semantic subtyping, developed by Frisch, Castagna, and Benzaken. valgebra is a runtime membership checker built on that model rather than a static type system, but it inherits the model's payoff: the combinators are not ad-hoc primitives, they are the Boolean operations on value-sets, and a refinement like "an int that is not a bool" is intersection(int, complement(bool)) — a composition of generators rather than a construct of its own.

The same line of work models the structural forms valgebra uses:

• Sequences as regular-expression types. A list or tuple schema is a regular expression over element schemas — the regular-tree-type approach from XDuce and CDuce. One node expresses fixed tuples, variadic tuples, and prefix-plus-tail lists uniformly.
• Maps as keyed-default functions. A dict, record, or map is named fields plus key-schema-keyed default clauses — the set-theoretic model of records and maps as quasi-constant functions.

Any is the top, spelled

Any and anything are the same set — every Python value — and the same node. The algebra reads the top for both, and every law that holds of one holds of the other: complement(Any) denotes nothing, and intersection(Any, complement(Any)) is decided empty.

Gradual typing holds the dynamic type apart from the top, and does so for a question this library does not ask. A static checker asks consistency at every site where a value crosses between typed and untyped code, and for that question the dynamic type is an interval rather than a point. A validator asks one question — does this value belong — and to it Any answers yes for every value. Holding an atom apart for a question nobody asks costs a decision that disagrees with the walk, which has always admitted every value under Any.

What is left of the distinction is the spelling, and the schema keeps it: repr(Validator(Any)) is Any and repr(Validator(anything)) is anything. The spelling is not part of the set — two schemas differing only in it are equal — so nothing decides anything by it.

Two deciders, and the guard between them

A relation between two schemas is answered twice over, and the vocabulary the rest of these pages use is the two names.

The rules read the two schemas' shapes and apply inclusion rules to them: a list against a list compares elements, a record against a record compares fields. They are fast, they answer the shapes a caller writes, and where no rule matches a pair they say so rather than guessing.

The sets are the other reading. Each kind of value has a representation closed under union, intersection and complement — the integers as interval sets, the strings and bytes as automata, the lists and tuples as automata over letters that are themselves sets, the sets as a powerset lattice, the dicts as a lattice of map atoms — so inclusion becomes one question about emptiness: a is below b exactly when a and the complement of b share no value. That decides pairs no rule about shapes reaches, and it costs about two orders of magnitude more than a rule, which is why it is asked second and only where the rules decline.

Each kind's representation is bounded: a union of dicts, objects or sets holds at most a fixed number of atoms, and a build spends a fixed allowance reaching one. Past either the sets refuse, and the refusal is an answer of its own -- "not proven" rather than "not true". That is why the conservative list on the decidability page has entries about size beside the entries about shape: a relation the sets would decide can still be one they decline to build, and the same relation decides under a larger bound.

Both answer in three values: proved, refuted, or neither. A refutation is a claim about a value — some member of the subject that the other schema rejects — so it is believed only where the subject is known to hold one. That is the witness guard, and it is why a schema denoting nothing is reported below everything rather than refuted against it: a mismatch of shapes names no value when there is no value to name. relation_to reports the three answers apart; is_subtype_of folds the last two into False.

What the algebra decides, and the conservative frontier

Deciding whether two arbitrary set-theoretic types are equal — equivalently, whether a type is empty — is decidable in EXPTIME, and the bound is older than either citation below is usually read as saying. For a language of regular tree types, with no arrows and no type variables, it follows from containment of tree automata, which Seidl proved EXPTIME-complete in 1990; Hosoya, Vouillon & Pierce state it for their type language as Theorem 1 and import the result from him. That is the language valgebra's fragment sits closest to. Gesbert, Genevès & Layaïda establish 2^O(n) for a larger language — the Castagna & Xu relation, with function types and type variables — which is the bound no other proof existed for, and which covers the fragment here because a superset's upper bound bounds a sublanguage.

valgebra does not need that decision to validate: membership is answered directly by the walk, not by reducing the schema. So the library is honest about which fragment each part settles:

• Settled by construction. The lattice laws, and the complement laws (X ∩ ¬X = ⊥, X ∪ ¬X = ⊤) for any X that is a set. So intersection(int, complement(int)) is nothing — one schema, which repr prints and == compares, and which no later call is needed to reach. A predicate and a class with an isinstance hook are the exceptions, because they answer by running code and the law is about sets.
• Decided rather than folded. A meet of two disjoint kinds keeps its spelling: intersection(int, str) reprs as itself, and intersection(int, str).is_empty() is True. Emptiness is a question about the set, and answering it is not the same as rewriting the term that names it.
• Decided by the comparison operators. is_subtype_of, is_equivalent, and is_empty decide a wider fragment than construction folds — class and literal inclusion, refinements (including the emptiness of contradictory bounds like Ge(10) & Le(0)), sequences, sets, records and mappings, and recursion at its greatest fixpoint. The decidability boundary lists exactly what is decided and what stays conservative.
• Conservative. A predicate refinement is opaque, and a narrow decidable tail and the runtime-undecidable constructs remain (the boundary records them). Every answer is sound: is_empty never reports a non-empty schema as empty, and a subtype is never claimed unless it provably holds.

The relation is defined by the set-theoretic emptiness test (s <: t iff [[s ∧ ¬t]] is empty), and it is decided two ways. Structural rules recurse over the schema tree, exact on the published fragment and conservative beyond it. Where they decline, a descriptor is built: each kind held as a set closed under union, intersection and complement, so the emptiness test is asked literally rather than approximated by a rule about the shape. It decides what a rule about shapes cannot — a container meet, a complement nested inside another, one regular language inside another, the ordering of two steps — and it is bounded, because building one costs about two orders of magnitude more than a rule that already answered. What is past those bounds, and what no finite descriptor holds, is what the boundary records as conservative.

Neither ever changes a membership decision: the walk answers membership directly, and both representations are sound.

References

The essential reading, in the order it maps onto valgebra:

1. Frisch, Castagna & Benzaken — "Semantic Subtyping: Dealing Set-Theoretically with Function, Union, Intersection, and Negation Types", JACM 55(4), 2008. doi:10.1145/1391289.1391293. The foundation: types as sets, subtyping as inclusion, full Boolean connectives.
2. Gesbert, Genevès & Layaïda — "A Logical Approach to Deciding Semantic Subtyping", TOPLAS 38(1), 2015. The decision procedure, and a 2^O(n) upper bound for set-theoretic types with arrows and type variables — a language larger than this one, which is why the bound transfers rather than being about the fragment here. Cited for why the full emptiness decision is deferred.
3. Hosoya, Vouillon & Pierce — "Regular Expression Types for XML", TOPLAS 27(1), 2005. Regular-tree types — the model behind sequences as one regex node. Their Theorem 1 states EXPTIME-completeness for that type language and takes the result from Seidl's 1990 proof for tree-automata containment, which is where it belongs.
4. Castagna — "Typing Records, Maps, and Structs", ICFP 2023. doi:10.1145/3607838. Records and maps as keyed-default functions.
5. Castagna, Lanvin, Petrucciani & Siek — "Gradual Typing: A New Perspective", PACMPL 3(POPL), 2019. The gradual dynamic type under set-theoretic connectives, held apart from the top and given a materialization relation of its own. Cited because valgebra declines it: what separates the dynamic type from the top is the consistency question, and a validator has no site for one, so Any here is the top (above).

A current synthesis is Castagna, "Programming with Union, Intersection, and Negation Types", 2024 (arXiv:2111.03354).