Abstraction model (track 2): Idris2 ABI core — Concept/Form/Transition + CorrespondenceKind

abi.ipkg

@@ -0,0 +1,26 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+--
+-- Idris2 package for the formally-typed ABI seam of the correspondence engine.
+--
+-- The seam lives in a single, case-consistent directory src/interface/Abi/
+-- (uppercase) so the physical path matches the `module Abi.*` namespace on
+-- EVERY filesystem (Idris2 requires capitalised namespace components).
+--
+-- Typecheck with the package (not a bare --check, which warns on module/path):
+--   idris2 --typecheck abi.ipkg      (or --build)
+
+package abi
+
+version = 0.1.0
+
+authors = "Jonathan D.A. Jewell"
+
+brief = "Formally-typed ABI seam (Idris2): Concept/Form/Transition + the six CorrespondenceKinds, grounded in Dyadic + Echo"
+
+sourcedir = "src/interface"
+
+depends = base
+
+modules = Abi.Carrier
+        , Abi.Correspondence

src/interface/Abi/Carrier.idr

@@ -0,0 +1,59 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+|||
+||| Abi.Carrier — the formal carrier of a cross-language equivalence *claim*.
+|||
+||| This is ORIGINAL MPL-2.0 code. It is conceptually grounded in — but does
+||| not import — two estate libraries, to keep the licence clean:
+|||
+|||   * the Dyadic `Relation` (reflexive/symmetric/transitive) from
+|||     hyperpolymath/proven-tests-and-benches  (AGPL-3.0-or-later, son-shared)
+|||   * the Echo loss-with-residue fibre `Echo f y := Sigma (x : A), f x = y`
+|||     from hyperpolymath/echo-types            (Agda)
+|||
+||| Importing the AGPL library into this MPL-2.0 repo would relicense it by
+||| linkage; the shapes are re-expressed here as fresh MPL-2.0 source instead.
+
+module Abi.Carrier
+
+%default total
+
+||| A binary relation over `a` together with its (asserted) algebraic
+||| properties. The carrier of an equivalence *claim*: a Concept is "the same
+||| idea" across Forms exactly when this relation is an equivalence.
+public export
+record Relation (a : Type) where
+  constructor MkRelation
+  name       : String
+  relates    : a -> a -> Bool
+  reflexive  : Bool
+  symmetric  : Bool
+  transitive : Bool
+
+||| Equivalence = reflexive AND symmetric AND transitive.
+public export
+isEquivalence : Relation a -> Bool
+isEquivalence (MkRelation _ _ r s t) = r && s && t
+
+||| The residue of a crossing A -> B: *what is lost, added, or inverted*.
+||| These are the grades of the Echo fibre, from empty (true iso) through
+||| inverted / lossy to empty-in-either-direction.
+public export
+data Residue : Type where
+  ||| True isomorphism — nothing lost (the fibre is inhabited and unique).
+  None         : Residue
+  ||| The crossing is a flip (e.g. 0- vs 1-indexing). Carries a note.
+  Inverted     : String -> Residue
+  ||| One-way loss / added machinery (a retraction): same intention, foreign
+  ||| mechanism. Carries a note of the machinery.
+  Lossy        : String -> Residue
+  ||| Forward fibre empty: the target concept has no source anchor. (Novel.)
+  AbsentSource : String -> Residue
+  ||| Backward fibre empty: the source concept has vanished in the target.
+  AbsentTarget : String -> Residue
+
+||| Is this crossing a true isomorphism (no residue)?
+public export
+isIso : Residue -> Bool
+isIso None = True
+isIso _    = False

src/interface/Abi/Correspondence.idr

