|
| 1 | +// SPDX-License-Identifier: MPL-2.0 |
| 2 | +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk> |
| 3 | += nextgen-typing — Normative Scope (Must / Intend / Wish) |
| 4 | +:toc: preamble |
| 5 | +:revdate: 2026-06-19 |
| 6 | + |
| 7 | +[abstract] |
| 8 | +Per-repo normative-scope record for nextgen-typing (the coordination monorepo for |
| 9 | +the Hyperpolymath *type-theory pipeline*). It is also the *home of the canonical |
| 10 | +AFFIRMATION exemplar* the estate's No-Bullshit discipline was modelled on. Estate |
| 11 | +rule (2026-06-19): every repo carries its own scoped table; crossover content is |
| 12 | +duplicated and marked until resolved, then wired into the other relevant repos. |
| 13 | +`◇` marks proposals not yet canonical. |
| 14 | + |
| 15 | +== Levels |
| 16 | + |
| 17 | +* *MUST* — required to be what it is (RFC 2119 normative). |
| 18 | +* *INTEND* — committed direction. |
| 19 | +* *WISH* — aspirational. |
| 20 | + |
| 21 | +== nextgen-typing (own) |
| 22 | + |
| 23 | +[cols="1,5", options="header"] |
| 24 | +|=== |
| 25 | +| Level | nextgen-typing |
| 26 | + |
| 27 | +| *MUST* |
| 28 | +| Be the *coordination monorepo for the type-theory pipeline* — coordinate the |
| 29 | + estate's typing disciplines and their hand-offs (the type-safe lowering through |
| 30 | + TangleIR, affine typing in AffineScript, structured-loss typing in echo-types), |
| 31 | + with implementations living in their own repos; uphold the *AFFIRMATION |
| 32 | + discipline it exemplifies* (dated, signed, falsifiable, *no intentional |
| 33 | + overclaim*); estate governance — LICENSE/SPDX, no banned files; honest |
| 34 | + coordination (coordinate, do not silently absorb per-component code). |
| 35 | + |
| 36 | +| *INTEND* |
| 37 | +| Keep the pipeline components in sync as each evolves; raise READINESS above `C`; |
| 38 | + finish RSR-template instantiation where residue remains; coordinate one coherent |
| 39 | + *type-safety narrative* across the estate (tangle's proven small-step core → |
| 40 | + AffineScript's affine guarantees → echo-types' graded/structured-loss reading); |
| 41 | + keep the `verification/`, `features/`, and `benches/` coordination surfaces |
| 42 | + honest and evidenced. |
| 43 | + |
| 44 | +| *WISH* |
| 45 | +| A unified, navigable type-theory pipeline with *verified* hand-offs between |
| 46 | + components ◇; a shared conformance surface for typing guarantees across the |
| 47 | + estate ◇; the pipeline cited as the estate's canonical type-safety map ◇. |
| 48 | +|=== |
| 49 | + |
| 50 | +== Cross-repo wiring |
| 51 | + |
| 52 | +nextgen-typing is the *type-theory coordination* node — one of three coordination |
| 53 | +monorepos alongside *nextgen-databases* (database/query/identity) and |
| 54 | +*nextgen-languages* (the language catalog). It coordinates rather than implements: |
| 55 | +the proving and type-checking live in *tangle* (TangleIR + the Lean-checked |
| 56 | +type-safe core), the affine-type guarantees in *AffineScript* (catalogued under |
| 57 | +nextgen-languages), and the type-theoretic structured-loss work in *echo-types*. |
| 58 | +The confirmed KRL-stack ladder (maintainer-confirmed 2026-06-19) — *krl → |
| 59 | +tangle/TangleIR → VerisimCore → Skein.jl / quandledb* — depends on tangle's |
| 60 | +type-safety, which this pipeline coordinates. |
| 61 | + |
| 62 | +Sibling repos' key concerns (keep in sync as crossover resolves): *tangle* — |
| 63 | +TangleIR + type-safe core; *echo-types* — structured-loss theory + the |
| 64 | +identity-fabric framing (Conway·Fichte / Bruner / Ricoeur); *nextgen-languages* — |
| 65 | +language catalog (AffineScript et al.); *nextgen-databases* — database/identity |
| 66 | +coordination; the KRL-stack faces *krl* / *quandledb* / *Skein.jl*. See |
| 67 | +`../../AFFIRMATION.adoc` (the canonical exemplar at this repo's root). |
0 commit comments