v1 plan: trustworthy cardinality reports, driven by eo

Status: active, consolidated implementation plan. Code baseline: 2a5bf523dd8545197f3123ed6b2532a04503f936.

This document consolidates the decisions from the eo reporting work, the reference discussions, and PR #10. It is the roadmap to maintain as that work proceeds. Older README and PR report snapshots are historical, not competing definitions of the current baseline. The milestones below do not claim that their remaining work is already implemented.

1. Outcome

Generate a useful, reproducible report for eo's core library, published as dev.constructive:cats-eo_3:0.16.0, then use its actual signatures to improve the general calculator.

The objective is correct numbers for each case, not a higher percentage of rows carrying a number. An unsupported case must remain explicitly unresolved rather than receive a convenient finite answer or a guessed infinity.

The working loop is:

1. Select an eo signature and recover everything it can access or capture.
2. Derive its expected count independently of the analyzer.
3. Add a regression containing the relevant source and scope.
4. Implement the general rule, not an exception for that signature.
5. Regenerate the report and explain every changed result.

2. Agreed counting contract

Two different questions

• Implementation cardinality: how many observationally distinct, pure, total, parametric implementations a signature admits in its accessible environment.
• Stored-value cardinality: how many values an instantiated data type holds. The existing constructor-input estimates are a separate, approximate view of this question.

For a generic construction signature taking x: A and y: A, returning A has two choices; constructing a fixed two-field Pair[A] has four: (x, x), (x, y), (y, x), (y, y). That is the intended generic constructor/apply count, not the stored-value cardinality of every instantiation. Pair[Int] has |Int|² = 2^64 under the fixed-width integer model.

Two available choices need not have different runtime values on every call. The implementations are distinguishable across admissible inputs. Conversely, two aliases of the same binding do not create another choice.

Scope and equivalence

• Include parameters, receiver fields, enclosing captures, accessible declarations, projections, and callable producers. Do not substitute a bindings-only count for this environment.
• Keep type binders distinct even when they share a spelling or can later be instantiated to the same concrete type. Keep term names separate from type names.
• Count modulo the supported observational equivalences: renaming, beta/eta normalization, and redundant elimination must not manufacture inhabitants.
• A supplied step: A => A and x: A admit x, step(x), step(step(x)), and so on: ω. Without a starting inhabitant, that cycle supplies no A: 0.
• A known identity is not an unconstrained producer. Repeated calls to it do not establish ω. Skipping a concrete member requires a justification that its results are already represented; parametricity is not a blanket justification for discarding unreadable captures or capabilities.
• Another abstract member can be a supplied capability. The declaration currently being measured is not its own supplied implementation, including through an inherited/overridden view.
• A numeric answer requires a complete analysis of the relevant environment. If an omitted capability might change the result, report ?, unless irrelevance is established.

Assumptions and output meanings

The model excludes divergence, effects, mutation-dependent behavior, exceptions, null, unsafe casts, reflection, and unrestricted runtime type/equality tests. It does not certify that an existing Scala body obeys these assumptions.

Functor, optic, or other algebraic laws are additional constraints, not implicit consequences of a signature.

• Finite(n): exact within the stated model, including 0.
• Countable / ω: a justified countably infinite family in that model.
• Unresolved / ?: unsupported syntax, incomplete scope/type analysis, or an exhausted analysis budget. Neither ω nor ε₀ is an unknown-value fallback.

A 0 is a scope-relative result under these assumptions, not a claim that an unsafe Scala body cannot be written. Stored-value estimates must not inherit the method counter's exactness claims.

3. References and their limits

• Bartosz Milewski, Parametricity: Money for Nothing and Theorems for Free: why uniform generic implementations are constrained by what they receive and capture.
• Alex Knvl, Counting type inhabitants: observational equivalence, sums/products/exponentials, quantification, empty types, and countable families.
• Bertrand Russell, On Some Difficulties in the Theory of Transfinite Numbers and Order Types (PLMS s2-4, pp. 29–53, 1907, DOI): which collections a definition may legitimately form, and cardinality versus order type. Its citation line of descent is inventoried in russell-citation-inventory (376 database-reported citing works, with per-record verification levels).
• Repository reference notes and executable examples.
• The evidence register: for each decision in the counting contract, the sources that justify it, how far each was verified, and the boundary past which it must not be stretched.

