|
| 1 | +{-# OPTIONS --safe --without-K #-} |
| 2 | +-- SPDX-License-Identifier: MPL-2.0 |
| 3 | +-- Copyright (c) 2026 Jonathan D.A. Jewell (hyperpolymath) |
| 4 | +-- |
| 5 | +-- ===================================================================== |
| 6 | +-- EchoTyping — echo-types integrated into the type-theory pipeline |
| 7 | +-- ===================================================================== |
| 8 | +-- |
| 9 | +-- This module wires the hyperpolymath/echo-types library (the canonical, |
| 10 | +-- mechanised formalisation of *fiber-based structured loss*) into the |
| 11 | +-- nextgen-typing verification layer. The thesis is concrete: |
| 12 | +-- |
| 13 | +-- The pipeline's information-LOSING typing operations — affine |
| 14 | +-- weakening (AffineScript: linear ⊑ affine) and refinement erasure |
| 15 | +-- (surface type ⇒ kernel type) — are not ad-hoc. Each is an instance |
| 16 | +-- of echo-types' `Echo f y := Σ A (λ x → f x ≡ y)`, the proof-relevant |
| 17 | +-- record of *which* inputs a non-injective map collapses together. |
| 18 | +-- |
| 19 | +-- By depending on echo-types here, the type system and its formalisation |
| 20 | +-- share ONE mechanised notion of structured loss rather than two drifting |
| 21 | +-- definitions. Every theorem below is machine-checked under |
| 22 | +-- `--safe --without-K`, zero postulates, against the real echo-types |
| 23 | +-- source (registered in ~/.agda/libraries as `echo-types`). |
| 24 | +-- |
| 25 | +-- See: |
| 26 | +-- * echo-types `EchoLinear.agda` (linear/affine modes; `weaken`) |
| 27 | +-- * echo-types `EchoResidue.agda` (`no-section-collapse-to-residue`) |
| 28 | +-- * echo-types `Echo.agda` (the fiber type itself) |
| 29 | +-- * nextgen-typing main chain: katagoria → typell → typed-wasm → PanLL |
| 30 | +-- (AffineScript & Ephapax cross-language calls go via typed-wasm). |
| 31 | + |
| 32 | +module EchoTyping where |
| 33 | + |
| 34 | +open import Echo using (Echo; echo-intro) |
| 35 | +open import EchoCharacteristic using (echo-true; echo-false; echo-true≢echo-false) |
| 36 | +open import EchoLinear |
| 37 | + using ( Mode; linear; affine; LEcho; weaken |
| 38 | + ; weaken-collapses-distinction; no-section-weaken |
| 39 | + ; affine-canonical; affine-all-equal |
| 40 | + ; _≤m_; linear≤linear; linear≤affine; affine≤affine |
| 41 | + ; degradeMode; degradeMode-comp ) |
| 42 | + |
| 43 | +open import Data.Product.Base using (Σ; _,_; _×_; proj₁; proj₂) |
| 44 | +open import Data.Empty using (⊥) |
| 45 | +open import Relation.Nullary using (¬_) |
| 46 | +open import Relation.Binary.PropositionalEquality using (_≡_; _≢_; refl) |
| 47 | + |
| 48 | + |
| 49 | +-- ===================================================================== |
| 50 | +-- § 1. Affine weakening (AffineScript subtyping) is structured loss. |
| 51 | +-- ===================================================================== |
| 52 | +-- |
| 53 | +-- AffineScript types are affine: a `linear` value (used exactly once) |
| 54 | +-- may be subsumed to an `affine` value (used at most once). That |
| 55 | +-- subsumption FORGETS the linearity obligation. echo-types models the |
| 56 | +-- two modes as `LEcho linear` / `LEcho affine` and the subsumption as |
| 57 | +-- `weaken`. We re-export the load-bearing facts under typing names so a |
| 58 | +-- silent upstream change to echo-types trips this module. |
| 59 | + |
| 60 | +-- The subtyping coercion linear ⊑ affine. |
| 61 | +affine-weakening : LEcho linear → LEcho affine |
| 62 | +affine-weakening = weaken |
| 63 | + |
| 64 | +-- Two distinct linear typings become indistinguishable once weakened: |
| 65 | +-- the type system cannot tell them apart at affine mode. |
| 66 | +affine-subtyping-forgets : |
| 67 | + affine-weakening echo-true ≡ affine-weakening echo-false |
| 68 | +affine-subtyping-forgets = weaken-collapses-distinction |
| 69 | + |
| 70 | +-- No type checker can recover the linear typing from an affine one: |
| 71 | +-- the weakening coercion has NO section. This is the formal statement |
| 72 | +-- that affine subtyping is irreversibly information-losing. |
| 73 | +affine-subtyping-irreversible : |
| 74 | + ¬ (Σ (LEcho affine → LEcho linear) |
| 75 | + (λ reify → ∀ e → reify (affine-weakening e) ≡ e)) |
| 76 | +affine-subtyping-irreversible = no-section-weaken |
| 77 | + |
| 78 | +-- At affine mode every witness is equal: the linearity evidence is gone |
| 79 | +-- (affine typing is proof-irrelevant in its residue). |
| 80 | +affine-typing-proof-irrelevant : ∀ (e₁ e₂ : LEcho affine) → e₁ ≡ e₂ |
| 81 | +affine-typing-proof-irrelevant = affine-all-equal |
| 82 | + |
| 83 | +-- The subsumption order on modes, and its echo-types degradation action. |
| 84 | +subsume : ∀ {m₁ m₂ : Mode} → m₁ ≤m m₂ → LEcho m₁ → LEcho m₂ |
| 85 | +subsume = degradeMode |
| 86 | + |
| 87 | +-- Subtyping is coherent: coercing in two steps agrees with the direct |
| 88 | +-- coercion (degradation composes). Type inferred from echo-types so the |
| 89 | +-- pipeline inherits coherence rather than re-proving it. |
| 90 | +subsume-coherent = degradeMode-comp |
| 91 | + |
| 92 | + |
| 93 | +-- ===================================================================== |
| 94 | +-- § 2. Refinement erasure is a fiber (the Echo of erasure). |
| 95 | +-- ===================================================================== |
| 96 | +-- |
| 97 | +-- A surface type system carries refinements (`pos`, `even`) that the |
| 98 | +-- typed-wasm / kernel layer erases to a single base type. Erasure is |
| 99 | +-- the lossy classifier; its Echo at the kernel type records WHICH |
| 100 | +-- surface refinement was discarded. This is a self-contained worked |
| 101 | +-- example: it builds the fiber, not merely re-exports it. |
| 102 | + |
| 103 | +data SurfaceTy : Set where |
| 104 | + nat : SurfaceTy -- the base type |
| 105 | + pos : SurfaceTy -- refinement: a positive nat |
| 106 | + even : SurfaceTy -- refinement: an even nat |
| 107 | + |
| 108 | +data KernelTy : Set where |
| 109 | + Nat : KernelTy |
| 110 | + |
| 111 | +-- The kernel forgets all refinements: a non-injective erasure. |
| 112 | +erase : SurfaceTy → KernelTy |
| 113 | +erase _ = Nat |
| 114 | + |
| 115 | +-- The structured loss of erasure at `Nat`: which surface type erased here. |
| 116 | +ErasedFrom : KernelTy → Set |
| 117 | +ErasedFrom k = Echo erase k |
| 118 | + |
| 119 | +-- `pos` and `even` are distinct surface typings whose Echoes both live |
| 120 | +-- over the SAME kernel type — the refinement is lost in the codomain but |
| 121 | +-- retained in the fiber. |
| 122 | +echo-from-pos : ErasedFrom Nat |
| 123 | +echo-from-pos = echo-intro erase pos |
| 124 | + |
| 125 | +echo-from-even : ErasedFrom Nat |
| 126 | +echo-from-even = echo-intro erase even |
| 127 | + |
| 128 | +-- Distinct surface refinements really are distinct (the loss is real). |
| 129 | +surface-distinct : pos ≢ even |
| 130 | +surface-distinct () |
| 131 | + |
| 132 | +-- Erasure is non-injective, witnessed concretely: two surface types that |
| 133 | +-- erase to one kernel type yet are not equal. `Echo erase Nat` is the |
| 134 | +-- object the kernel would need to invert erasure — and cannot, in |
| 135 | +-- general, by the same no-section argument as affine weakening. |
| 136 | +erasure-non-injective : |
| 137 | + Σ SurfaceTy (λ s₁ → Σ SurfaceTy (λ s₂ → |
| 138 | + (erase s₁ ≡ erase s₂) × (s₁ ≢ s₂))) |
| 139 | +erasure-non-injective = pos , even , refl , surface-distinct |
| 140 | + |
| 141 | + |
| 142 | +-- ===================================================================== |
| 143 | +-- § 3. Headline pins (these names are the public typing API of Echo). |
| 144 | +-- ===================================================================== |
| 145 | +-- |
| 146 | +-- TP-ECHO-1 : affine subtyping forgets a distinction (§1) |
| 147 | +-- TP-ECHO-2 : affine subtyping is irreversible (no section)(§1) |
| 148 | +-- TP-ECHO-3 : refinement erasure is non-injective (§2) |
| 149 | +-- |
| 150 | +-- A green typecheck of this module is the proof that the pipeline's |
| 151 | +-- structured-loss typing operations are exactly echo-types echoes. |
| 152 | + |
| 153 | +TP-ECHO-1 : affine-weakening echo-true ≡ affine-weakening echo-false |
| 154 | +TP-ECHO-1 = affine-subtyping-forgets |
| 155 | + |
| 156 | +TP-ECHO-2 : |
| 157 | + ¬ (Σ (LEcho affine → LEcho linear) |
| 158 | + (λ reify → ∀ e → reify (affine-weakening e) ≡ e)) |
| 159 | +TP-ECHO-2 = affine-subtyping-irreversible |
| 160 | + |
| 161 | +TP-ECHO-3 : |
| 162 | + Σ SurfaceTy (λ s₁ → Σ SurfaceTy (λ s₂ → |
| 163 | + (erase s₁ ≡ erase s₂) × (s₁ ≢ s₂))) |
| 164 | +TP-ECHO-3 = erasure-non-injective |
0 commit comments