feat(betlang): wire-first toolchain pass + bet:Dist T on the unified runtime (#65)

## What this is

Brings the 2026-06-15 **wire-first toolchain pass** + **`bet : Dist T`**
work onto the reconciled `main` (which already carries the parallel
session's TP-5 intro/elim core and the checker's occurs-check +
let-polymorphism). The parallel reconciliation merge resolved the
TP-5/checker collisions but dropped this session's wiring; this PR
re-applies it surgically on top.

Full rationale and the journey's design decisions:
**`docs/decisions/2026-06-15-betlang-wiring-and-bet-dist-t.adoc`** (8
ADRs).

## Highlights

**`bet : Dist T` (option a) — checker + interpreter + codegen aligned
with the Lean proof**
- `check_bet`/`check_weighted_bet`/`check_conditional_bet` return `Dist
T`; `bet { 1,2,3 } + 1` is now correctly rejected. `echo(bet …) : Echo
(Dist T)`.
- Interpreter **unified onto `bet_rt::Value`** (one runtime): `bet →
Value::Dist`, `sample` draws; AST lambdas **closure-converted** into
native `bet_rt` closures. `bet-rt` and `bet-rand` are no longer
orphaned.
- JS codegen emits **distribution objects** so `sample` works end-to-end
(verified under deno).

**Wire-first pass**
- Justfile: was *unparseable* (`//` line 1) — fixed + Rust recipes
(`build-rust`/`test-rust`/`check`/`run`/`compile`/`repl-rust`).
- Workspace greened: `bet-wasm` (E0308), `bet-viz` (`im` dep +
`Histogram`→`Rectangle` + textplots lifetimes), `bet-chapel`
(`rand_pcg`); **3 real `bet-rt` bugs** fixed (queue order, `printf %s`
quoting, msgpack `List`→`Bytes`).
- `cbindgen` no longer **strips the SPDX header** from generated
`betlang.h` (was an automated licence edit).
- CLI `bet compile … --target js|llvm|beam`; LSP wired to the **real
parser + type checker** (real parse/type diagnostics with spans;
obsolete "LALR conflicts" deps re-enabled).
- Interpreter surfaces unimplemented forms as **errors, not silent
`Unit`**.
- `examples/dice.bet` — first working `.bet` fixture.

## Reconciliation choices (honoring owner adjudication)
- **TP-5** kept at origin's `echoIntro`/`echoElim` core. The richer
comonad-law surface (this session's `MultiStep` shadow of
`EchoGradedComonad.agda`) is **TP-5b** (deferred, P3) — preserved in
local `964d106` + the ADR.
- Origin's **occurs-check + let-polymorphism kept** (complementary; the
audit had flagged both gaps).
- `docs/echo-types.adoc` left at origin's baseline (owner-managed).

## Verification
- **317 workspace tests pass**; `lake build` green;
`tools/proof-scan.sh` clean (no banned escape hatches).
- End-to-end: `bet check/run/compile examples/dice.bet` all work.

## Deferred / for follow-up (ADR-8)
Racket→Rust authority declaration (left as-is); eager-vs-lazy runtime
operational model; TP-5b; SEM-1/STAT-1/STAT-2 (Mathlib decision);
ABI-1..5 (Idris2 recipe + CI).

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Author: hyperpolymath

Justfile

@@ -1,5 +1,5 @@
-// SPDX-License-Identifier: MPL-2.0
-// Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+# SPDX-License-Identifier: MPL-2.0
+# Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
 # betlang - Development Tasks
 # AUTHORITY: AUTHORITY_STACK.mustfile-nickel.scm
 # All operations MUST be invoked via `just <recipe>`.
@@ -84,6 +84,34 @@ test-tooling:
 clean-tooling:
     cargo clean
 