@@ -0,0 +1,149 @@
+-- SPDX-License-Identifier: MPL-2.0
+-- Copyright (c) 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+|||
+||| Abi.Correspondence — the abstraction model: Concept / Form / Transition and
+||| the six graded CorrespondenceKinds. The formal heart of an engine that
+||| *classifies* cross-language correspondences (it does not translate, and
+||| claims no Curry-Howard fidelity). See docs/theory/CORRESPONDENCE-MODEL.adoc.
+
+module Abi.Correspondence
+
+import Abi.Carrier
+
+%default total
+
+--------------------------------------------------------------------------------
+-- Strata ("levels of objects")
+--------------------------------------------------------------------------------
+
+||| The strata of meaning. Classification runs *per stratum*: a correspondence
+||| can hold at one and break at another — and that divergence is the signal.
+public export
+data Stratum = Surface | Structure | Intention | Trope | Invariant
+
+public export
+Eq Stratum where
+  (==) Surface   Surface   = True
+  (==) Structure Structure = True
+  (==) Intention Intention = True
+  (==) Trope     Trope     = True
+  (==) Invariant Invariant = True
+  (==) _         _         = False
+
+--------------------------------------------------------------------------------
+-- The six CorrespondenceKinds (graded Echo fibres)
+--------------------------------------------------------------------------------
+
+||| The kind of a cross-language correspondence — a typed/graded verdict, not a
+||| boolean "relates". Each kind is a grade of the Echo fibre with a pedagogy.
+public export
+data CorrespondenceKind : Type where
+  ||| Intention + behaviour coincide; residue ~ empty. e.g. `def` -> `define`.
+  Cognate : CorrespondenceKind
+  ||| Surface matches, semantics diverge. e.g. BASIC `=` vs Erlang `=`.
+  FalseFriend : CorrespondenceKind
+  ||| Related but inverted. e.g. 0- vs 1-indexing.
+  Antonym : CorrespondenceKind
+  ||| Same intention, foreign mechanism, large residue. e.g. subtraction in JTV
+  ||| (reversible / add-only) is `add` run backwards.
+  AlienRealization : CorrespondenceKind
+  ||| Forward fibre empty: nothing to map from. e.g. static types from asm+JS.
+  Novel : CorrespondenceKind
+  ||| Backward fibre empty: a relied-on concept is gone. e.g. `return` in ReScript.
+  Vanished : CorrespondenceKind
+
+public export
+Eq CorrespondenceKind where
+  (==) Cognate          Cognate          = True
+  (==) FalseFriend      FalseFriend      = True
+  (==) Antonym          Antonym          = True
+  (==) AlienRealization AlienRealization = True
+  (==) Novel            Novel            = True
+  (==) Vanished         Vanished         = True
+  (==) _                _                = False
+
+||| The pedagogy prescribed by each kind.
+public export
+data Pedagogy = Transfer | Warn | Remap | Bridge | TeachDeNovo | ReRoute
+
+||| Total map: every kind has exactly one pedagogy. No shame — even the traps
+||| are taught, not scolded.
+public export
+pedagogy : CorrespondenceKind -> Pedagogy
+pedagogy Cognate          = Transfer
+pedagogy FalseFriend      = Warn
+pedagogy Antonym          = Remap
+pedagogy AlienRealization = Bridge
+pedagogy Novel            = TeachDeNovo
+pedagogy Vanished         = ReRoute
+
+||| The residue shape characteristic of each kind (its Echo-fibre grade).
+public export
+residueShape : CorrespondenceKind -> Residue
+residueShape Cognate          = None
+residueShape FalseFriend      = Lossy "surface-corresponds; semantics diverge"
+residueShape Antonym          = Inverted "related but inverted"
+residueShape AlienRealization = Lossy "same intention; foreign mechanism"
+residueShape Novel            = AbsentSource "no source anchor"
+residueShape Vanished         = AbsentTarget "concept gone in the target"
+
+--------------------------------------------------------------------------------
+-- Form / Concept / Transition
+--------------------------------------------------------------------------------
+
+||| A representative of a Concept *in one language*.
+public export
+record Form where
+  constructor MkForm
+  language : String   -- e.g. "erlang", "rescript", "jtv"
+  surface  : String   -- the token / snippet, e.g. "X = 5"
+
+||| A Concept — the invariant / equivalence-class (the recurring trope) —
+||| carried by an (asserted) equivalence Relation over its Forms.
+public export
+record Concept where
+  constructor MkConcept
+  name    : String         -- e.g. "name-binding"
+  carrier : Relation Form  -- certifies "same idea" across Forms
+
+||| A per-stratum verdict: does the correspondence hold at this stratum?
+public export
+record StratumVerdict where
+  constructor MkVerdict
+  stratum : Stratum
+  holds   : Bool
+
+||| A directed correspondence Form(from) -> Form(to): the classified crossing,
+||| its residue, the per-stratum verdicts, and an optional `witness` anchoring
+||| the claim to a proof/test — the invariant-path governance front-end, used
+||| where the certifiable math pays.
+public export
+record Transition where
+  constructor MkTransition
+  concept : String
+  from    : Form
+  to      : Form
+  kind    : CorrespondenceKind
+  residue : Residue
+  strata  : List StratumVerdict
+  witness : Maybe String
+
+--------------------------------------------------------------------------------
+-- The false-friend signature
+--------------------------------------------------------------------------------
+
+||| Look up the verdict at a given stratum.
+public export
+verdictAt : Stratum -> List StratumVerdict -> Maybe Bool
+verdictAt _ []        = Nothing
+verdictAt s (v :: vs) = if v.stratum == s then Just v.holds else verdictAt s vs
+
+||| The false-friend signature, made precise: *corresponds at the Surface
+||| stratum yet diverges at the Intention stratum*. This is the whole reason
+||| classification runs per stratum rather than as a single boolean.
+public export
+isFalseFriendShape : List StratumVerdict -> Bool
+isFalseFriendShape vs =
+  case (verdictAt Surface vs, verdictAt Intention vs) of
+    (Just True, Just False) => True
+    _                       => False

