|
| 1 | += The Echo abstraction barrier (consumer-side, narrow scope) |
| 2 | +:toc: macro |
| 3 | +:toclevels: 2 |
| 4 | +:sectnums: |
| 5 | +:sectnumlevels: 2 |
| 6 | +:icons: font |
| 7 | + |
| 8 | +[.lead] |
| 9 | +Companion essay to `proofs/agda/EchoAbstractionBarrier.agda`. The |
| 10 | +module ships two theorems and a deliberately narrow scope. This file |
| 11 | +explains the narrowness — what the abstraction barrier is, what it |
| 12 | +guarantees, what it does *not* guarantee, and why the narrow form is |
| 13 | +the strongest honest statement available under |
| 14 | +`--safe --without-K`. |
| 15 | + |
| 16 | +[IMPORTANT] |
| 17 | +==== |
| 18 | +This is Track B of the "Echo ≠ Σ" identity-claim consolidation |
| 19 | +(`roadmap.adoc` §Lane 2; sceptic-facing map at |
| 20 | +`core/skepticisms/is-this-just-sigma-types.md` §4). The theorems below |
| 21 | +respect the R-2026-05-18 retraction discipline: the claim is a |
| 22 | +*consumer-side free theorem at the headline affine instance*, NOT a |
| 23 | +general Reynolds-style parametricity result. The scope narrowness is |
| 24 | +load-bearing. |
| 25 | +==== |
| 26 | + |
| 27 | +toc::[] |
| 28 | + |
| 29 | +== What an abstraction barrier means here |
| 30 | + |
| 31 | +A raw dependent pair `Σ A (λ x → f x ≡ y)` exposes `proj₁`. A consumer |
| 32 | +of such a pair can always recover the original `x`. That makes the |
| 33 | +"forgetting" half of any loss-grade story a *convention*, not a |
| 34 | +guarantee — nothing in the type stops the consumer from looking. |
| 35 | + |
| 36 | +The Echo interface, at the affine mode, refuses to export `proj₁`. |
| 37 | +But "refuses to export" is meaningless prose without a checked |
| 38 | +artefact: a sceptic reasonably asks "what stops me writing |
| 39 | +`proj₁ ∘ to-sigma`?" The abstraction barrier is the answer. It is |
| 40 | +the pair of theorems that, together, say: |
| 41 | + |
| 42 | +. *At the affine instance, no consumer can do what the Σ-projection |
| 43 | + does.* (Theorem `affine-consumer-cannot-distinguish`.) |
| 44 | +. *The Σ-projection does it.* (Theorem `sigma-distinguishes`.) |
| 45 | + |
| 46 | +The first is the guarantee. The second is the negative companion that |
| 47 | +makes the guarantee non-trivial: it exhibits the concrete behaviour |
| 48 | +the affine interface is designed to prevent. |
| 49 | + |
| 50 | +== The two theorems |
| 51 | + |
| 52 | +=== `affine-consumer-cannot-distinguish` |
| 53 | + |
| 54 | +[source,agda] |
| 55 | +---- |
| 56 | +affine-consumer-cannot-distinguish : |
| 57 | + {X : Set ℓ} (g : LEcho affine → X) → |
| 58 | + g (weaken echo-true) ≡ g (weaken echo-false) |
| 59 | +affine-consumer-cannot-distinguish g = |
| 60 | + cong g (affine-all-equal (weaken echo-true) (weaken echo-false)) |
| 61 | +---- |
| 62 | + |
| 63 | +Any consumer `g` at the affine mode produces the same result on the |
| 64 | +two known-distinct linear echoes (`echo-true` and `echo-false`) after |
| 65 | +they have been weakened. This holds *for every consumer type* `X` and |
| 66 | +*every function* `g : LEcho affine → X`, because the affine residue |
| 67 | +carrier is contractible — `EchoLinear.affine-canonical` and |
| 68 | +`affine-all-equal` discharge it in one `cong`. |
| 69 | + |
| 70 | +The reason this is non-trivial: the underlying linear echoes ARE |
| 71 | +distinguishable. `EchoCharacteristic.echo-true≢echo-false` is a |
| 72 | +theorem. The barrier is that crossing from linear to affine via |
| 73 | +`weaken` collapses the distinction *structurally*, and no affine |
| 74 | +consumer can recover it. The Σ-projection on the linear side would |
| 75 | +recover it; the Σ-projection on the affine side cannot, because the |
| 76 | +affine carrier has only one inhabitant up to definitional equality. |
| 77 | + |
| 78 | +=== `sigma-distinguishes` |
| 79 | + |
| 80 | +[source,agda] |
| 81 | +---- |
| 82 | +sigma-distinguishes : |
| 83 | + Σ (Echo collapse tt → Bool) |
| 84 | + (λ g → g echo-true ≢ g echo-false) |
| 85 | +sigma-distinguishes = proj₁ , true≢false |
| 86 | +---- |
| 87 | + |
| 88 | +The Σ-projection `proj₁ : Echo collapse tt → Bool` IS a consumer that |
| 89 | +distinguishes `echo-true` from `echo-false`. The proof is `true≢false` |
| 90 | +directly, because `proj₁ (echo-intro collapse true)` reduces |
| 91 | +definitionally to `true` (via `echo-intro f x = x , refl`) and the |
| 92 | +mirror case reduces to `false`. |
| 93 | + |
| 94 | +This is the load-bearing artefact. Without it, the claim "the affine |
| 95 | +interface refuses `proj₁`" is content-free — what would `proj₁` even |
| 96 | +do? The negative companion answers exactly that question, and the |
| 97 | +answer is "distinguish the two linear echoes". The affine interface |
| 98 | +deliberately refuses to export it. |
| 99 | + |
| 100 | +== What this is NOT |
| 101 | + |
| 102 | +The scope guardrail in the module preamble lists three narrowings. |
| 103 | +They are repeated here in essay form because external readers tend to |
| 104 | +read essays before module headers, and the narrowings are the most |
| 105 | +load-bearing thing about this module. |
| 106 | + |
| 107 | +=== Not full Reynolds parametricity |
| 108 | + |
| 109 | +A general Reynolds-style result would say: for every consumer type |
| 110 | +`X`, every echo carrier `A`, every map `f : A → B`, every output |
| 111 | +`y : B`, and every function `g : Echo f y → X` *at the appropriate |
| 112 | +interface*, `g` cannot inspect `x` beyond what the interface allows. |
| 113 | +Agda has no parametricity primitive. Stating this requires either an |
| 114 | +axiom or a paper-level metatheorem. Both violate the no-postulate |
| 115 | +invariant. |
| 116 | + |
| 117 | +The narrow form here — consumer-side at the headline affine instance |
| 118 | +— is what survives `--safe --without-K`. It says the right thing at |
| 119 | +the one instance where the carrier is contractible and the |
| 120 | +quantification over consumers (`{X : Set ℓ}`) is non-vacuous because |
| 121 | +*every* consumer satisfies the equation. |
| 122 | + |
| 123 | +=== Not a higher-order parametricity claim |
| 124 | + |
| 125 | +`affine-consumer-cannot-distinguish` does not claim that consumers |
| 126 | +*cannot detect the difference between two linear preimages*. It |
| 127 | +claims that consumers *of weakened linear preimages* assign them the |
| 128 | +same value. The detection happens on the linear side (and is the |
| 129 | +content of `echo-true≢echo-false`); the barrier is at the |
| 130 | +linear→affine boundary, and the theorem is what survives crossing it. |
| 131 | + |
| 132 | +=== Not a categorical universal property |
| 133 | + |
| 134 | +The Echo interface is not characterised in this module as a terminal |
| 135 | +cone over anything. The pullback characterisation lives in |
| 136 | +`EchoPullback.agda` and is itself narrowed (per R-2026-05-18) to a |
| 137 | +funext-relative pointwise mediator property. The abstraction barrier |
| 138 | +here is a separate, narrower claim that does not depend on the |
| 139 | +pullback machinery. |
| 140 | + |
| 141 | +== Why two theorems and not one |
| 142 | + |
| 143 | +A single positive theorem (`cannot-distinguish`) is a wish without |
| 144 | +the negative companion. The reader can always ask: "but couldn't some |
| 145 | +other consumer, written cleverly, distinguish them anyway?" The |
| 146 | +answer at the affine instance is *no*, and the reason is structural |
| 147 | +(`affine-canonical`). But the reader's question deserves a checked |
| 148 | +answer, not a structural argument. The negative companion provides |
| 149 | +it: the only consumer that distinguishes the two linear echoes is |
| 150 | +`proj₁` or a function of `proj₁`, and that is *exactly* the function |
| 151 | +the affine interface refuses to export. |
| 152 | + |
| 153 | +The pair is the artefact. Either alone is half the story. |
| 154 | + |
| 155 | +== Honest comparison to neighbour disciplines |
| 156 | + |
| 157 | +* *Granule / QTT.* Stronger general parametricity available via the |
| 158 | + language's quantitative judgments. Echo's claim here is narrower |
| 159 | + (instance-level, consumer-side, in Agda without a parametricity |
| 160 | + primitive). See `docs/echo-types/comparators.adoc` for the |
| 161 | + axis-by-axis breakdown. |
| 162 | +* *Linear Haskell.* The linearity-mode information is at the type |
| 163 | + level but Haskell consumers can still inspect linear values via |
| 164 | + `seq` and other escape hatches. Echo's contractibility argument |
| 165 | + closes that gap at the affine carrier specifically, because the |
| 166 | + carrier *is* a singleton up to definitional equality. |
| 167 | +* *Lens / optic laws.* The witness-transport leg of `map-over` looks |
| 168 | + optic-shaped but the affine-mode contractibility argument has no |
| 169 | + optic analogue: lenses can inspect their source via `view`. Echo's |
| 170 | + refusal of `proj₁` at affine mode is the structural difference. |
| 171 | + |
| 172 | +== Cross-references |
| 173 | + |
| 174 | +* Agda module: `proofs/agda/EchoAbstractionBarrier.agda` (this file's |
| 175 | + companion). |
| 176 | +* Sceptic-facing map: `core/skepticisms/is-this-just-sigma-types.md` |
| 177 | + §4 and `docs/echo-types/sigma-distinctness-map.adoc` §"Demand 4". |
| 178 | +* The retraction governing the narrowing discipline: |
| 179 | + `docs/retractions.adoc` R-2026-05-18. |
| 180 | +* Carrier-parametricity (model side): `EchoRelModel.agda` and |
| 181 | + `docs/echo-types/conservativity.adoc`. That work is at the *model* |
| 182 | + level (Pillar D); this module is at the *consumer* level — the two |
| 183 | + are not the same statement. |
| 184 | +* Comparator framing: `docs/echo-types/comparators.adoc`. |
0 commit comments