diff --git a/abi.ipkg b/abi.ipkg new file mode 100644 index 0000000..53a4a79 --- /dev/null +++ b/abi.ipkg @@ -0,0 +1,26 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +-- +-- 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 diff --git a/src/interface/Abi/Carrier.idr b/src/interface/Abi/Carrier.idr new file mode 100644 index 0000000..95f5727 --- /dev/null +++ b/src/interface/Abi/Carrier.idr @@ -0,0 +1,59 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +||| +||| 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 diff --git a/src/interface/Abi/Correspondence.idr b/src/interface/Abi/Correspondence.idr new file mode 100644 index 0000000..a0bba3a --- /dev/null +++ b/src/interface/Abi/Correspondence.idr @@ -0,0 +1,149 @@ +-- SPDX-License-Identifier: MPL-2.0 +-- Copyright (c) 2026 Jonathan D.A. Jewell +||| +||| 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 diff --git a/src/interface/Abi/README.adoc b/src/interface/Abi/README.adoc new file mode 100644 index 0000000..a2f05f7 --- /dev/null +++ b/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.