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.
Douglas Joseph Huntington Moore (Thu,) studied this question.