From 9eff2134c69cd0ea1ac9e2768f3c498c0ec2351c Mon Sep 17 00:00:00 2001
From: "Jonathan D.A. Jewell" <6759885+hyperpolymath@users.noreply.github.com>
Date: Sat, 2 May 2026 23:29:41 +0100
Subject: [PATCH] docs(AI.a2ml): add 4 idiomatic patterns + 3 directives from
 idaptik feedback
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Closes #45 #46 #47 #48 #49 #50 #52.

Adds patterns surfaced during the IDApTIK Wave 3 pilot exercise:

* per-element-error-extraction (closes #46) — polymorphic-per-element
  helper for accumulating errors from heterogeneously-typed Validation
  values; eliminates the dominant ReScript→AffineScript migration
  antipattern documented in idaptik's ProvenBridge.idr (4 sites).

* fuel-based-total-recursion (closes #47) — canonical pattern for
  provably-total recursive parsers/interpreters. Counter-pattern to
  depth-tracking, which the totality checker cannot see as
  well-founded (depth increments rather than decreases).

* validation-chain-over-tuple-match (closes #49) — Validation
  applicative chain replaces N-tuple `case` matches. N>=5 tuple
  matches blow ambiguity-resolution budgets in real translation
  (verified in idaptik's parseLevelJson).

* status-sum-vs-string-enum (closes #52) — sum types replace
  stringly-typed dispatch. Small but pervasive.

Adds three new directives:

* stdlib-floor (closes #45) — Validation/Result/Option/Either are
  stdlib floor; reject re-implementations.

* eta-style (closes #48) — eta-expand definitions when a function
  has named pi-binders. Point-free is a parser-cascade trigger.

* no-side-effect-imports (closes #50) — `let _ = X.foo` for
  module-load side effects must rewrite to explicit registration in
  AffineScript (no module-load-time side effect in wasm).

All seven additions cross-reference idaptik's commit hyperpolymath/idaptik@98f110ce
and the LESSONS.md catalogue at idaptik/migration/main/LESSONS.md.
---
 .../frontier-programming-practices/AI.a2ml    | 34 +++++++++++++++++++
 1 file changed, 34 insertions(+)

diff --git a/docs/guides/frontier-programming-practices/AI.a2ml b/docs/guides/frontier-programming-practices/AI.a2ml
index 14e0749..b506455 100644
--- a/docs/guides/frontier-programming-practices/AI.a2ml
+++ b/docs/guides/frontier-programming-practices/AI.a2ml
@@ -138,6 +138,34 @@
       (composition "phantom + effect rows")
       (purpose "Mark values or functions as pure or impure in the type system for optimisation or testing.")
       (sketch "fn pure_compute(x: Int): Int  // no effect row = pure\nfn io_op(): String / {IO}  // effect row declares IO"))
+
+    (pattern
+      (name "per-element-error-extraction")
+      (composition "polymorphic-per-element + Validation")
+      (purpose "Accumulate errors from heterogeneously-typed Validation values without forcing them into a uniform list.")
+      (anti-pattern "List (Validation E a) when each element has a different `a` — non-starter type-theoretically; cannot unify a single `a` across heterogeneous components.")
+      (sketch "let allErrs = errsOf v1 ++ errsOf v2 ++ errsOf v3\n     where errsOf : Validation E a -> List E"))
+
+    (pattern
+      (name "fuel-based-total-recursion")
+      (composition "Nat parameter + structural decrease")
+      (purpose "Make recursive parsers / interpreters / search algorithms provably total without sized types.")
+      (anti-pattern "Depth tracking with `if depth > N then bail` — runtime guarantee, not provable. Totality checker cannot see incrementing parameters as well-founded.")
+      (sketch "fn parse(fuel: Nat, input: List Char) { match fuel { Z => Err(\"depth\"); S(f) => recurse(f, ...) } }"))
+
+    (pattern
+      (name "validation-chain-over-tuple-match")
+      (composition "Validation applicative + <*>")
+      (purpose "Accumulate errors across N independent extractions without N-tuple matches.")
+      (anti-pattern "case (a, b, c, d, e, f, g) of (Ok, Ok, Ok, ...) => ... — N>=5 tuple matches blow type inference / ambiguity-resolution budgets.")
+      (sketch "MkRecord <$> a <*> b <*> c <*> d <*> e <*> f <*> g"))
+
+    (pattern
+      (name "status-sum-vs-string-enum")
+      (composition "sum types")
+      (purpose "Distinguish status / kind values at compile time. Replaces stringly-typed dispatch (\"compromised\" / \"clean\" / etc.).")
+      (anti-pattern "dispatch(deviceId, \"compromised\") — typo \"compromied\" silently mis-matches at runtime.")
+      (sketch "type DeviceStatus = Compromised | Clean | Suspect | Unknown\nfn dispatch(d: DeviceId, s: DeviceStatus)"))
   )
 
   (agent-behavior
@@ -157,6 +185,12 @@
       (rule "Work that belongs in the Typed WASM project goes to the Typed WASM project. Never add it to AffineScript as a shortcut."))
     (honesty-in-documentation
       (rule "STATE.a2ml, README, and related docs must reflect what the code actually enforces, not what it aspires to. A 'dune build passing' is not a behavioural test and does not count as 'feature complete'."))
+    (stdlib-floor
+      (rule "Validation[E,A], Result[E,A], Option[A], and Either[E,A] are stdlib floor. Reject any project that re-implements them. Pointing migrators at canonical types prevents the heterogeneous-list-as-homogeneous antipattern."))
+    (eta-style
+      (rule "When a function has named pi-binders ((name : Type) -> ...), prefer eta-expanded definitions over point-free. Point-free is a parser-cascade trigger when the eta-rewrite's argument name disagrees with the declared signature's name."))
+    (no-side-effect-imports
+      (rule "AffineScript modules do not run code at load time. Migrating ReScript/JS code that uses `let _ = X.foo` for module-load side effects must be rewritten to call an explicit registration function. There is no implicit module-load-time side effect to hook in wasm."))
   )
 
   (relationship-with-typed-wasm-project