src/interface/Abi/README.adoc

@@ -0,0 +1,41 @@
+// SPDX-License-Identifier: MPL-2.0
+= ABI seam — the correspondence model (Idris2)
+
+The formally-typed core of the engine that *classifies* cross-language
+correspondences. Typecheck with `idris2 --typecheck abi.ipkg` from the repo root.
+
+== Modules
+
+* `Abi.Carrier` — the carrier of an equivalence *claim*: a `Relation` (with its
+  reflexive / symmetric / transitive properties and `isEquivalence`) and the
+  `Residue` of a crossing — the grades of the Echo fibre, from `None` (true iso)
+  through `Inverted` / `Lossy` to `AbsentSource` / `AbsentTarget` (empty fibre).
+* `Abi.Correspondence` — `Concept` / `Form` / `Transition`, the six
+  `CorrespondenceKind`s (cognate / false-friend / antonym / alien-realization /
+  novel / vanished), the `Stratum` ladder, each kind's `pedagogy` and
+  `residueShape`, and the precise *false-friend signature* (`isFalseFriendShape`):
+  corresponds at the `Surface` stratum yet diverges at the `Intention` stratum.
+
+See `docs/theory/CORRESPONDENCE-MODEL.adoc` for the full design.
+
+== Licence note (cite, don't import)
+
+This seam is original *MPL-2.0* code. It is conceptually grounded in two estate
+libraries but deliberately does **not** import them, to keep the licence clean:
+
+* the Dyadic `Relation` from `hyperpolymath/proven-tests-and-benches`
+  (AGPL-3.0-or-later, son-shared) — importing it would relicense this repo by
+  linkage;
+* the Echo loss-with-residue fibre `Echo f y := Sigma (x : A), f x = y` from
+  `hyperpolymath/echo-types` (Agda).
+
+The shapes are re-expressed here as fresh MPL-2.0 source rather than depended on.
+`abi.ipkg` therefore lists `depends = base` only.
+
+== Status
+
+Authored ahead of the toolchain: Idris2 is not present in every environment, so
+this is verified by `idris2 --typecheck abi.ipkg` in a tooled session / CI, not
+yet in the authoring environment. The Zig FFI side of the seam
+(`src/interface/ffi/`) and the AffineScript host binding that consumes this ABI
+follow as later slices of the abstraction-model pivot.