+# --- Rust toolchain recipes (the working compiler/interpreter pipeline) ------
+# These drive the real multi-crate Rust implementation under compiler/, runtime/
+# and tools/. (The Racket recipes above target the historical core/*.rkt tree.)
+
+# Build the entire Rust workspace (all crates)
+build-rust:
+    cargo build --workspace
+
+# Test the entire Rust workspace
+test-rust:
+    cargo test --workspace
+
+# Type-check a betlang source file with the Rust checker
+check FILE:
+    cargo run -q -p bet -- check {{FILE}}
+
+# Run a betlang source file with the Rust interpreter
+run FILE:
+    cargo run -q -p bet -- run {{FILE}}
+
+# Compile a betlang source file to a backend (TARGET = js | llvm | beam)
+compile FILE TARGET="js":
+    cargo run -q -p bet -- compile {{FILE}} --target {{TARGET}}
+
+# Start the Rust REPL
+repl-rust:
+    cargo run -q -p bet -- repl
+
 # ============================================================================
 # PROOFS (formal verification — see docs/AFFINESCRIPT-ALIGNMENT.adoc)
 # ============================================================================

bindings/chapel/Cargo.toml

@@ -18,6 +18,7 @@ libc = "0.2"
 # Core
 rand.workspace = true
 rand_distr.workspace = true
+rand_pcg.workspace = true   # seedable PCG generator for `bet_seed`
 
 [build-dependencies]
 cbindgen = "0.28"

bindings/chapel/build.rs

@@ -10,6 +10,15 @@ fn main() {
         .with_language(cbindgen::Language::C)
         .with_include_guard("BET_CHAPEL_H")
         .with_documentation(true)
+        // Preserve the SPDX/copyright header on the generated file. cbindgen
+        // overwrites include/betlang.h wholesale on every build; without this
+        // the licence header is silently stripped each time (an automated
+        // licence edit, which estate policy forbids — keep it manual & stable).
+        .with_header(
+            "// SPDX-License-Identifier: MPL-2.0\n\
+             // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>\n\
+             // GENERATED by cbindgen (build.rs) — do not edit by hand.",
+        )
         .generate()
         .expect("Unable to generate bindings")
         .write_to_file("include/betlang.h");

bindings/chapel/include/betlang.h

@@ -1,5 +1,7 @@
 // SPDX-License-Identifier: MPL-2.0
 // Copyright (c) Jonathan D.A. Jewell <j.d.a.jewell@open.ac.uk>
+// GENERATED by cbindgen (build.rs) — do not edit by hand.
+
 #ifndef BET_CHAPEL_H
 #define BET_CHAPEL_H
 
@@ -143,4 +145,4 @@ void bet_seed(uint64_t seed);
  */
 const char *bet_version(void);
 
-#endif /* BET_CHAPEL_H */
+#endif  /* BET_CHAPEL_H */

compiler/bet-check/src/lib.rs

@@ -837,7 +837,10 @@ fn check_bet(bet: &BetExpr, env: &mut CheckEnv, span: Span) -> CompileResult<Typ
 
     env.unify(&t0, &t1, Some(span))?;
     env.unify(&t0, &t2, Some(span))?;
-    Ok(env.resolve(&t0))
+    // A `bet` introduces probabilistic choice: it has type `Dist T`, not `T`.
+    // (Matches the mechanised rule `tBet : … → HasType … (Ty.dist T)` in
+    // proofs/BetLang.lean; eliminate with `sample : Dist 'a -> 'a`.)
+    Ok(Type::Dist(Box::new(env.resolve(&t0))))
 }
 
 /// Check a weighted bet: branches unify, weights must be numeric.
@@ -863,7 +866,8 @@ fn check_weighted_bet(
     for i in 1..branch_types.len() {
         env.unify(&branch_types[0], &branch_types[i], Some(span))?;
     }
-    Ok(env.resolve(&branch_types[0]))
+    // Weighted bet, like uniform bet, is a distribution: `Dist T`.
+    Ok(Type::Dist(Box::new(env.resolve(&branch_types[0]))))
 }
 
 /// Check a conditional bet: condition is Bool/Ternary, all branches unify.
@@ -892,7 +896,9 @@ fn check_conditional_bet(
     env.unify(&true_ty, &f0, Some(span))?;
     env.unify(&true_ty, &f1, Some(span))?;
     env.unify(&true_ty, &f2, Some(span))?;
-    Ok(env.resolve(&true_ty))
+    // Conditional bet also yields a distribution over `T`: point-mass on the
+    // `if_true` value when the condition holds, else the ternary distribution.
+    Ok(Type::Dist(Box::new(env.resolve(&true_ty))))
 }
 
 // ============================================
