Dispositional Typing: Eliminating Unsafe Annotations through First-Class Role Algebra

Dispositional Typing: Eliminating Unsafe Annotations through First-Class Role Algebra The paper asks whether First-Classness — the design principle that has guided fifty years of programming-language evolution, from Strachey's 1967 distinction between first- and second-class values through to Rust's ownership model — can be stated as a formal constraint rather than left as an informal heuristic. Applied to the holder/held asymmetry implicit in lvalue/rvalue structure, the First-Classness constraint induces a four-element role algebra ε, i, j, η: the four ways in which the two complementary poles (holder = F, the "toHave" disposition; held = M, the "toBe" disposition) can combine across a directed data-flow edge. The algebra is shown to be the unique minimal closed system that refines the lvalue/rvalue distinction while privileging no pole over its complement, and its composition table is fixed by the balance law j − ε + i = η. This algebra serves as the semantic basis for a static memory-safety analysis at the level of a compiler's Static Single Assignment (SSA) form. Each data-flow edge receives a dispositional tag, and memory safety reduces to a single global criterion: every closed walk in a region must be admissible, composing either to the identity η or to a residual whose spatial, lifetime, or contract boundary is certified by an explicit projector. The analysis requires no programmer annotations and adds under 2% to compilation time. The contribution is fivefold: (i) a derivation of the role algebra from the First-Classness axiom, with proofs of minimality and closure; (ii) an SSA-level backward inference pass using linear-time propagation, Tarjan SCC discovery, and a bounded-label saturation procedure for closed walks, requiring no new IR nodes; (iii) a soundness theorem with a full abstract-interpretation proof; (iv) initial results from a Clang plug-in on a 35-function C corpus, where 67% of safe patterns and 55% of unsafe patterns receive correct definitive verdicts, with no incorrect definitive verdict observed; and (v) a reframing — drawing on a companion result for the universal genetic code — in which the same algebra partitions a domain into 21 families with a structural residue, so that the unsafe verdict is treated as a certified structural residue of First-Classness closure rather than as a separately stipulated warning category. The paper is written as a programming-languages contribution: the emphasis falls on the algebraic formulation, its relation to existing semantic structure (abstract interpretation, separation logic, substructural type systems), and its use in compiler analysis.