α ⊣ γ
Forget, soundly.
An abstraction retains enough information to answer a question. A genuine adjunction specifies the best approximation expressible in that abstraction.
01 / The organizing idea
One universe.
Several different jobs.
The closest precedent is Patrick Cousot’s Types as Abstract Interpretations: derive type information from the semantics of an untyped language. Scott’s universal domains and PER models supply two other pieces.
The strong version of the idea is general semantics + partial evidence procedures + certified abstractions + certified transformations. These parts can cooperate without all being the same construction.
n² = n
Choose representatives.
A normalizer can select a canonical part of a universal space. Idempotence gives a retraction; an order adjunction needs more structure.
p ≃ p′
Change the execution.
An optimization preserves the observations you care about. Whether it is faster is a separate claim, with a separate cost model.
The three closest foundations: Cousot on types as abstractions · Scott on retracts of a universal domain · PERs and realizability. The unifying architecture is a synthesis of these ideas, not an established theorem equating every type system.
02 / Experiment one
How much can
you afford to forget?
A concrete set says exactly which values are possible. An abstract domain stores a description. Soundness means the description includes every real possibility; it can also admit possibilities that were never there.
The abstraction workbenchFinite universe U = {0, …, 11}
Remember
Click values to change the concrete set X.
In XAdmitted by abstraction onlyExcluded
3extra values
Precision lost when the abstract description is interpreted back in U.
α(X) ≤ a ⇔ X ⊆ γ(a)
The adjunction: α chooses the best expressible approximation.
Soundness gives inclusion. Exact recovery is a stronger condition.
Exact setsAll distinctions available
Reduced product → interval / parityCombining two views can recover precision. Interval and parity alone are incomparable.
The lattice here orders abstractions. Fix the concrete lattice C. Each abstraction induces an upper closure ρ = γα. Order these closures pointwise: smaller outputs mean more precision. Their lattice combines or forgets distinctions; it does not rank execution speed.
Abstract interpretation establishes the sound approximation framework. Upper closure operators organize abstract domains. In this finite example, intersecting interval and parity concretizations computes their reduced product.
03 / Experiment two
A type can say
what counts as equal.
A partial equivalence relation (PER) stores two things: which values belong, and which members are identified. Symmetry and transitivity make self-relatedness into membership. That is a close match to the proposed stream spaces.
All 15 PERs on U = {0, 1, 2}Upward = more related pairs
Click a node to set
A block such as 01 identifies 0 and 1. A bar separates classes; an omitted value is not a member. Edges are immediate inclusions.
A
B
A ∨ B
Rows and columns are 0, 1, 2. Filled cells are related pairs. Orange outlines mark pairs closure added beyond the union.
A genuine adjoint triple
Δ ⊣ support ⊣ ∇
Choose S. R is the current result above. ΔS relates each member only to itself; ∇S relates every pair of members.
S =
Each pair of inclusion tests always agrees. That equivalence—not speed—is what makes these adjunctions.
Meet = intersection
Keep only pairs shared by both relations. Symmetry and transitivity survive intersection.
Join = closure of union
If one relation identifies 0 with 1, and another identifies 1 with 2, their join must identify 0 with 2 as well.
Top ≠ discrete equality
At the top, all three values belong and are equal. The relation 0 | 1 | 2 has the same members, with all distinctions intact.
The lattice and Δ ⊣ support ⊣ ∇ are direct derivations from the PER definition. PERs and their maps provide the established semantic setting. The five nodes with full support already form the nondistributive partition lattice M₃: this is not a Boolean lattice of predicates.
04 / The research atlas
Forty families.
More than one axis.
Choose a family to inspect what it knows, how it connects to stream types, and where the analogy stops. Lines connect nearby ideas and techniques; they do not claim subtyping, relative strength, or an adjunction.
Some systems span several neighborhoods. Ownership combines resources, state, and logical relations; privacy combines quantitative bounds with relational reasoning; dependent types retain proofs and transport that a plain membership predicate erases. Search filters the map, including descriptions; selecting a connection clears the filter.
05 / Experiment three
Adjoints are about
universal properties.
A function changes the context of a predicate. Moving a predicate forward can mean “some element in this fiber” or “every element in this fiber.” These two quantifiers are the actual adjoints to pulling a predicate back.
Quantifiers as change of context∃f ⊣ f* ⊣ ∀f
Choose P ⊆ X
Toggle a, b, c, d. The function f maps each column to the target below it. The last fiber is empty.
∅
Toggle u, v, w to choose Q ⊆ Y. Purple means “in Q.”
The three ways to move
∃fPAt least one chosen point in the fiber
f*QEvery point whose target belongs to Q
∀fPEvery point in the fiber belongs to P
Watch w. No point maps to it. Existential quantification excludes it; universal quantification includes it vacuously. No enumeration needs to discover a member of that empty fiber.
For dependent types, retain the family structure. In suitable categories of families, this becomes Σf ⊣ f* ⊣ Πf. A telescope composes contexts. Its fibers must respect equality and substitution; when values change context, transport may be required.
Lawvere’s quantifiers-as-adjoints construction is the foundation. The finite predicate experiment displays the poset version; it does not model all the proof data of dependent type theory.
06 / Experiment four
A search strategy
is not a truth oracle.
To check a universal claim, give each input a task. Some return evidence, some loop. Fair scheduling can stop one task from starving the rest. It cannot make an unfinished universal claim true or false.
The evidence schedulerToy dispatches · deterministic
Current evidence
Open
Open
↗ Proved↘ Refuted
More evidence moves upward. Proved and Refuted have no common upper answer in this three-point order.Try three contrasts. A serial search gets stuck on T1 in the first scenario; a fair search reaches T2’s counterexample. Finite success proves the universal claim only with coverage. Passing every test seen so far in an open-ended stream still leaves the claim Open.
The three-valued evidence discipline is related to runtime verification. Fair search deals with starvation; semidecision and observation explain why lack of evidence does not generally decide the other answer. Changing a control resets the experiment.
07 / Experiment five
Same result.
Different journey.
Type information can justify an optimization. A correctness proof establishes equivalent observations. A cost argument establishes an improvement. Neither says that the two executions must take the same internal steps.
Equality and cost are separate claimsA mathematical example
Accumulate from zero
0 + 1 + 2 + ⋯ + n
observable result
Use the closed form
n × (n + 1) ÷ 2
observable result
3 arithmetic operations
Cost model: each addition, multiplication, and division costs one unit. Loop control is omitted, arithmetic is exact, and there is no constant folding. These are mathematical operation counts, not measured disp timings. Bit complexity and machine overflow require different contracts.
Why the equality holds beyond the slider
For n = 0, both sides are zero. If the first n integers sum to n(n + 1)/2, adding n + 1 gives (n + 1)(n + 2)/2. Induction proves the formula for every natural n.
The proof certifies the result, while the separate operation counts compare these particular evaluation strategies. Trying thirty-one slider positions would not prove the general identity.
Verified compilation commonly uses simulations that allow different internal steps. Equality saturation stores known equal expressions and extracts according to a cost model. Proof-carrying code separates expensive proof construction from checking a supplied certificate.
08 / What survives the unification
There is no single
“more typed” direction.
The objects and the order determine the lattice. A relation can identify more values, an analysis can distinguish fewer behaviors, and an implementation can use fewer steps. These are different comparisons.
| What is ordered | What “up” means | The structure you get |
|---|---|---|
| Predicates on U | Admit more members | Powerset Boolean lattice, classically. Smaller sets are stronger predicates. |
| PERs on U | Add related pairs | Complete, generally nondistributive lattice. Membership and equality both move. |
| Partitions of a fixed S | Identify more members | Partition lattice. The carrier stays fixed. |
| Abstract domains over C | Lose precision | Complete lattice of upper closures, ordered pointwise. |
| Predicates in contexts | Entailment in each context | Indexed logical orders; quantifiers connect contexts. |
| Proof-bearing types | No single scalar order | Categories, possibly higher categories. Maps and proof identities matter. |
| Checker answers | Acquire decisive evidence | Open below Proved and Refuted. A poset, not a lattice as given. |
| Implementations | A chosen cost comparison | Usually a preorder or a Pareto order. No general lattice guarantee. |
One encoding is not one semantics.
Trees can encode heaps, traces, proofs, and distributions. Ownership still needs state and resources; probability needs weights; hyperproperties compare multiple runs. A returned-value relation alone forgets those distinctions.
Arrow types hit a computability boundary.
Totality over naturals has the shape ∀x ∃t: execution returns a valid answer within t steps. General membership is Π⁰₂, beyond positive semidecision. Resuming every task does not make every semantic function type enumerable.
Infinite does not always mean unsearchable.
Some compact higher-type spaces support exhaustive checking under totality and continuity assumptions. That is a property of the represented space and predicate—not permission to declare an unfinished enumeration complete.
Proofs carry more than a Boolean.
Dependent families need coherent substitution and transport. Higher identity types retain paths between proofs. Truncation deliberately forgets that structure; an ordinary equality checker does not reconstruct it.
A normalizer needs a contract.
Idempotence gives a retraction. A quotient must also respect the base equality and choose valid representatives. A left order adjoint additionally needs monotonicity and an extensive closure property in the chosen order.
A certificate needs a validator.
A finite list does not certify its own coverage. A proof search strategy does not establish its own soundness. Even a finite set of transition schemas needs a theorem covering every permitted instantiation.
A coherent architecture for the stream types idea
Meaning
Choose the values, state, observations, and relation laws.
Claims
State membership, equality, coverage, invariants, and bounds.
Evidence
Search fairly or supply a certificate. Validate what it proves.
Strategies
Exploit certified facts. Compare costs separately.
Types can be reusable knowledge that makes general computation cheaper. Adjunctions explain some of the ways that knowledge is organized—not every way it is used.
These boundaries combine searchable-space results, higher identity and truncation, and the logical and semantic distinctions in the atlas. Recommendations here are design analysis; they do not imply these features are implemented in disp.
Reading room
Follow the original ideas.
Primary sources from the companion research note, with PDF page or section links where available. The ontology’s connections are comparative judgments; each paper establishes its own results under its own assumptions. The recent effects paper is a June 2026 draft, not a universal theorem about effect systems.
Open the annotated source index
For derivations, additional caveats, and specific corrections to the stream plan, read the full research note. All experiments run locally. No network, account, or build step is required; following a paper link opens its external source.