The 27 reference examples are evidence for the supported algebra, not a proof that the Scala frontend extracts every environment correctly. Ordinary |B|^|A| is not a substitute for analyzing universally quantified signatures. Higher-kinded/Yoneda arguments need their stated assumptions; they do not provide an automatic solution for arbitrary eo evidence.

Keep mathematical models distinct from runtime representations: a mathematical powerset is not automatically Scala's finite Set, and an idealized terminal top type is not unrestricted Scala Any. Audit the reference notes where they currently overstate frontend support or the safety of ignoring concrete members.

4. Starting point

The following infrastructure exists; its presence does not make the complete frontend sound:

• Source indexing and type resolution: two passes, declaration/binder identities, source aliases, restricted products, and enum cases.
• Environment measurement: captures, alias provenance, and initial support for inherited declarations.
• Inhabitation solver: free atoms, products, finite sums, arrow introduction, first-order producers, productivity and live-cycle analysis, exact BigInt arithmetic with explicit resource limits.
• Frontend regressions: selectors, constructors, productive/unproductive cycles, shadowing, aliases, declared slots, simple inheritance, and several unsupported-representation guards.
• Reporting and the sbt plugin: project sources or explicit files/directories/source jars; separate implementation and stored-value sections; report artifacts; report-then-fail for unreadable/unparsable inputs.
• Scripted tests cover a project report and a fixture source jar. The last recorded full core suite contained 187 passing examples; this documentation change does not constitute a rerun.

The original plugin walking skeleton, basic per-definition reporting, readable sizes, artifact writing, and report-then-fail work are already present. The remaining effort is primarily counting correctness, expressiveness, and reproducible real-library validation.

5. eo baseline

Input: cats-eo 0.16.0 sources. The source archive's SHA-256 is:

61907fc2f4e1c0892fa8723c7a014af942b825b64a916a9b53dd64b3f12dbfe3

The last reported run at the code baseline above was:

The full report is retained at baselines/eo-core-0.16.0.txt, with the analyzer revision, the input's SHA-256, the Scala/tool versions, the command and the analysis limits in its header, so a later run can be diffed against it from the repository alone. It is still provisional analyzer output, not 17 independently validated answers: the rows carry row identity but no review ledger yet, and the retention is the first half of this milestone rather than treating the table as a golden correctness oracle.

The unresolved backlog includes type resolution, abstract/member-bearing representations, higher-kinded parameters, qualified environments, unsupported type syntax, mutable captures, inferred results, higher-order application, and sum-producing callables. Reasons overlap: do not add their bucket totals or assume that every "unresolved type" is a missing primitive.

Earlier 41 finite / 3 countable / 436 unresolved and 10 / 3 / 467 snapshots are superseded. A drop in resolved rows can be a correctness improvement when previously omitted scope is found.

6. Milestones, in order

V1.1 — Establish a reproducible, reviewable baseline

Status: started. The report a run produces is retained (see the baseline); row identity and a review ledger are still to come.

• Retain the full eo report with the analyzer revision, input coordinate/checksum, Scala/tool versions, command, and analysis limits. Use a repository-relative artifact location, not a developer-specific cache path.
• Establish stable row identity from source, owner, declaration kind, and signature, including overloads. Keep a small review ledger separating emitted counts from independently validated counts and unresolved obligations.
• Reconcile historical README/reference claims with the counting contract above.

Acceptance: another checkout can reproduce the inventory and report from the pinned source archive; input-order changes do not change results; every baseline row has a review status. Report generation and correctness validation remain distinct.

V1.2 — Close scope and identity gaps before extending the algebra

Status: partial implementation; soundness work remains.

Extend the existing regressions with focused source-to-count cases for:

• Declaration identity across files and overloads. The current self-exclusion check compares source offsets; equal offsets in different files must not identify the same declaration.
• Multi-level and diamond inheritance, composed type substitutions, qualified parent names, overrides, and private/protected visibility. Do not silently ignore an unresolved relevant parent or resolve an ambiguous parent by taking the first match.
• Method-owned type binders in declared polymorphic capabilities, method-body versus signature scopes, term/type namespace collisions, and shadowed-but-qualified receiver fields.
• Imports/exports, including wildcards and renames; companions and nested modules sharing class binders; relevant receiver capabilities outside the immediate lexical chain.
• Value aliases, destructuring, and concrete method bodies. Prove normalization or irrelevance; otherwise preserve an unresolved obligation instead of treating a skipped body as complete.
• Separate permission to construct a nominal value from permission to project its members. Constructor visibility, extra parameter lists, enum case constraints, and abstract members must not become fictitious public products.

