|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | += Correspondence Model: the engine that *classifies*, not translates |
| 3 | +:toc: macro |
| 4 | +:toclevels: 3 |
| 5 | +:icons: font |
| 6 | + |
| 7 | +[NOTE] |
| 8 | +==== |
| 9 | +*Status: living design spec.* This is the conceptual foundation for the engine — |
| 10 | +authored ahead of the toolchain (AffineScript/Idris2/Zig not yet installable here), so |
| 11 | +it is verified by inspection against estate exemplars, not yet by build. One worked |
| 12 | +example (JTV grammar v2) is stubbed pending repository access; see <<open-questions>>. |
| 13 | +==== |
| 14 | + |
| 15 | +toc::[] |
| 16 | + |
| 17 | +== What this engine is (and is not) |
| 18 | + |
| 19 | +This is *Duolingo / Rosetta Stone for programming languages* — a |
| 20 | +language-*comprehension and transfer* engine. It works **one layer above text |
| 21 | +editing**, on *syntactic and semantic intention*, so that the effort a person spent |
| 22 | +learning language A *transfers* when they move to B (JS → TypeScript, Ruby, Prolog, C, |
| 23 | +or exotic targets like QPL, Arrow, JTV). *Transfer learning across languages is the |
| 24 | +product.* |
| 25 | + |
| 26 | +It is *not*: |
| 27 | + |
| 28 | +* *Not "the next best IDE."* It does not compete on contrast, project-management |
| 29 | + widgets, pop-up notepads, shortcuts, or well-trodden attention/memory/workflow |
| 30 | + ergonomics. That is **PanLL**'s job (PanLL + eNSAID = the _contact_ between human, |
| 31 | + tool, task, and environment). This engine *feeds* PanLL; it is not PanLL. |
| 32 | +* *Not a linter.* "Proximal/distal scope-colouring" and "spot the missing `;` / extra |
| 33 | + `)`" are precisely what this is *not*. The differentiator is an engine that |
| 34 | + **computes and classifies cross-language equivalence**, not one that looks it up. |
| 35 | +* *Not a universal translator.* A verified any-language→any-language compiler with full |
| 36 | + Curry–Howard fidelity would be nice; it is *not the goal*. We do not need — and will |
| 37 | + not attempt — to do this "to the dot" on everything. |
| 38 | + |
| 39 | +== Division of labour |
| 40 | + |
| 41 | +[cols="1,3"] |
| 42 | +|=== |
| 43 | +| *We build* | the general engine + the interface + the classification vocabulary + |
| 44 | +the residue model + a reference language pack. |
| 45 | +| *The community builds* | the *per-language modules* — which pairs of constructs are |
| 46 | +cognate vs. false-friend vs. novel, with their residues. These are authored as |
| 47 | +**cartridges** (see `standards/cartridges/`). |
| 48 | +|=== |
| 49 | + |
| 50 | +The engine is language-agnostic. The nextgen-language collection is merely the |
| 51 | +substrate we dogfood. |
| 52 | + |
| 53 | +== The object model: Concept / Form / Transition |
| 54 | + |
| 55 | +[cols="1,3"] |
| 56 | +|=== |
| 57 | +| *Concept* | The invariant / equivalence-class — the recurring _trope_ (e.g. |
| 58 | +"bind a name to a value", "iterate a collection", "fail recoverably"). |
| 59 | +| *Form* | A representative of a Concept *in one language* (e.g. `let` in ReScript, |
| 60 | +`=` in Erlang, `def` in Python). A Concept has many Forms across many languages. |
| 61 | +| *Transition* | A directed correspondence Form(A) → Form(B): the Echo-refined map |
| 62 | +plus its *residue* (what is lost, added, or inverted in crossing). |
| 63 | +|=== |
| 64 | + |
| 65 | +A *lesson* is a Concept presented through the learner's known Form, the target Form, |
| 66 | +and the Transition between them — narrated without shame ("you already know this; |
| 67 | +here's the catch"). |
| 68 | + |
| 69 | +== Levels of objects (strata) |
| 70 | + |
| 71 | +Classification runs *per stratum of meaning*, not on flat text: |
| 72 | + |
| 73 | +. *Surface* — tokens, lexemes (`=`, `def`, `match`). |
| 74 | +. *Structure* — AST shape, scoping, arity. |
| 75 | +. *Semantic intention* — what the construct _does_ (bind? mutate? branch?). |
| 76 | +. *Abstraction / trope* — the Concept it instantiates. |
| 77 | +. *Cross-language invariant* — the preserved quantity certifying "same idea". |
| 78 | + |
| 79 | +The interface lets a learner move *up and down* these strata and *across* view-modes. |
| 80 | +A correspondence can hold at one stratum and break at another — and that divergence is |
| 81 | +itself the most valuable signal (see false friends, below). |
| 82 | + |
| 83 | +== The formal carrier |
| 84 | + |
| 85 | +The model is grounded in the estate's own formalism, not a bespoke mapping table. |
| 86 | + |
| 87 | +* *Carrier = Dyadic `Relation`* |
| 88 | + (`proven-tests-and-benches/src/ProvenTests/TypeSafe/Dyadic.idr`): |
| 89 | + `{ relates; reflexive; symmetric; transitive }`. Equivalence = refl ∧ sym ∧ trans — |
| 90 | + the symmetries and transitivities, as a checkable structure. |
| 91 | +* *Crossings are lossy-with-residue = Echo fibre* |
| 92 | + (`Echo f y := Σ (x : A), f x ≡ y`, `hyperpolymath/echo-types`, Agda): the residue |
| 93 | + (a proof term) is precisely _what is lost or added_ going A→B. A non-isomorphic |
| 94 | + Transition (e.g. the absence of `return` in ReScript) is a map whose residue we |
| 95 | + *surface*, never hide. |
| 96 | +* *Typed residue-lenses = the three Echo bridges* (`Bridge.idr`): `EchoChoreo` |
| 97 | + (protocol/sequencing), `EchoEpistemic` (visibility/knowledge), `EchoTropical` |
| 98 | + (cost, min-plus). Extensible. |
| 99 | +* *Composition = transitivity; symmetry distinguishes iso from retraction.* A clean |
| 100 | + isomorphism ⇒ no residue (true equivalence); a retraction ⇒ one-way loss |
| 101 | + (residue = the delta). |
| 102 | +* *`invariant-path` = the governance front-end.* It anchors each equivalence _claim_ to |
| 103 | + its two code locations plus a witness (proof/test), human-in-the-loop and editable. |
| 104 | + |
| 105 | +[IMPORTANT] |
| 106 | +==== |
| 107 | +*Honesty note on "knot theory."* The owner's framing — *types → carrier · tropes → |
| 108 | +recurring equivalence-figures · knot theory → certificate* — is load-bearing for |
| 109 | +intuition, but there is *no literal knot-invariant computation* here, and the |
| 110 | +knot-theory lens is flagged (by the owner) as "perceived as rhetoric, pending |
| 111 | +historical confirmation". We use *invariant* in the precise sense of a _preserved |
| 112 | +quantity that certifies "same idea"_, and keep knot theory as an aspirational lens, not |
| 113 | +a faked dependency. |
| 114 | +==== |
| 115 | + |
| 116 | +[#taxonomy] |
| 117 | +== The Rosetta false-friends taxonomy |
| 118 | + |
| 119 | +The one judgement that matters is *"is this safe to transfer, or is it a trap?"* |
| 120 | +`def` → `define` might be _nothing but a rename_ — or it might look like that and not |
| 121 | +be. So the Dyadic relation is not a boolean `relates`; it is a *typed/graded* |
| 122 | +`CorrespondenceKind`, realised as grades of the Echo fibre: |
| 123 | + |
| 124 | +[cols="1,3,2"] |
| 125 | +|=== |
| 126 | +| Kind | Signature | Pedagogy |
| 127 | + |
| 128 | +| *Cognate / true friend* |
| 129 | +| Intention + behaviour coincide; residue ≈ ∅. _Example:_ `def` → `define`. |
| 130 | + But "just a rename" is a hypothesis to *verify*, never assume. |
| 131 | +| *Transfer directly.* |
| 132 | + |
| 133 | +| *False friend / homonym* |
| 134 | +| Surface matches, semantics diverge. _Example:_ BASIC `=` (mutable assignment) vs. |
| 135 | + Erlang `=` (single-assignment bind/unify). Detected by *per-stratum* classification: |
| 136 | + surface-corresponds ∧ semantics-diverge **is** the false-friend signature. |
| 137 | +| *Flag the trap.* |
| 138 | + |
| 139 | +| *Antonym / inverted* |
| 140 | +| Related but behaves oppositely. _Examples:_ 0- vs. 1-indexing; truthiness |
| 141 | + conventions; stack-growth direction. Residue = the flip. |
| 142 | +| *Remap the intuition.* |
| 143 | + |
| 144 | +| *Alien realization* |
| 145 | +| Same intention, foreign mechanism, large residue. _Example:_ subtraction in a |
| 146 | + reversible/add-only language (JTV) is `add` run backwards; divide via reversed |
| 147 | + repeated-add. Also: recursion-only languages, CPS, monadic IO for "just print". |
| 148 | +| *Bridge with effort; explain the machinery.* |
| 149 | + |
| 150 | +| *Novel / no anchor* |
| 151 | +| Forward fibre empty: `∄ x. f x ≡ y`. The target has a concept with nothing to map |
| 152 | + _from_. _Examples:_ static types coming from assembly + JS; ownership/borrowing; |
| 153 | + affine/linear use-once; Prolog `cut`; JTV totality and information-flow labels. |
| 154 | +| *Teach de novo — there is no transfer.* |
| 155 | + |
| 156 | +| *Vanished* |
| 157 | +| Backward fibre empty: `∄ y`. A concept the learner relied on is _gone_. |
| 158 | + _Examples:_ `return` in ReScript; `null` in a null-free language; mutable variables |
| 159 | + in a pure language. |
| 160 | +| *Un-learn / re-route.* |
| 161 | +|=== |
| 162 | + |
| 163 | +The residue therefore ranges from ∅ (true iso) through inverted/large to |
| 164 | +empty-in-either-direction (novel / vanished). This taxonomy *is* the Duolingo/Rosetta |
| 165 | +pedagogy: transfer cognates, warn on false friends, remap antonyms, bridge the alien, |
| 166 | +teach the novel, re-route the vanished. |
| 167 | + |
| 168 | +== Engine ↔ cartridge boundary |
| 169 | + |
| 170 | +We cannot do this "to the dot", and we do not try. Responsibilities split cleanly: |
| 171 | + |
| 172 | +* *Engine (ours):* the `CorrespondenceKind` vocabulary, the residue/fibre model, the |
| 173 | + per-stratum classifier, the Dyadic/Echo carrier, and the certifiable Idris2/Echo math |
| 174 | + — applied *where it pays* (high-value or dangerous correspondences), not everywhere. |
| 175 | +* *Cartridge (per-language, community):* the _facts_ — for this language, which Forms |
| 176 | + instantiate which Concepts, and for each Transition the kind + residue + a witness. |
| 177 | + |
| 178 | +A cartridge fact, sketched: |
| 179 | + |
| 180 | +[source] |
| 181 | +---- |
| 182 | +(transition |
| 183 | + (concept "name-binding") |
| 184 | + (from (lang "basic") (form "X = 5")) |
| 185 | + (to (lang "erlang") (form "X = 5")) |
| 186 | + (kind false-friend) ; surface-cognate, semantic-divergent |
| 187 | + (strata (surface corresponds) (semantic diverges)) |
| 188 | + (residue "BASIC rebinds destructively; Erlang binds once and unifies — \ |
| 189 | + re-`=` fails unless the value matches") |
| 190 | + (witness "proofs/erlang_single_assignment.idr")) ; optional, where it pays |
| 191 | +---- |
| 192 | + |
| 193 | +== Rendering: "levels of objects", not chrome |
| 194 | + |
| 195 | +The view-modes are the rendered strata, switchable and non-destructive (each conforms |
| 196 | +to the estate *overlay-protocol* — additive, non-modifying, idempotent, Idris2-ABI |
| 197 | +proved): |
| 198 | + |
| 199 | +* *focus* — show only what's needed now; |
| 200 | +* *glyph* — Makaton-style symbols (accessible, low-cognitive-load); |
| 201 | +* *blockly / scratch* — flowchart of structure; |
| 202 | +* *raw code* — the text itself; |
| 203 | +* *side-by-side* — multi-language diff with step-sync. |
| 204 | + |
| 205 | +Accessibility is a first-class contract, not a coat of paint: Hyperpolymath |
| 206 | +Accessibility Standard, Level *A* minimum → *AA* (keyboard-only operation, ≥4.5:1 |
| 207 | +contrast, colourblind-safe palettes, ARIA/screen-reader, reduced-motion, plain-language |
| 208 | +mode, high-contrast glyph variants). |
| 209 | + |
| 210 | +== Downstream: feeding PanLL |
| 211 | + |
| 212 | +The engine *emits*, it does not own the IDE. Analyses become `octads` written to |
| 213 | +VeriSimDB (`:8097`) plus `Groove` signals; PanLL panels subscribe and re-render. |
| 214 | +Relevant octad types: `inline-annotation` (per-construct claims), |
| 215 | +`ecosystem-link` (intra-program relationships), `proof-status` (where a Transition |
| 216 | +carries a witness). Ergonomics are read from `.machine_readable/ENSAID_CONFIG.a2ml`. |
| 217 | + |
| 218 | +[#open-questions] |
| 219 | +== Open questions / placeholders |
| 220 | + |
| 221 | +* *JTV grammar v2* — the canonical worked example for *alien-realization* and |
| 222 | + *novel/no-anchor* kinds. The `julia-the-viper` repo is a not-checked-out submodule |
| 223 | + and currently outside session scope; constructs to be tagged against <<taxonomy>> |
| 224 | + once the grammar is available. From the T1 proof spec, JTV is reversible + total + |
| 225 | + effect-typed (I/O, state, crypto) + information-flow-typed (public/private/secret) + |
| 226 | + capability-secured — i.e. dense with novel-concept correspondences. |
| 227 | +* *Stratum granularity* — whether 5 strata suffice, or "intention" needs splitting |
| 228 | + (operational vs. denotational). |
| 229 | +* *Where the math pays* — the policy for when a Transition _must_ carry an Idris2/Echo |
| 230 | + witness vs. an asserted-but-unproven classification. |
| 231 | + |
| 232 | +== References |
| 233 | + |
| 234 | +* `proven-tests-and-benches/src/ProvenTests/TypeSafe/Dyadic.idr`, `…/Bridge.idr` |
| 235 | +* `hyperpolymath/echo-types` — loss-with-residue (Agda) |
| 236 | +* `standards/overlay-protocol/`, `standards/ensaid-config/`, |
| 237 | + `standards/accessibility/`, `standards/cartridges/`, `standards/panll-panels/` |
0 commit comments