Bibliography

The sources behind the model: the arithmetic, the parametricity that constrains generic code, the recursion and abstraction rules, and the definability discipline that says a count is only meaningful once a language, a scope and an equivalence are fixed. How far each source was verified — inspected, bibliography-verified, metadata-verified — is recorded per claim in the evidence register.

Counting and inhabitation

• Alex Knvl, Counting type inhabitants (24 November 2018) — the arithmetic this calculator implements: sums, products, exponentials, quantification, recursion and the infinite tiers. (archived, live mirror)
• Gabriel Scherer & Didier Rémy, Which simple types have a unique inhabitant? (ICFP 2015) — uniqueness of inhabitation modulo βη equivalence with sums: the method side's "how many implementations" question, decided.
• Gabriel Scherer, Deciding equivalence with sums and the empty type (POPL 2017) — βη equivalence with sums and Nothing is decidable and coincides with contextual equivalence.
• Paweł Urzyczyn, Inhabitation in typed lambda-calculi (a syntactic approach) (TLCA 1997) — inhabitation is undecidable for the second-order λ-calculus: why a polymorphic count above one needs an exact reduction, never a guess.
• José Espírito Santo, Ralph Matthes & Luís Pinto, Coinductive proof search for polarized logic (TYPES 2020) — proof search shaped by polarity; the search the solver approximates.
• Jonas Duregård, Patrik Jansson & Meng Wang, Feat: functional enumeration of algebraic types (Haskell Symposium 2012) — enumerating the inhabitants a count reports.
• Chris Taylor, The Algebra of Algebraic Data Types (2013, blog series) — the sum/product/exponential reading for a general audience.

Parametricity

• John C. Reynolds, Types, abstraction and parametric polymorphism, Information Processing 83 (IFIP), North-Holland, pp. 513–523 — where the uniformity of generic code was first stated.
• John C. Reynolds, Polymorphism is not set-theoretic (Semantics of Data Types, LNCS 173, 1984) — why a polymorphic type cannot be read as a set intersection.
• Andrew M. Pitts, Polymorphism is set theoretic, constructively (TACS 1991, LNCS 526) — the constructive reading that restores it.
• Philip Wadler, Theorems for free! (FPCA 1989) — the free theorems behind ∀a. (a, a) => a counting 2.
• Robert Atkey, Relational Parametricity for Higher Kinds (CSL 2012) — parametricity at the kinds the higher-kinded rules refuse to guess.
• Dimitrios Vytiniotis & Stephanie Weirich, Parametricity, Type Equality and Higher-order Polymorphism (JFP 20(2), 2010) — why type equality is inhabited only by the identity.
• Paolo Pistone & Luca Tranchini, The Yoneda reduction of polymorphic types (CSL 2021) — Yoneda isomorphisms as a type-level rewriting that eliminates quantifiers.
• Bartosz Milewski, Parametricity: Money for Nothing and Theorems for Free (2014, blog) — the accessible exposition.

Recursion, types and abstraction

• M. B. Smyth & G. D. Plotkin, The Category-Theoretic Solution of Recursive Domain Equations (SIAM J. Comput. 11(4), 1982) — recursive equations solved as least and greatest fixed points; the μ/ν distinction the recursion rules follow.
• John C. Mitchell & Gordon D. Plotkin, Abstract types have existential type (TOPLAS 10(3), 1988) — an abstract type as a packed existential: the record reading of a capability.
• Luca Cardelli & Xavier Leroy, Abstract types and the dot notation (DEC SRC Research Report 56, 1990) — path-dependent types read as existential opening.
• William R. Cook, On understanding data abstraction, revisited (OOPSLA/Onward! 2009) — abstract data types and objects as two distinct forms of data abstraction.
• William R. Cook & Jens Palsberg, A Denotational Semantics of Inheritance and its Correctness (DAIMI PB 284, 1989; Information and Computation, 1994) — self-reference as a fixed point: why an overridable member stays open.

Definability and foundations

• Bertrand Russell, On Some Difficulties in the Theory of Transfinite Numbers and Order Types (1907, Proceedings of the London Mathematical Society s2-4, 29–53) — a foundational reference for the counting model: which collections a definition may legitimately form, the discipline the counting contract applies when it fixes a scope, a language and an equivalence. The citation inventory records what was read and what remains an access gap.
• Luna & Taylor, Cantor's Proof in the Full Definable Universe (Australasian Journal of Logic 9, 2010) — Cantor's argument restricted to the definable universe; the way out is that definitional contexts restrict the scope of quantifiers.
• Fan, Hobson's Conception of Definable Numbers (History and Philosophy of Logic 41(2), 2020) — language-relative definability in the Hobson–Richard tradition.
• Russell's paradox, Stanford Encyclopedia of Philosophy — the secondary account used where the 1907 full text is paywalled.

Scala

• Martin Odersky et al., Simplicitly: foundations and applications of implicit function types (PACMPL 2, POPL 2018) — the contextual argument rules the model reads.
• Lionel Parreaux, Aleksander Boruch-Gruszecki & Paolo G. Giarrusso, Towards improved GADT reasoning in Scala (Scala 2019) — GADT constraints as equations over type variables.
• Fen Hu & Ondřej Lhoták, Undecidability of D<: and its decidable fragments (POPL 2020) — the subtyping the resolver walks, and where it becomes undecidable.
• David Blanvillain, Philipp Brachthäuser, Martin Kjaer & Martin Odersky, Type-Level Programming with Match Types (POPL 2022) — match types, which the model keeps stuck until instantiation.
• Scala Improvement Process SIP-58, named tuples (2024) — the product reading of named tuples.

Practice

• Yaron Minsky, Effective ML (Jane Street) — the origin of "make illegal states unrepresentable".
• Alexis King, Parse, don't validate (2019) — narrowing at the boundary as a design discipline.
• The Hidden Powers of Total Program Cardinality and part 2 — the wider programme the calculator serves.
• The type system is saving your code — the original blog post.
• Keep your types small — the Scala Love talk.

Repository evidence

• Evidence register — one entry per decision, with its sources and how far each was verified.
• Russell citation inventory — 376 database-reported citing works, with per-record verification levels.
• v1 plan — the counting contract, the eo baseline and the remaining work.
• Research notes — the per-rule notes behind the pages above.
• Baselines — recorded report runs with their inputs and limits.
• Otmar Ertl, New cardinality estimation algorithms for HyperLogLog sketches (2017) — the measurement direction the plan holds as future exploration.
• Quality gates — the formatter, linter, coverage, mutation and duplicate checks the build runs, the same toolchain eo uses.