Skip to content
Merged

p2 #596

Show file tree
Hide file tree
Changes from 8 commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion ROADMAP.md
Original file line number Diff line number Diff line change
Expand Up @@ -142,7 +142,6 @@ Findings from two reflective analyses (integration loop health, `main@b014746` a
- **Triple `MethodTranslation` schema** across `dsl/extdeps/languages/{rust,python,go}/runtime.dag`: same shape; only the per-target template field-name differs. Dissolution: single generic `MethodTranslation` with a `target: LanguageId` discriminator.
- **`effects.dag` dual authority** — `dsl/std/effects.dag` (395 lines) vs `src/v3/std/effects.dag` (818 lines, diverged 2×). Dissolution: decide authoritative location, collapse the other; name a convergence lane.
- **`container_to_algebra` table duplicates type aliases** — `dsl/std/types.dag:140-153` is the string-keyed table; `types.dag:211-214` declares `type List<T> = FreeMonoid<T>` etc. Dissolution: derive the table from the aliases or delete it.
- **`FileClassification` and `FileEntry` carry identical fields** — `dsl/std/filesystem.dag:27-34` vs `44-51` (same 6 fields, same types). Dissolution: one record; the other becomes an alias or is deleted.
- **Parallel string-keyed authorities in types.dag + coercion.dag**: `kernel_primitives` (65-74), `container_arity` (79-91), `ordered_collections` (125-130), `TypeCheckpoint.dag_name: String` (38-44), `InhabitantDecl.algebra: String` (59-65). Header labels as transitional. Dissolution: derive from structural declarations.

### P3 — modeling gaps
Expand Down
146 changes: 118 additions & 28 deletions docs/lens-library-design.md
Original file line number Diff line number Diff line change
Expand Up @@ -217,24 +217,88 @@ hand-found in existing reviews.
the same structural shape, flagging duplicates regardless of
name.

**Alias policy (load-bearing before ship):** Implementers need an
explicit split that reviewers can gate on — not “transparent vs
opaque,” but **which pairs are excluded vs which pairs are findings**.

Per `feedback_naming_is_aliasing` (see `CODING.md` — "Names are
namespaces, not aliases"), a type alias is a **namespace into** an
existing authority; that governs **Rule 1**. Redundant **second**
names for the **same** authority still violate single naming surface —
that is **Rule 2**.

**Rule 1 — Alias vs canonical (exclusion, never a finding):** If
declaration `D` exists only to re-name canonical declaration `C`
(same expanded type / same refinement witness chain), then **do not**
emit `(D, C)` as a duplicate pair. Examples: `type FileClassification =
FileEntry` (PR #596) must not collide with `FileEntry` in the
product channel; `type IssueId = NonEmptyStr where brand("IssueId")`
must not collide with its expanded refinement node as “two different
surfaces for one fact.” Rule 1 is asymmetric: the canonical row keeps
the bucket; aliases are absorbed into it.

**Rule 2 — Alias vs alias (detection, always a finding when it fires):**
If **two distinct declarations** `D1` and `D2` **both** normalize to
the **same** structural surrogate **and neither pair is covered by Rule
1 relative to the other** (i.e. they are peers, not namespace→canonical),
emit a finding. Examples: `NonEmptyStr` and `NonEmptyString` both
`String where non_empty` → same refinement fingerprint (see channel
(2) below); two independent `data` rows with identical bodies; two
record types with identical field maps (pre-#596 `FileEntry` vs
`FileClassification`). Rule 2 is what the audit lists as “expected
initial findings” once Rule 1 stops false positives.

**Channels (how Rules 1–2 map to hashes):**

1. **Product / coproduct / `data` channel** — Hash materialized bodies.
Apply **Rule 1** by skipping or folding pure nominal `type A = B`
(no `where`) into `B`'s bucket when `ignore_pure_nominal_type_aliases`
is true (default). **Rule 2** remains: two materialized bodies with
the same hash still collide.
2. **Refinement-alias channel** — For `type Name = Carrier where …`,
hash `(resolved_carrier_id, canonical_refinement_fingerprint)`.
**Rule 1:** do not count `Name` against `Carrier` alone. **Rule 2:**
two names with the **same** fingerprint collide (`NonEmptyStr` /
`NonEmptyString`). Distinct predicates / brands → distinct
fingerprints → no collision.

3. **Re-exports** — `ignore_re_exports` filters forward-only pairs
across module boundaries (orthogonal to Rules 1–2).

The sketch `DuplicatesConfig` below includes
`ignore_pure_nominal_type_aliases` (default **true**) to implement Rule
1 in channel (1) only. Refinement channel (2) stays **on** by default
so Rule 2 refinement twins stay in the expected-findings set.

Implementation keys off the same lowered-type facts the typechecker
already has (alias vs nominal record vs refinement spine), not source
substring heuristics.

**Motivation from the reviewer's std/extdeps audit (2026-04-15):**

- `FileClassification` and `FileEntry` in `dsl/std/filesystem.dag`
are the same record shape (same fields, same types), each
claiming to be "what Filesystem.probe returns."
- **`FileClassification` vs `FileEntry`** in `dsl/std/filesystem.dag`
were the same record shape (same fields, same types), each
claiming to be "what Filesystem.probe returns." **Resolved in PR
#596:** one `FileEntry` record and `type FileClassification =
FileEntry` (probe-surface name preserved). Still a motivating
example for why duplicate-shape detection matters on code before
the fix.
- `wire_contract: VariantEncoding = StringVariant { naming:
SnakeCase }` declared identically in `llm.dag`, `anthropic.dag`,
and `openai.dag` — two redundant duplicates of the imported
value.
- `default_edition: String = "2021"` declared in both `cargo.dag`
and `rust/imports.dag`.
- `NonEmptyStr` and `NonEmptyString` — two aliases for the same
refined type in `dsl/std/types.dag`.
- `NonEmptyStr` / `NonEmptyString` (audit-era example) — two names for
the same `String where …` refinement; channel **(2)** in §2.1, not
a product-body duplicate. (Today `types.dag` may only carry one
spelling; the lens contract still names the class.)

All four were hand-found in a single review pass. A
`lens_structural_duplicates` applied to `dsl/std/` and
`dsl/extdeps/` would return all four automatically, plus any
others the reviewer missed.
At the time of the audit, four examples were hand-found in a single
pass. One (`FileClassification` / `FileEntry`, PR #596) is already
dissolved. A `lens_structural_duplicates` applied to `dsl/std/` and
`dsl/extdeps/` would still flag the remaining shapes from that pass
plus any others the reviewer missed.

**Signature:**

Expand All @@ -252,6 +316,10 @@ pub struct DuplicatesConfig {
/// explicit import relationship are ignored (a re-export
/// is not a duplicate).
pub ignore_re_exports: bool,
/// When true (default), implements §2.1 **Rule 1** in the product
/// channel: pure nominal `type A = B` (no `where`) folds into `B`.
/// Rule 2 refinement twins use a separate channel and stay on.
pub ignore_pure_nominal_type_aliases: bool,
}

pub struct Duplicate {
Expand All @@ -268,6 +336,9 @@ pub enum DuplicateKind {
/// Two type declarations with compatible but differently-named
/// structures (e.g., same fields in different order).
CompatibleType,
/// Two refinement aliases naming the same (carrier, refinement)
/// fact — §2.1 Rule 2, channel (2).
IdenticalRefinementSurface,
}

impl StructuralDuplicatesLens {
Expand All @@ -282,31 +353,42 @@ impl StructuralDuplicatesLens {

1. Walk every declaration in `dag.declarations()` that matches
`config.include_types` or `config.include_data`.
2. For each type declaration, compute a structural hash over its
field shape: `hash({ (field_name, field_type_declaration_id)
for each field })`. For each data declaration, compute a
structural hash over its body: `hash(body_connective)`.
3. Collect hashes into a `HashMap<u64, Vec<DeclarationId>>`.
4. Emit a `Duplicate` for every hash with more than one
declaration.
2. **Product / coproduct / `data` channel:** For each declaration with
a materialized body, compute a structural hash over its field
layout or `data` connective. If `ignore_pure_nominal_type_aliases`
is set, apply **Rule 1**: omit or fold pure nominal `type A = B`
into `B`'s bucket (never emit alias-vs-canonical here).
3. **Refinement-alias channel:** For each `type Name = Carrier where …`,
compute `hash(resolved_carrier_id, canonical_refinement_id)`.

This comment was marked as resolved.

Apply **Rule 1** when comparing to bare `Carrier` (no false
collision). Apply **Rule 2** among refinement rows with the same
fingerprint.
4. Emit a `Duplicate` for every hash bucket that **Rule 2** says has
peer collisions, tagging `DuplicateKind` accordingly.
5. If `ignore_re_exports` is set, filter out duplicates where one
declaration imports the other transitively.

**Expected initial findings** (from the reviewer's audit):

- `FileClassification` / `FileEntry` in `dsl/std/filesystem.dag`
- `NonEmptyStr` / `NonEmptyString` in `dsl/std/types.dag`
- `wire_contract` in `llm.dag` vs `anthropic.dag` vs `openai.dag`
- `default_edition` in `cargo.dag` vs `rust/imports.dag`
- Probably others nobody has noticed yet

**Test plan:**

- Unit test: construct a Dag with two records of identical shape
and different names, assert the lens reports them.
- Unit test (**Rule 2**, product): two records, identical field maps,
different names — assert `IdenticalType` (or `CompatibleType`).
- Unit test: construct a Dag where one declaration re-exports
another; assert the lens does NOT report it when
`ignore_re_exports` is true.
- Unit test (**Rule 1**, product): one record plus `type Alias =
Record` (no `where`); assert **no** alias-vs-canonical duplicate when
`ignore_pure_nominal_type_aliases` is true (PR #596 shape).
- Unit test (**Rule 2**, refinement): `type X = String where p` and
`type Y = String where p` with the same canonical refinement id;
assert `IdenticalRefinementSurface` (alias-vs-alias, not
alias-vs-`String`).
- Unit test: construct a Dag with three data declarations of the
same value; assert the lens reports all three.
- Integration test: run the lens against `dsl/std/` and
Expand Down Expand Up @@ -792,11 +874,15 @@ The recommended order for building the initial library:
record return, block body, record literal in expression position)
and pinned by a parse-failure test that flips when the parser
grows those features.
2. **`lens_structural_duplicates`** — next. Simple structural hash
+ collision detection. Expected to catch the
`FileClassification`/`FileEntry` duplicate, the `wire_contract`
duplicates, `default_edition` duplication, and probably others.
Gives immediate value on existing std/ and extdeps/ code.
2. **`lens_structural_duplicates`** — next. §2.1 **Rules 1–2** across
two channels (product/`data` hash + refinement-surface hash).
Expected to catch the `wire_contract` duplicates,
`default_edition` duplication, `NonEmptyStr` / `NonEmptyString`
refinement twins (Rule 2), and probably others. (The
`FileClassification` / `FileEntry` duplicate from the same audit was
dissolved manually in PR #596 — Rule 1 covers `type
FileClassification = FileEntry` vs `FileEntry`.) Gives immediate
value on existing std/ and extdeps/ code.
3. **`lens_layer_opacity`** — third, the most sophisticated of the
three because it needs the `BoundarySpec` reverse index and
multiple consumer kinds. The one that validates the thesis's
Expand Down Expand Up @@ -914,10 +1000,14 @@ The library is successful when:
dsl/lens_config.dag` locally and see the same output the CI
sees.
3. **At least one high-value finding is closed by a lens-driven
fix.** Concrete target: the `FileClassification`/`FileEntry`
duplicate is surfaced by `lens_structural_duplicates`, fixed
by merging the two declarations, and the fix's regression
test is the lens returning empty on subsequent runs.
fix.** The `FileClassification`/`FileEntry` duplicate was fixed
ahead of the lens (PR #596: one record + `type FileClassification =
FileEntry`, i.e. **Rule 1** applies and must not regress). Concrete
remaining audit-class targets still include `wire_contract` /
`default_edition` and `NonEmptyStr` vs `NonEmptyString` (**Rule 2**
refinement peers). After fixes land, CI expects **Rule 2** clean
on those classes while **Rule 1** continues to suppress false
alias-vs-canonical pairs (§2.1).
4. **The existing layer-opacity grep-gate proposal in
`INVARIANTS.md` is fully superseded** — the §"Layer opacity"
invariant points at `lens_layer_opacity` as its primary
Expand Down
32 changes: 11 additions & 21 deletions dsl/std/filesystem.dag
Original file line number Diff line number Diff line change
Expand Up @@ -17,38 +17,28 @@ import std.types { FilePath, MimeType, EntryKind, SymlinkTarget }
// EntryKind and SymlinkTarget are defined in std.types (the lower module)
// and imported here to avoid circular dependencies.

// -- Layer 0.5: Classification (moved from types.dag) -------------------------

// What Filesystem.probe returns -- classifies a path's referent.
// Includes entry kind (regular file, directory, symlink, etc.)
// and symlink target resolution. The encoding field is optional
// because directories, missing paths, and special files have no encoding.
type FileClassification {
path: FilePath
kind: EntryKind
encoding: Encoding? // null for dirs/missing/other
symlink_target: SymlinkTarget? // null unless kind = Symlink
size: Int
mime: MimeType?
}

// -- Layer 1: Categories ---------------------------------------------------

// "What is a filesystem entry?" -- the complete invariant.
// This is what Filesystem.probe returns: everything we know about a path.
// -- Layer 0.5–1: File referent (single record) -----------------------------
//
// One carrier for "everything we know about a path's referent" — whether
// obtained from Filesystem.probe or held as an entry in a listing.
// Encoding is null for directories, missing paths, and special files;
// symlink_target is null unless kind = Symlink.
//
// Parallels Language in languages.dag:
// Language = { id, name, extensions, comment, naming, types }
// FileEntry = { path, kind, encoding?, symlink_target?, size, mime? }
type FileEntry {
path: FilePath
kind: EntryKind
encoding: Encoding? // only for RegularFile or Symlink->TargetFile
symlink_target: SymlinkTarget? // only for kind = Symlink
encoding: Encoding?
symlink_target: SymlinkTarget?
size: Int
mime: MimeType?
}

// API name for probe output — same carrier as FileEntry (P2 decompression).
type FileClassification = FileEntry

// "What is a readable file?" -- the subset we can fs.read().
// A path is readable when it resolves to a regular text file,
// either directly or through a symlink.
Expand Down
4 changes: 2 additions & 2 deletions dsl/std/types.dag
Original file line number Diff line number Diff line change
Expand Up @@ -406,8 +406,8 @@ type SymlinkTarget
type TextFilePath = FilePath where content(Text)
type BinaryFilePath = FilePath where content(Binary)

// FileClassification: moved to std/filesystem.dag (co-located with
// FileEntry and Encoding import from std/encoding.dag).
// FileEntry / FileClassification: std/filesystem.dag — one record, alias
// name for probe-shaped API; Encoding from std/encoding.dag.

type MimeType = String where pattern("^[a-z]+/[a-z0-9.+-]+$")

Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -7,7 +7,7 @@ dsl/std/float.dag 6 3155 2942092bfc8bff49
dsl/std/integer.dag 13 8930 bd26da8af7eca748
dsl/std/logic.dag 5 5586 c4823f2b02ffff2d
dsl/std/string_type.dag 4 1845 3810f615d6874bcd
dsl/std/types.dag 109 138959 e45860e122dcf5fd
dsl/std/types.dag 109 138959 b528343cf5a07a1e
src/v3/compiler/operators.dag 5 47157 b0bd76b89101c791
src/v3/compiler/pipeline.dag 26 47004 4df6f9da32f6a5b5
src/v3/compiler/regen.dag 10 27220 e7431380d0c23555
Expand Down
Loading