Acceptance: each omission either has a supported rule with positive and adversarial regression tests or remains ?. Re-audit all 15 finite and both ω baseline outputs, especially the six zeros and declarations that might delegate to themselves. Do not assume those counts survive.

V1.3 — Build the eo case ledger and executable corpus

Status: the definition half is well under way; the method cases below still need their derivations. baselines/eo-core-0.16.0-unresolved.md catalogues every definition row that carries no number: what moved it as the estimate learned to substitute arguments, to read the source set as one scope, to reduce match types, to classify an open abstraction and to model the lattice's ends — and the six gaps that remain (type lambdas, an inert match type over a free parameter, a refinement, a path-dependent member type, a name outside the sources, and opaque representations, which are ? by contract).

Start with the following archive-relative locations under dev/constructive/eo/. These are working cases, not assertions that the current full-library report already produces their counts.

Keep the synthetic fixed-product Pair regression. PSVec.of(b0, b1) is not a substitute: its result can have varying length, so two inputs do not imply four implementations.

For each case, record the original signature/location, relevant scope, assumptions, a derivation, expected count or specific unresolved obligation, test link, and report delta. Compile reduced Scala fixtures when accessibility or binding behavior is part of the argument; parser acceptance alone does not establish that a reproduction is valid Scala.

Acceptance: each promoted eo answer has an independent derivation and a source-to-report regression, not just a shape-level test or a copied analyzer output.

V1.4 — Extend the supported fragment from those cases

Status: incremental work, selected by case evidence rather than bucket size.

Implemented fragment since this plan's initial baseline: definition-scope opaque representations. Six independently derived Direct rows in the eo checkout moved from unresolved to Finite(1). Exported aliases do not widen visibility; inherited substitution failures remain diagnostics. The harder opaque/higher-kinded/evidence cases below are still open.

1. Capabilities and branching: receiver/given member access, callable sum-result elimination, and then supported higher-order application. Preserve branch-local captures, totality, and observational equivalence.
2. Finite ground types: add compact, exact or explicitly symbolic reasoning for fixed-width types. Do not enumerate 2^32 values or reuse rounded legacy Size bounds as exact method counts. State the primitive operations/equivalences the model permits.
3. Closed algebraic representations: validate enum restrictions and extend to genuinely closed sealed sums. An arbitrary trait with methods is not a sum of all visible subclasses. Recursive data needs a structural/productivity argument.
4. eo's harder types: higher-kinded and bounded parameters, typeclass evidence, associated and path-dependent types, refinements, match types, type lambdas, and scope-sensitive opaque representations. Add one justified fragment at a time; unsupported interactions stay ?.
5. Inferred signatures: decide what typed evidence is needed instead of inventing return types from source text. Any compiler-assisted mode requires an explicit design decision.

Acceptance for each extension: literature or a written derivation, solver tests where applicable, frontend regressions, an eo case that motivates it, and documented limits. Resource limits report unresolved work; they never silently approximate an exact answer.

V1.5 — Make the report a dependable user workflow

Status: basic tasks exist; reproducibility and broader integration remain.

• Keep implementation counts and stored-value estimates visibly separate. Include scope/model assumptions, unresolved reasons, and unambiguous source locations.
• Preserve reports and per-signature deltas as reviewable artifacts. Explain inventory changes when better discovery finds additional declarations; do not freeze the number 480 forever.
• Exercise actual plugin use with the pinned eo sources, in addition to small fixtures. Extend scripted coverage for multiple subprojects, same-named files, custom report paths, repeated runs after source changes, and report-then-fail behavior.
• Update user documentation from the retained report, not hand-edited totals.

Acceptance: the documented command reproduces a complete, attributable report, errors cannot masquerade as an analysis of all inputs, and every newly claimed number is traceable to reviewed case evidence.

