Count generic method cardinality, and report what blocks the rest - #10
Merged
Merged
Conversation
CI ·
|
| Gate | Result |
|---|---|
| Formatting (scalafmt) | ✅ success |
| Semantic rules (scalafix) | ✅ success |
| Tests + coverage (scoverage) | ✅ 90.15% statements (floor 80%), 83.66% branches |
| Plugin tests (scripted) | ✅ success |
| Duplicate code (CPD) | ✅ no duplicates over 100 tokens |
| Documentation site (Laika) | ✅ renders under target/site |
Quality ·
|
| Report | Result |
|---|---|
| Mutation testing (stryker4s, report only) | |
| Code Health (CodeScene) | ✅ no new findings |
Workflow run · mutation report in the stryker4s-reports artifact
kryptt
changed the title
…eleton) The report work (per-file, per-definition cardinality of an sbt project) needs an sbt plugin. This is the M0 walking skeleton agreed in the plan: - core: the existing calculator, moved to core/ and packaged as 'cardinality' (empty-package members cannot be referenced from packaged code, which the plugin now needs to do). - plugin: sbt-cardinality, an auto-triggered plugin whose cardinalityReport task runs Counter over every Compile source and logs one line per file plus a total. Def.uncached: a report must never be served stale from sbt 2's task cache. Tested end-to-end with scripted. - Everything builds with Scala 3.8.4, the version sbt 2.0.x runs plugins on: Scala 3 binary compatibility is backward only, so 3.9-built artifacts could not load inside sbt, while 3.9 users can consume 3.8.4 artifacts unchanged. - Gates follow the layout: CPD scans both modules' main sources, the scripted suite is a new CI gate, the coverage floor is scoped to core (scripted runs outside scoverage instrumentation) and ratchets 65 -> 80 to sit just below the measured ~84% baseline, and mutation testing is scoped to core/stryker. Skeleton limits, to be grown next: raw Size toString output (M2 renders), flat per-file lines (M1 builds the per-definition tree), and .get on parse results (M1/M3 report every parse error with positions before failing).
…bounded
M1 and M2 of the report plan. The calculator now walks the definitions a source
introduces — classes, enums, modules, type aliases, opaque types, nested ones
included — and returns each with the cardinality it holds, the line it is
defined on, and the type names that stopped it from being bounded.
- `Counter.definitions` records the walk `Counter.source` already performed and
descends into the bodies of the definitions it finds, so an ADT whose cases
live inside its trait or companion — the common Scala 3 shape, and every ADT
in `eo` — is counted and listed. Nested values still add nothing: they are
state derived from the fields, which already count it.
- `Counter.source` sums what the walk contributes, so a nested definition is
now part of a source's cardinality: `sealed trait Light { case object Red … }`
was 0 before and is 3.
- An unbounded size carries its reason. The scope records the type names the
calculator could not resolve — `String`, a type parameter, a match type, an
unmodelled constructor such as `Fst`, a collection whose length is unbounded —
so a report says why instead of printing ω.
- `Size.render` (M2): exact up to 1024, `2^n` above, `ω`/`τ` for the two
infinities, Float and Double marked lossy, since their count of bit patterns
is an upper bound rather than a cardinality.
- `Report.of` reads a file, a directory or a `-sources.jar` — the shape a
published library ships — and renders what it found: the summary separates
the definitions that are unbounded only because of their own type parameters,
then one line per definition, ordered by cardinality, names the types it could
not bound. A source it cannot read or parse is reported rather than thrown.
`defnIn` stays the one rule for what a definition contributes; the walk adds the
rows and the descent, so the two cannot drift apart.
core: 89.3% statements / 82.0% branches, up from the 84/79 baseline.
- `cardinalityReport` logs the report of the project's `Compile` sources and writes it to `target/cardinality/report.txt` (`cardinalityReportFile`), so a build can keep it, diff it, or post it as an artifact. - `cardinalityReportOf <path>...` runs the same report over sources the build does not compile itself — a directory, a single file, or the `-sources.jar` a published library ships. That is how a dependency's types get measured from outside its build; the first real run, over `eo-core` 0.16.0, is in the README, along with what it says. - Both tasks write the report, log it, and only then fail when a source could not be read or parsed: a report over sources the calculator could not read is incomplete, and failing quietly would present what it did find as the whole story. (M3's report-then-fail, one milestone early.) - Scripted: the walking skeleton's scenario now mirrors a golden report, and a new scenario packages a fixture library's sources jar and reports on it, so the library path is covered end to end without network access.
The mutation report on this branch's first push (report-only, 69.7% of all mutants) pointed at assertions the new code was missing. Each of these now fails when the line it guards is mutated: - a source's total counts a top-level value, not just its definitions (`Counter.source`'s `top = true`), - a row that is bounded says nothing about being unbounded (`Report.render`), - a sources jar keeps the entries that are not Scala out of the report, - a signature carries every parameter it declares, and the summary counts a definition whose parameters are only partly unresolved — so the count is `exists` over the parameters, not `forall`.
A signature's cardinality is the number of canonical pure, total, parametric implementations it admits with everything in scope — not the count of stored values an instantiated data type holds. `choose[A](x: A, y: A): A` has two (x or y); the constructor of `Pair[A](x: A, y: A)` has four ways to build its product, while `Pair[Int]` still holds 2^64 values. `Inhabitation` solves that count over shapes — free atoms, products, sums, arrows — with exact BigInt arithmetic: - a productive fixed point first, then cycle detection over the live rules, so a re-appliable producer (`x`, `step: A => A`) is ω while a cycle with no starting inhabitant is 0, not ω; - provenance distinguishes values: two bindings of the same shape are one construction only when they name the same source; - finite sums in scope are split exhaustively, so a `Boolean` argument branches; - what the fragment cannot decide — higher-order application, elimination of an opaque sum-producing callable, an arithmetic or state budget — is `Unresolved` with the reason, never a finite guess or an invented infinity.
Two passes over the supplied sources: the first indexes declarations, lexical owners and their binders; the second resolves each signature against them and counts what a total, parametric implementation of it could construct. - Captures are real: enclosing constructor fields and values, enclosing method parameters, local values, and named producers; a product input is projected into its fields. Value aliases fold onto the value they name (including forward chains), and an alias whose source cannot be resolved fails closed rather than inventing an opaque value that would make an identity function look like a productive cycle. - Binder identity is per declaration: a shadowed `A` is not an outer `A`, a method body's type alias does not leak into its signature, and a value that a parameter shadows stays counted through its receiver (`this.x`). - A total parametric method cannot invent a value it never receives, so inherited or declared members and unrelated imports do not block a count; a signature that mentions a concrete atom (`Int`, `Boolean`) with an open environment does, because there an outside producer could change it. - Case-class products are only products when the whole product is public: one parameter list, no private or protected fields, no extra members, not abstract. - The report leads with the method counts, sums the reasons into a triage list (`N unresolved on: …`) and keeps the stored-value estimate below it as its own section, with `?` wherever that estimate is unresolved — a guess is not a proof of infinity, and an opaque representation is not a singleton. Over eo-core 0.16.0: 480 signatures, 41 finite, 3 countably infinite, 436 unresolved with named reasons. Coverage 85.2% statements / 78.6% branches.
CodeScene flagged the new module for nested complexity, and it was right: `goal` built its rules in one deeply nested match, and `run` walked, decided and counted in one body. Both are now a small dispatcher over named passes — a rule per shape (`split`, `constructors`, `producers`, `application`), a least-productive fixed point, and a `Live` view whose reasons, cycle detection and exact arithmetic are separate walks. `return` is gone too: the repository bans it via scalafix.
The quality gate measured `measurement` at cyclomatic complexity 32 and `namedType` at 24, against a threshold of 9. Both are now dispatchers over named steps: a `Measurement` that holds the scope and reports one part at a time (scanning a frame, folding aliases, flagging what is reachable, resolving the result, counting), and a `namedType` that separates the builtins it spells itself from a source type's representation. No diagnostic changed: the analysis over 66 input batteries — every builtin spelling, shadowing, captures, qualification, cross-file and forward aliases, givens, imports, extensions, enums, recursion — prints byte-identical output before and after.
The gate's next two findings: `index` was a 134-line dispatcher (threshold 70) and `parameterized` took seven arguments. `index` now names one method per declaration kind — package, package object, class, template, object, given, extension, method — with the class's constructor target and the template's body split out, and `parameterized` carries one `Applied` record instead of seven arguments.
The gate's last finding: `indexTemplate` took eight arguments. The body a definition opens — its node, name, statements, binders and constructor inputs — travels as a `Template`, built by one method per declaration kind.
`docs/counting-type-inhabitants.md` records Alex Knvl's *Counting type inhabitants* as the reference this solver follows, and `ReferenceInhabitantsSpec` runs its worked examples — 27 of them, all green: `Either Bool (Maybe Bool) ~ 5`, `Maybe Bool -> Bool ~ 8`, `Bool -> Maybe Bool ~ 9`, `∀a. a -> a ~ 1`, `∀a. (a,a) -> a ~ 2`, `∀a. (a,a) -> (a,a) ~ 4`, composition and `filter`-style signatures, `∀a. (a -> a) -> a -> a ~ ℵ₀` and the unseeded `~ 0`, plus the negation family (`x -> 0` has at most one inhabitant, `(x -> 0) -> 0 ~ 1` iff `x > 0`). Two solver fixes come out of it: - Absurd elimination. An inhabited empty type proves the context impossible, and every expression under that assumption is observationally equal — the unique map out of the empty type. `∀a. (a -> 0) -> a -> 0 ~ 1` and two empty-result functions are indistinguishable, so an empty target is now a rule of its own and an empty-result callable is a negation rather than an opaque sum. - `∀a. (a -> a) -> a ~ 0`: an unproductive cycle stays 0 rather than an unknown. The frontend audit that came with the reference found four scope bugs, all fixed here: - The indexing split dropped type registration for traits and enums: an enum's cases resolved to Unit and a trait's members to "abstract", which are *false finite* counts. Both register again, and an enum is the sum of its cases. - A declared member is a slot the caller fills, so `def seed: A` supplies an A and `def step(a: A): A` supplies a callable that can be reapplied (ω, not 1). Inherited declarations travel too, resolved through the subclass's type arguments so `extends Base[A]` reads Base's A as this A. - A *concrete* member is a specific inhabitant of its type, and a total parametric body can only draw values from the environment it already has: it neither adds a choice nor blocks one, so it is no longer a diagnostic. - An import or an export can shadow a name the model reads as a builtin, and that is the one way a name outside the lexical chain changes an answer here; a module nested inside the target's own scope shares its binders and is part of the scope.
The gate reads a file over 600 lines of code and a module over 75 functions as unhealthy, and `scanParents` nested six deep. The measurement — the scope one signature sees, its aliases, its captures, its count — moves to `Measurement.scala` behind a package-private `Resolver` trait that the index implements, so no resolution logic is duplicated. `scanParents` flattens into `scanParent`/`scanDeclared`/`inherited`. No behavior change: the analysis over the 53 real eo-core sources is byte-identical before and after (480 signatures, same sha256), as are two batteries of the analyzer's own sources.
The same free theorem that keeps a concrete method out of the environment applies to a value: a total parametric body can only compute what the scope already holds, so an unreadable body — `val step: A => A = id`, `val (a, b) = pair` — names one of those bindings rather than adding a choice. Blocking the count on it was the larger error: the reviewer's known-identity case now reads 1 (only `seed`) where it read `?`, and 85 eo-core signatures stop being blocked by a reason that was never a reason. Aliases are still followed, because an alias *names* a binding and so raises the precision of the count.
A declared member is a slot the caller fills, but the signature under measurement is not one of its own slots. Binding it let `CanGet.get(s: S): A` claim an implementation by calling itself: it read 1 where the honest answer is 0 (nothing in that scope supplies an A), and four more eo declarations read 1 for the same reason. `CanGetOption.getOption(s: S): Option[A]` now reads 1 -- only `None` is constructible -- and `CanPlace.place(b: B): T => T` reads 1, the identity. eo-core: 15 finite, 2 countably infinite, 463 unresolved.
Russell 1907 (PLMS s2-4, pp. 29-53) is the foundational reference for the counting contract's first discipline: a definition does not automatically license a collection, and cardinality is not order type. Two documents now carry that connection into something a review can check. - docs/research/code-cardinality-foundations.md: the evidence register. For each decision in the counting contract (scope before counting, mathematical inhabitants vs expressible implementations, parametricity, productivity, cardinality vs order, labeled approximation, `?` as a first-class answer, budget honesty) it names the sources, how far each was verified (executable / inspected / bibliography-verified / metadata-verified / classical), and the boundary past which each must not be cited. Reynolds 1984, Pitts 1987, Wadler 1989, Smyth & Plotkin 1982 and the definability literature (Luna & Taylor 2010, Fan 2020) are verified at the stated levels from Crossref, publisher pages or fetched abstracts. - docs/research/russell-citation-inventory.md + russell-citations.json: every citing work the public indexes report for Russell 1907 — OpenAlex 301 (all cursor pages), Semantic Scholar 212 (single page), Crossref count 70; 376 after a DOI-or-title+year union. Database-reported is kept distinct from verified: one bibliography-verified citer (Fan 2020), abstract-inspected (Luna & Taylor 2010), the rest title-screened with per-record source flags. The plan's reference section links both and directs reviews to answer from the register, not from memory.
The report's walk was written against the Counter the branch forked from, where a name was read as its statement passed and a forward reference was `omega`. The algebra under it has changed since: recursive types are solved as least fixed points, lazy cycles as greatest ones, sizes are epsilon0-tier polynomials, and a member signature is an additive reading of its own. A report that kept the old walk would print the old numbers. The walk now solves each body once — `solve` over the body's equations, the same call the source total makes — and hands every definition the value a reference to it has, so a row and its reference always agree: `Succ` in a Peano `Nat` reads `omega` (not a question mark), a lazy `Timeline` reads `omega`, a function space over a countable type reads `epsilon0`, and what the report cannot bound is `?` with the unresolved names that stopped it. Since `omega` and `epsilon0` are answers now, they no longer mark a row as unresolved by themselves; only a name outside the calculator's vocabulary (or an opaque representation) does. A capacity is a bound, not a count, so the report says so: "finite capacities are upper bounds". The first run over real code found the name rule wanting: eo-core's `object Modify` reported the `epsilon0` of `class Modify`, because a companion module and its type are both called `Modify` and the scope kept one value per name. A type now claims the name it shares with its module — a type reference means the type — while the module is worth one value either way, as a row and as a contribution. (`CardinalitySpec`, `ReportSpec`.) Verification: `core/test` all 9 suites green (389 examples, 18 pending); `plugin/scripted` green with the shipped expectations; the run over eo-core 0.16.0 (53 sources, 134 definitions) reads 40 unresolved, 2 with more than one value, 53 with one value, 5 with no values, 34 abstract — the two `2^32` array builders are its only non-module finite sizes, and the generic classes are `?` because their own type parameters are what stop the count. The report fixture now carries the features: `sealed trait Nat`/`Zero`/`Succ`, a lazy `Timeline` and a `Reducer` whose function space is epsilon0.
The branch restructured the sources into `core/` and `plugin/`, and main's docs landed after the fork, so several references only make sense on one side of the merge: - README and `docs/` linked `src/main/...` and `src/test/...` paths that moved under `core/`; the GitHub blob links in `docs/type-arithmetic.md` and `docs/index.md` 404'd. - Laika rejects the docs' internal links: an anchor id maps `.` and a leading digit to `_` (`#_2-agreed-counting-contract`), and a quoted `[polymorphic]` read as a reference link with no target. The `ci.yml` documentation gate fails on both, so they are escaped and re-anchored. - CodeScene's strict gate matched `src/**`, which the restructure emptied; `**/src/**` covers both modules again. - The README's report snapshot and eo-core baseline were the pivot's format (`unbounded by:`). Both now read the merged report: rows of `number, name, kind, location`, `?` for unresolved names, the summary lines the report actually prints, and the numbers of a fresh eo-core 0.16.0 run.
The task was a common setting, so aggregation ran it for core and plugin as well and wrote the same site three times per invocation. It belongs to the repository, not to a module.
The unused overload was dead weight next to the solver's one real merge (a round's evaluated names, which carries no notes of its own).
The plan still spelled the tier above countable as tau, which #16 replaced with the analysis' epsilon0 tier.
The plan's first milestone asked for the full report to survive, not just the table of totals: a run is only comparable to a later one when the artifact, the analyzer revision, the input's checksum, the tool versions and the analysis limits travel together. `docs/baselines/eo-core-0.16.0.txt` carries all of that in its header and the report underneath it, and the plan and README point at it instead of at numbers with no artifact behind them. The run is the rebased plugin over `cats-eo_3-0.16.0-sources.jar`, whose SHA-256 matches the one the plan already recorded. Its summary: 53 sources, 134 definitions — 40 unresolved, 2 with more than one value (the `2^32` array builders), 53 with one value, 5 with no values, 34 abstract — and 480 signatures: 15 finite, 2 countably infinite, 463 unresolved. The site now links `counting-type-inhabitants.md` from the landing page and the navigation order, and Laika copies the baseline next to the plan that cites it.
kryptt
force-pushed
the
feat/sbt-plugin-skeleton
branch
from
September 30, 2026 21:53
7d9ec73 to
cf5ee45
Compare
|
🚀 Cloudflare Pages preview for https://3683770d.scala-cardinality-site.pages.dev Built from |
…lacks The baseline has 134 definition rows and 40 of them are `?`. This adds the other half of that baseline: a ledger that says, for each of the 40, what stopped it, what would move it, and the order the work is worth doing in (`docs/baselines/eo-core-0.16.0-unresolved.md`). What the ledger found: - The dominant gap is not a counting rule but an answer class. eo's optics are generic and built from functions over their parameters (`Getter[S, A](read: S => A)`), so a definition's stored-value estimate is a function of its instantiation. 29 of the 40 rows are this kind, and the report says `unresolved: S, A` where it should say that no number exists for a template. - One gap is simply wrong answers: an applied user-defined type is never resolved. `case class Use(p: Pair[Boolean])` reports `ω`, `unresolved: Pair`, where 4 is the answer — and the same for a match type applied to a concrete tuple (`Fst[(Boolean, Boolean)]`). - The estimate's scope is one source file, so `Box` in `A.scala` and `Use(b: Box)` in `B.scala` reads `ω` even though the report holds both sources; the method side of the same report already indexes all of them. - Three rows are `?` by design (opaque representations) and five are honest unboundedness (unsealed capabilities a caller implements); neither is a gap. The three capabilities that fix wrong answers rather than missing reasons are pinned as pending targets in `ReportSpec`, so specs2 reports them as pending today and fails if the marker ever goes stale once a rule lands. The plan's V1.3 milestone links the ledger and moves from "candidates identified" to "the definition half is started".
`case class Use(p: Pair[Boolean])` read `ω`, `unresolved: Pair`, where 4 is the answer: an applied user-defined type was never resolved, only the builtin constructors (`Option`, `Either`, `Set`, the collections) were. That is wrong for any project with parameterised types, and it is the machinery every other item on the ledger's list needs. A scope now carries the definitions themselves — each with its type parameters and its equation — alongside the solved values, and `C[args]` reads the definition's equation with its parameters bound to what the arguments are worth (`Pair[Boolean]` is `Pair`'s `a: A, b: A` with `A := 2`). An argument that is itself unresolved keeps its own reason, so `BijectionIso[S, S, A, A]` reads as `S` and `A` rather than as a name the file defines. Two recursive readings stay careful. An instantiation that is exactly the definition's own parameters — `Node[A]` inside `Node`'s equation — borrows the fixed point the solver already has for the name, so a parameterised recursion keeps its μ/ν reading. Any other instantiation entered while its own name is being substituted is a cycle the name-keyed solver has no fixed point for, and keeps the old fallback: ω with the name as the reason. On eo-core the three concrete applications now read right and three rows name their own parameters instead of an internal type (`Iso[S, A]` said `unresolved: BijectionIso`); `ModifyF` still names `Fst`/`Snd`, which live in another file — the next step. Suite: 391 examples, 2 pending.
After the substitution step the estimate still read one file at a time, so a type a sibling file defines counted as an unknown name: `Box` in `A.scala` and `Use(b: Box)` in `B.scala` read `ω`, `unresolved: Box`, where 2 is the answer, even though `Report` hands the whole source set to the same run. `Counter.Library` is now that set: every source's top-level definitions grouped by the package they are read in, each package solved as one system, so a definition can reference a sibling file's names — and a sealed hierarchy that spans files sums as a whole, which the name-keyed solver could not do before. `Report.of` builds the library once and reads every source against it; `Counter.source` and `Counter.definitions` take it as an optional argument, and `Library.empty` keeps the single-file reading that the specs use. What resolves, and what stays unresolved, is a rule with a reason: - the file's own definitions and solved values come first, as before; - then its own package's members, which need no import; - then a name that exactly one package across the source set defines, which is the shape an import of a single name has; - a name a body imports directly is left to the import — the calculator does not follow imports, so a library answer for it would be a guess; - a name two packages define stays unresolved rather than guessed. The plugin fixture now splits the Peano family across two files, and its expected report reads `example.Cursor` (in one file) as `ω` through `Nat` (in the other) — the end-to-end proof that a project's sources are read as one set. Suite: 398 examples, 1 pending (the match-type target).
A row whose only reasons are the type parameters it declares has no number to show — every instantiation has its own, and the caller supplies it — but the report read `unresolved: S, A` exactly as it read a name the sources do not define. That is the wrong class of answer: it sends a reader looking for a missing rule where there is none. `Definition` now carries reasons by kind — `Parameter`, `HigherKinded`, `Open`, `Unknown`, `Syntax` — and the report reads them: a row that depends on its instantiation says so (`depends on its instantiation (A, S, T, B)`), a row an open abstraction unbounds will say that, and any other row lists what it could not read as before. The summary counts the classes apart, so `?` no longer means one thing. On eo-core the definition summary moves from 40 unresolved to: 18 unresolved · 22 instantiation-dependent · 2 with more than one value · 53 with one value · 5 with no values · 34 abstract. The 22 are the optics templates (`BijectionIso[S, T, A, B]`, `GetReplaceLens[S, T, A, B]`, the `X` aliases); the remaining 18 mix a parameter with a match type, a higher-kinded parameter, an open trait, `Any`/`Null`, a refinement or a name outside the sources — the next steps on the list. The plugin fixtures show both: `example.Holder[A]` reads `depends on its instantiation (A)` while `example.Reducer` keeps `unresolved: String`. Suite: 398 examples, 1 pending.
A reference to an unsealed trait has no bound to compute: any subtype anywhere can add values, so `CanModify[S, A] = CanModifyP[S, S, A, A]` could never be a number, whatever the calculator learns. It was reported as `unresolved: CanModifyP`, which sends a reader looking for a rule that would not help. The bodies now record the abstractions they leave open — unsealed traits and abstract classes, which the library knows per package too — and a name that resolves to one is the `Open` kind. The report says `open to implementations (CanModifyP)` and counts it as `unbounded by an open abstraction`, apart from what the calculator could not read. A sealed parent is not open: its children are the sum, and the row for a reference through it is a number. On eo-core the definition summary moves to: 14 unresolved · 22 instantiation-dependent · 4 unbounded by an open abstraction · 2 with more than one value · 53 with one value · 5 with no values · 34 abstract — the four are the capability aliases (`CanModify`, `CanModifyA`, `CanModifyF`, `CanPut`). Suite: 400 examples, 1 pending.
`type Fst[T] = T match { case (f, s) => f }` applied to a tuple was `ω`,
`unresolved: Fst`: the applied alias went through its body, and a match type is
not a size the algebra can read. `Fst[(Boolean, Boolean)]` is `Boolean` —
2 — and for eo-style code, `Fst[A]` over a free parameter stays inert, which
is the honest reading.
An alias whose body is a match type now carries that body with its definition,
and applying it reduces on the argument's *syntax*, which no size can carry:
the case pattern is matched against the scrutinee (the definition's parameters
already replaced by the arguments), the first case that matches gives its body
with the pattern's binders replaced by the parts of the scrutinee they stood
for, and the result is read as a type. A pattern variable is spelled the way
Scala 3 spells one — a lowercase name — so `case Int => Boolean` matches by
spelling and `case x => x` binds whatever it is given. A tuple pattern matches
a tuple scrutinee of the same arity, an unread pattern binds nothing, and a
match type no case matches stays unreduced: the report names it rather than
guessing, which is what eo's `Fst[A]`/`Snd[A]` over free parameters keep
reading.
Suite: 402 examples, 18 pending (`ArticleCardinalitySpec`'s targets). On
eo-core the definition summary is 15 unresolved · 21 instantiation-dependent ·
4 unbounded by an open abstraction · 2 with more than one value · 53 with one
value · 5 with no values · 34 abstract; `ModifyF[A, B]` moved from pure
instantiation-dependence to `unresolved: A, B, a match type`, which is what it
is — both readings are waiting on the caller.
`F[_]` and `F[_, _]` were `unresolved: F`: the same reason a misspelled class gets, for a parameter that is the caller's by construction. eo's three `Forget`-carrying definitions read that way, and the method side already phrases the same gap as `bounded or higher-kinded parameter F[_]`, so the two halves of a report now speak the same language. A binder carries how many parameters it takes, and an applied `F[A]` over one reasons `HigherKinded(name, arity)`, which renders as `F[_]` or `F[_, _]`. A row whose reasons are all parameters — plain or higher-kinded — stays in the instantiation-dependent class: the number exists, the caller has it.
`Null` and `Any` were unmodelled names, so `PSVec.Slice[+B](arr: Array[Any], offset: Int, length: Int)` — a real array-backed vector — read `unresolved: Any`, and `AssocSndZ`'s `Array[Int] | Null` did too. Both are the lattice's ends, and the calculator can say what they are: `Null` has the one value `null`, and `Any` is the top, which nothing the analysis can place is above — so it sits at the ε₀ tier, the analysis' top. Other top-ish names (`AnyRef`, `Matchable`) stay unmodelled rather than guessed. On eo-core two rows read as numbers now: `Slice` is `ω` (its fields multiply a countable array space) and `AssocSndZ` depends on `Xo` alone. The definition summary reads: 13 unresolved · 22 instantiation-dependent · 4 unbounded by an open abstraction · 3 with more than one value · 53 with one value · 5 with no values · 34 abstract. Suite: 404 examples.
A match type that no case matches is inert over whatever the argument is, so the argument's own reason belongs on the row: eo's `Affine.Miss[A]` reads `unresolved: A, a match type` rather than losing the parameter that decides whether the case would ever fire.
The artifacts still described the state before the counting work: the baseline said 40 unresolved rows, the ledger listed substitution, cross-source scope and match-type reduction as missing, and the README and plan carried the old counts. The baseline is regenerated from the run at this revision, and the ledger now reads as a ledger of what moved and what is left: of the first baseline's 40 `?` rows, 31 moved — one became a number (`PSVec.Slice` is `ω`), 22 read `depends on its instantiation (…)`, 4 read `open to implementations (…)`, and the rest name a match type or a higher-kinded parameter instead of an internal type name. Six gaps 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 stay `?` by contract. The plan's baseline table, its V1.3 status and the README's eo paragraph follow the same numbers.
CodeScene's gate read the merged Counter as three new issues: 792 lines of code in one file, 117 functions in one module, and `instantiation` at a cyclomatic complexity of 9. The file had grown with the new machinery rather than been reorganised around it. Three pieces move to where they belong, with no behaviour change: `Scope.scala` carries what a read is made of (the names a body solves, the world around them, and the library of other sources), `Walk.scala` carries the walk that measures a source definition by definition, and `MatchTypes.scala` carries the match-type reduction. `Library` becomes a top-level type of the `cardinality` package, which is what it is — the report's view of a whole source set. `instantiation` keeps the lookup and delegates the read to a named helper, so neither half carries the whole complexity. Verified by the suite (404 examples), both scripted scenarios, and the eo run: the regenerated report is byte-identical to the baseline, so the split moved code and nothing else.
`sealed trait Nat` read `—` in the report while a reference to it read `ω`: the abstract row had no size of its own, even where the solver had a solved sum. The same held for every sealed family in eo (`Affine`, `PSVec`, `Optic`), whose consumers were reading numbers the parents' rows denied. An abstract row now reads the value a reference to it has: the solved sum for a sealed parent whose cases the source set defines — the children's reasons landing on the parent's row, so a family with a parameter still says why — and `—` only for an abstraction nobody summed. That exposed a second bug behind it: `sealedSums` skipped a sealed parent when a *companion object* shared its name (the trait was diffed away by the object's name), which is why the plugin fixture's `sealed trait Shape` had no sum at all; the parent keeps its equation and the type still claims the name. Plugin fixtures, both scripted scenarios, the eo baseline and the plan's table follow: `Nat` reads `ω`, eo's abstract rows carry their sums (81 with one value, 6 without a number), and the suite is 404 examples green.
CodeScene's gate read the split-out `Scope` as primitive-obsessed: half of its arguments were primitives and half of the arguments to its 45 functions were strings. It is a name-keyed store — the heuristic is pointing at the key. `TypeName` is that key, opaque the way this codebase treats a value it does not want confused with its own text: a name *is* its string at runtime, and the compiler keeps it apart from a package path, a printed signature or a report's prose. `TypeName.of` is the boundary a printed name crosses, `TypeName.path` a dotted package path, and `name.value` the text a row, an error or a sum needs. The refactor reaches through the scope, the walk, the solver's name-keyed maps and sets, and the match-type reducer; `bareName`/`bareTarget`/`initParent` stay `String` on purpose — they compare *syntax*, not keys. Verified by 404 examples, both scripted scenarios, and the eo run: the regenerated report is byte-identical to the baseline, so this moved types and nothing else.
CodeScene's gate read `Counter.instantiated` as an excess-argument function (six, max four); the lookup's result travels as the tuple it already is, so the read takes what it is reading plus where it came from.
Three rows of the eo carrier family were reported as gaps in the calculator
rather than as what they are:
- `type Forget[F[_]] = [X, A] =>> ForgetK[F, X, A]` names a *function* on
types. It has no value space of its own — applying it to arguments is where
a size would come from — so its row is `—` with the `constructor` kind and
the summary counts type constructors apart from what is unresolved.
- `Optic[S, T, A, B, MultiFocus[PSVec]] { type X = Xo }` is the trait it
refines plus member bindings: a refinement is now read as its base type, so
`ComposedTraversal` reads `open to implementations (Optic)` — a fact about
the sources rather than a missing rule.
- A qualified name a report cannot resolve is described as written (`af.Z`),
since the owner is what a reader needs to look it up.
Not done, and named in the ledger rather than pretended: β-application of a
constructor alias and opaque transparency inside the defining package. Neither
is reachable from a *definition's* stored types in eo — its signatures use
them, and the method side's own model reads them.
eo-core: 13 unresolved → 10, 4 open → 5, 2 constructors. Suite: 406 examples,
both scripted scenarios, site renders; baseline, ledger, plan table and README
follow the new numbers.
`type X = af.Z` read `unresolved: Z`, losing the one thing a reader needs: which instance's member it is. A qualified reference now resolves when the sources supply the owner's type, and is reported as written otherwise. - `Outer.B` (a named owner), `Foo[Boolean].B` (an applied one), and `x.B` over a value whose declared type the sources give: the member's body is read with the owner's parameters replaced by what the reference supplied. - a member a body declares abstract (`type Z` with no body) is supplied by whoever implements the owner, so the reference is `open to implementations (x.Z)` rather than an unknown name. - anything else — a qualifier whose type the sources do not give — keeps the reference as its reason: eo's `ComposedTraversal.X` now reads `unresolved: af.Z`. Two fixes fell out of running it over eo. `Walk`/`Scope`/`MatchTypes` printed trees without the Scala 3 dialect, so `Library.of` crashed on the first `inline def` eo's sources contain (`Scala213 doesn't support inline modifiers`) — the given now sits in every file that prints, as it already did in `Counter` and `MethodAnalysis`. And a library frame is looked up by `members` as well as by values and equations, so a trait can be the owner of a member. eo-core: 10 rows unresolved (unchanged), one reason improved. Suite: 410 examples, both scripted scenarios, site renders.
… scope Review notes: the modelled base types were a `Map` private to `Counter` matched with a guard and a lookup, and the binder case asked the scope twice whether it knew a name. `BaseTypes` holds the table where it belongs and answers both ways: as the extractor `case Type.Name(BaseTypes(size)) => size`, and as `get` for a caller that is checking rather than matching. `Scope.Parameter` is the same idea for the other question — `case scope.Parameter(size) => size` reads the binding this read gives a type parameter, which is what the two-line guard was spelling out. Verified by 410 examples, both scripted scenarios, and the eo run: the report is byte-identical, so this moved where the tables live and nothing else.
`BaseTypes.unapply` took the name, so `typeIn` still had to peel the `Type.Name` itself before the extractor could see it. It takes the type now and delegates to `get` once it knows the shape is a name, so the match reads `case BaseTypes(size) => size` and the table keeps one lookup. Verified by 410 examples, both scripted scenarios, and the eo run (unchanged).
An opaque type's row read `?` by policy while its own file could see the body: `opaque type Id = Byte` sat next to genuine singletons and `Direct[X, A] = A` said nothing at all. The policy was protecting against a misreading that the number does not have to invite. The row now reads the representation, in the scope that defines it: `Id` is 2^8, `Direct[X, A]` is `|A|` (instantiation-dependent), `ForgetK[F, X, A]` is `F[A]` and `MultiFocusK[F, X, A]` is `(X, F[A])`. The `opaque` kind stays on the row, so the contract is still visible: *outside* the defining scope a reference is one opaque value, which is what the body's equation keeps saying and what a new test pins for both readings at once. eo-core: 10 unresolved → 7, 22 instantiation-dependent → 25. Suite: 411 examples, both scripted scenarios, site renders; baseline, ledger, plan table and README follow. Still named as missing, in the ledger: *reference-level* transparency — a field inside the defining scope typed by the opaque still reads the outside one-value binding.
`class User(id: Id, active: Boolean)` outside the scope that defines the opaque `Id` is 1 × 2 — both halves were pinned (`CardinalitySpec`'s opaque case is one opaque value, the product rule is `Pair`), the combination was not. `ReportSpec.crossSourceOpaque` now reads the exact shape, and a new *pending* target in `ArticleCardinalitySpec` pins the truth for the case the calculator does not model yet: declared next to the opaque, `Id` is `Byte`, so `User` is 2^8 × 2 = 2^9 — it fails today at 2 and turns into an assertion when reference-level transparency lands.
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
The report plan (laid out in the Delta thread): the calculator measures a real codebase, counts
what a generic method can actually be, and names what blocks the rest.
What
core/and packaged ascardinality— empty-package memberscannot be referenced from packaged code, which the plugin needs to do.
Counter.definitionswalks a source's definitions — classes, enums,modules, type aliases, opaque types, nested ones included — with the cardinality each holds, the
names the calculator could not bound, and the line it sits on.
Inhabitationcounts the canonical pure, total,parametric implementations a signature admits with everything in scope —
choose[A](x: A, y: A): Ais 2,
Pair's constructor is 4,use[A](x: A, step: A => A): Ais ω, a cycle with no startinginhabitant is 0. Exact
BigIntarithmetic, provenance-carrying bindings, a least-productive fixedpoint and cycle detection. The stored-value estimate over definitions stays a separate section:
Pair[Int]is still2^64.MethodAnalysis): two passes — index declarations, owners and binders, then resolveeach signature against them. Captures include enclosing fields, enclosing parameters, local
values, callable producers and product projections; binder identity is per declaration. Nothing
resolves outside the supplied sources: no dependency resolution.
?with its reason, and the section headersums the reasons into a triage list.
ω/τare never fallbacks. A source the report cannot readis reported, not thrown.
cardinalityReportwrites and logs the report for the project'sCompilesources(
cardinalityReportFile), andcardinalityReportOf <path>...reports on any Scala sources — adirectory, a file, or a library's published sources jar. Both fail after logging when a source
could not be read, and both are covered by scripted tests, the library one by packaging a fixture
sources jar.
scoped to core and stays at 80.
The first real run: eo-core 0.16.0 (
dev.constructive %% cats-eo), 480 signaturesThe 4 is the
Pair[A](x, y)rule on real code; the 0s are declarations whose signature cannot beimplemented from its scope alone (the free-theorem reading); ω is a captured endomorphism being
reapplied.
Next milestones, by what the triage list says
using ev: Unknown[A]or anabstract
given seed: Ais a slot a caller fills, and should bind like a parameter — while aforeign given cannot hold this method's binders and should not block anything.
F[_]/F[_, _].Verification
core/testFull: 153 examples green — the solver's semantics, the scope and binder rules, thereport walk and rendering, unreadable and unparsable input.
plugin/scripted: both scenarios green.scalafmtAll; scalafmtSbt; scalafixAll --checkclean;coverageAllgreen at 85.0% stmt / 78.3%branch (floor 80); CPD clean; CodeScene reports no new findings after splitting the passes the
gate read as complex.
survivors live, and it is the next test-investment target.
Validated against the inhabitant-counting reference
docs/counting-type-inhabitants.mdrecords Alex Knvl's Counting type inhabitants as thespecification this solver follows, and
ReferenceInhabitantsSpecruns 27 of its worked examples:products, sums and exponentials (
Either Bool (Maybe Bool) ~ 5,Maybe Bool -> Bool ~ 8,Bool -> Maybe Bool ~ 9,Nothing -> Bool ~ 1,Bool -> Nothing ~ 0), rank-1 polymorphism(
∀a. a -> a ~ 1,∀a. (a,a) -> a ~ 2,∀a. (a,a) -> (a,a) ~ 4, composition,filter-stylesignatures), recursive types (
∀a. (a -> a) -> a -> a ~ ℵ₀,∀a. (a -> a) -> a ~ 0) and thenegation family (
(x -> 0) -> 0 ~ 1iffx > 0). Two solver corrections came out of it: absurdelimination for inhabited empty types, and keeping an unproductive cycle at 0.
An audit of the frontend against the same reference found and fixed four scope bugs: the CodeScene
split had silently dropped trait/enum type registration (false finite counts — an enum is now the
sum of its cases); a declared member is a slot the caller fills (
def seed: Asupplies anA,def step(a: A): Asupplies a re-appliable callable → ω), inherited declarations resolved throughthe subclass's type arguments; a concrete member neither binds nor blocks, because a total
parametric body can only compute what the environment already holds; and import/export shadowing of
a modelled builtin is the one way something outside the lexical chain changes an answer here.
eo-core, as it reads now
The finite count moved down from 41 because eo's traits now genuinely contribute their declared
capabilities (
F[_],modifyF,foldMap[M]), which this fragment cannot express — the soundreading of those signatures. Next, in order: primitive shapes (
Int,Long,Charas finiteinhabitants sets, the article's
Int ~ 2^32), sealed hierarchies as sums (237 signatures), andrefining which inherited capability can produce the target's shape.