@@ -1265,7 +1271,11 @@ mod tests {
             ],
         };
         let result = check_expr(&dummy(Expr::Bet(bet)), &mut env);
-        assert_eq!(result.expect("TODO: handle error"), Type::Int);
+        // `bet` introduces probabilistic choice, so its type is `Dist Int`.
+        assert_eq!(
+            result.expect("TODO: handle error"),
+            Type::Dist(Box::new(Type::Int))
+        );
     }
 
     #[test]
@@ -1699,9 +1709,11 @@ mod tests {
         );
     }
 
-    /// The core primitive bridges to Echo by composition at the type level:
-    /// `echo(bet a b c) : Echo T`. (Runtime branch-tag retention — `bet_echo` —
-    /// remains deferred; the *type* story needs no new primitive.)
+    /// The core primitive bridges to Echo by composition at the type level.
+    /// Since `bet a b c : Dist T`, the composite is `echo(bet a b c) : Echo (Dist T)`
+    /// — the retained-loss residue over the *distribution*. (Runtime branch-tag
+    /// retention — `bet_echo` — remains deferred; the *type* story needs no new
+    /// primitive.)
     #[test]
     fn test_bet_echo_bridge_by_composition() {
         let mut env = CheckEnv::new();
@@ -1714,8 +1726,8 @@ mod tests {
         };
         let e = call("echo", vec![dummy(Expr::Bet(bet))]);
         assert_eq!(
-            check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo Int"),
-            Type::Echo(Box::new(Type::Int))
+            check_expr(&e, &mut env).expect("echo (bet 1 2 3) : Echo (Dist Int)"),
+            Type::Echo(Box::new(Type::Dist(Box::new(Type::Int))))
         );
     }
 

compiler/bet-codegen/src/lib.rs

@@ -102,24 +102,36 @@ pub fn codegen_module(module: &Module, target: Target) -> CompileResult<CodeOutp
 fn js_preamble() -> &'static str {
     r#"// === Betlang Runtime Preamble ===
 
-// Uniform ternary choice among exactly 3 alternatives
+// Uniform ternary choice among exactly 3 alternatives.
+// `bet` has type `Dist T`: it returns a *distribution object* (sample with
+// `__bet_sample`), not an eager draw — consistent with the checker/interpreter.
 function __bet_uniform(a, b, c) {
-  const r = Math.random();
-  if (r < 1/3) return a;
-  if (r < 2/3) return b;
-  return c;
+  return {
+    name: 'bet',
+    sample() {
+      const r = Math.random();
+      if (r < 1/3) return a;
+      if (r < 2/3) return b;
+      return c;
+    },
+  };
 }
 
-// Weighted ternary choice (weights normalised internally)
+// Weighted ternary choice (weights normalised internally). Returns a Dist.
 function __bet_weighted(alts, weights) {
-  const total = weights.reduce((s, w) => s + w, 0);
-  const r = Math.random() * total;
-  let cumul = 0;
-  for (let i = 0; i < alts.length; i++) {
-    cumul += weights[i];
-    if (r < cumul) return alts[i];
-  }
-  return alts[alts.length - 1];
+  return {
+    name: 'weighted_bet',
+    sample() {
+      const total = weights.reduce((s, w) => s + w, 0);
+      const r = Math.random() * total;
+      let cumul = 0;
+      for (let i = 0; i < alts.length; i++) {
+        cumul += weights[i];
+        if (r < cumul) return alts[i];
+      }
+      return alts[alts.length - 1];
+    },
+  };
 }
 
 // --- Distribution objects ---

compiler/bet-eval/Cargo.toml

@@ -8,6 +8,9 @@ license.workspace = true
 [dependencies]
 bet-syntax = { path = "../bet-syntax" }
 bet-core = { path = "../bet-core" }
+bet-rt = { path = "../../runtime/bet-rt" }       # the unified runtime Value (Dist, …)
+bet-rand = { path = "../../runtime/bet-rand" }   # centralised ternary/weighted RNG
+im.workspace = true                              # bet_rt::Value::List is im::Vector
 rand.workspace = true
 rand_distr.workspace = true
 thiserror.workspace = true