7. Verification for implementation changes

Use the existing gates, without treating them as substitutes for the eo derivations:

sbt 'core/testFull'
sbt 'scalafmtCheckAll' 'scalafmtSbtCheck' 'scalafixAll --check'
sbt 'plugin/scripted'
sbt coverageAll

Confirm that tests actually execute: sbt 2 task-cache hits and testQuick output are not a new full test run. The core statement coverage floor is 80%; keep it at least there and improve tests around surviving mutations. CPD and configured CodeScene checks remain code quality gates; mutation testing remains report-only and guides test investment.

For refactors, compare complete before/after eo output as well as tests. For behavioral changes, review each changed row rather than demanding a byte-identical report. Keep source-order, alpha-renaming, alias-provenance, productive/blocked-cycle, empty-type, and resource-limit regressions in the corpus.

When a review questions a number, answer from the evidence register, not from memory.

The existing plugin workflow, in a build with this plugin installed, is:

show cardinalityReportFile
cardinalityReportOf /absolute/path/to/cats-eo_3-0.16.0-sources.jar

The default artifact is relative to sbt's actual target setting; do not assume that sbt 2 uses the flat path target/cardinality/report.txt. Obtaining the pinned jar is separate from analysis.

8. Boundaries and decisions still open

Agreed boundaries

• Analyze explicitly supplied Scala files, directories, and source archives. No automatic dependency resolution, fetching, or execution of the analyzed library.
• Keep calculation and reporting logic in the core library, independent of sbt; the plugin is only the integration layer.
• Do not assume optic/functor laws or support for unsafe/effectful Scala to make eo rows resolve.

Decisions to make when needed

• A maximum package-search distance upward/laterally was proposed, not selected or implemented. First define Scala accessibility within the supplied source set. If a configurable search bound is added, record it in the report and surface any relevant truncation.
• Whether explicitly supplied compiler metadata is needed for inferred/dependent signatures. Do not silently turn source reporting into compilation or dependency resolution.
• How to present very large exact counts symbolically, separately from rounded estimates.
• Any future lawful-implementation count must be an explicitly named, separately justified mode.

9. Completion and immediate next step

The v1 reporting workflow is ready when the supported fragment is documented and tested, the eo run is reproducible, numeric rows have independent full-scope justification, and unresolved rows have specific tracked obligations. A deliberately unsupported fragment needs an explicit scope decision, not a fabricated number.

That does not mean the longer-term goal of getting every eo case right is finished while cases remain unresolved. Keep them on the ledger and continue the same derivation/test/report loop.

Next implementation pass: retain the V1.1 baseline, add the V1.2 declaration-identity and inheritance regressions, then revalidate the currently numeric eo rows before expanding support.

10. Future exploration: HyperLogLog measurement

Status: deferred exploration, outside v1's correctness engine and completion criteria.

Reference: Otmar Ertl, New cardinality estimation algorithms for HyperLogLog sketches (2017), paper. It develops corrected and maximum-likelihood estimators, including joint estimation of intersections, relative complements, and unions from two sketches.

Potential uses:

• Bounded implementation enumeration: estimate the distinct canonical constructions generated within a declared search budget when retaining an exact set becomes too expensive.
• Observed runtime diversity: an explicitly opt-in, separate measurement of distinct values produced by a workload, compared with the statically permitted state space.
• Overlap experiments: estimate overlap between large generated sets of constructions from different capabilities. Ertl's joint estimator is relevant here; tagged sum constructors remain distinct and must not be treated as an untagged set union.

Prerequisites and limits:

• Define element identity and supported normalization before hashing. HLL cannot discover observational equivalence, repair an incomplete scope, or enumerate inhabitants for us.
• Sketching reduces memory for counting a supplied stream, not the cost of generating that stream. Prototype only when an actual workload justifies it; small sets should remain exact.
• Label estimates separately from exact implementation counts and stored-value estimates. Record sketch precision/error, hash configuration, and enumeration bounds or workload coverage. Sketch error does not account for inhabitants that were never generated or observed.
• A finite sketch cannot prove ω, completeness, or impossibility. An estimate must not replace an unresolved static answer or be presented as a rigorous bound on the full inhabitant set.
• Validate any prototype against exact counts on tractable cases before using it on larger ones.