ReScript→AffineScript migration: toolchain + Types.affine (module 1 of 17)#26
Merged
Conversation
The three "Safety Proofs" in src/abi/Foreign.idr (stabilityBounded,
positionalDeterministic, paradoxMonotonic) were not proofs: each fabricated
its evidence with cast ()/cast Refl over an IO action. Replace them with
genuine, self-contained Idris2 modules, machine-checked under Idris 2 v0.8.0
(no believe_me / assert_total / cast / postulate):
- Stability.idr : stability score is bounded in [0,100] (clamp model of
compiler/src/Types.res calculateStability).
- Positional.idr : positional-operator behaviour is deterministic over the
pure model of the Zig FFI (a genuine Refl, not IO cast Refl).
- Paradox.idr : the two threshold-gated factors are monotone; the blanket
"paradox detection monotonic" claim is RETRACTED -- proving
it honestly surfaced that scope_leakage is prime-gated and
therefore non-monotone (line 7 prime, line 8 not).
Foreign.idr is reduced to an honest, self-contained ABI binding layer.
Add error-lang-abi.ipkg and verification/check-proofs.sh (idris2 --check all
four modules). Rewrite PROOF-NEEDS.md to record what is proved, what is
retracted, the toolchain, and open conformance obligations.
The language's satirical "100% production-ready / formally verified"
self-presentation in README/WHITEPAPER is intentional and left intact; this
change only makes the underlying proof artifacts real and honest.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
…integration) Adds docs/Trope-Particularity-Integration.adoc — a design (not yet implemented) for lowering Error-Lang's Echo operations and stability factors to the language-neutral Trope IR (hyperpolymath/trope-checker, v0.1 prevent profile) and consuming the verified verdict + witness. - Object/effect/grade correspondence: Echo<A,B> <-> Trope[Phi], EchoR <-> FloatingQuality, echo/echo_to_residue/echo_input/echo_output <-> preserve/ detach/project. echo_to_residue IS detach (bond=Severed, irrecoverable), matching the [Stab-Erase] debit and "decomposition must be visible". - stabilityFactor -> grade mapping; the silent instabilities (GlobalState, RaceCondition) land on the deceptive Conflated bottom -> a lowering fault under the prevent profile. - Verdict mapping: scalar calculateStability -> use-model floor + p-sufficient/ p-insufficient + witness edge (the invariant-path argmin Stability.idr already reasons about). - Architecture (reference, never vendor; schema is the trust boundary), the per-front-end O2 lowering-correctness obligations (L-Echo/L-Grade/L-Silent/ L-Floor), and a 4-phase plan. Builds on docs/Echo-Decomposition.adoc; references echo-types, trope-checker and trope-particularity-workbench by URL only. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Hypatia structural_drift flagged `src/idris2/` and `src/aggregate/` in the trope-integration design as dangling references "surviving a directory rename". Both are deliberately *external*: the trope-checker repo's Idris2 core and the panic-attack repo's aggregate module. Reword as unambiguously external (drop the bare `src/<dir>/` form) so the heuristic no longer reads them as internal error-lang tree paths. No substantive content change. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
First module of the compiler's migration to AffineScript (the Hyperpolymath language policy bans ReScript). Adds compiler/src/Types.affine, a faithful port of compiler/src/Types.res, verified green with `affinescript check`: - all token / AST / error / stability types (structs + enums + match) - ReScript inline-record variants lowered to positional constructor args - token variants Float/String renamed FloatTok/StringTok (reserved type keywords in AffineScript) - Echo types (TyEcho / TyEchoResidue) shaped Trope-IR-ready per docs/Trope-Particularity-Integration.adoc (Phase 0) - make_default_state, stability_impact, calculate_stability, error_code_to_string Toolchain, so the .affine sources are reproducibly CI-verifiable: - scripts/install-affinescript-toolchain.sh — builds the AffineScript compiler from distro OCaml packages (independent of opam.ocaml.org) + installs the binary and stdlib under a discoverable share/ path - verification/check-affinescript.sh — typechecks all compiler/src/*.affine Types.res is retained until its dependents migrate; format_diagnostic is deferred pending the string / affine-borrow pass. Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
The .res -> .affine port needs sibling compiler modules to import the shared AST
(Location/Token/Position/...) from Types. AffineScript's module resolver exported
imported enum constructors but dropped imported struct/alias type definitions, so
cross-module struct field access failed ("Field not found"). Per the chosen
approach (fix the resolver, not single-file/accessors):
- patches/affinescript-module-struct-fields.patch: threads imported modules'
type_env + constructor_env into the importing module's typecheck context
(typecheck.ml check_program gains ?import_type_env/?import_constructor_env;
resolve.ml import_type_defs copies them across all three import forms;
bin/main.ml passes them at the check/compile/eval entry points). Documented in
patches/README.adoc; pending upstream to hyperpolymath/affinescript.
- compiler/src/Types.affine: now a proper `module Types;` with `pub` exports.
- verification/check-affinescript.sh: checks from compiler/src so `use Types::{...}`
resolves via the loader's current-dir search.
- scripts/install-affinescript-toolchain.sh: applies the patch after cloning,
before building (idempotent).
Verified: a module importing Types' structs with nested field access, struct
construction, and enum-field matching type-checks; affinescript's own stdlib
cross-module imports (http_fetch/option/io) still pass.
Co-Authored-By: Claude Opus 4.8 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
hyperpolymath
marked this pull request as ready for review
June 23, 2026 22:34
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
What
Kicks off the compiler's migration from ReScript (banned by the Hyperpolymath language policy) to AffineScript, with a reproducible, CI-verifiable toolchain.
compiler/src/Types.affine— a faithful port ofcompiler/src/Types.res(the foundational module: tokens, the full AST, errors, stability), verified green withaffinescript check.scripts/install-affinescript-toolchain.sh— builds the AffineScript compiler (hyperpolymath/affinescript, OCaml/dune) from distro OCaml packages, independent ofopam.ocaml.org, and installs the binary + stdlib under a discoverableshare/path.verification/check-affinescript.sh— typechecks everycompiler/src/*.affine(companion tocheck-proofs.sh).Port conventions established here (apply to all following modules)
array<T>→[T],option<T>→Option<T>,dict<k,v>→Dict<k,v>, tuples kept.Float/String→FloatTok/StringTok(Float/Stringare reserved type keywords).use prelude::*;forOption/Some/None;fold/max/trunc/int_to_stringare builtins.Trope-IR readiness (Phase 0)
The Echo types are shaped to lower cleanly to the Trope IR per the just-merged
docs/Trope-Particularity-Integration.adoc:TyEcho↔Trope[Φ],TyEchoResidue↔FloatingQuality. No runtime coupling yet.Scope / honesty
Types.resis retained until its dependents are migrated (thecompiler/ReScript path doesn't build today regardless).format_diagnosticis deferred to the string / affine-borrow pass.Check Workflow Stalenessgovernance check fails onmaintoo (stalestandardsworkflow pins); it is unrelated to this change.Next
Lexer→Cst/Parser→TypeChecker/TypeSuperposition→VM/Bytecode/Codegen→ … , each gated byaffinescript check, deleting each.resas its.affinelands.🤖 Generated with Claude Code
https://claude.ai/code/session_0195yA45jSSP7YDPwJSpw4bM
Generated by Claude Code