From 5227895cbbcfb443a3e0d5b29ab27722f5178d23 Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 16:00:35 +0000 Subject: [PATCH] docs(wiki): replace stale betlang placeholder with an accurate page The betlang language page was a thin placeholder describing a generic sampling/inference PPL (bernoulli/sample/observe/infer). It omitted the actual language: the ternary (bet A B C) lazy core, the probabilistic-CAS framing, Echo structured-loss types (functor/comonad surface), the 14-system uncertainty number tower, and the Lean 4 axiom-free metatheory. Rewritten accurately in the umbrella house style, cross-linking betlang's in-repo wiki and the upstream echo-types spine. https://claude.ai/code/session_01QGi8GND5yNWgDyfReVEPYs --- wiki/languages/betlang.md | 87 ++++++++++++++++++++++----------------- 1 file changed, 49 insertions(+), 38 deletions(-) diff --git a/wiki/languages/betlang.md b/wiki/languages/betlang.md index d62902c..c6fdc6c 100644 --- a/wiki/languages/betlang.md +++ b/wiki/languages/betlang.md @@ -4,60 +4,71 @@ Copyright (c) Jonathan D.A. Jewell --> # betlang -> Probabilistic programming language - -**Status:** 📝 Placeholder - contributions welcome +**Tagline:** A symbolic probabilistic metalanguage — a *probabilistic computer algebra system*, not a betting language. ## Overview -betlang is a probabilistic programming language built on Racket, enabling explicit modeling of uncertainty through sampling and inference. - -## Core Invariant - -**All uncertainty must be explicitly modeled—no hidden randomness.** +BetLang is built on one idea: **computation is structured choice under uncertainty.** +Its core primitive is the ternary form `(bet A B C)` — a probabilistic, **lazy** choice +between three branches (only the selected branch is evaluated). This makes BetLang closer +to a *probabilistic CAS* than a simulation DSL: it is symbolic-first, compositional, and +treats uncertainty as a first-class **typed** object rather than as noise to average away. -## Key Features +## Philosophy -- First-class probability distributions -- Bayesian inference primitives -- Conditioning and observation -- Sampling and expectation +- **Ternary over binary** — real-world decisions are rarely yes/no; the musical ternary + form (A–B–A) gives compositional structure, and Dutch-book coherence needs ≥3 outcomes. +- **Uncertainty as structure** — not noise, but a first-class object the type system tracks. +- **Symbolic first** — computation stays inspectable and composable. -## Example +## Core Primitive ```racket #lang betlang -; Define a biased coin -(define coin (bernoulli 0.7)) +(bet 'win 'draw 'lose) ; uniform ternary choice (lazy) +(bet/weighted '(common 7) '(uncommon 2) '(rare 1)) ; non-uniform +(bet/conditional pred A B C) ; predicate-driven +(bet (expensive) (cheap-approx) (fallback)) ; only one branch is evaluated +``` -; Model with observation -(define (model) - (let ([heads (sample coin)]) - (observe (= heads #t)) ; condition on heads - heads)) +## Type System -; Run inference -(define posterior (infer model 1000)) -``` +BetLang's checker (`bet-check`, Rust) is Hindley–Milner with two domain-specific pillars: -## Use Cases +- **Echo types** — *structured loss* as a typed object. When a `bet` collapses three + branches to one (or a `sample` marginalises a draw), `Echo T` retains a proof-relevant + residue of what was lost; `Echo T` is deliberately **distinct from `T`** (no implicit + forgetting). The operations form a functor + comonad surface (`echo`, `echo_output`, + `echo_map`, `echo_duplicate`, `echo_to_residue`, `sample_echo`), the ungraded ghost + shadow of the graded comonad proved in [`echo-types`](https://github.com/hyperpolymath/echo-types) (Agda). +- **The uncertainty number tower** — 14 uncertainty-aware number systems (Gaussian, + interval/affine, fuzzy, Bayesian, VaR/CVaR, surreal, p-adic, imprecise, Dempster–Shafer, + …). These *are* the type system, not add-ons. -- Bayesian modeling -- Machine learning prototyping -- Statistical inference -- Uncertainty quantification -- A/B testing analysis +## Formal Verification -## Getting Started +The core calculus is mechanised in **Lean 4** (`proofs/BetLang.lean`, CI-checked): +**Progress**, **Preservation**, and the **distribution monad laws** — with an +**axiom-free core** (the `substTop_preserves_typing` axiom was discharged) and **zero +`sorry`**. This is BetLang's differentiator versus untyped numeric/CAS tools (R, Octave, +Scilab, Mathematica, Maple): *typed, proof-anchored uncertainty*. -```bash -cd betlang -racket main.rkt -``` +## Architecture + +Four layers with separated responsibilities: **Racket** (authoritative semantics) · +**Julia** (compute kernel / number tower) · **Lean 4** (proofs) · **Rust** (compiler +tooling — `bet-core`, `bet-check`, `bet-parse`). + +## Status + +Active. Racket frontend authoritative; Lean proofs machine-checked (axiom-free core); +Rust checker handles Echo formers **and** the typed echo operations; Julia backend in +active development. ## See Also -- [[Duet Language]] - AI-assisted verification -- [[Ensemble Language]] - AI integration -- [[NEUROSYM.scm]] - Neuro-symbolic patterns +- BetLang repository wiki (in-repo `wiki/`): Home · Type-System · Echo-Types · Formal-Verification · Number-Tower +- [[Ephapax]] — linear/affine once-only semantics (sibling language) +- [[AffineScript]] — affine-typed primary application language +- Upstream: [`echo-types`](https://github.com/hyperpolymath/echo-types) (Agda, source of truth) · [`EchoTypes.jl`](https://github.com/hyperpolymath/EchoTypes.jl) (executable shadow)