diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
index 0000000..b19435a
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,112 @@
+# Changelog
+
+All notable changes to the Goth programming language are documented in this file.
+
+## [0.2.0] - 2026-01-31
+
+Bug fixes, type checker improvements, and quality-of-life cleanup.
+
+### Type Checker
+- Cast validation: `as?` (try cast) now returns `Option<T>` instead of bare `T`
+- Record update: `Expr::Update` validates field names and types against base record
+- LetRec: extracts type annotations from `Pattern::Typed` and `Expr::Annot` instead of using `Type::Hole` for all bindings
+- Do blocks: full type threading through Map, Filter, Bind, Op, and Let operations
+- Fresh type variables: Forall instantiation uses unique `_t0`, `_t1`... variables instead of `Type::Hole`
+- Added `fromChars` type signature to builtins
+
+### Interpreter
+- `eval_filter` now propagates predicate errors instead of silently dropping elements
+- Added `fromChars` primitive for string round-tripping (`fromChars (chars s) = s`)
+- Closure equality now compares captured environment, not just code
+- Terminal raw mode: replaced unsafe `static mut` with `Mutex`, added `atexit` handler and `catch_unwind` for panic-safe terminal restoration
+- REPL `:quit` now restores terminal state before exiting
+
+### Pretty Printer
+- Implemented `OpDecl` pretty printing (was `todo!()` panic)
+- Operator precedence now delegates to `BinOp::precedence()` — no more drift between parser and printer
+
+### Documentation
+- Added CHANGELOG.md
+- LANGUAGE.md: documented 8 missing operators (⍀, ∘, ⊗, ⤇, ◁, ⊕, ▷, ≡)
+- LANGUAGE.md: clarified all integer types are i128 at runtime
+- Removed empty `examples/string/` and `examples/data-structures/` directories
+
+### Dependencies
+- thiserror: 1.0 → 2.0 (all crates)
+- Added `license` and `repository` to goth-check Cargo.toml
+
+## [0.1.0] - 2026-01-31
+
+Initial public release.
+
+### Language
+
+- De Bruijn indexed lambda calculus with curried multi-argument functions
+- Pattern matching with literal, tuple, array, variant, wildcard, guard, and or-patterns
+- Recursive bindings (`let rec`)
+- Do-notation for tensor pipelines (map, filter, bind, let, binary ops)
+- Tensor (array) types with shape tracking and broadcasting
+- Record types with labeled fields and update syntax
+- Variant (sum) types with constructor syntax
+- Uncertainty propagation: first-class `±` values with automatic error propagation through all math operations
+- Cast expressions: `as` (static), `as!` (force), `as?` (try, returns Option)
+- Unicode operator surface: `λ`, `→`, `↦`, `▸`, `⤇`, `∘`, `⊕`, `⊗`, `Σ`, `Π`, `⌿`, `⍀`, `▷`, `◁`, `≤`, `≥`, `≠`, `∧`, `∨`, `±`
+- ASCII aliases for all Unicode operators
+- String literals as character tensors
+- Effect annotations (parsed and stored, not yet enforced)
+- Type annotations with refinement types (parsed, partially checked)
+- Module system with `use` imports and file-based resolution
+
+### Standard Library
+
+- `prelude.goth` — core utilities (identity, const, flip, compose, arithmetic helpers)
+- `math.goth` — trigonometric, hyperbolic, logarithmic, and special functions
+- `list.goth` — list operations (map, filter, fold, zip, take, drop, reverse, sort, minimum, maximum)
+- `option.goth` — generic Option type (some, none, map, flatMap, getOrElse, etc.)
+- `result.goth` — generic Result type (ok, err, map, flatMap, recover, etc.)
+- `string.goth` — string manipulation (split, join, trim, contains, replace, etc.)
+- `tui.goth` — terminal UI helpers (ANSI escapes, cursor control, raw mode)
+- `crypto.goth` — pure-Goth SHA-256, SHA-1, MD5, HMAC, and PBKDF2
+
+### Interpreter
+
+- Tree-walking evaluator with global environment and closure capture
+- Partial application for all functions
+- 127 evaluator tests covering arithmetic, closures, patterns, tensors, uncertainty, I/O
+- Built-in primitives: math functions, string operations, file I/O, byte I/O, terminal control
+- Checked integer arithmetic (overflow returns error, not panic)
+- Checked shift/power operations with bounds validation
+- Thread-safe terminal state management with atexit and panic cleanup
+
+### Type Checker
+
+- Bidirectional type checking (inference + checking modes)
+- Type unification with occurs check
+- Shape unification for tensor dimensions
+- 76 type checker tests
+- Handles: let, let rec (with annotations), if/else, match, binary/unary ops, tuples, records, arrays, casts, do-blocks, field access, indexing, slicing, annotations
+- Fresh type variable generation for polymorphic instantiation
+- Type substitution across all type forms including Variant, Exists, App, Effectful, Interval
+
+### Parser
+
+- Full Goth syntax including Unicode and ASCII operator forms
+- Proper error reporting on unrecognized tokens (no silent drops)
+- Proper error reporting on unrecognized operators (no silent fallback)
+- Module parsing with declarations, function definitions, and type definitions
+- 111 parser tests
+
+### Tooling
+
+- CLI (`goth`): file execution, expression evaluation (`-e`), REPL, type checking (`-c`)
+- REPL with syntax-aware multi-line input, history, and colored output
+- AST-first LLM workflow: `--to-json` / `--from-json` for JSON AST round-tripping
+- Pretty printer for Goth syntax from AST
+
+### Known Limitations
+
+- Type checker is advisory — programs run regardless of type errors
+- Variant constructor validation requires ADT registry (not yet implemented)
+- Effect system is parsed but not enforced
+- No parametric polymorphism at runtime (evaluator is type-erased)
+- Closure equality compares code only, not captured environment
diff --git a/LANGUAGE.md b/LANGUAGE.md
index 8148afa..48f2b64 100644
--- a/LANGUAGE.md
+++ b/LANGUAGE.md
@@ -22,8 +22,8 @@
 
 | Type | Example | Notes |
 |------|---------|-------|
-| Integer | `42`, `-7` | 64-bit signed |
-| Float | `3.14`, `2.718` | 64-bit |
+| Integer | `42`, `-7` | Arbitrary precision (`ℤ`), backed by i128 |
+| Float | `3.14`, `2.718` | 64-bit (`F64`) |
 | Boolean | `true`, `false` or `⊤`, `⊥` | |
 | Char | `'a'`, `'\n'` | Unicode |
 | String | `"hello"` | UTF-8 |
@@ -57,21 +57,21 @@ Goth uses de Bruijn indices instead of named variables. This eliminates shadowin
 
 In multi-arg function declarations, `₀` = **last** argument (most recently bound):
 ```goth
-╭─ sub : I64 → I64 → I64
+╭─ sub : ℤ → ℤ → ℤ
 ╰─ ₁ - ₀            # ₁ = first arg, ₀ = second arg (sub 10 3 = 7)
 ```
 
 For single-arg functions, `₀` is the sole argument:
 ```goth
-╭─ square : I64 → I64
+╭─ square : ℤ → ℤ
 ╰─ ₀ × ₀            # ₀ = the argument
 ```
 
 Let bindings shift indices:
 ```goth
-╭─ example : I64 → I64
-╰─ let x ← ₀ × 2 in    # ₀ = argument
-   let y ← ₀ + 1 in    # ₀ = x, ₁ = argument
+╭─ example : ℤ → ℤ
+╰─ let x = ₀ × 2 in    # ₀ = argument
+   let y = ₀ + 1 in    # ₀ = x, ₁ = argument
    ₀ + ₁               # ₀ = y, ₁ = x, ₂ = argument
 ```
 
@@ -83,31 +83,37 @@ Let bindings shift indices:
 
 | Type | Description |
 |------|-------------|
-| `I64` | 64-bit signed integer |
-| `I32` | 32-bit signed integer |
+| `ℤ` | Integer (backed by i128 at runtime) |
+| `ℕ` | Natural number (non-negative integer, i128 at runtime) |
+| `F` | Generic float (resolves to F64) |
+| `I64` | 64-bit signed integer (i128 at runtime) |
+| `I32` | 32-bit signed integer (i128 at runtime) |
 | `F64` | 64-bit float |
 | `F32` | 32-bit float |
 | `Bool` | Boolean |
 | `Char` | Unicode character |
+| `String` | UTF-8 string (tensor of Char) |
 | `()` | Unit type |
 
+All integer types (`ℤ`, `ℕ`, `I64`, `I32`, etc.) are stored as i128 at runtime. The type distinctions exist for documentation and type checking but are not enforced by the interpreter. The standard library primarily uses `ℤ`, `F`, and `Bool` for polymorphic signatures.
+
 ### Composite Types
 
 ```goth
-I64 → I64                -- Function type
-I64 → I64 → I64          -- Curried function
-[n]I64                   -- Vector of n integers
-[m n]F64                 -- m×n matrix of floats
-⟨I64, Bool⟩              -- Tuple (product)
-⟨x: I64, y: I64⟩         -- Record
+ℤ → ℤ                    # Function type
+ℤ → ℤ → ℤ               # Curried function
+[n]ℤ                     # Vector of n integers
+[m n]F64                 # m×n matrix of floats
+⟨ℤ, Bool⟩               # Tuple (product)
+⟨x: ℤ, y: ℤ⟩            # Record
 ```
 
 ### Type Variables
 
 Lowercase names are type variables:
 ```goth
-α → α                    -- Polymorphic identity
-[n]α → [n]α              -- Shape-preserving map
+α → α                    # Polymorphic identity
+[n]α → [n]α              # Shape-preserving map
 ```
 
 ---
@@ -117,23 +123,23 @@ Lowercase names are type variables:
 Shapes are part of the type system and checked at compile time.
 
 ```goth
-[3]I64                   -- Exactly 3 integers
-[2 3]F64                 -- 2×3 matrix
-[n]I64                   -- Vector of unknown length n
-[m n]F64                 -- m×n matrix (shape variables)
+[3]ℤ                     # Exactly 3 integers
+[2 3]F64                 # 2×3 matrix
+[n]ℤ                     # Vector of unknown length n
+[m n]F64                 # m×n matrix (shape variables)
 ```
 
 Shape checking catches dimension mismatches:
 ```goth
--- Error: Dimension mismatch at position 0: expected 5, found 3
-╭─ bad : [3]I64 → [5]I64
+# Error: Dimension mismatch at position 0: expected 5, found 3
+╭─ bad : [3]ℤ → [5]ℤ
 ╰─ ₀
 ```
 
 Shape variables unify:
 ```goth
--- OK: input and output have same shape
-╭─ double : [n]I64 → [n]I64
+# OK: input and output have same shape
+╭─ double : [n]ℤ → [n]ℤ
 ╰─ ₀ ↦ (λ→ ₀ × 2)
 ```
 
@@ -153,13 +159,13 @@ ASCII alternative: `/-` for `╭─`, `\-` for `╰─`
 ### Examples
 
 ```goth
-╭─ square : I64 → I64
+╭─ square : ℤ → ℤ
 ╰─ ₀ × ₀
 
-╭─ add : I64 → I64 → I64
+╭─ add : ℤ → ℤ → ℤ
 ╰─ ₀ + ₁
 
-╭─ sumSquares : [n]I64 → I64
+╭─ sumSquares : [n]ℤ → ℤ
 ╰─ Σ (₀ ↦ (λ→ ₀ × ₀))
 ```
 
@@ -176,22 +182,21 @@ ASCII: `\->` for `λ→`
 
 Functions can call themselves by name:
 ```goth
-╭─ factorial : I64 → I64
+╭─ factorial : ℤ → ℤ
 ╰─ if ₀ ≤ 1 then 1 else ₀ × factorial (₀ - 1)
 ```
 
 ### Let Bindings
 
 ```goth
-let x ← expr in body         -- Bind x, use in body
-let x : Type ← expr in body  -- With type annotation
-let x ← a; y ← b in c        -- Sequential bindings
+let x = expr in body          # Bind x, use in body (= or ← accepted)
+let x : Type = expr in body   # With type annotation
 ```
 
 Type annotations enable compile-time shape checking:
 ```goth
-let v : [3]F64 ← [1.0, 2.0, 3.0] in v    -- OK
-let v : [5]F64 ← [1.0, 2.0, 3.0] in v    -- Error: shape mismatch
+let v : [3]F64 = [1.0, 2.0, 3.0] in v    # OK
+let v : [5]F64 = [1.0, 2.0, 3.0] in v    # Error: shape mismatch
 ```
 
 ---
@@ -229,14 +234,50 @@ let v : [5]F64 ← [1.0, 2.0, 3.0] in v    -- Error: shape mismatch
 | `∨` | `\|\|` | Or |
 | `¬` | `!` | Not |
 
+### Bitwise
+
+| Unicode | ASCII | Operation | Example |
+|---------|-------|-----------|---------|
+| | `bitand` | Bitwise AND | `bitand 255 15` → `15` |
+| | `bitor` | Bitwise OR | `bitor 240 15` → `255` |
+| `⊻` | `bitxor` | Bitwise XOR | `⊻ 255 170` → `85` |
+| | `shl` | Shift left | `shl 1 8` → `256` |
+| | `shr` | Shift right | `shr 256 4` → `16` |
+
+All bitwise operations are curried functions on integer (`ℤ`) values.
+
+### Structural Equality
+
+| Unicode | ASCII | Operation | Example |
+|---------|-------|-----------|---------|
+| `≡` | `===` | Structural equality | `[1,2] ≡ [1,2]` → `⊤` |
+
 ### Array Operations
 
 | Unicode | ASCII | Operation | Example |
 |---------|-------|-----------|---------|
 | `↦` | `-:` | Map | `arr ↦ (λ→ ₀ × 2)` |
 | `▸` | `\|>` | Filter | `arr ▸ (λ→ ₀ > 5)` |
+| `⤇` | `>>=` | Bind (flatmap) | `[1,2] ⤇ (λ→ [₀, ₀×2])` → `[1,2,2,4]` |
+| `⌿` | `fold` | Fold/reduce | `⌿ (λ→ λ→ ₁ + ₀) 0 [1,2,3]` → `6` |
+| `⍀` | `scan` | Scan (prefix sums) | `⍀ (λ→ λ→ ₁ + ₀) 0 [1,2,3]` → `[1,3,6]` |
 | `Σ` | `+/` | Sum | `Σ [1, 2, 3]` |
 | `Π` | `*/` | Product | `Π [1, 2, 3]` |
+| `⊕` | `++` | Concatenate | `[1,2] ⊕ [3,4]` → `[1,2,3,4]` |
+| `⊗` | `zip` | Zip (pair elements) | `[1,2] ⊗ [3,4]` → `[⟨1,3⟩, ⟨2,4⟩]` |
+
+### Function Operations
+
+| Unicode | ASCII | Operation | Example |
+|---------|-------|-----------|---------|
+| `∘` | `.:` | Compose | `(f ∘ g) x` = `f (g x)` |
+
+### I/O Operations
+
+| Unicode | ASCII | Operation | Example |
+|---------|-------|-----------|---------|
+| `▷` | `>>` | Write | `"hello" ▷ "file.txt"` |
+| `◁` | `<<` | Read | `◁ "file.txt"` |
 
 ### Indexing
 
@@ -291,7 +332,7 @@ Patterns:
 ```goth
 enum Option α where Some α | None
 
-╭─ getOrDefault : I64 → I64
+╭─ getOrDefault : ℤ → ℤ
 ╰─ match (Some ₀) {
      Some x → x
      None → 0
@@ -343,8 +384,8 @@ Each `.goth` file is a module. The `use` declaration takes a string path (relati
 
 | Name | Signature | Description |
 |------|-----------|-------------|
-| `ι`, `iota` | `I64 → [n]I64` | `[0, 1, ..., n-1]` |
-| `range` | `I64 → I64 → [m]I64` | `[start, ..., end-1]` |
+| `ι`, `iota` | `ℤ → [n]ℤ` | `[0, 1, ..., n-1]` |
+| `range` | `ℤ → ℤ → [m]ℤ` | `[start, ..., end-1]` |
 
 ### Reductions
 
@@ -352,7 +393,7 @@ Each `.goth` file is a module. The `use` declaration takes a string path (relati
 |------|-----------|-------------|
 | `Σ`, `sum` | `[n]α → α` | Sum elements |
 | `Π`, `prod` | `[n]α → α` | Product elements |
-| `len` | `[n]α → I64` | Array length |
+| `len` | `[n]α → ℤ` | Array length |
 
 ### Transformations
 
@@ -360,9 +401,10 @@ Each `.goth` file is a module. The `use` declaration takes a string path (relati
 |------|-----------|-------------|
 | `↦` (map) | `[n]α → (α → β) → [n]β` | Apply to each |
 | `▸` (filter) | `[n]α → (α → Bool) → [m]α` | Keep matching |
+| `⌿`, `fold` | `(α → β → α) → α → [n]β → α` | Left fold with accumulator |
 | `reverse` | `[n]α → [n]α` | Reverse order |
-| `take` | `I64 → [n]α → [m]α` | Take first k elements |
-| `drop` | `I64 → [n]α → [m]α` | Drop first k elements |
+| `take` | `ℤ → [n]α → [m]α` | Take first k elements |
+| `drop` | `ℤ → [n]α → [m]α` | Drop first k elements |
 | `⧺` | `String → String → String` | Concatenate strings |
 | `⊕` | `[n]α → [m]α → [p]α` | Concatenate arrays |
 
@@ -409,12 +451,22 @@ Supported functions: `+`, `-`, `×`, `/`, `^`, `√`, `exp`, `ln`, `log10`, `log
 
 | Name | Signature | Description |
 |------|-----------|-------------|
-| `toInt` | `α → I64` | Convert to integer |
+| `toInt` | `α → ℤ` | Convert to integer |
 | `toFloat` | `α → F64` | Convert to float |
-| `toChar` | `I64 → Char` | Integer to character |
-| `parseInt` | `String → I64` | Parse string as integer |
+| `toChar` | `ℤ → Char` | Integer to character |
+| `parseInt` | `String → ℤ` | Parse string as integer |
 | `parseFloat` | `String → F64` | Parse string as float |
 
+### Bitwise Operations
+
+| Name | Signature | Description |
+|------|-----------|-------------|
+| `bitand` | `ℤ → ℤ → ℤ` | Bitwise AND |
+| `bitor` | `ℤ → ℤ → ℤ` | Bitwise OR |
+| `⊻`, `bitxor` | `ℤ → ℤ → ℤ` | Bitwise XOR |
+| `shl` | `ℤ → ℤ → ℤ` | Shift left (0..127) |
+| `shr` | `ℤ → ℤ → ℤ` | Shift right (0..127) |
+
 ### I/O
 
 | Name | Signature | Description |
@@ -423,6 +475,8 @@ Supported functions: `+`, `-`, `×`, `/`, `^`, `√`, `exp`, `ln`, `log10`, `log
 | `readLine` | `() → String` | Read line from stdin |
 | `readFile` | `String → String` | Read file contents |
 | `writeFile` | `String → String → ()` | Write content to file path |
+| `⧏`, `readBytes` | `ℤ → String → [n]ℤ` | Read n bytes from file as byte array |
+| `⧐`, `writeBytes` | `[n]ℤ → String → ()` | Write byte array to file |
 | `▷` | `String → String → ()` | Write operator: `"content" ▷ "path"` |
 | `toString` | `α → String` | Convert value to string |
 | `strConcat`, `⧺` | `String → String → String` | Concatenate strings |
@@ -434,34 +488,34 @@ Supported functions: `+`, `-`, `×`, `/`, `^`, `√`, `exp`, `ln`, `log10`, `log
 ### Factorial
 
 ```goth
-╭─ factorial : I64 → I64
+╭─ factorial : ℤ → ℤ
 ╰─ if ₀ ≤ 1 then 1 else ₀ × factorial (₀ - 1)
 
-╭─ main : () → I64
+╭─ main : () → ℤ
 ╰─ factorial 10
 ```
 
 ### Sum of Squares
 
 ```goth
-╭─ main : () → I64
+╭─ main : () → ℤ
 ╰─ Σ ((ι 10) ↦ λ→ ₀ × ₀)
 ```
 
 ### Filter Even Numbers
 
 ```goth
-╭─ main : () → I64
+╭─ main : () → ℤ
 ╰─ Σ ((ι 20) ▸ λ→ (₀ % 2) = 0)
 ```
 
 ### Cross-Function Calls
 
 ```goth
-╭─ square : I64 → I64
+╭─ square : ℤ → ℤ
 ╰─ ₀ × ₀
 
-╭─ main : () → I64
+╭─ main : () → ℤ
 ╰─ square 9
 ```
 
@@ -470,7 +524,7 @@ Supported functions: `+`, `-`, `×`, `/`, `^`, `√`, `exp`, `ln`, `log10`, `log
 ```goth
 enum Option α where Some α | None
 
-╭─ main : () → I64
+╭─ main : () → ℤ
 ╰─ match (Some 42) {
      Some x → x × 2
      None → 0
@@ -479,6 +533,60 @@ enum Option α where Some α | None
 
 ---
 
+## Standard Library
+
+The `stdlib/` directory contains reusable modules imported via `use`:
+
+```goth
+use "stdlib/random.goth"
+use "stdlib/math.goth"
+```
+
+### Modules
+
+| Module | Description |
+|--------|-------------|
+| `prelude.goth` | Core combinators (`id`, `const`, `flip`, `compose`) |
+| `list.goth` | List/array operations |
+| `math.goth` | Math functions with uncertainty propagation |
+| `option.goth` | Generic Option type (`some`/`none`, `mapOpt`, `flatMapOpt`, ...) |
+| `result.goth` | Generic Result type (`ok`/`err`, `mapRes`, `flatMapRes`, ...) |
+| `string.goth` | String manipulation |
+| `io.goth` | I/O utilities |
+| `canvas.goth` | Canvas/graphics operations |
+| `tui.goth` | Terminal UI operations |
+| `random.goth` | Seeded PRNG (xorshift64) with state-passing pattern |
+
+### Random Number Generation
+
+The `random.goth` module provides a seeded PRNG using xorshift64. All RNG functions return `⟨value, nextSeed⟩` tuples for explicit state threading:
+
+```goth
+use "stdlib/random.goth"
+
+╭─ main : ℤ → [n]F64
+╰─ let seed = entropy ⟨⟩
+   in let ⟨vals, _⟩ = randFloats ₁ seed
+   in vals
+```
+
+| Function | Signature | Description |
+|----------|-----------|-------------|
+| `entropy` | `() → I64` | Seed from `/dev/urandom` |
+| `bytesToSeed` | `[8]I64 → I64` | Pack 8 bytes into seed |
+| `xorshift64` | `I64 → I64` | Raw state transition |
+| `randFloat` | `I64 → ⟨F64, I64⟩` | Uniform float in [0, 1) |
+| `randFloatRange` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Uniform float in [lo, hi) |
+| `randInt` | `I64 → I64 → I64 → ⟨I64, I64⟩` | Uniform integer in [lo, hi] |
+| `randBool` | `F64 → I64 → ⟨Bool, I64⟩` | Boolean with probability p |
+| `randNormal` | `I64 → ⟨F64, I64⟩` | Standard normal (Box-Muller) |
+| `randGaussian` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Normal with mean and stddev |
+| `randFloats` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk uniform floats |
+| `randInts` | `I64 → I64 → I64 → I64 → ⟨[n]I64, I64⟩` | Bulk uniform integers |
+| `randNormals` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk normal values |
+
+---
+
 ## Compilation
 
 The `gothic` compiler produces native executables via LLVM:
diff --git a/LLM_SPEC.md b/LLM_SPEC.md
index d9eaa29..9c0752e 100644
--- a/LLM_SPEC.md
+++ b/LLM_SPEC.md
@@ -54,10 +54,13 @@ Arithmetic:   +  -  ×  /  %  ^  ±  (% also written as mod, ± also +-)
 Comparison:   =  ≠  <  >  ≤  ≥
 Equality:     =  (value)  ≡/==  (structural)  ≣/===  (referential, reserved)
 Logical:      ∧  ∨  ¬            (or &&  ||  !)
+Bitwise:      bitand  bitor  ⊻/bitxor  shl  shr
 Map:          arr ↦ λ→ body      (or arr -: \-> body)
 Filter:       arr ▸ λ→ body      (or arr |> \-> body)
+Fold:         ⌿ (λ→ λ→ ₁+₀) 0 arr  (or fold f acc arr)
 Sum:          Σ arr              (or +/ arr)
 Product:      Π arr              (or */ arr)
+Byte I/O:     ⧏ n "path"  (readBytes)    ⧐ bytes "path"  (writeBytes)
 ```
 
 ## Common Patterns
@@ -173,6 +176,40 @@ Goth has first-class uncertain values. Create with `±`, and uncertainty propaga
 
 Propagation rules: additive (√(δa²+δb²)) for `+`/`-`, relative error for `×`/`/`, derivative-based for math functions (`√`, `sin`, `cos`, `exp`, `ln`, etc.).
 
+## Standard Libraries
+
+### Random Numbers (`stdlib/random.goth`)
+
+Seeded PRNG using xorshift64. All RNG functions return `⟨value, nextSeed⟩` tuples — thread the seed through sequential calls.
+
+```goth
+use "stdlib/random.goth"
+╭─ main : I64 → F64
+╰─ let seed = entropy ⟨⟩
+   in let ⟨x, s1⟩ = randFloat seed
+   in x
+```
+
+Key functions: `entropy` (OS seed), `randFloat` (uniform [0,1)), `randFloatRange` (uniform [lo,hi)), `randInt` (uniform [lo,hi]), `randNormal` (standard normal), `randFloats`/`randInts`/`randNormals` (bulk generation).
+
+### Cryptography (`stdlib/crypto.goth`)
+
+Pure-Goth cryptographic hashes and encoding using bitwise primitives. No FFI.
+
+```goth
+use "stdlib/crypto.goth"
+╭─ main : () → String
+╰─ sha256 "hello"
+# → "2cf24dba5fb0a30e26e83b2ac5b9e29e1b161e5c1fa7425e73043362938b9824"
+```
+
+Key functions: `sha256` (FIPS 180-4), `md5` (RFC 1321), `blake3` (≤ 64 bytes), `base64EncodeStr`/`base64Decode` (RFC 4648), `hexEncode`.
+
+Implementation notes:
+- All 32-bit operations must mask with `bitand X 4294967295` (Goth uses i128)
+- SHA-256 = big-endian word packing; MD5, BLAKE3 = little-endian
+- Use `fold` over `iota N` for round-based block processing
+
 ## Common Mistakes
 
 1. **Wrong index after let**: Each `let` shifts indices by 1
@@ -243,6 +280,10 @@ Propagation rules: additive (√(δa²+δb²)) for `+`/`-`, relative error for `
 | `⍉` | `transpose` |
 | `·` | `dot` |
 | `±` | `+-` |
+| `⌿` | `fold` |
+| `⊻` | `bitxor` |
+| `⧏` | `readBytes` |
+| `⧐` | `writeBytes` |
 
 ## Enforcement Notes
 
diff --git a/README.md b/README.md
index 4d6a134..468b093 100644
--- a/README.md
+++ b/README.md
@@ -31,7 +31,7 @@ The interpreted version of the language is the canonical language.
 ./target/release/goth
 
 # Run a file
-./target/release/goth ../examples/factorial.goth
+./target/release/goth ../examples/recursion/factorial.goth
 
 # Evaluate expression
 ./target/release/goth -e "Σ [1, 2, 3, 4, 5]"
@@ -39,14 +39,22 @@ The interpreted version of the language is the canonical language.
 
 #### Examples
 
-[`add_main.goth`](./examples/add_main.goth)
-[`factorial.goth`](./examples/factorial.goth)
-[`fibonacci.goth`](./examples/fibonacci.goth)
-[`math_comprehensive.goth`](./examples/math_comprehensive.goth)
-[`matmul.goth`](./examples/matmul.goth)
-[`primes.goth`](./examples/primes.goth)
-[`test_iota.goth`](./examples/test_iota.goth)
-[`use_math.goth`](./examples/use_math.goth)
+See [`examples/README.md`](./examples/README.md) for a full listing organized by category.
+
+| Category | Examples |
+|----------|---------|
+| [`basic/`](./examples/basic/) | identity, double, square, abs, sign, is_even, max, min |
+| [`recursion/`](./examples/recursion/) | factorial, fibonacci, gcd, ackermann, collatz, hyperop |
+| [`higher-order/`](./examples/higher-order/) | map, filter, fold, compose, pipeline, zip |
+| [`numeric/`](./examples/numeric/) | harmonic, pi, exp, sqrt, gamma |
+| [`algorithms/`](./examples/algorithms/) | isPrime, count_primes, nth_prime, binary_search, modpow |
+| [`contracts/`](./examples/contracts/) | abs_post, div_safe, factorial_contract, sqrt_safe |
+| [`tco/`](./examples/tco/) | naive vs tail-call-optimized pairs |
+| [`io/`](./examples/io/) | stdout, stderr, file write |
+| [`uncertainty/`](./examples/uncertainty/) | measurement, error propagation through arithmetic |
+| [`simulation/`](./examples/simulation/) | heat diffusion, wave equation, Laplace, power iteration |
+| [`random/`](./examples/random/) | PRNG, Buffon's needle, Monte Carlo integration |
+| [`crypto/`](./examples/crypto/) | SHA-256, MD5, BLAKE3, Base64, file hashing |
 
 ### Compiler
 
@@ -118,13 +126,10 @@ The language is not particularly efficient to execute, but it is designed to be
 ### Planned
 
 - Refinement type solving (needs Z3)
-- Effect type checking
+- Effect type enforcement (currently parsed but not enforced)
 - Dependent shape inference
 - Polymorphism (let-generalization)
-- Native code compilation (MLIR → LLVM)
-- Comment syntax
-- Module system
-- Standard library
+- Bigint backing for ℕ/ℤ types
 - Package manager
 - Language server protocol (LSP)
 - Debugger
@@ -135,9 +140,9 @@ The language is not particularly efficient to execute, but it is designed to be
 
 - All syntax is parsed but not all features are type-checked.
 - Contracts are runtime-only (no static proving yet).
-- Shape variables are tracked but not unified.
 - Effect annotations are parsed but not enforced.
 - Refinement types are parsed but predicates not solved.
+- Comment syntax (`#`), module system (`use`), and standard library (11 modules) are implemented.
 
 ## Design
 
diff --git a/benchmark/grok-expert/CLAUDE-SKILLS.md b/benchmark/grok-expert/CLAUDE-SKILLS.md
index 1baab7c..6c9952d 100644
--- a/benchmark/grok-expert/CLAUDE-SKILLS.md
+++ b/benchmark/grok-expert/CLAUDE-SKILLS.md
@@ -146,7 +146,7 @@ A Goth module contains declarations:
 }
 ```
 
-Operators: `Add`, `Sub`, `Mul`, `Div`, `Mod`, `Pow`, `Eq`, `Neq`, `Lt`, `Gt`, `Leq`, `Geq`, `And`, `Or`, `PlusMinus`
+Operators: `Add`, `Sub`, `Mul`, `Div`, `Mod`, `Pow`, `Eq`, `Neq`, `Lt`, `Gt`, `Leq`, `Geq`, `And`, `Or`, `PlusMinus`, `Write`, `Read`, `Map`, `Filter`, `Compose`, `Bind`, `Concat`, `ZipWith`
 
 #### Unary Operations
 ```json
@@ -417,19 +417,63 @@ Built-in operators (not standalone functions):
 |-----------|---------|-------|---------|
 | Map | `↦` | `-:` | `[1,2,3] ↦ (λ→ ₀ × 2)` → `[2 4 6]` |
 | Filter | `▸` | `\|>_` | `[1,2,3,4,5] ▸ (λ→ ₀ > 2)` → `[3 4 5]` |
+| Fold | `⌿` | `fold` | `⌿ (λ→ λ→ ₁ + ₀) 0 [1,2,3]` → `6` |
 | Sum | `Σ` | `+/` | `Σ [1,2,3,4,5]` → `15` |
 | Product | `Π` | `*/` | `Π [1,2,3,4,5]` → `120` |
 | Compose | `∘` | `.:` | `f ∘ g` (f after g) |
 | Bind | `⤇` | `=>>` | Monadic bind |
+| Write | `▷` | `\|>` | `"hello" ▷ stdout` or `"data" ▷ "/tmp/out.txt"` |
+
+**Fold** is a 3-argument curried function: `fold f acc arr`. The function `f` takes `(accumulator, element)` and returns the new accumulator. Inside the fold lambda, `₁` = accumulator, `₀` = current element.
 
 **In JSON AST:**
 ```json
 {"BinOp": ["Map", {"Array": [...]}, {"Lam": ...}]}
 {"BinOp": ["Filter", {"Array": [...]}, {"Lam": ...}]}
+{"BinOp": ["Write", {"Lit": {"String": "hello"}}, {"Name": "stdout"}]}
+{"BinOp": ["Write", {"Lit": {"String": "data"}}, {"Lit": {"String": "/tmp/out.txt"}}]}
 ```
 
 ### 3. Input/Output
 
+**`print`** — prints any value followed by a newline, returns `()`:
+```goth
+print("Hello, world!")
+```
+
+**`▷` (write operator)** — writes to a stream or file, returns `()`. No newline is appended:
+```goth
+"hello" ▷ stdout      # write to stdout (no newline)
+"error" ▷ stderr      # write to stderr
+"data"  ▷ "/tmp/f.txt" # write to file
+```
+
+**`⧏` (readBytes)** — reads n bytes from a file path, returns `[n]I64` array of byte values (0-255):
+```goth
+⧏ 8 "/dev/urandom"    # read 8 bytes of entropy
+readBytes 4 "/tmp/f"   # ASCII fallback
+```
+
+**`⧐` (writeBytes)** — writes a byte array to a file path:
+```goth
+⧐ [72, 101, 108] "/tmp/out"   # write bytes
+writeBytes [0, 255] "/tmp/bin" # ASCII fallback
+```
+
+`stdout` and `stderr` are built-in stream constants. When the RHS of `▷` is a stream, the content is written to that stream. When it is a string, it is treated as a file path.
+
+**In JSON AST:**
+```json
+// print (function application)
+{"App": [{"Name": "print"}, {"Lit": {"String": "hello"}}]}
+
+// ▷ stdout (BinOp Write with stream)
+{"BinOp": ["Write", {"Lit": {"String": "hello"}}, {"Name": "stdout"}]}
+
+// ▷ file (BinOp Write with path)
+{"BinOp": ["Write", {"Lit": {"String": "data"}}, {"Lit": {"String": "/tmp/f.txt"}}]}
+```
+
 **Array output:** Printed as `[1 2 3]` (space-separated, no commas)
 
 **Tuple output:** Printed as `⟨1, 2, 3⟩`
@@ -490,9 +534,11 @@ Built-in operators (not standalone functions):
 
 **Math functions:** `√` (sqrt), `Γ` (gamma), `ln`, `exp`, `sin`, `cos`, `tan`, `abs`, `⌊` (floor), `⌈` (ceil), `log₁₀`, `log₂`
 
-**Array operations:** `len`, `Σ` (sum), `Π` (product), `↦` (map), `▸` (filter), `iota`, `range`
+**Array operations:** `len`, `Σ` (sum), `Π` (product), `↦` (map), `▸` (filter), `⌿` (fold), `iota`, `range`, `⊕` (concat)
+
+**Bitwise operations:** `bitand`, `bitor`, `⊻`/`bitxor`, `shl`, `shr` — all curried `I64 → I64 → I64`
 
-**No bitwise ops** currently. Use arithmetic equivalents if needed.
+**Byte I/O:** `⧏`/`readBytes` (`I64 → String → [n]I64`), `⧐`/`writeBytes` (`[n]I64 → String → ()`)
 
 ### 8. Execution Environment
 
@@ -508,13 +554,95 @@ Built-in operators (not standalone functions):
 ### 9. Extending Benchmarks
 
 **Current gaps to consider:**
-- String manipulation (limited support currently)
 - Data structures (trees, graphs - would need ADTs)
-- More numeric algorithms (integration, differentiation)
+- More numeric algorithms (differentiation)
 - Property-based contract testing
 
 **Stick to:** Pure functional algorithms that fit the current type system.
 
+## Standard Library: Random Numbers
+
+The `stdlib/random.goth` module provides seeded PRNG using xorshift64. Import with `use "stdlib/random.goth"`.
+
+**Key design pattern:** All RNG functions return `⟨value, nextSeed⟩` tuples. Thread the seed through sequential calls:
+
+```goth
+use "stdlib/random.goth"
+
+╭─ main : () → ⟨F64, F64, F64⟩
+╰─ let seed = entropy ⟨⟩
+   in let ⟨v1, s1⟩ = randFloat seed
+   in let ⟨v2, s2⟩ = randFloat s1
+   in let ⟨v3, s3⟩ = randFloat s2
+   in ⟨v1, v2, v3⟩
+```
+
+**Available functions:**
+
+| Function | Signature | Description |
+|----------|-----------|-------------|
+| `entropy` | `() → I64` | Seed from `/dev/urandom` |
+| `bytesToSeed` | `[8]I64 → I64` | Pack 8 bytes into seed |
+| `xorshift64` | `I64 → I64` | Raw state transition |
+| `randFloat` | `I64 → ⟨F64, I64⟩` | Uniform [0, 1) |
+| `randFloatRange` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Uniform [lo, hi) |
+| `randInt` | `I64 → I64 → I64 → ⟨I64, I64⟩` | Uniform [lo, hi] |
+| `randBool` | `F64 → I64 → ⟨Bool, I64⟩` | Boolean with probability p |
+| `randNormal` | `I64 → ⟨F64, I64⟩` | Standard normal (Box-Muller) |
+| `randGaussian` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Normal(mean, stddev) |
+| `randFloats` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk uniform floats |
+| `randInts` | `I64 → I64 → I64 → I64 → ⟨[n]I64, I64⟩` | Bulk uniform integers |
+| `randNormals` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk normal values |
+
+**De Bruijn index note:** When using `let ⟨v, s⟩ = randFloat seed in ...`, the destructuring introduces 2 bindings, so raw De Bruijn indices in the body shift by 2. Named variables (`v`, `s`, `seed`) are unaffected — prefer named references when possible.
+
+## Standard Library: Cryptography
+
+The `stdlib/crypto.goth` module provides pure-Goth implementations of cryptographic hash functions and encoding. All algorithms are implemented entirely in Goth using bitwise primitives — no FFI or Rust crate dependencies. Import with `use "stdlib/crypto.goth"`.
+
+**Key design pattern:** All hash functions take a `String` and return a hex-encoded `String`. Internally, strings are converted to byte arrays via `bytes`, processed through block-oriented compression functions using `fold`, and rendered back to hex strings.
+
+```goth
+use "stdlib/crypto.goth"
+
+╭─ main : String → String
+╰─ let contents = readFile ₀
+   in let _ = print ("SHA-256: " ⧺ sha256 ₀)
+   in let _ = print ("MD5:    " ⧺ md5 ₁)
+   in "BLAKE3: " ⧺ blake3 ₂
+```
+
+**Public functions:**
+
+| Function | Signature | Description |
+|----------|-----------|-------------|
+| `sha256` | `String → String` | SHA-256 hash (NIST FIPS 180-4), arbitrary-length input |
+| `sha256Bytes` | `[n]I64 → String` | SHA-256 from raw byte array |
+| `md5` | `String → String` | MD5 digest (RFC 1321), arbitrary-length input |
+| `blake3` | `String → String` | BLAKE3 hash (single chunk, ≤ 64 bytes) |
+| `base64EncodeStr` | `String → String` | Base64 encode a string (RFC 4648) |
+| `base64Encode` | `[n]I64 → String` | Base64 encode a byte array |
+| `base64Decode` | `String → [n]I64` | Base64 decode to byte array |
+| `hexEncode` | `[n]I64 → String` | Hex-encode a byte array |
+
+**Internal helpers** (also exported, useful for custom hash constructions):
+
+| Function | Description |
+|----------|-------------|
+| `add32`, `not32`, `rotr32`, `rotl32` | 32-bit masked arithmetic and rotation |
+| `byteToHex`, `wordsToHex`, `wordsToHexLE` | Hex encoding (big-endian and little-endian) |
+| `blockToWords`, `blockToWordsLE` | Byte-to-word packing (BE and LE) |
+| `sha256Pad`, `md5Pad` | Message padding with length encoding |
+| `sha256Compress`, `md5Compress`, `blake3Compress` | Single-block compression functions |
+| `aset` | Functional array element update: `aset arr idx val` |
+
+**Implementation notes for LLMs:**
+- Goth integers are i128 internally; all 32-bit hash operations must mask with `bitand X 4294967295` after every addition, rotation, or shift
+- SHA-256 uses big-endian word packing; MD5 and BLAKE3 use little-endian
+- BLAKE3 is limited to single-chunk messages (≤ 64 bytes); SHA-256 and MD5 handle arbitrary length via multi-block processing
+- De Bruijn index tracking is critical in hash compression loops — annotate every `let` with a comment showing the current index state (e.g., `# ₀=ki ₁=roundIdx ₂=st ₃=schedule`)
+- Use `fold` over `iota N` for round-based processing; inside the fold lambda, `₁` = accumulator, `₀` = round index
+
 ## Goth Syntax ↔ JSON
 
 | Goth Syntax | JSON AST |
diff --git a/crates/Cargo.lock b/crates/Cargo.lock
index a744dbb..03fa664 100644
--- a/crates/Cargo.lock
+++ b/crates/Cargo.lock
@@ -480,27 +480,27 @@ dependencies = [
 
 [[package]]
 name = "goth-ast"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "bincode",
  "pretty_assertions",
  "serde",
  "serde_json",
- "thiserror",
+ "thiserror 2.0.18",
 ]
 
 [[package]]
 name = "goth-check"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "goth-ast",
  "goth-parse",
- "thiserror",
+ "thiserror 2.0.18",
 ]
 
 [[package]]
 name = "goth-cli"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "clap",
  "colored",
@@ -509,36 +509,37 @@ dependencies = [
  "goth-check",
  "goth-eval",
  "goth-parse",
+ "libc",
  "rustyline",
  "serde_json",
 ]
 
 [[package]]
 name = "goth-eval"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "goth-ast",
  "libc",
  "ordered-float",
  "pretty_assertions",
- "thiserror",
+ "thiserror 2.0.18",
 ]
 
 [[package]]
 name = "goth-parse"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "bincode",
  "goth-ast",
  "logos",
  "pretty_assertions",
  "serde_json",
- "thiserror",
+ "thiserror 2.0.18",
 ]
 
 [[package]]
 name = "goth-server"
-version = "0.1.0"
+version = "0.2.0"
 dependencies = [
  "axum",
  "clap",
@@ -549,7 +550,7 @@ dependencies = [
  "reqwest",
  "serde",
  "serde_json",
- "thiserror",
+ "thiserror 2.0.18",
  "tokio",
  "tower 0.4.13",
  "tower-http",
@@ -1279,7 +1280,7 @@ checksum = "ba009ff324d1fc1b900bd1fdb31564febe58a8ccc8a6fdbb93b543d33b13ca43"
 dependencies = [
  "getrandom 0.2.17",
  "libredox",
- "thiserror",
+ "thiserror 1.0.69",
 ]
 
 [[package]]
@@ -1642,7 +1643,16 @@ version = "1.0.69"
 source = "registry+https://github.com/rust-lang/crates.io-index"
 checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52"
 dependencies = [
- "thiserror-impl",
+ "thiserror-impl 1.0.69",
+]
+
+[[package]]
+name = "thiserror"
+version = "2.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "4288b5bcbc7920c07a1149a35cf9590a2aa808e0bc1eafaade0b80947865fbc4"
+dependencies = [
+ "thiserror-impl 2.0.18",
 ]
 
 [[package]]
@@ -1656,6 +1666,17 @@ dependencies = [
  "syn",
 ]
 
+[[package]]
+name = "thiserror-impl"
+version = "2.0.18"
+source = "registry+https://github.com/rust-lang/crates.io-index"
+checksum = "ebc4ee7f67670e9b64d05fa4253e753e016c6c95ff35b89b7941d6b856dec1d5"
+dependencies = [
+ "proc-macro2",
+ "quote",
+ "syn",
+]
+
 [[package]]
 name = "thread_local"
 version = "1.1.9"
diff --git a/crates/Cargo.toml b/crates/Cargo.toml
index 8859624..d6c087d 100644
--- a/crates/Cargo.toml
+++ b/crates/Cargo.toml
@@ -14,12 +14,12 @@ members = [
 # "goth-llvm",
 
 [workspace.package]
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 license = "MIT"
 repository = "https://github.com/goth-lang/goth"
 
 [workspace.dependencies]
-thiserror = "1.0"
+thiserror = "2.0"
 serde = { version = "1.0", features = ["derive"] }
 serde_json = "1.0"
\ No newline at end of file
diff --git a/crates/goth-ast/Cargo.toml b/crates/goth-ast/Cargo.toml
index 85fbfd5..1a2a88a 100644
--- a/crates/goth-ast/Cargo.toml
+++ b/crates/goth-ast/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "goth-ast"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "Abstract Syntax Tree for the Goth programming language"
 license = "MIT"
@@ -10,7 +10,7 @@ repository = "https://github.com/goth-lang/goth"
 serde = { version = "1.0", features = ["derive", "rc"] }
 serde_json = "1.0"
 bincode = "1.3"
-thiserror = "1.0"
+thiserror = "2.0"
 
 [dev-dependencies]
 pretty_assertions = "1.4"
diff --git a/crates/goth-ast/src/pretty.rs b/crates/goth-ast/src/pretty.rs
index cab93ec..73f0757 100644
--- a/crates/goth-ast/src/pretty.rs
+++ b/crates/goth-ast/src/pretty.rs
@@ -89,7 +89,7 @@ impl Pretty {
             Decl::Class(c) => self.print_class(c),
             Decl::Impl(i) => self.print_impl(i),
             Decl::Let(l) => self.print_let_decl(l),
-            Decl::Op(_) => todo!("op decl pretty printing"),
+            Decl::Op(o) => self.print_op_decl(o),
             Decl::Use(u) => {
                 self.write("use \"");
                 self.write(&u.path);
@@ -219,6 +219,21 @@ impl Pretty {
         self.newline();
     }
 
+    fn print_op_decl(&mut self, o: &crate::decl::OpDecl) {
+        self.write("op ");
+        self.write(&o.name);
+        self.write(" ");
+        self.write(&o.glyph);
+        self.write(" (");
+        self.write(&o.ascii);
+        self.write(") : ");
+        self.print_type(&o.signature);
+        self.write(&format!(" [prec={}, assoc={:?}]", o.precedence, o.assoc));
+        self.write(if self.config.unicode { " ← " } else { " <- " });
+        self.print_expr(&o.body);
+        self.newline();
+    }
+
     /// Pretty print a type
     pub fn print_type(&mut self, ty: &Type) {
         match ty {
@@ -648,18 +663,9 @@ pub fn print_type(ty: &Type) -> String {
 // ============ Operator Helpers ============
 
 /// Get operator precedence (higher = tighter binding)
+/// Must match BinOp::precedence() in op.rs
 fn binop_prec(op: &crate::op::BinOp) -> u8 {
-    use crate::op::BinOp;
-    match op {
-        BinOp::Or => 2,
-        BinOp::And => 3,
-        BinOp::Eq | BinOp::Neq => 4,
-        BinOp::Lt | BinOp::Gt | BinOp::Leq | BinOp::Geq => 5,
-        BinOp::Add | BinOp::Sub | BinOp::PlusMinus => 6,
-        BinOp::Mul | BinOp::Div | BinOp::Mod => 7,
-        BinOp::Pow => 8,
-        _ => 5,
-    }
+    op.precedence()
 }
 
 /// Get operator string representation
diff --git a/crates/goth-check/Cargo.toml b/crates/goth-check/Cargo.toml
index f87070c..e5de182 100644
--- a/crates/goth-check/Cargo.toml
+++ b/crates/goth-check/Cargo.toml
@@ -1,12 +1,14 @@
 [package]
 name = "goth-check"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "Type checker for the Goth programming language"
+license = "MIT"
+repository = "https://github.com/goth-lang/goth"
 
 [dependencies]
 goth-ast = { path = "../goth-ast" }
-thiserror = "1.0"
+thiserror = "2.0"
 
 [dev-dependencies]
 goth-parse = { path = "../goth-parse" }
\ No newline at end of file
diff --git a/crates/goth-check/src/builtins.rs b/crates/goth-check/src/builtins.rs
index ac1f1af..b6b2e12 100644
--- a/crates/goth-check/src/builtins.rs
+++ b/crates/goth-check/src/builtins.rs
@@ -565,6 +565,13 @@ pub fn primitive_type(name: &str) -> Option<Type> {
                 Type::Tensor(Shape(vec![Dim::Var("n".into())]), Box::new(Type::Prim(PrimType::Char))),
             ))
         }
+        "fromChars" => {
+            // [n]Char → String (convert array of characters to string)
+            Some(Type::func(
+                Type::Tensor(Shape(vec![Dim::Var("n".into())]), Box::new(Type::Prim(PrimType::Char))),
+                Type::Tensor(Shape(vec![Dim::Var("m".into())]), Box::new(Type::Prim(PrimType::Char))),
+            ))
+        }
         // Aggregation
         "sum" | "Σ" => {
             // ∀n α. [n]α → α (sum of numeric array)
@@ -680,6 +687,50 @@ pub fn primitive_type(name: &str) -> Option<Type> {
                 Type::Tensor(Shape(vec![Dim::Var("m".into())]), Box::new(Type::Prim(PrimType::Char))),
             ))
         }
+        "readBytes" | "⧏" => {
+            // I64 → String → [?]I64 (read N bytes from file path)
+            Some(Type::func_n(
+                [
+                    Type::Prim(PrimType::I64),
+                    Type::Tensor(Shape(vec![Dim::Var("n".into())]), Box::new(Type::Prim(PrimType::Char))),
+                ],
+                Type::Tensor(Shape(vec![Dim::Var("m".into())]), Box::new(Type::Prim(PrimType::I64))),
+            ))
+        }
+        "writeBytes" | "⧐" => {
+            // [?]I64 → String → () (write bytes to file path)
+            Some(Type::func_n(
+                [
+                    Type::Tensor(Shape(vec![Dim::Var("n".into())]), Box::new(Type::Prim(PrimType::I64))),
+                    Type::Tensor(Shape(vec![Dim::Var("m".into())]), Box::new(Type::Prim(PrimType::Char))),
+                ],
+                Type::unit(),
+            ))
+        }
+        "fold" | "⌿" => {
+            // (α → β → α) → α → [?]β → α
+            Some(Type::Forall(
+                vec![
+                    TypeParam { name: "α".into(), kind: TypeParamKind::Type },
+                    TypeParam { name: "β".into(), kind: TypeParamKind::Type },
+                ],
+                Box::new(Type::func_n(
+                    [
+                        Type::func(Type::Var("α".into()), Type::func(Type::Var("β".into()), Type::Var("α".into()))),
+                        Type::Var("α".into()),
+                        Type::Tensor(Shape(vec![Dim::Var("n".into())]), Box::new(Type::Var("β".into()))),
+                    ],
+                    Type::Var("α".into()),
+                )),
+            ))
+        }
+        "bitand" | "bitor" | "bitxor" | "⊻" | "shl" | "shr" => {
+            // I64 → I64 → I64
+            Some(Type::func_n(
+                [Type::Prim(PrimType::I64), Type::Prim(PrimType::I64)],
+                Type::Prim(PrimType::I64),
+            ))
+        }
         "writeFile" => {
             // String → String → Unit (write content to file)
             Some(Type::func_n(
diff --git a/crates/goth-check/src/context.rs b/crates/goth-check/src/context.rs
index c5422b4..e798e28 100644
--- a/crates/goth-check/src/context.rs
+++ b/crates/goth-check/src/context.rs
@@ -2,21 +2,25 @@
 
 use std::collections::{HashMap, HashSet};
 use goth_ast::types::Type;
+use goth_ast::shape::Dim;
 
 /// Type checking context
 #[derive(Debug, Clone)]
 pub struct Context {
     /// Type stack for de Bruijn indices (index 0 = last element)
     stack: Vec<Type>,
-    
+
     /// Global name → type bindings
     globals: HashMap<String, Type>,
-    
+
     /// Type variables in scope
     type_vars: HashSet<String>,
-    
+
     /// Shape variables in scope
     shape_vars: HashSet<String>,
+
+    /// Counter for generating fresh type/shape variable names
+    fresh_counter: u32,
 }
 
 impl Context {
@@ -26,6 +30,7 @@ impl Context {
             globals: HashMap::new(),
             type_vars: HashSet::new(),
             shape_vars: HashSet::new(),
+            fresh_counter: 0,
         }
     }
 
@@ -107,6 +112,20 @@ impl Context {
         self.shape_vars.contains(name)
     }
 
+    /// Generate a fresh type variable
+    pub fn fresh_type_var(&mut self) -> Type {
+        let name = format!("_t{}", self.fresh_counter);
+        self.fresh_counter += 1;
+        Type::Var(name.into())
+    }
+
+    /// Generate a fresh shape/dimension variable
+    pub fn fresh_shape_var(&mut self) -> Dim {
+        let name = format!("_d{}", self.fresh_counter);
+        self.fresh_counter += 1;
+        Dim::Var(name.into())
+    }
+
     /// Execute with type variables in scope
     pub fn with_type_vars<T>(&mut self, vars: &[String], f: impl FnOnce(&mut Self) -> T) -> T {
         for v in vars {
diff --git a/crates/goth-check/src/infer.rs b/crates/goth-check/src/infer.rs
index 31ffe0c..4f7caed 100644
--- a/crates/goth-check/src/infer.rs
+++ b/crates/goth-check/src/infer.rs
@@ -68,13 +68,34 @@ pub fn infer(ctx: &mut Context, expr: &Expr) -> TypeResult<Type> {
         }
         
         Expr::LetRec { bindings, body } => {
-            // For recursive bindings, we need type annotations
-            // For now, assume all are lambdas with holes
-            let placeholder_types: Vec<Type> = bindings.iter()
-                .map(|_| Type::Hole)
+            // Extract type annotations from Pattern::Typed or Expr::Annot
+            let binding_types: Vec<Type> = bindings.iter()
+                .map(|(pat, val)| {
+                    // Check pattern for type annotation
+                    if let Pattern::Typed(_, ty) = pat {
+                        return ty.clone();
+                    }
+                    // Check value for type annotation
+                    if let Expr::Annot(_, ty) = val {
+                        return ty.clone();
+                    }
+                    Type::Hole
+                })
                 .collect();
-            
-            ctx.with_bindings(&placeholder_types, |ctx| {
+
+            ctx.with_bindings(&binding_types, |ctx| {
+                // Type-check each binding body against its declared type
+                for (i, (_pat, val)) in bindings.iter().enumerate() {
+                    match &binding_types[i] {
+                        Type::Hole => {
+                            // No annotation — just infer to catch internal errors
+                            let _ = infer(ctx, val);
+                        }
+                        ann_ty => {
+                            let _ = check(ctx, val, ann_ty);
+                        }
+                    }
+                }
                 infer(ctx, body)
             })
         }
@@ -312,9 +333,12 @@ pub fn infer(ctx: &mut Context, expr: &Expr) -> TypeResult<Type> {
             Ok(ty.clone())
         }
         
-        Expr::Cast { expr, target, .. } => {
-            let _ = infer(ctx, expr)?;
-            Ok(target.clone())
+        Expr::Cast { expr, target, kind } => {
+            let _source_ty = infer(ctx, expr)?;
+            match kind {
+                goth_ast::expr::CastKind::Try => Ok(Type::Option(Box::new(target.clone()))),
+                goth_ast::expr::CastKind::Static | goth_ast::expr::CastKind::Force => Ok(target.clone()),
+            }
         }
         
         // ============ Special ============
@@ -323,6 +347,138 @@ pub fn infer(ctx: &mut Context, expr: &Expr) -> TypeResult<Type> {
         
         Expr::Disabled(_) => Ok(Type::unit()),
         
+        Expr::Update { base, fields } => {
+            let base_ty = infer(ctx, base)?;
+            match &base_ty {
+                Type::Tuple(tuple_fields) => {
+                    for (name, val_expr) in fields {
+                        // Find the field in the record type
+                        let field_ty = tuple_fields.iter()
+                            .find(|f| f.label.as_deref() == Some(name.as_ref()))
+                            .map(|f| &f.ty)
+                            .ok_or_else(|| TypeError::FieldNotFound {
+                                field: name.to_string(),
+                                ty: base_ty.clone(),
+                            })?;
+                        check(ctx, val_expr, field_ty)?;
+                    }
+                    Ok(base_ty.clone())
+                }
+                _ => Err(TypeError::FieldNotFound {
+                    field: "update".to_string(),
+                    ty: base_ty,
+                })
+            }
+        }
+
+        Expr::Do { init, ops } => {
+            use goth_ast::expr::DoOp;
+            let mut current_ty = infer(ctx, init)?;
+
+            for op in ops {
+                current_ty = match op {
+                    DoOp::Map(f) => {
+                        match &current_ty {
+                            Type::Tensor(shape, elem_ty) => {
+                                // f: A → B, applied element-wise
+                                match f {
+                                    Expr::Lam(body) => {
+                                        let ret_ty = ctx.with_binding(*elem_ty.clone(), |ctx| {
+                                            infer(ctx, body)
+                                        })?;
+                                        Type::Tensor(shape.clone(), Box::new(ret_ty))
+                                    }
+                                    _ => {
+                                        let f_ty = infer(ctx, f)?;
+                                        match f_ty {
+                                            Type::Fn(_, ret) => Type::Tensor(shape.clone(), ret),
+                                            _ => Type::Hole,
+                                        }
+                                    }
+                                }
+                            }
+                            _ => Type::Hole,
+                        }
+                    }
+
+                    DoOp::Filter(pred) => {
+                        match &current_ty {
+                            Type::Tensor(_, elem_ty) => {
+                                // pred: A → Bool
+                                match pred {
+                                    Expr::Lam(body) => {
+                                        let pred_ty = ctx.with_binding(*elem_ty.clone(), |ctx| {
+                                            infer(ctx, body)
+                                        })?;
+                                        let _ = unify(&pred_ty, &Type::Prim(PrimType::Bool))?;
+                                    }
+                                    _ => {
+                                        let _ = infer(ctx, pred)?;
+                                    }
+                                }
+                                // Result has unknown length, same element type
+                                Type::Tensor(
+                                    goth_ast::shape::Shape(vec![goth_ast::shape::Dim::Var("?".into())]),
+                                    elem_ty.clone(),
+                                )
+                            }
+                            _ => Type::Hole,
+                        }
+                    }
+
+                    DoOp::Bind(f) => {
+                        match &current_ty {
+                            Type::Tensor(_, elem_ty) => {
+                                // f: A → [m]B (flatmap)
+                                match f {
+                                    Expr::Lam(body) => {
+                                        let ret_ty = ctx.with_binding(*elem_ty.clone(), |ctx| {
+                                            infer(ctx, body)
+                                        })?;
+                                        match ret_ty {
+                                            Type::Tensor(_, inner_elem) => Type::Tensor(
+                                                goth_ast::shape::Shape(vec![goth_ast::shape::Dim::Var("?".into())]),
+                                                inner_elem,
+                                            ),
+                                            _ => Type::Hole,
+                                        }
+                                    }
+                                    _ => {
+                                        let f_ty = infer(ctx, f)?;
+                                        match f_ty {
+                                            Type::Fn(_, ret) => match *ret {
+                                                Type::Tensor(_, inner_elem) => Type::Tensor(
+                                                    goth_ast::shape::Shape(vec![goth_ast::shape::Dim::Var("?".into())]),
+                                                    inner_elem,
+                                                ),
+                                                _ => Type::Hole,
+                                            },
+                                            _ => Type::Hole,
+                                        }
+                                    }
+                                }
+                            }
+                            _ => Type::Hole,
+                        }
+                    }
+
+                    DoOp::Op(binop, e) => {
+                        let right_ty = infer(ctx, e)?;
+                        binop_type(binop.clone(), &current_ty, &right_ty).unwrap_or(Type::Hole)
+                    }
+
+                    DoOp::Let(pat, e) => {
+                        let val_ty = infer(ctx, e)?;
+                        let bindings = pattern_types(pat, &val_ty)?;
+                        ctx.push_many(&bindings);
+                        val_ty
+                    }
+                };
+            }
+
+            Ok(current_ty)
+        }
+
         _ => {
             // Fallback for unhandled cases
             Ok(Type::Hole)
@@ -340,15 +496,14 @@ fn infer_app(ctx: &mut Context, func_ty: &Type, arg: &Expr) -> TypeResult<Type>
         
         Type::Forall(params, body) => {
             // Instantiate with fresh type variables
-            // For now, just use holes
             let mut subst = Subst::new();
             for p in params {
                 match p.kind {
                     goth_ast::types::TypeParamKind::Type => {
-                        subst.types.insert(p.name.to_string(), Type::Hole);
+                        subst.types.insert(p.name.to_string(), ctx.fresh_type_var());
                     }
                     goth_ast::types::TypeParamKind::Shape => {
-                        subst.shapes.insert(p.name.to_string(), goth_ast::shape::Dim::Var("?".into()));
+                        subst.shapes.insert(p.name.to_string(), ctx.fresh_shape_var());
                     }
                     _ => {}
                 }
diff --git a/crates/goth-check/src/subst.rs b/crates/goth-check/src/subst.rs
index fe27283..04aa332 100644
--- a/crates/goth-check/src/subst.rs
+++ b/crates/goth-check/src/subst.rs
@@ -114,10 +114,36 @@ pub fn apply_type(subst: &Subst, ty: &Type) -> Type {
                 predicate: predicate.clone(), // Predicates need separate handling
             }
         }
+        Type::Variant(arms) => {
+            Type::Variant(
+                arms.iter().map(|arm| goth_ast::types::VariantArm {
+                    name: arm.name.clone(),
+                    payload: arm.payload.as_ref().map(|t| apply_type(subst, t)),
+                }).collect()
+            )
+        }
+        Type::Exists(params, body) => {
+            // Don't substitute bound variables (same as Forall)
+            let mut inner_subst = subst.clone();
+            for p in params {
+                inner_subst.types.remove(p.name.as_ref());
+            }
+            Type::Exists(params.clone(), Box::new(apply_type(&inner_subst, body)))
+        }
+        Type::App(f, args) => {
+            Type::App(
+                Box::new(apply_type(subst, f)),
+                args.iter().map(|a| apply_type(subst, a)).collect(),
+            )
+        }
+        Type::Effectful(inner, effects) => {
+            Type::Effectful(Box::new(apply_type(subst, inner)), effects.clone())
+        }
+        Type::Interval(inner, intervals) => {
+            Type::Interval(Box::new(apply_type(subst, inner)), intervals.clone())
+        }
         // Primitives and holes don't change
         Type::Prim(_) | Type::Hole => ty.clone(),
-        // TODO: Handle remaining cases
-        _ => ty.clone(),
     }
 }
 
diff --git a/crates/goth-cli/Cargo.toml b/crates/goth-cli/Cargo.toml
index 749303b..7c92db9 100644
--- a/crates/goth-cli/Cargo.toml
+++ b/crates/goth-cli/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "goth-cli"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "Command-line interface and REPL for the Goth programming language"
 license = "MIT"
@@ -29,3 +29,6 @@ clap = { version = "4.4", features = ["derive"] }
 colored = "2.1"
 dirs = "5.0"
 serde_json = "1.0"
+
+[target.'cfg(unix)'.dependencies]
+libc = "0.2"
diff --git a/crates/goth-cli/src/main.rs b/crates/goth-cli/src/main.rs
index d09be46..e2429e1 100644
--- a/crates/goth-cli/src/main.rs
+++ b/crates/goth-cli/src/main.rs
@@ -95,6 +95,26 @@ struct Args {
 }
 
 fn main() {
+    // Register atexit handler to restore terminal if raw mode was entered
+    #[cfg(unix)]
+    unsafe {
+        extern "C" fn cleanup() { goth_eval::prim::restore_terminal(); }
+        libc::atexit(cleanup);
+    }
+
+    // Wrap execution in catch_unwind so panics restore terminal state
+    let result = std::panic::catch_unwind(std::panic::AssertUnwindSafe(|| {
+        run_main();
+    }));
+
+    if result.is_err() {
+        goth_eval::prim::restore_terminal();
+        eprintln!("goth: internal error (panic). Terminal restored.");
+        std::process::exit(1);
+    }
+}
+
+fn run_main() {
     let args = Args::parse();
 
     // ============ AST-First LLM Workflow ============
@@ -610,7 +630,10 @@ fn handle_command(cmd: &str, evaluator: &mut Evaluator, type_checker: &mut TypeC
 
     match command {
         ":help" | ":h" | ":?" => print_help(),
-        ":quit" | ":q" => std::process::exit(0),
+        ":quit" | ":q" => {
+            goth_eval::prim::restore_terminal();
+            std::process::exit(0);
+        }
         ":ast" => {
             if let Some(expr_str) = arg {
                 match parse_expr(expr_str) {
@@ -974,7 +997,7 @@ fn run_to_json_expr(source: &str, compact: bool) {
 fn print_banner() {
     println!("{}", r#"
    ╔═══════════════════════════════════════╗
-   ║             𝖌𝖔𝖙𝖍  v0.1.0              ║
+   ║             𝖌𝖔𝖙𝖍  v0.2.0              ║
    ║   Functional • Tensors • Refinements  ║
    ╚═══════════════════════════════════════╝
 "#.cyan());
diff --git a/crates/goth-eval/Cargo.toml b/crates/goth-eval/Cargo.toml
index 1807d4a..40d0b47 100644
--- a/crates/goth-eval/Cargo.toml
+++ b/crates/goth-eval/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "goth-eval"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "Interpreter for the Goth programming language"
 license = "MIT"
@@ -8,7 +8,7 @@ repository = "https://github.com/goth-lang/goth"
 
 [dependencies]
 goth-ast = { path = "../goth-ast" }
-thiserror = "1.0"
+thiserror = "2.0"
 ordered-float = { version = "4.2", features = ["serde"] }
 
 [target.'cfg(unix)'.dependencies]
diff --git a/crates/goth-eval/src/error.rs b/crates/goth-eval/src/error.rs
index b02acf6..acf3bcb 100644
--- a/crates/goth-eval/src/error.rs
+++ b/crates/goth-eval/src/error.rs
@@ -35,6 +35,8 @@ pub enum EvalError {
     EffectNotAllowed(String),
     #[error("IO error: {0}")]
     IoError(String),
+    #[error("Arithmetic overflow: {0}")]
+    Overflow(String),
     #[error("Not implemented: {0}")]
     NotImplemented(String),
     #[error("Internal error: {0}")]
diff --git a/crates/goth-eval/src/eval.rs b/crates/goth-eval/src/eval.rs
index be78551..26cf80a 100644
--- a/crates/goth-eval/src/eval.rs
+++ b/crates/goth-eval/src/eval.rs
@@ -59,14 +59,20 @@ impl Evaluator {
             ("readLine", PrimFn::ReadLine), ("read_line", PrimFn::ReadLine),
             ("readKey", PrimFn::ReadKey), ("read_key", PrimFn::ReadKey),  // Read single key
             ("readFile", PrimFn::ReadFile), ("writeFile", PrimFn::WriteFile),
+            ("readBytes", PrimFn::ReadBytes), ("⧏", PrimFn::ReadBytes),
+            ("writeBytes", PrimFn::WriteBytes), ("⧐", PrimFn::WriteBytes),
             ("rawModeEnter", PrimFn::RawModeEnter), ("rawModeExit", PrimFn::RawModeExit),  // Terminal raw mode
             ("sleep", PrimFn::Sleep),  // Sleep for milliseconds
             ("toInt", PrimFn::ToInt), ("toFloat", PrimFn::ToFloat), ("toBool", PrimFn::ToBool), ("toChar", PrimFn::ToChar),
             ("parseInt", PrimFn::ParseInt), ("parseFloat", PrimFn::ParseFloat),
             ("toString", PrimFn::ToString), ("str", PrimFn::ToString),
-            ("chars", PrimFn::Chars),
+            ("chars", PrimFn::Chars), ("fromChars", PrimFn::FromChars),
             ("strConcat", PrimFn::StrConcat), ("⧺", PrimFn::StrConcat),  // double plus
-            ("filter", PrimFn::Filter), ("map", PrimFn::Map), ("fold", PrimFn::Fold),
+            ("filter", PrimFn::Filter), ("map", PrimFn::Map), ("fold", PrimFn::Fold), ("⌿", PrimFn::Fold),
+            // Bitwise operations
+            ("bitand", PrimFn::BitAnd), ("bitor", PrimFn::BitOr),
+            ("bitxor", PrimFn::BitXor), ("⊻", PrimFn::BitXor),
+            ("shl", PrimFn::Shl), ("shr", PrimFn::Shr),
             ("index", PrimFn::Index),
             ("take", PrimFn::Take), ("↑", PrimFn::Take),  // APL take
             ("drop", PrimFn::Drop), ("↓", PrimFn::Drop),  // APL drop
@@ -235,7 +241,16 @@ impl Evaluator {
                                 Ok(TcoResult::Done(result))
                             }
                         }
-                        Value::Primitive(prim) => Ok(TcoResult::Done(prim::apply_prim(prim, args)?)),
+                        Value::Primitive(prim) => {
+                            if prim == PrimFn::Fold && args.len() == 3 {
+                                let func = args.remove(0);
+                                let acc = args.remove(0);
+                                let arr = args.remove(0);
+                                Ok(TcoResult::Done(self.eval_fold(func, acc, arr)?))
+                            } else {
+                                Ok(TcoResult::Done(prim::apply_prim(prim, args)?))
+                            }
+                        }
                         _ => Err(EvalError::type_error("function", &func)),
                     }
                 } else {
@@ -437,8 +452,48 @@ impl Evaluator {
 
     fn eval_filter(&mut self, arr: Value, pred: Value) -> EvalResult<Value> {
         match arr {
-            Value::Tensor(t) => { let results: Vec<Value> = t.iter().filter_map(|elem| { let keep = self.apply(pred.clone(), elem.clone()).ok()?; match keep { Value::Bool(true) => Some(elem), _ => None } }).collect(); Ok(self.values_to_tensor_shaped(vec![results.len()], results)) }
-            Value::Tuple(vs) => { let results: Vec<Value> = vs.into_iter().filter_map(|elem| { let keep = self.apply(pred.clone(), elem.clone()).ok()?; match keep { Value::Bool(true) => Some(elem), _ => None } }).collect(); Ok(Value::Tuple(results)) }
+            Value::Tensor(t) => {
+                let mut results = Vec::new();
+                for elem in t.iter() {
+                    let keep = self.apply(pred.clone(), elem.clone())?;
+                    if keep == Value::Bool(true) {
+                        results.push(elem);
+                    }
+                }
+                Ok(self.values_to_tensor_shaped(vec![results.len()], results))
+            }
+            Value::Tuple(vs) => {
+                let mut results = Vec::new();
+                for elem in vs {
+                    let keep = self.apply(pred.clone(), elem.clone())?;
+                    if keep == Value::Bool(true) {
+                        results.push(elem);
+                    }
+                }
+                Ok(Value::Tuple(results))
+            }
+            _ => Err(EvalError::type_error("Tensor or Tuple", &arr)),
+        }
+    }
+
+    fn eval_fold(&mut self, func: Value, init: Value, arr: Value) -> EvalResult<Value> {
+        match arr {
+            Value::Tensor(t) => {
+                let mut acc = init;
+                for elem in t.iter() {
+                    let partial = self.apply(func.clone(), acc)?;
+                    acc = self.apply(partial, elem)?;
+                }
+                Ok(acc)
+            }
+            Value::Tuple(vs) => {
+                let mut acc = init;
+                for elem in vs {
+                    let partial = self.apply(func.clone(), acc)?;
+                    acc = self.apply(partial, elem)?;
+                }
+                Ok(acc)
+            }
             _ => Err(EvalError::type_error("Tensor or Tuple", &arr)),
         }
     }
@@ -548,7 +603,8 @@ fn prim_arity(prim: PrimFn) -> usize {
         PrimFn::Print | PrimFn::Write | PrimFn::ReadLine | PrimFn::ReadKey | PrimFn::ReadFile | PrimFn::Sleep => 1,
         PrimFn::Flush | PrimFn::RawModeEnter | PrimFn::RawModeExit => 1,  // Terminal control (take unit)
         PrimFn::Lines | PrimFn::Words | PrimFn::Bytes => 1,  // String splitting (unary)
-        PrimFn::WriteFile => 2,  // WriteFile takes path and content
+        PrimFn::WriteFile | PrimFn::ReadBytes | PrimFn::WriteBytes => 2,  // Binary I/O takes 2 args
+        PrimFn::Fold => 3,  // fold f acc arr
         PrimFn::StrEq | PrimFn::StartsWith | PrimFn::EndsWith | PrimFn::Contains => 2,  // String comparison (binary)
         _ => 2,  // Range, StrConcat, Take, Drop, Index etc take 2 args
     }
diff --git a/crates/goth-eval/src/prim.rs b/crates/goth-eval/src/prim.rs
index 155e869..863445a 100644
--- a/crates/goth-eval/src/prim.rs
+++ b/crates/goth-eval/src/prim.rs
@@ -6,7 +6,23 @@ use ordered_float::OrderedFloat;
 
 // Store original terminal settings for raw mode restoration
 #[cfg(unix)]
-static mut ORIGINAL_TERMIOS: Option<libc::termios> = None;
+static ORIGINAL_TERMIOS: std::sync::Mutex<Option<libc::termios>> = std::sync::Mutex::new(None);
+
+/// Restore terminal to its original settings if raw mode was entered.
+/// Safe to call multiple times — no-ops if terminal is already restored.
+#[cfg(unix)]
+pub fn restore_terminal() {
+    use std::os::unix::io::AsRawFd;
+    if let Ok(mut guard) = ORIGINAL_TERMIOS.lock() {
+        if let Some(termios) = guard.take() {
+            let fd = std::io::stdin().as_raw_fd();
+            unsafe { libc::tcsetattr(fd, libc::TCSANOW, &termios); }
+        }
+    }
+}
+
+#[cfg(not(unix))]
+pub fn restore_terminal() {}
 
 // ============ Uncertainty propagation helpers ============
 
@@ -196,7 +212,9 @@ pub fn apply_prim(prim: PrimFn, args: Vec<Value>) -> EvalResult<Value> {
                         return Err(EvalError::IoError("Failed to get terminal attributes".to_string()));
                     }
                     // Save original termios for restoration
-                    ORIGINAL_TERMIOS = Some(termios);
+                    if let Ok(mut guard) = ORIGINAL_TERMIOS.lock() {
+                        *guard = Some(termios);
+                    }
                     // Disable canonical mode and echo
                     termios.c_lflag &= !(libc::ICANON | libc::ECHO);
                     // Set minimum characters and timeout
@@ -216,16 +234,7 @@ pub fn apply_prim(prim: PrimFn, args: Vec<Value>) -> EvalResult<Value> {
         PrimFn::RawModeExit => {
             #[cfg(unix)]
             {
-                use std::os::unix::io::AsRawFd;
-                let fd = std::io::stdin().as_raw_fd();
-                unsafe {
-                    if let Some(termios) = ORIGINAL_TERMIOS {
-                        if libc::tcsetattr(fd, libc::TCSANOW, &termios) != 0 {
-                            return Err(EvalError::IoError("Failed to restore terminal attributes".to_string()));
-                        }
-                        ORIGINAL_TERMIOS = None;
-                    }
-                }
+                restore_terminal();
                 Ok(Value::Unit)
             }
             #[cfg(not(unix))]
@@ -267,10 +276,47 @@ pub fn apply_prim(prim: PrimFn, args: Vec<Value>) -> EvalResult<Value> {
             fs::write(&path, &contents).map_err(|e| EvalError::IoError(format!("Failed to write '{}': {}", path, e)))?;
             Ok(Value::Unit)
         }
+        PrimFn::ReadBytes => {
+            if args.len() != 2 { return Err(EvalError::ArityMismatch { expected: 2, got: args.len() }); }
+            let count = match &args[0] {
+                Value::Int(n) => *n as usize,
+                _ => return Err(EvalError::type_error("Int", &args[0])),
+            };
+            let path = match &args[1] {
+                Value::Tensor(t) => t.to_string_value().ok_or_else(|| EvalError::type_error("String", &args[1]))?,
+                _ => return Err(EvalError::type_error("String", &args[1])),
+            };
+            use std::io::Read;
+            let mut file = std::fs::File::open(&path)
+                .map_err(|e| EvalError::IoError(format!("Failed to open '{}': {}", path, e)))?;
+            let mut buf = vec![0u8; count];
+            file.read_exact(&mut buf)
+                .map_err(|e| EvalError::IoError(format!("Failed to read {} bytes from '{}': {}", count, path, e)))?;
+            let byte_vals: Vec<i128> = buf.iter().map(|&b| b as i128).collect();
+            Ok(Value::Tensor(Tensor::from_ints(byte_vals)))
+        }
+        PrimFn::WriteBytes => {
+            if args.len() != 2 { return Err(EvalError::ArityMismatch { expected: 2, got: args.len() }); }
+            let bytes: Vec<u8> = match &args[0] {
+                Value::Tensor(t) => t.to_vec().iter().map(|v| match v {
+                    Value::Int(n) => Ok(*n as u8),
+                    _ => Err(EvalError::type_error("Int", v)),
+                }).collect::<Result<Vec<u8>, _>>()?,
+                _ => return Err(EvalError::type_error("Tensor", &args[0])),
+            };
+            let path = match &args[1] {
+                Value::Tensor(t) => t.to_string_value().ok_or_else(|| EvalError::type_error("String", &args[1]))?,
+                _ => return Err(EvalError::type_error("String", &args[1])),
+            };
+            std::fs::write(&path, &bytes)
+                .map_err(|e| EvalError::IoError(format!("Failed to write '{}': {}", path, e)))?;
+            Ok(Value::Unit)
+        }
         PrimFn::Iota => unary_args(&args, iota),
         PrimFn::Range => binary_args(&args, range),
         PrimFn::ToString => unary_args(&args, to_string),
         PrimFn::Chars => unary_args(&args, chars),
+        PrimFn::FromChars => unary_args(&args, from_chars),
         PrimFn::StrConcat => binary_args(&args, str_concat),
         PrimFn::Take => binary_args(&args, take),
         PrimFn::Drop => binary_args(&args, drop_fn),
@@ -282,6 +328,11 @@ pub fn apply_prim(prim: PrimFn, args: Vec<Value>) -> EvalResult<Value> {
         PrimFn::StartsWith => binary_args(&args, starts_with),
         PrimFn::EndsWith => binary_args(&args, ends_with),
         PrimFn::Contains => binary_args(&args, str_contains),
+        PrimFn::BitAnd => binary_args(&args, bitand),
+        PrimFn::BitOr => binary_args(&args, bitor),
+        PrimFn::BitXor => binary_args(&args, bitxor),
+        PrimFn::Shl => binary_args(&args, shl),
+        PrimFn::Shr => binary_args(&args, shr),
         _ => Err(EvalError::not_implemented(format!("primitive: {:?}", prim))),
     }
 }
@@ -315,7 +366,7 @@ fn add(left: Value, right: Value) -> EvalResult<Value> {
             let (b, db) = uncertain_parts(&right).unwrap();
             Ok(make_uncertain(a + b, db))
         }
-        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a + b)),
+        (Value::Int(a), Value::Int(b)) => a.checked_add(*b).map(Value::Int).ok_or_else(|| EvalError::Overflow(format!("{} + {} overflows", a, b))),
         (Value::Float(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(a.0 + b.0))),
         (Value::Int(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(*a as f64 + b.0))),
         (Value::Float(a), Value::Int(b)) => Ok(Value::Float(OrderedFloat(a.0 + *b as f64))),
@@ -347,7 +398,7 @@ fn sub(left: Value, right: Value) -> EvalResult<Value> {
             let (b, db) = uncertain_parts(&right).unwrap();
             Ok(make_uncertain(a - b, db))
         }
-        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a - b)),
+        (Value::Int(a), Value::Int(b)) => a.checked_sub(*b).map(Value::Int).ok_or_else(|| EvalError::Overflow(format!("{} - {} overflows", a, b))),
         (Value::Float(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(a.0 - b.0))),
         (Value::Int(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(*a as f64 - b.0))),
         (Value::Float(a), Value::Int(b)) => Ok(Value::Float(OrderedFloat(a.0 - *b as f64))),
@@ -377,7 +428,7 @@ fn mul(left: Value, right: Value) -> EvalResult<Value> {
             let (b, db) = uncertain_parts(&right).unwrap();
             Ok(make_uncertain(a * b, (a * db).abs()))
         }
-        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a * b)),
+        (Value::Int(a), Value::Int(b)) => a.checked_mul(*b).map(Value::Int).ok_or_else(|| EvalError::Overflow(format!("{} × {} overflows", a, b))),
         (Value::Float(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(a.0 * b.0))),
         (Value::Int(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(*a as f64 * b.0))),
         (Value::Float(a), Value::Int(b)) => Ok(Value::Float(OrderedFloat(a.0 * *b as f64))),
@@ -433,6 +484,53 @@ fn modulo(left: Value, right: Value) -> EvalResult<Value> {
     }
 }
 
+fn bitand(left: Value, right: Value) -> EvalResult<Value> {
+    match (&left, &right) {
+        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a & b)),
+        _ => Err(EvalError::type_error_msg(format!("Cannot bitand {} and {}", left.type_name(), right.type_name())))
+    }
+}
+
+fn bitor(left: Value, right: Value) -> EvalResult<Value> {
+    match (&left, &right) {
+        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a | b)),
+        _ => Err(EvalError::type_error_msg(format!("Cannot bitor {} and {}", left.type_name(), right.type_name())))
+    }
+}
+
+fn bitxor(left: Value, right: Value) -> EvalResult<Value> {
+    match (&left, &right) {
+        (Value::Int(a), Value::Int(b)) => Ok(Value::Int(a ^ b)),
+        _ => Err(EvalError::type_error_msg(format!("Cannot bitxor {} and {}", left.type_name(), right.type_name())))
+    }
+}
+
+fn shl(left: Value, right: Value) -> EvalResult<Value> {
+    match (&left, &right) {
+        (Value::Int(a), Value::Int(b)) => {
+            if *b < 0 || *b > 127 {
+                Err(EvalError::Overflow(format!("shift left by {} out of range 0..127", b)))
+            } else {
+                Ok(Value::Int(a << (*b as u32)))
+            }
+        }
+        _ => Err(EvalError::type_error_msg(format!("Cannot shl {} and {}", left.type_name(), right.type_name())))
+    }
+}
+
+fn shr(left: Value, right: Value) -> EvalResult<Value> {
+    match (&left, &right) {
+        (Value::Int(a), Value::Int(b)) => {
+            if *b < 0 || *b > 127 {
+                Err(EvalError::Overflow(format!("shift right by {} out of range 0..127", b)))
+            } else {
+                Ok(Value::Int(a >> (*b as u32)))
+            }
+        }
+        _ => Err(EvalError::type_error_msg(format!("Cannot shr {} and {}", left.type_name(), right.type_name())))
+    }
+}
+
 fn pow(left: Value, right: Value) -> EvalResult<Value> {
     match (&left, &right) {
         // (a ± δa) ^ (b ± δb): full general case
@@ -460,9 +558,25 @@ fn pow(left: Value, right: Value) -> EvalResult<Value> {
             let unc = if a > 0.0 { (result * a.ln() * db).abs() } else { 0.0 };
             Ok(make_uncertain(result, unc))
         }
-        (Value::Int(a), Value::Int(b)) => if *b >= 0 { Ok(Value::Int(a.pow(*b as u32))) } else { Ok(Value::Float(OrderedFloat((*a as f64).powi(*b as i32)))) },
+        (Value::Int(a), Value::Int(b)) => {
+            if *b < 0 {
+                Ok(Value::Float(OrderedFloat((*a as f64).powi(*b as i32))))
+            } else if *b > u32::MAX as i128 {
+                Err(EvalError::Overflow(format!("exponent {} too large", b)))
+            } else {
+                a.checked_pow(*b as u32)
+                    .map(|r| Value::Int(r))
+                    .ok_or_else(|| EvalError::Overflow(format!("{} ^ {} overflows i128", a, b)))
+            }
+        }
         (Value::Float(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat(a.0.powf(b.0)))),
-        (Value::Float(a), Value::Int(b)) => Ok(Value::Float(OrderedFloat(a.0.powi(*b as i32)))),
+        (Value::Float(a), Value::Int(b)) => {
+            if *b > i32::MAX as i128 || *b < i32::MIN as i128 {
+                Ok(Value::Float(OrderedFloat(a.0.powf(*b as f64))))
+            } else {
+                Ok(Value::Float(OrderedFloat(a.0.powi(*b as i32))))
+            }
+        }
         (Value::Int(a), Value::Float(b)) => Ok(Value::Float(OrderedFloat((*a as f64).powf(b.0)))),
         _ => Err(EvalError::type_error_msg(format!("Cannot raise {} to power {}", left.type_name(), right.type_name()))),
     }
@@ -474,7 +588,7 @@ fn negate(value: Value) -> EvalResult<Value> {
             let (a, da) = uncertain_parts(&value).unwrap();
             Ok(make_uncertain(-a, da))
         }
-        Value::Int(n) => Ok(Value::Int(-n)),
+        Value::Int(n) => n.checked_neg().map(Value::Int).ok_or_else(|| EvalError::Overflow(format!("negation of {} overflows", n))),
         Value::Float(f) => Ok(Value::Float(OrderedFloat(-f.0))),
         Value::Tensor(t) => Ok(Value::Tensor(t.map(|x| negate(x).unwrap_or(Value::Error("negate failed".into()))))),
         _ => Err(EvalError::type_error("numeric", &value)),
@@ -924,6 +1038,28 @@ fn chars(value: Value) -> EvalResult<Value> {
     }
 }
 
+/// fromChars: Convert an array of characters to a string
+fn from_chars(value: Value) -> EvalResult<Value> {
+    match value {
+        Value::Tensor(t) => {
+            // If already a char tensor (string), return as-is
+            if t.to_string_value().is_some() {
+                return Ok(Value::Tensor(t));
+            }
+            // Otherwise try to collect Char values into a string
+            let mut s = String::with_capacity(t.len());
+            for v in t.iter() {
+                match v {
+                    Value::Char(c) => s.push(c),
+                    _ => return Err(EvalError::type_error("Char", &v)),
+                }
+            }
+            Ok(Value::string(&s))
+        }
+        _ => Err(EvalError::type_error("Tensor", &value)),
+    }
+}
+
 /// strConcat: Concatenate two strings
 fn str_concat(left: Value, right: Value) -> EvalResult<Value> {
     match (&left, &right) {
diff --git a/crates/goth-eval/src/value.rs b/crates/goth-eval/src/value.rs
index fd457a3..168a030 100644
--- a/crates/goth-eval/src/value.rs
+++ b/crates/goth-eval/src/value.rs
@@ -68,13 +68,14 @@ pub enum PrimFn {
     Index, Slice, Take, Drop,
     Iota, Range,  // Sequence generation
     MatMul, Dot, Outer, Inner, Norm,
-    Chars, ToString, StrConcat,
-    Print, Write, Flush, ReadLine, ReadKey, ReadFile, WriteFile,
+    Chars, FromChars, ToString, StrConcat,
+    Print, Write, Flush, ReadLine, ReadKey, ReadFile, WriteFile, ReadBytes, WriteBytes,
     RawModeEnter, RawModeExit, Sleep,
     ToInt, ToFloat, ToBool, ToChar,
     ParseInt, ParseFloat,  // String parsing
     Lines, Words, Bytes,  // String splitting for wc
     StrEq, StartsWith, EndsWith, Contains,  // String comparison
+    BitAnd, BitOr, BitXor, Shl, Shr,  // Bitwise operations
 }
 
 #[derive(Debug, Clone)]
@@ -284,7 +285,13 @@ impl Env {
     pub fn extend(&self, other: &Env) -> Self { let mut values = self.values.clone(); values.extend(other.values.iter().cloned()); Env { values, globals: Rc::clone(&self.globals) } }
 }
 
-impl PartialEq for Closure { fn eq(&self, other: &Self) -> bool { self.arity == other.arity && self.body == other.body } }
+impl PartialEq for Closure {
+    fn eq(&self, other: &Self) -> bool {
+        self.arity == other.arity
+            && self.body == other.body
+            && self.env.values == other.env.values
+    }
+}
 impl PartialEq for Thunk { fn eq(&self, other: &Self) -> bool { self.expr == other.expr } }
 
 impl std::fmt::Display for Value {
diff --git a/crates/goth-mlir/Cargo.toml b/crates/goth-mlir/Cargo.toml
index 4965122..cad849f 100644
--- a/crates/goth-mlir/Cargo.toml
+++ b/crates/goth-mlir/Cargo.toml
@@ -17,7 +17,7 @@ text-emit = []
 [dependencies]
 goth-ast = { path = "../goth-ast" }
 goth-mir = { path = "../goth-mir" }
-thiserror = "1.0"
+thiserror = "2.0"
 regex = "1.10"
 # Rust bindings to MLIR (optional, requires LLVM 17+)
 melior = { version = "0.18", optional = true }
diff --git a/crates/goth-parse/Cargo.toml b/crates/goth-parse/Cargo.toml
index 052d33a..98a220f 100644
--- a/crates/goth-parse/Cargo.toml
+++ b/crates/goth-parse/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "goth-parse"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "Parser for the Goth programming language"
 license = "MIT"
@@ -8,7 +8,7 @@ repository = "https://github.com/goth-lang/goth"
 
 [dependencies]
 goth-ast = { path = "../goth-ast" }
-thiserror = "1.0"
+thiserror = "2.0"
 logos = "0.14"
 serde_json = "1.0"
 bincode = "1.3"
diff --git a/crates/goth-parse/src/lexer.rs b/crates/goth-parse/src/lexer.rs
index 083e3cd..9695f78 100644
--- a/crates/goth-parse/src/lexer.rs
+++ b/crates/goth-parse/src/lexer.rs
@@ -383,7 +383,7 @@ pub enum Token {
 
     // ============ APL-style single character identifiers ============
     // Note: ⧺ (concat) is now a dedicated token, not an identifier
-    #[regex(r"[⍳⍴⌽⍉·…↑↓]", priority = 5, callback = |lex| lex.slice().to_string())]
+    #[regex(r"[⍳⍴⌽⍉·…↑↓⧏⧐⊻⌿]", priority = 5, callback = |lex| lex.slice().to_string())]
     AplIdent(String),
 
     // ============ Primitive Types ============
@@ -417,6 +417,9 @@ pub enum Token {
     TyInt,
     #[token("Unit")]
     TyUnit,
+
+    /// Invalid/unrecognized token (not generated by logos; constructed by the lexer)
+    Error(String),
 }
 
 fn parse_index(s: &str) -> Option<u32> {
@@ -584,6 +587,7 @@ impl fmt::Display for Token {
             Token::Bind => write!(f, "⤇"),
             Token::Sum => write!(f, "Σ"),
             Token::Prod => write!(f, "Π"),
+            Token::Error(s) => write!(f, "<invalid: {}>", s),
             _ => write!(f, "{:?}", self),
         }
     }
@@ -636,14 +640,16 @@ impl<'a> Lexer<'a> {
     }
 
     fn next_inner(&mut self) -> Option<Spanned<Token>> {
-        loop {
-            match self.inner.next() {
-                Some(Ok(token)) => {
-                    return Some(Spanned::new(token, Loc::from_span(self.inner.span())));
-                }
-                Some(Err(_)) => continue, // Skip invalid tokens
-                None => return None,
+        match self.inner.next() {
+            Some(Ok(token)) => {
+                Some(Spanned::new(token, Loc::from_span(self.inner.span())))
+            }
+            Some(Err(_)) => {
+                let span = self.inner.span();
+                let text = self.source[span.clone()].to_string();
+                Some(Spanned::new(Token::Error(text), Loc::from_span(span)))
             }
+            None => None,
         }
     }
 
diff --git a/crates/goth-parse/src/parser.rs b/crates/goth-parse/src/parser.rs
index a4a6383..9812923 100644
--- a/crates/goth-parse/src/parser.rs
+++ b/crates/goth-parse/src/parser.rs
@@ -112,7 +112,7 @@ impl<'a> Parser<'a> {
                     if l_bp >= min_bp {
                         self.next(); // consume operator
                         let rhs = self.parse_expr_bp(r_bp)?;
-                        lhs = self.make_binop(op, lhs, rhs);
+                        lhs = self.make_binop(op, lhs, rhs)?;
                         continue; // Check for more operators/applications
                     }
                 }
@@ -736,7 +736,7 @@ impl<'a> Parser<'a> {
                     DoOp::Let(pat, e)
                 }
                 Some(t) if t.is_binop() => {
-                    let op = self.token_to_binop(&t);
+                    let op = self.token_to_binop(&t)?;
                     self.next();
                     DoOp::Op(op, self.parse_expr()?)
                 }
@@ -750,40 +750,43 @@ impl<'a> Parser<'a> {
     }
 
     /// Convert token to BinOp
-    fn token_to_binop(&self, token: &Token) -> BinOp {
+    fn token_to_binop(&self, token: &Token) -> ParseResult<BinOp> {
         match token {
-            Token::Plus => BinOp::Add,
-            Token::Minus => BinOp::Sub,
-            Token::Star => BinOp::Mul,
-            Token::Slash => BinOp::Div,
-            Token::Caret => BinOp::Pow,
-            Token::Percent => BinOp::Mod,
-            Token::PlusMinus => BinOp::PlusMinus,
-            Token::Eq => BinOp::Eq,
-            Token::StructEq => BinOp::StructEq,
-            Token::Neq => BinOp::Neq,
-            Token::Lt => BinOp::Lt,
-            Token::Gt => BinOp::Gt,
-            Token::Leq => BinOp::Leq,
-            Token::Geq => BinOp::Geq,
-            Token::And => BinOp::And,
-            Token::Or => BinOp::Or,
-            Token::Map => BinOp::Map,
-            Token::Filter => BinOp::Filter,
-            Token::Bind => BinOp::Bind,
-            Token::Compose => BinOp::Compose,
-            Token::ZipWith => BinOp::ZipWith,
-            Token::Concat => BinOp::Concat,
-            Token::Write => BinOp::Write,
-            Token::Read => BinOp::Read,
-            _ => BinOp::Add, // fallback
+            Token::Plus => Ok(BinOp::Add),
+            Token::Minus => Ok(BinOp::Sub),
+            Token::Star => Ok(BinOp::Mul),
+            Token::Slash => Ok(BinOp::Div),
+            Token::Caret => Ok(BinOp::Pow),
+            Token::Percent => Ok(BinOp::Mod),
+            Token::PlusMinus => Ok(BinOp::PlusMinus),
+            Token::Eq => Ok(BinOp::Eq),
+            Token::StructEq => Ok(BinOp::StructEq),
+            Token::Neq => Ok(BinOp::Neq),
+            Token::Lt => Ok(BinOp::Lt),
+            Token::Gt => Ok(BinOp::Gt),
+            Token::Leq => Ok(BinOp::Leq),
+            Token::Geq => Ok(BinOp::Geq),
+            Token::And => Ok(BinOp::And),
+            Token::Or => Ok(BinOp::Or),
+            Token::Map => Ok(BinOp::Map),
+            Token::Filter => Ok(BinOp::Filter),
+            Token::Bind => Ok(BinOp::Bind),
+            Token::Compose => Ok(BinOp::Compose),
+            Token::ZipWith => Ok(BinOp::ZipWith),
+            Token::Concat => Ok(BinOp::Concat),
+            Token::Write => Ok(BinOp::Write),
+            Token::Read => Ok(BinOp::Read),
+            _ => Err(ParseError::Unexpected {
+                found: Some(token.clone()),
+                expected: "binary operator".into(),
+            }),
         }
     }
 
     /// Create binary operation expression
-    fn make_binop(&self, token: Token, lhs: Expr, rhs: Expr) -> Expr {
-        let op = self.token_to_binop(&token);
-        Expr::BinOp(op, Box::new(lhs), Box::new(rhs))
+    fn make_binop(&self, token: Token, lhs: Expr, rhs: Expr) -> ParseResult<Expr> {
+        let op = self.token_to_binop(&token)?;
+        Ok(Expr::BinOp(op, Box::new(lhs), Box::new(rhs)))
     }
 
     // ============ Pattern Parsing ============
diff --git a/crates/goth-server/Cargo.toml b/crates/goth-server/Cargo.toml
index ebdf1c6..5b2b3bb 100644
--- a/crates/goth-server/Cargo.toml
+++ b/crates/goth-server/Cargo.toml
@@ -1,6 +1,6 @@
 [package]
 name = "goth-server"
-version = "0.1.0"
+version = "0.2.0"
 edition = "2021"
 description = "HTTP server for the Goth programming language - REST API and web interface"
 license = "MIT"
@@ -31,7 +31,7 @@ serde_json = "1.0"
 clap = { version = "4.4", features = ["derive"] }
 
 # Utilities
-thiserror = "1.0"
+thiserror = "2.0"
 tracing = "0.1"
 tracing-subscriber = { version = "0.3", features = ["env-filter"] }
 
diff --git a/docs/CLAUDE-SKILLS.md b/docs/CLAUDE-SKILLS.md
index 75b6900..6c9952d 100644
--- a/docs/CLAUDE-SKILLS.md
+++ b/docs/CLAUDE-SKILLS.md
@@ -417,12 +417,15 @@ Built-in operators (not standalone functions):
 |-----------|---------|-------|---------|
 | Map | `↦` | `-:` | `[1,2,3] ↦ (λ→ ₀ × 2)` → `[2 4 6]` |
 | Filter | `▸` | `\|>_` | `[1,2,3,4,5] ▸ (λ→ ₀ > 2)` → `[3 4 5]` |
+| Fold | `⌿` | `fold` | `⌿ (λ→ λ→ ₁ + ₀) 0 [1,2,3]` → `6` |
 | Sum | `Σ` | `+/` | `Σ [1,2,3,4,5]` → `15` |
 | Product | `Π` | `*/` | `Π [1,2,3,4,5]` → `120` |
 | Compose | `∘` | `.:` | `f ∘ g` (f after g) |
 | Bind | `⤇` | `=>>` | Monadic bind |
 | Write | `▷` | `\|>` | `"hello" ▷ stdout` or `"data" ▷ "/tmp/out.txt"` |
 
+**Fold** is a 3-argument curried function: `fold f acc arr`. The function `f` takes `(accumulator, element)` and returns the new accumulator. Inside the fold lambda, `₁` = accumulator, `₀` = current element.
+
 **In JSON AST:**
 ```json
 {"BinOp": ["Map", {"Array": [...]}, {"Lam": ...}]}
@@ -445,6 +448,18 @@ print("Hello, world!")
 "data"  ▷ "/tmp/f.txt" # write to file
 ```
 
+**`⧏` (readBytes)** — reads n bytes from a file path, returns `[n]I64` array of byte values (0-255):
+```goth
+⧏ 8 "/dev/urandom"    # read 8 bytes of entropy
+readBytes 4 "/tmp/f"   # ASCII fallback
+```
+
+**`⧐` (writeBytes)** — writes a byte array to a file path:
+```goth
+⧐ [72, 101, 108] "/tmp/out"   # write bytes
+writeBytes [0, 255] "/tmp/bin" # ASCII fallback
+```
+
 `stdout` and `stderr` are built-in stream constants. When the RHS of `▷` is a stream, the content is written to that stream. When it is a string, it is treated as a file path.
 
 **In JSON AST:**
@@ -519,9 +534,11 @@ print("Hello, world!")
 
 **Math functions:** `√` (sqrt), `Γ` (gamma), `ln`, `exp`, `sin`, `cos`, `tan`, `abs`, `⌊` (floor), `⌈` (ceil), `log₁₀`, `log₂`
 
-**Array operations:** `len`, `Σ` (sum), `Π` (product), `↦` (map), `▸` (filter), `iota`, `range`
+**Array operations:** `len`, `Σ` (sum), `Π` (product), `↦` (map), `▸` (filter), `⌿` (fold), `iota`, `range`, `⊕` (concat)
+
+**Bitwise operations:** `bitand`, `bitor`, `⊻`/`bitxor`, `shl`, `shr` — all curried `I64 → I64 → I64`
 
-**No bitwise ops** currently. Use arithmetic equivalents if needed.
+**Byte I/O:** `⧏`/`readBytes` (`I64 → String → [n]I64`), `⧐`/`writeBytes` (`[n]I64 → String → ()`)
 
 ### 8. Execution Environment
 
@@ -537,13 +554,95 @@ print("Hello, world!")
 ### 9. Extending Benchmarks
 
 **Current gaps to consider:**
-- String manipulation (limited support currently)
 - Data structures (trees, graphs - would need ADTs)
-- More numeric algorithms (integration, differentiation)
+- More numeric algorithms (differentiation)
 - Property-based contract testing
 
 **Stick to:** Pure functional algorithms that fit the current type system.
 
+## Standard Library: Random Numbers
+
+The `stdlib/random.goth` module provides seeded PRNG using xorshift64. Import with `use "stdlib/random.goth"`.
+
+**Key design pattern:** All RNG functions return `⟨value, nextSeed⟩` tuples. Thread the seed through sequential calls:
+
+```goth
+use "stdlib/random.goth"
+
+╭─ main : () → ⟨F64, F64, F64⟩
+╰─ let seed = entropy ⟨⟩
+   in let ⟨v1, s1⟩ = randFloat seed
+   in let ⟨v2, s2⟩ = randFloat s1
+   in let ⟨v3, s3⟩ = randFloat s2
+   in ⟨v1, v2, v3⟩
+```
+
+**Available functions:**
+
+| Function | Signature | Description |
+|----------|-----------|-------------|
+| `entropy` | `() → I64` | Seed from `/dev/urandom` |
+| `bytesToSeed` | `[8]I64 → I64` | Pack 8 bytes into seed |
+| `xorshift64` | `I64 → I64` | Raw state transition |
+| `randFloat` | `I64 → ⟨F64, I64⟩` | Uniform [0, 1) |
+| `randFloatRange` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Uniform [lo, hi) |
+| `randInt` | `I64 → I64 → I64 → ⟨I64, I64⟩` | Uniform [lo, hi] |
+| `randBool` | `F64 → I64 → ⟨Bool, I64⟩` | Boolean with probability p |
+| `randNormal` | `I64 → ⟨F64, I64⟩` | Standard normal (Box-Muller) |
+| `randGaussian` | `F64 → F64 → I64 → ⟨F64, I64⟩` | Normal(mean, stddev) |
+| `randFloats` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk uniform floats |
+| `randInts` | `I64 → I64 → I64 → I64 → ⟨[n]I64, I64⟩` | Bulk uniform integers |
+| `randNormals` | `I64 → I64 → ⟨[n]F64, I64⟩` | Bulk normal values |
+
+**De Bruijn index note:** When using `let ⟨v, s⟩ = randFloat seed in ...`, the destructuring introduces 2 bindings, so raw De Bruijn indices in the body shift by 2. Named variables (`v`, `s`, `seed`) are unaffected — prefer named references when possible.
+
+## Standard Library: Cryptography
+
+The `stdlib/crypto.goth` module provides pure-Goth implementations of cryptographic hash functions and encoding. All algorithms are implemented entirely in Goth using bitwise primitives — no FFI or Rust crate dependencies. Import with `use "stdlib/crypto.goth"`.
+
+**Key design pattern:** All hash functions take a `String` and return a hex-encoded `String`. Internally, strings are converted to byte arrays via `bytes`, processed through block-oriented compression functions using `fold`, and rendered back to hex strings.
+
+```goth
+use "stdlib/crypto.goth"
+
+╭─ main : String → String
+╰─ let contents = readFile ₀
+   in let _ = print ("SHA-256: " ⧺ sha256 ₀)
+   in let _ = print ("MD5:    " ⧺ md5 ₁)
+   in "BLAKE3: " ⧺ blake3 ₂
+```
+
+**Public functions:**
+
+| Function | Signature | Description |
+|----------|-----------|-------------|
+| `sha256` | `String → String` | SHA-256 hash (NIST FIPS 180-4), arbitrary-length input |
+| `sha256Bytes` | `[n]I64 → String` | SHA-256 from raw byte array |
+| `md5` | `String → String` | MD5 digest (RFC 1321), arbitrary-length input |
+| `blake3` | `String → String` | BLAKE3 hash (single chunk, ≤ 64 bytes) |
+| `base64EncodeStr` | `String → String` | Base64 encode a string (RFC 4648) |
+| `base64Encode` | `[n]I64 → String` | Base64 encode a byte array |
+| `base64Decode` | `String → [n]I64` | Base64 decode to byte array |
+| `hexEncode` | `[n]I64 → String` | Hex-encode a byte array |
+
+**Internal helpers** (also exported, useful for custom hash constructions):
+
+| Function | Description |
+|----------|-------------|
+| `add32`, `not32`, `rotr32`, `rotl32` | 32-bit masked arithmetic and rotation |
+| `byteToHex`, `wordsToHex`, `wordsToHexLE` | Hex encoding (big-endian and little-endian) |
+| `blockToWords`, `blockToWordsLE` | Byte-to-word packing (BE and LE) |
+| `sha256Pad`, `md5Pad` | Message padding with length encoding |
+| `sha256Compress`, `md5Compress`, `blake3Compress` | Single-block compression functions |
+| `aset` | Functional array element update: `aset arr idx val` |
+
+**Implementation notes for LLMs:**
+- Goth integers are i128 internally; all 32-bit hash operations must mask with `bitand X 4294967295` after every addition, rotation, or shift
+- SHA-256 uses big-endian word packing; MD5 and BLAKE3 use little-endian
+- BLAKE3 is limited to single-chunk messages (≤ 64 bytes); SHA-256 and MD5 handle arbitrary length via multi-block processing
+- De Bruijn index tracking is critical in hash compression loops — annotate every `let` with a comment showing the current index state (e.g., `# ₀=ki ₁=roundIdx ₂=st ₃=schedule`)
+- Use `fold` over `iota N` for round-based processing; inside the fold lambda, `₁` = accumulator, `₀` = round index
+
 ## Goth Syntax ↔ JSON
 
 | Goth Syntax | JSON AST |
diff --git a/docs/GOTH-LANGUAGE-REFERENCE-v0.1.md b/docs/GOTH-LANGUAGE-REFERENCE-v0.1.md
index ec55a43..51d8daa 100644
--- a/docs/GOTH-LANGUAGE-REFERENCE-v0.1.md
+++ b/docs/GOTH-LANGUAGE-REFERENCE-v0.1.md
@@ -1184,6 +1184,18 @@ or(⊤, ⊥)               # ⊤
 not(⊤)                 # ⊥
 ```
 
+### Bitwise Operations
+
+```goth
+bitand 255 15          # 15
+bitor 240 15           # 255
+bitxor 255 170         # 85     (also: ⊻ 255 170)
+shl 1 8               # 256
+shr 256 4             # 16
+```
+
+All bitwise operations are curried: `I64 → I64 → I64`.
+
 ### Array/Tensor Operations
 
 ```goth
@@ -1193,6 +1205,7 @@ len([1, 2, 3, 4, 5])           # 5
 shape([[1, 2], [3, 4]])        # [2, 2]
 reverse([1, 2, 3])             # [3, 2, 1]
 concat([1, 2], [3, 4])         # [1, 2, 3, 4]
+⌿ (λ→ λ→ ₁ + ₀) 0 [1, 2, 3]  # 6  (fold/reduce)
 ```
 
 **Linear algebra:**
@@ -1248,6 +1261,18 @@ print("Hello, world!")
 **Unicode:** `▷`
 **ASCII:** `|>`
 
+**Read bytes from file:**
+```goth
+⧏ 8 "/dev/urandom"            # read 8 bytes → [8]I64
+readBytes 4 "/tmp/data.bin"    # ASCII fallback
+```
+
+**Write bytes to file:**
+```goth
+⧐ [72, 101, 108] "/tmp/out"   # write byte array to file
+writeBytes [0, 255] "/tmp/bin" # ASCII fallback
+```
+
 `stdout` and `stderr` are built-in stream constants. The `▷` operator dispatches on the right-hand side: a stream value writes to that stream (without a newline), a string value writes to that file path.
 
 **Read from file:**
diff --git a/docs/PROJECT-STATUS.md b/docs/PROJECT-STATUS.md
index 6827114..994c3e7 100644
--- a/docs/PROJECT-STATUS.md
+++ b/docs/PROJECT-STATUS.md
@@ -73,15 +73,17 @@ Tree-walking interpreter for testing and REPL.
 - Full expression evaluation
 - Closure semantics
 - Pattern matching
-- **50+ primitive functions:**
+- **60+ primitive functions:**
   - Math: add, sub, mul, div, mod, neg, abs, exp, ln, sqrt, sin, cos, tan, pow, floor, ceil, round
   - Comparison: eq, neq, lt, gt, leq, geq
   - Logic: and, or, not
-  - Tensor: sum, prod, len, shape, reverse, concat, dot, norm, matmul, transpose, iota, range, take, drop, index
+  - Bitwise: bitand, bitor, bitxor/⊻, shl, shr
+  - Tensor: sum, prod, len, shape, reverse, concat, dot, norm, matmul, transpose, iota, range, take, drop, index, fold/⌿
   - String: toString, chars, strConcat, lines, words, bytes, strEq, startsWith, endsWith, contains
   - Type: toInt, toFloat, toBool, toChar, parseInt, parseFloat
-  - I/O: print, write, flush, readLine, readKey, sleep, readFile, writeFile
+  - I/O: print, write, flush, readLine, readKey, sleep, readFile, writeFile, readBytes/⧏, writeBytes/⧐
   - TUI: rawModeEnter, rawModeExit
+- **Standard library** (`stdlib/`): 10 modules including random number generation (xorshift64 PRNG)
 
 ### 5. **goth-mir** (3,291 lines, 50 tests) - WORKING
 
diff --git a/examples/README.md b/examples/README.md
index eefd005..de4761d 100644
--- a/examples/README.md
+++ b/examples/README.md
@@ -237,6 +237,46 @@ open heat2d.svg
 
 ---
 
+## random/
+
+Monte Carlo methods and randomness using the `random.goth` standard library. All examples use `entropy ⟨⟩` for OS-seeded PRNG and thread state through folds via tuples.
+
+| File | Description | Example |
+|------|-------------|---------|
+| `rand_floats.goth` | Generate n uniform random floats in [0, 1) | `5 → [0.23 0.87 ...]` |
+| `buffon_pi.goth` | Estimate π via Buffon's needle experiment | `10000 → 3.14...` |
+| `mc_integrate.goth` | Monte Carlo integration of ∫₀¹ e⁻ˣ² dx | `10000 → 0.746...` |
+| `mc_importance.goth` | Importance sampling with proposal q(x) = 2(1−x) | `10000 → 0.746...` |
+| `mc_antithetic.goth` | Antithetic variates vs naive MC (returns both estimates) | `10000 → ⟨0.74..., 0.74...⟩` |
+
+**Demonstrates:** `entropy`, `randFloat`, `randFloats`, `randFloatRange`, fold-threaded PRNG state, tuple destructuring (`⟨val, seed⟩`), contracts on stochastic results, `use` imports.
+
+---
+
+## crypto/
+
+Cryptographic hash functions and encoding — pure Goth implementations using bitwise primitives. All algorithms are implemented entirely in Goth via the `crypto.goth` standard library.
+
+| File | Description | Example |
+|------|-------------|---------|
+| `sha256.goth` | SHA-256 hash (NIST FIPS 180-4) | `sha256 "hello" → 2cf24d...` |
+| `md5.goth` | MD5 message digest (RFC 1321) | `md5 "hello" → 5d4140...` |
+| `blake3.goth` | BLAKE3 hash (single chunk, ≤ 64 bytes) | `blake3 "hello" → ea8f16...` |
+| `base64.goth` | Base64 encode/decode (RFC 4648) | `base64EncodeStr "hello" → "aGVsbG8="` |
+| `hashfile.goth` | Hash a file with SHA-256, MD5, and BLAKE3 | `hashfile.goth <path>` |
+
+```sh
+# Hash a text file
+cargo run --quiet --package goth-cli -- ../examples/crypto/hashfile.goth /tmp/test.txt
+# SHA-256: 2cf24dba...
+# MD5:    5d41402a...
+# BLAKE3: ea8f163d...
+```
+
+**Demonstrates:** `bitand`, `bitor`, `bitxor`, `shl`, `shr`, 32-bit masking on i128, fold-based block processing, `bytes`, `index`, `readFile`, `strConcat`/`⧺`, `use` imports.
+
+---
+
 ## Language Features Covered
 
 | Feature | Examples |
@@ -251,10 +291,13 @@ open heat2d.svg
 | Sum/Product (`Σ`/`Π`) | numeric, higher-order, simulation |
 | Iota (`ι`) | numeric, simulation |
 | Array concat (`⊕`) | higher-order |
-| String concat (`⧺`) | simulation |
+| String concat (`⧺`) | simulation, crypto |
 | Conditionals (`if/then/else`) | basic, recursion, algorithms |
-| Contracts (`⊢`/`⊨`) | contracts |
+| Contracts (`⊢`/`⊨`) | contracts, random |
 | Uncertainty (`±`) | uncertainty |
-| File I/O (`▷`, `writeFile`) | io, simulation |
-| Module imports (`use`) | simulation (tunable variants) |
+| File I/O (`▷`, `writeFile`, `readFile`) | io, simulation, crypto |
+| Module imports (`use`) | simulation, random, crypto |
 | Tail-call optimization | tco |
+| Bitwise ops (`bitand`, `bitor`, `bitxor`, `shl`, `shr`) | crypto |
+| Tuple destructuring (`⟨a, b⟩`) | random |
+| PRNG / entropy | random |
diff --git a/examples/crypto/base64.goth b/examples/crypto/base64.goth
new file mode 100644
index 0000000..3b269ff
--- /dev/null
+++ b/examples/crypto/base64.goth
@@ -0,0 +1,11 @@
+# Base64 encode/decode — pure Goth implementation (RFC 4648)
+use "../../stdlib/crypto.goth"
+
+╭─ main : () → String
+╰─ let _ = print (base64EncodeStr "hello")
+   in let _ = print (base64EncodeStr "foo")
+   in let _ = print (base64EncodeStr "f")
+   # Round-trip: decode(encode("hello")) → byte values of "hello"
+   in let rt = base64Decode (base64EncodeStr "hello")
+   in let _ = print ₀
+   in base64EncodeStr "Hello, World"
diff --git a/examples/crypto/blake3.goth b/examples/crypto/blake3.goth
new file mode 100644
index 0000000..3b83e1f
--- /dev/null
+++ b/examples/crypto/blake3.goth
@@ -0,0 +1,8 @@
+# BLAKE3 cryptographic hash — pure Goth implementation
+# For messages ≤ 64 bytes (single chunk, single block).
+use "../../stdlib/crypto.goth"
+
+╭─ main : () → String
+╰─ let _ = print (blake3 "")
+   in let _ = print (blake3 "abc")
+   in blake3 "hello"
diff --git a/examples/crypto/hashfile.goth b/examples/crypto/hashfile.goth
new file mode 100644
index 0000000..57f9b27
--- /dev/null
+++ b/examples/crypto/hashfile.goth
@@ -0,0 +1,13 @@
+# Hash a file — prints SHA-256, MD5, and BLAKE3 digests
+# Usage: goth hashfile.goth <filepath>
+# Note: BLAKE3 is limited to files ≤ 64 bytes (single-chunk impl).
+use "../../stdlib/crypto.goth"
+
+╭─ main : String → String
+╰─ let contents = readFile ₀
+   # ₀=contents
+   in let _ = print ("SHA-256: " ⧺ sha256 ₀)
+   # ₀=_ ₁=contents
+   in let _ = print ("MD5:    " ⧺ md5 ₁)
+   # ₀=_ ₁=_ ₂=contents
+   in "BLAKE3: " ⧺ blake3 ₂
diff --git a/examples/crypto/md5.goth b/examples/crypto/md5.goth
new file mode 100644
index 0000000..7490c36
--- /dev/null
+++ b/examples/crypto/md5.goth
@@ -0,0 +1,7 @@
+# MD5 message digest — pure Goth implementation (RFC 1321)
+use "../../stdlib/crypto.goth"
+
+╭─ main : () → String
+╰─ let _ = print (md5 "")
+   in let _ = print (md5 "abc")
+   in md5 "hello"
diff --git a/examples/crypto/sha256.goth b/examples/crypto/sha256.goth
new file mode 100644
index 0000000..e197408
--- /dev/null
+++ b/examples/crypto/sha256.goth
@@ -0,0 +1,9 @@
+# SHA-256 cryptographic hash — pure Goth implementation
+# All test vectors verified against NIST FIPS 180-4.
+use "../../stdlib/crypto.goth"
+
+╭─ main : () → String
+╰─ let _ = print (sha256 "")
+   in let _ = print (sha256 "abc")
+   in let _ = print (sha256 "hello")
+   in sha256 "abcdbcdecdefdefgefghfghighijhijkijkljklmklmnlmnomnopnopq"
diff --git a/examples/random/buffon_pi.goth b/examples/random/buffon_pi.goth
new file mode 100644
index 0000000..d3d13d0
--- /dev/null
+++ b/examples/random/buffon_pi.goth
@@ -0,0 +1,20 @@
+# Estimate π via Buffon's needle experiment.
+# Drop n needles (length 1) on parallel lines (spacing 1).
+# P(cross) = 2/π → π = 2n/crossings.
+use "../../stdlib/random.goth"
+
+╭─ main : I64 → F64
+│ ⊢ ₀ > 0
+│ ⊨ ₀ > 2.0 ∧ ₀ < 4.0
+╰─ let n = ₀
+   in let seed = entropy ⟨⟩
+   in let ⟨crossings, _⟩ = ⌿ (λ→ λ→
+        let acc = ₁
+        in let ⟨y, s1⟩ = randFloatRange 0.0 0.5 (acc.1)
+        in let ⟨theta, s2⟩ = randFloatRange 0.0 1.5707963267948966 s1
+        in let crossed = if y < 0.5 × sin theta then 1 else 0
+        in ⟨acc.0 + crossed, s2⟩)
+      ⟨0, seed⟩
+      (ι n)
+   in if crossings < 1 then 0.0
+      else 2.0 × toFloat n / toFloat crossings
diff --git a/examples/random/mc_antithetic.goth b/examples/random/mc_antithetic.goth
new file mode 100644
index 0000000..027ec54
--- /dev/null
+++ b/examples/random/mc_antithetic.goth
@@ -0,0 +1,25 @@
+# Variance reduction: naive MC vs antithetic variates
+# for ∫₀¹ e⁻ˣ² dx ≈ 0.7468
+# Antithetic pairs (x, 1-x) reduce variance.
+use "../../stdlib/random.goth"
+
+╭─ main : I64 → ⟨F64, F64⟩
+│ ⊢ ₀ > 0
+╰─ let n = ₀
+   in let seed = entropy ⟨⟩
+   in let ⟨naive_total, s1⟩ = ⌿ (λ→ λ→
+        let acc = ₁
+        in let ⟨x, s⟩ = randFloat (acc.1)
+        in let fx = exp (0.0 - x × x)
+        in ⟨acc.0 + fx, s⟩)
+      ⟨0.0, seed⟩
+      (ι n)
+   in let ⟨anti_total, _⟩ = ⌿ (λ→ λ→
+        let acc = ₁
+        in let ⟨x, s⟩ = randFloat (acc.1)
+        in let fx = exp (0.0 - x × x)
+        in let fmx = exp (0.0 - (1.0 - x) × (1.0 - x))
+        in ⟨acc.0 + (fx + fmx) / 2.0, s⟩)
+      ⟨0.0, s1⟩
+      (ι n)
+   in ⟨naive_total / toFloat n, anti_total / toFloat n⟩
diff --git a/examples/random/mc_importance.goth b/examples/random/mc_importance.goth
new file mode 100644
index 0000000..f7cf706
--- /dev/null
+++ b/examples/random/mc_importance.goth
@@ -0,0 +1,20 @@
+# Importance sampling: ∫₀¹ e⁻ˣ² dx with proposal q(x) = 2(1-x)
+# Reduces variance by sampling where the integrand is large.
+use "../../stdlib/random.goth"
+
+╭─ main : I64 → F64
+│ ⊢ ₀ > 0
+│ ⊨ ₀ > 0.5 ∧ ₀ < 1.0
+╰─ let n = ₀
+   in let seed = entropy ⟨⟩
+   in let ⟨total, _⟩ = ⌿ (λ→ λ→
+        let acc = ₁
+        in let ⟨u, s1⟩ = randFloat (acc.1)
+        in let x = 1.0 - √(1.0 - u)
+        in let qx = 2.0 × (1.0 - x)
+        in let fx = exp (0.0 - x × x)
+        in let weight = if qx < 0.0001 then 0.0 else fx / qx
+        in ⟨acc.0 + weight, s1⟩)
+      ⟨0.0, seed⟩
+      (ι n)
+   in total / toFloat n
diff --git a/examples/random/mc_integrate.goth b/examples/random/mc_integrate.goth
new file mode 100644
index 0000000..4c93b4e
--- /dev/null
+++ b/examples/random/mc_integrate.goth
@@ -0,0 +1,17 @@
+# Monte Carlo integration: ∫₀¹ e⁻ˣ² dx ≈ 0.7468
+# Estimator: (1/n) Σ f(xᵢ), xᵢ ~ Uniform(0,1)
+use "../../stdlib/random.goth"
+
+╭─ main : I64 → F64
+│ ⊢ ₀ > 0
+│ ⊨ ₀ > 0.5 ∧ ₀ < 1.0
+╰─ let n = ₀
+   in let seed = entropy ⟨⟩
+   in let ⟨total, _⟩ = ⌿ (λ→ λ→
+        let acc = ₁
+        in let ⟨x, s1⟩ = randFloat (acc.1)
+        in let fx = exp (0.0 - x × x)
+        in ⟨acc.0 + fx, s1⟩)
+      ⟨0.0, seed⟩
+      (ι n)
+   in total / toFloat n
diff --git a/examples/random/rand_floats.goth b/examples/random/rand_floats.goth
new file mode 100644
index 0000000..3fc4f9a
--- /dev/null
+++ b/examples/random/rand_floats.goth
@@ -0,0 +1,9 @@
+# Generate n uniform random floats in [0, 1)
+# Postcondition: sum of values < n (since each is in [0,1))
+use "../../stdlib/random.goth"
+
+╭─ main : I64 → [n]F64
+│ ⊨ Σ ₀ < toFloat ₁
+╰─ let seed = entropy ⟨⟩
+   in let ⟨vals, _⟩ = randFloats ₁ seed
+   in vals
diff --git a/stdlib/crypto.goth b/stdlib/crypto.goth
new file mode 100644
index 0000000..9f30977
--- /dev/null
+++ b/stdlib/crypto.goth
@@ -0,0 +1,647 @@
+# Goth Standard Library - Cryptographic Hash Functions
+# Pure Goth implementation of SHA-256 (FIPS 180-4).
+#
+# Usage:
+#   use "stdlib/crypto.goth"
+#   sha256 "hello"    # → "2cf24dba5fb0a30e26e83b2ac5b9e29e..."
+#
+# All operations use 32-bit masked integers via Goth's i128 arithmetic
+# with bitwise primitives: bitand, bitor, bitxor (⊻), shl, shr.
+
+# ============ 32-bit Arithmetic Helpers ============
+
+let mask32 = 4294967295
+
+# ₁ + ₀ mod 2^32
+╭─ add32 : I64 → I64 → I64
+╰─ bitand (₁ + ₀) mask32
+
+# NOT ₀ (32-bit)
+╭─ not32 : I64 → I64
+╰─ ⊻ ₀ mask32
+
+# Rotate right: ₁=shift, ₀=value
+╭─ rotr32 : I64 → I64 → I64
+╰─ bitand (bitor (shr ₀ ₁) (shl ₀ (32 - ₁))) mask32
+
+# ============ SHA-256 Logical Functions ============
+
+# Ch(₂,₁,₀) = (₂ AND ₁) XOR (NOT ₂ AND ₀)
+╭─ sha256Ch : I64 → I64 → I64 → I64
+╰─ ⊻ (bitand ₂ ₁) (bitand (not32 ₂) ₀)
+
+# Maj(₂,₁,₀) = (₂ AND ₁) XOR (₂ AND ₀) XOR (₁ AND ₀)
+╭─ sha256Maj : I64 → I64 → I64 → I64
+╰─ ⊻ (⊻ (bitand ₂ ₁) (bitand ₂ ₀)) (bitand ₁ ₀)
+
+# Σ0(₀) = rotr2 XOR rotr13 XOR rotr22
+╭─ sha256Sigma0 : I64 → I64
+╰─ ⊻ (⊻ (rotr32 2 ₀) (rotr32 13 ₀)) (rotr32 22 ₀)
+
+# Σ1(₀) = rotr6 XOR rotr11 XOR rotr25
+╭─ sha256Sigma1 : I64 → I64
+╰─ ⊻ (⊻ (rotr32 6 ₀) (rotr32 11 ₀)) (rotr32 25 ₀)
+
+# σ0(₀) = rotr7 XOR rotr18 XOR shr3
+╭─ sha256sigma0 : I64 → I64
+╰─ ⊻ (⊻ (rotr32 7 ₀) (rotr32 18 ₀)) (shr ₀ 3)
+
+# σ1(₀) = rotr17 XOR rotr19 XOR shr10
+╭─ sha256sigma1 : I64 → I64
+╰─ ⊻ (⊻ (rotr32 17 ₀) (rotr32 19 ₀)) (shr ₀ 10)
+
+# ============ SHA-256 Constants ============
+
+let sha256K = [
+  1116352408, 1899447441, 3049323471, 3921009573,
+  961987163, 1508970993, 2453635748, 2870763221,
+  3624381080, 310598401, 607225278, 1426881987,
+  1925078388, 2162078206, 2614888103, 3248222580,
+  3835390401, 4022224774, 264347078, 604807628,
+  770255983, 1249150122, 1555081692, 1996064986,
+  2554220882, 2821834349, 2952996808, 3210313671,
+  3336571891, 3584528711, 113926993, 338241895,
+  666307205, 773529912, 1294757372, 1396182291,
+  1695183700, 1986661051, 2177026350, 2456956037,
+  2730485921, 2820302411, 3259730800, 3345764771,
+  3516065817, 3600352804, 4094571909, 275423344,
+  430227734, 506948616, 659060556, 883997877,
+  958139571, 1322822218, 1537002063, 1747873779,
+  1955562222, 2024104815, 2227730452, 2361852424,
+  2428436474, 2756734187, 3204031479, 3329325298
+]
+
+let sha256H0 = [
+  1779033703, 3144134277, 1013904242, 2773480762,
+  1359893119, 2600822924, 528734635, 1541459225
+]
+
+# ============ Hex Encoding ============
+
+let hexChars = "0123456789abcdef"
+
+# Byte (0-255) → 2-char hex string
+╭─ byteToHex : I64 → String
+╰─ let hi = index hexChars (shr ₀ 4)
+   # ₀=hi ₁=byte
+   in let lo = index hexChars (bitand ₁ 15)
+   # ₀=lo ₁=hi
+   in toString ₁ ⧺ toString ₀
+
+# 32-bit words → hex string (8 hex chars per word, big-endian)
+╭─ wordsToHex : [n]I64 → String
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=word
+     let b0 = byteToHex (bitand (shr ₀ 24) 255)
+     # ₀=b0 ₁=word ₂=acc
+     in let b1 = byteToHex (bitand (shr ₁ 16) 255)
+     # ₀=b1 ₁=b0 ₂=word ₃=acc
+     in let b2 = byteToHex (bitand (shr ₂ 8) 255)
+     # ₀=b2 ₁=b1 ₂=b0 ₃=word ₄=acc
+     in let b3 = byteToHex (bitand ₃ 255)
+     # ₀=b3 ₁=b2 ₂=b1 ₃=b0 ₄=word ₅=acc
+     in ₅ ⧺ ₃ ⧺ ₂ ⧺ ₁ ⧺ ₀
+   ) "" ₀
+
+# Byte array → hex string
+╭─ hexEncode : [n]I64 → String
+╰─ ⌿ (λ→ λ→ ₁ ⧺ byteToHex ₀) "" ₀
+
+# ============ Message Padding ============
+
+# Pad byte array per SHA-256: append 0x80, pad zeros to ≡56 mod 64,
+# append 64-bit big-endian bit length.
+╭─ sha256Pad : [n]I64 → [m]I64
+╰─ let msgLen = len ₀
+   # ₀=msgLen ₁=msg
+   in let bitLen = ₀ × 8
+   # ₀=bitLen ₁=msgLen ₂=msg
+   in let padded = ₂ ⊕ [128]
+   # ₀=padded ₁=bitLen ₂=msgLen
+   in let rem = (₂ + 1) % 64
+   # ₀=rem ₁=padded ₂=bitLen ₃=msgLen
+   in let zerosNeeded = if ₀ ≤ 56 then 56 - ₀ else 120 - ₀
+   # ₀=zerosNeeded ₁=rem ₂=padded ₃=bitLen
+   in let withZeros = ⌿ (λ→ λ→ ₁ ⊕ [0]) ₂ (ι ₀)
+   # ₀=withZeros ₁=zerosNeeded ₂=rem ₃=padded ₄=bitLen
+   in ₀ ⊕ [
+        bitand (shr ₄ 56) 255,
+        bitand (shr ₄ 48) 255,
+        bitand (shr ₄ 40) 255,
+        bitand (shr ₄ 32) 255,
+        bitand (shr ₄ 24) 255,
+        bitand (shr ₄ 16) 255,
+        bitand (shr ₄ 8) 255,
+        bitand ₄ 255
+      ]
+
+# ============ Block Processing ============
+
+# Extract 16 big-endian 32-bit words from block at offset.
+# ₁=data ₀=offset
+╭─ blockToWords : [n]I64 → I64 → [16]I64
+╰─ ⌿ (λ→ λ→
+     # In fold body: ₁=acc ₀=wordIdx ₂=offset ₃=data
+     let i = ₀ × 4 + ₂
+     # ₀=i ₁=wordIdx ₂=acc ₃=offset ₄=data
+     in let w = add32 (add32 (add32
+           (shl (index ₄ ₀) 24)
+           (shl (index ₄ (₀ + 1)) 16))
+           (shl (index ₄ (₀ + 2)) 8))
+           (index ₄ (₀ + 3))
+     # ₀=w ₁=i ₂=wordIdx ₃=acc
+     in ₃ ⊕ [₀]
+   ) [] (ι 16)
+
+# Expand 16 words → 64-word schedule.
+# W[i] = σ1(W[i-2]) + W[i-7] + σ0(W[i-15]) + W[i-16]
+╭─ expandSchedule : [16]I64 → [64]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=W(growing) ₀=iter(ignored)
+     let wLen = len ₁
+     # ₀=wLen ₁=iter ₂=W
+     in let w2  = index ₂ (₀ - 2)
+     # ₀=w2 ₁=wLen ₂=iter ₃=W
+     in let w7  = index ₃ (₁ - 7)
+     # ₀=w7 ₁=w2 ₂=wLen ₃=iter ₄=W
+     in let w15 = index ₄ (₂ - 15)
+     # ₀=w15 ₁=w7 ₂=w2 ₃=wLen ₄=iter ₅=W
+     in let w16 = index ₅ (₃ - 16)
+     # ₀=w16 ₁=w15 ₂=w7 ₃=w2
+     in let wNew = add32 (add32 (add32 (sha256sigma1 ₃) ₂) (sha256sigma0 ₁)) ₀
+     # ₀=wNew ₁=w16 ₂=w15 ₃=w7 ₄=w2 ₅=wLen ₆=iter ₇=W
+     in ₇ ⊕ [₀]
+   ) ₀ (ι 48)
+
+# SHA-256 compression: 64 rounds on state [a,b,c,d,e,f,g,h].
+# Access state elements by index to avoid deep let nesting.
+# ₁=W(schedule) ₀=state
+╭─ sha256Compress : [64]I64 → [8]I64 → [8]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=st ₀=roundIdx ₂=state(init) ₃=W
+     let ki = index sha256K ₀
+     # ₀=ki ₁=roundIdx ₂=st ₃=state(init) ₄=W
+     in let wi = index ₄ ₁
+     # ₀=wi ₁=ki ₂=roundIdx ₃=st
+     in let t1 = add32 (add32 (add32 (add32
+           (index ₃ 7)
+           (sha256Sigma1 (index ₃ 4)))
+           (sha256Ch (index ₃ 4) (index ₃ 5) (index ₃ 6)))
+           ₁) ₀
+     # ₀=t1 ₁=wi ₂=ki ₃=roundIdx ₄=st
+     in let t2 = add32 (sha256Sigma0 (index ₄ 0)) (sha256Maj (index ₄ 0) (index ₄ 1) (index ₄ 2))
+     # ₀=t2 ₁=t1 ₂=wi ₃=ki ₄=roundIdx ₅=st
+     in [add32 ₁ ₀,
+         index ₅ 0,
+         index ₅ 1,
+         index ₅ 2,
+         add32 (index ₅ 3) ₁,
+         index ₅ 4,
+         index ₅ 5,
+         index ₅ 6]
+   ) ₀ (ι 64)
+
+# Element-wise add32 of two 8-word arrays.
+# ₁=hash ₀=compressed
+╭─ hashAdd : [8]I64 → [8]I64 → [8]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=idx ₂=compressed ₃=hash
+     ₁ ⊕ [add32 (index ₃ ₀) (index ₂ ₀)]
+   ) [] (ι 8)
+
+# Process one 64-byte block.
+# ₂=data ₁=blockOffset ₀=currentHash
+╭─ processBlock : [n]I64 → I64 → [8]I64 → [8]I64
+╰─ let w16 = blockToWords ₂ ₁
+   # ₀=w16 ₁=hash ₂=offset ₃=data
+   in let w64 = expandSchedule ₀
+   # ₀=w64 ₁=w16 ₂=hash
+   in let compressed = sha256Compress ₀ ₂
+   # ₀=compressed ₁=w64 ₂=w16 ₃=hash
+   in hashAdd ₃ ₀
+
+# ============ SHA-256 Entry Points ============
+
+# SHA-256(string) → 64-char hex digest
+╭─ sha256 : String → String
+╰─ let padded = sha256Pad (bytes ₀)
+   # ₀=padded ₁=string
+   in let numBlocks = len ₀ / 64
+   # ₀=numBlocks ₁=padded
+   in let finalHash = ⌿ (λ→ λ→
+     # ₁=hash ₀=blockIdx ₂=numBlocks ₃=padded
+     processBlock ₃ (₀ × 64) ₁
+   ) sha256H0 (ι ₀)
+   # ₀=finalHash
+   in wordsToHex ₀
+
+# SHA-256(bytes) → 64-char hex digest
+╭─ sha256Bytes : [n]I64 → String
+╰─ let padded = sha256Pad ₀
+   # ₀=padded ₁=inputBytes
+   in let numBlocks = len ₀ / 64
+   # ₀=numBlocks ₁=padded
+   in let finalHash = ⌿ (λ→ λ→
+     processBlock ₃ (₀ × 64) ₁
+   ) sha256H0 (ι ₀)
+   in wordsToHex ₀
+
+# ================================================================
+# MD5 (RFC 1321)
+# ================================================================
+
+# Left rotation (MD5 uses left, SHA-256 uses right)
+# ₁=shift ₀=value
+╭─ rotl32 : I64 → I64 → I64
+╰─ bitand (bitor (shl ₀ ₁) (shr ₀ (32 - ₁))) mask32
+
+# 32-bit words → hex string, LITTLE-ENDIAN byte order
+# (MD5 output is LE, unlike SHA-256 which is BE)
+╭─ wordsToHexLE : [n]I64 → String
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=word
+     let b0 = byteToHex (bitand ₀ 255)
+     # ₀=b0 ₁=word ₂=acc
+     in let b1 = byteToHex (bitand (shr ₁ 8) 255)
+     # ₀=b1 ₁=b0 ₂=word ₃=acc
+     in let b2 = byteToHex (bitand (shr ₂ 16) 255)
+     # ₀=b2 ₁=b1 ₂=b0 ₃=word ₄=acc
+     in let b3 = byteToHex (bitand (shr ₃ 24) 255)
+     # ₀=b3 ₁=b2 ₂=b1 ₃=b0 ₄=word ₅=acc
+     in ₅ ⧺ ₃ ⧺ ₂ ⧺ ₁ ⧺ ₀
+   ) "" ₀
+
+# Extract 16 LITTLE-ENDIAN 32-bit words from a 64-byte block at offset.
+# ₁=data ₀=offset
+╭─ blockToWordsLE : [n]I64 → I64 → [16]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=wordIdx ₂=offset ₃=data
+     let i = ₀ × 4 + ₂
+     # ₀=i ₁=wordIdx ₂=acc ₃=offset ₄=data
+     in let w = add32 (add32 (add32
+           (index ₄ ₀)
+           (shl (index ₄ (₀ + 1)) 8))
+           (shl (index ₄ (₀ + 2)) 16))
+           (shl (index ₄ (₀ + 3)) 24)
+     # ₀=w ₁=i ₂=wordIdx ₃=acc
+     in ₃ ⊕ [₀]
+   ) [] (ι 16)
+
+# MD5 padding: same structure as SHA-256 but length is LITTLE-ENDIAN
+╭─ md5Pad : [n]I64 → [m]I64
+╰─ let msgLen = len ₀
+   # ₀=msgLen ₁=msg
+   in let bitLen = ₀ × 8
+   # ₀=bitLen ₁=msgLen ₂=msg
+   in let padded = ₂ ⊕ [128]
+   # ₀=padded ₁=bitLen ₂=msgLen
+   in let rem = (₂ + 1) % 64
+   # ₀=rem ₁=padded ₂=bitLen
+   in let zerosNeeded = if ₀ ≤ 56 then 56 - ₀ else 120 - ₀
+   # ₀=zerosNeeded ₁=rem ₂=padded ₃=bitLen
+   in let withZeros = ⌿ (λ→ λ→ ₁ ⊕ [0]) ₂ (ι ₀)
+   # ₀=withZeros ₁=zerosNeeded ₂=rem ₃=padded ₄=bitLen
+   in ₀ ⊕ [
+        bitand ₄ 255,
+        bitand (shr ₄ 8) 255,
+        bitand (shr ₄ 16) 255,
+        bitand (shr ₄ 24) 255,
+        bitand (shr ₄ 32) 255,
+        bitand (shr ₄ 40) 255,
+        bitand (shr ₄ 48) 255,
+        bitand (shr ₄ 56) 255
+      ]
+
+# MD5 T constants: floor(2^32 × |sin(i+1)|) for i = 0..63
+let md5T = [
+  3614090360, 3905402710, 606105819, 3250441966, 4118548399, 1200080426, 2821735955, 4249261313,
+  1770035416, 2336552879, 4294925233, 2304563134, 1804603682, 4254626195, 2792965006, 1236535329,
+  4129170786, 3225465664, 643717713, 3921069994, 3593408605, 38016083, 3634488961, 3889429448,
+  568446438, 3275163606, 4107603335, 1163531501, 2850285829, 4243563512, 1735328473, 2368359562,
+  4294588738, 2272392833, 1839030562, 4259657740, 2763975236, 1272893353, 4139469664, 3200236656,
+  681279174, 3936430074, 3572445317, 76029189, 3654602809, 3873151461, 530742520, 3299628645,
+  4096336452, 1126891415, 2878612391, 4237533241, 1700485571, 2399980690, 4293915773, 2240044497,
+  1873313359, 4264355552, 2734768916, 1309151649, 4149444226, 3174756917, 718787259, 3951481745
+]
+
+# Per-round left-rotation amounts
+let md5S = [
+  7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22, 7, 12, 17, 22,
+  5, 9, 14, 20, 5, 9, 14, 20, 5, 9, 14, 20, 5, 9, 14, 20,
+  4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23, 4, 11, 16, 23,
+  6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21, 6, 10, 15, 21
+]
+
+# Per-round message word index
+let md5G = [
+  0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15,
+  1, 6, 11, 0, 5, 10, 15, 4, 9, 14, 3, 8, 13, 2, 7, 12,
+  5, 8, 11, 14, 1, 4, 7, 10, 13, 0, 3, 6, 9, 12, 15, 2,
+  0, 7, 14, 5, 12, 3, 10, 1, 8, 15, 6, 13, 4, 11, 2, 9
+]
+
+# MD5 initial hash: A=0x67452301 B=0xefcdab89 C=0x98badcfe D=0x10325476
+let md5H0 = [1732584193, 4023233417, 2562383102, 271733878]
+
+# MD5 compression: 64 rounds on state [a,b,c,d].
+# Each round: new_b = b + rotl(a + F(b,c,d) + M[g[i]] + T[i], s[i])
+# Then rotate: a←d, b←new_b, c←b, d←c
+# ₁=M(16 words) ₀=state([a,b,c,d])
+╭─ md5Compress : [16]I64 → [4]I64 → [4]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=st ₀=i ₂=state(init) ₃=M
+     let a = index ₁ 0
+     # ₀=a ₁=i ₂=st ₃=init ₄=M
+     in let b = index ₂ 1
+     # ₀=b ₁=a ₂=i ₃=st ₄=init ₅=M
+     in let c = index ₃ 2
+     # ₀=c ₁=b ₂=a ₃=i ₄=st ₅=init ₆=M
+     in let d = index ₄ 3
+     # ₀=d ₁=c ₂=b ₃=a ₄=i ₅=st ₆=init ₇=M
+     in let f = if ₄ < 16
+                then bitor (bitand ₂ ₁) (bitand (not32 ₂) ₀)
+                else if ₄ < 32
+                then bitor (bitand ₀ ₂) (bitand (not32 ₀) ₁)
+                else if ₄ < 48
+                then ⊻ (⊻ ₂ ₁) ₀
+                else ⊻ ₁ (bitor ₂ (not32 ₀))
+     # ₀=f ₁=d ₂=c ₃=b ₄=a ₅=i ₆=st ₇=init ₈=M
+     in let mk = index ₈ (index md5G ₅)
+     # ₀=mk ₁=f ₂=d ₃=c ₄=b ₅=a ₆=i ₇=st ₈=init ₉=M
+     in let ti = index md5T ₆
+     # ₀=ti ₁=mk ₂=f ₃=d ₄=c ₅=b ₆=a ₇=i ₈=st ₉=init
+     in let si = index md5S ₇
+     # ₀=si ₁=ti ₂=mk ₃=f ₄=d ₅=c ₆=b ₇=a ₈=i ₉=st
+     in let newB = add32 ₆ (rotl32 ₀ (add32 (add32 (add32 ₇ ₃) ₂) ₁))
+     # ₀=newB ₁=si ₂=ti ₃=mk ₄=f ₅=d ₆=c ₇=b ₈=a ₉=i
+     in [₅, ₀, ₇, ₆]
+   ) ₀ (ι 64)
+
+# Element-wise add32 of two 4-word arrays.
+╭─ hashAdd4 : [4]I64 → [4]I64 → [4]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=idx ₂=compressed ₃=hash
+     ₁ ⊕ [add32 (index ₃ ₀) (index ₂ ₀)]
+   ) [] (ι 4)
+
+# Process one 64-byte block for MD5.
+# ₂=data ₁=blockOffset ₀=currentHash
+╭─ md5ProcessBlock : [n]I64 → I64 → [4]I64 → [4]I64
+╰─ let words = blockToWordsLE ₂ ₁
+   # ₀=words ₁=hash ₂=offset ₃=data
+   in let compressed = md5Compress ₀ ₁
+   # ₀=compressed ₁=words ₂=hash
+   in hashAdd4 ₂ ₀
+
+# MD5(string) → 32-char hex digest (little-endian output)
+╭─ md5 : String → String
+╰─ let padded = md5Pad (bytes ₀)
+   # ₀=padded ₁=string
+   in let numBlocks = len ₀ / 64
+   # ₀=numBlocks ₁=padded
+   in let finalHash = ⌿ (λ→ λ→
+     # ₁=hash ₀=blockIdx ₂=numBlocks ₃=padded
+     md5ProcessBlock ₃ (₀ × 64) ₁
+   ) md5H0 (ι ₀)
+   # ₀=finalHash
+   in wordsToHexLE ₀
+
+# ================================================================
+# BLAKE3
+# ================================================================
+
+# Functional array set: return new array with arr[idx] = val.
+# ₂=arr ₁=idx ₀=val
+╭─ aset : [n]I64 → I64 → I64 → [n]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=i ₂=val ₃=idx ₄=arr
+     ₁ ⊕ [if ₀ = ₃ then ₂ else index ₄ ₀]
+   ) [] (ι (len ₂))
+
+# BLAKE3 G mixing function.
+# ₅=a ₄=b ₃=c ₂=d ₁=mx ₀=my → ⟨a', b', c', d'⟩
+╭─ blake3G : I64 → I64 → I64 → I64 → I64 → I64 → ⟨I64, I64, I64, I64⟩
+╰─ let a1 = add32 (add32 ₅ ₄) ₁
+   # ₀=a1 ₁=my ₂=mx ₃=d ₄=c ₅=b
+   in let d1 = rotr32 16 (⊻ ₃ ₀)
+   # ₀=d1 ₁=a1 ₂=my ₃=mx ₄=d ₅=c ₆=b
+   in let c1 = add32 ₅ ₀
+   # ₀=c1 ₁=d1 ₂=a1 ₃=my
+   in let b1 = rotr32 12 (⊻ ₇ ₀)
+   # ₀=b1 ₁=c1 ₂=d1 ₃=a1 ₄=my
+   in let a2 = add32 (add32 ₃ ₀) ₄
+   # ₀=a2 ₁=b1 ₂=c1 ₃=d1
+   in let d2 = rotr32 8 (⊻ ₃ ₀)
+   # ₀=d2 ₁=a2 ₂=b1 ₃=c1
+   in let c2 = add32 ₃ ₀
+   # ₀=c2 ₁=d2 ₂=a2 ₃=b1
+   in let b2 = rotr32 7 (⊻ ₃ ₀)
+   # ₀=b2 ₁=c2 ₂=d2 ₃=a2
+   in ⟨₃, ₀, ₁, ₂⟩
+
+# Diagonal position tables for BLAKE3
+let b3DiagB = [5, 6, 7, 4]
+let b3DiagC = [10, 11, 8, 9]
+let b3DiagD = [15, 12, 13, 14]
+
+# BLAKE3 column round: G on columns (d, d+4, d+8, d+12) for d=0..3
+# Message pairs: (m[d*2], m[d*2+1])
+# ₁=state ₀=message
+╭─ blake3ColRound : [16]I64 → [16]I64 → [16]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=st(acc) ₀=d ₂=msg ₃=st_orig
+     let ⟨a, b, c, d2⟩ = blake3G (index ₁ ₀) (index ₁ (₀ + 4)) (index ₁ (₀ + 8)) (index ₁ (₀ + 12)) (index ₂ (₀ × 2)) (index ₂ (₀ × 2 + 1))
+     # ₀=d2 ₁=c ₂=b ₃=a ₄=d(col) ₅=st ₆=msg
+     in aset (aset (aset (aset ₅ ₄ ₃) (₄ + 4) ₂) (₄ + 8) ₁) (₄ + 12) ₀
+   ) ₁ (ι 4)
+
+# BLAKE3 diagonal round: G on diagonals
+# Diag d: positions (d, diagB[d], diagC[d], diagD[d])
+# Message pairs: (m[8+d*2], m[8+d*2+1])
+# ₁=state ₀=message
+╭─ blake3DiagRound : [16]I64 → [16]I64 → [16]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=st(acc) ₀=d ₂=msg
+     let bi = index b3DiagB ₀
+     # ₀=bi ₁=d ₂=st ₃=msg
+     in let ci = index b3DiagC ₁
+     # ₀=ci ₁=bi ₂=d ₃=st ₄=msg
+     in let di = index b3DiagD ₂
+     # ₀=di ₁=ci ₂=bi ₃=d ₄=st ₅=msg
+     in let ⟨a, b, c, d2⟩ = blake3G (index ₄ ₃) (index ₄ ₂) (index ₄ ₁) (index ₄ ₀) (index ₅ (₃ × 2 + 8)) (index ₅ (₃ × 2 + 9))
+     # ₀=d2 ₁=c ₂=b ₃=a ₄=di ₅=ci ₆=bi ₇=d ₈=st ₉=msg
+     in aset (aset (aset (aset ₈ ₇ ₃) ₆ ₂) ₅ ₁) ₄ ₀
+   ) ₁ (ι 4)
+
+# BLAKE3 message word permutation
+let b3Perm = [2, 6, 3, 10, 7, 0, 4, 13, 1, 11, 12, 5, 9, 14, 15, 8]
+
+╭─ blake3Permute : [16]I64 → [16]I64
+╰─ ⌿ (λ→ λ→
+     # ₁=acc ₀=i ₂=msg
+     ₁ ⊕ [index ₂ (index b3Perm ₀)]
+   ) [] (ι 16)
+
+# One BLAKE3 round: column round then diagonal round.
+# ₁=state ₀=message
+╭─ blake3Round : [16]I64 → [16]I64 → [16]I64
+╰─ let st1 = blake3ColRound ₁ ₀
+   # ₀=st1 ₁=msg ₂=st
+   in blake3DiagRound ₀ ₁
+
+# BLAKE3 compression: 7 rounds with message permutation between rounds.
+# ₁=state(16 words) ₀=message(16 words) → final state(16 words)
+╭─ blake3Compress : [16]I64 → [16]I64 → [16]I64
+╰─ let result = ⌿ (λ→ λ→
+     # ₁=⟨st,m⟩ ₀=roundIdx
+     let newSt = blake3Round (₁.0) (₁.1)
+     # ₀=newSt ₁=roundIdx ₂=⟨st,m⟩
+     in let newM = if ₁ < 6 then blake3Permute (₂.1) else ₂.1
+     # ₀=newM ₁=newSt
+     in ⟨₁, ₀⟩
+   ) ⟨₁, ₀⟩ (ι 7)
+   # ₀=result=⟨finalSt,finalM⟩
+   in ₀.0
+
+# Pad message bytes to 64 bytes with trailing zeros (for BLAKE3 block).
+╭─ blake3PadBlock : [n]I64 → [64]I64
+╰─ let padLen = 64 - len ₀
+   # ₀=padLen ₁=msg
+   in ⌿ (λ→ λ→ ₁ ⊕ [0]) ₁ (ι ₀)
+
+# BLAKE3 hash for messages ≤ 64 bytes (single chunk, single block).
+# Initializes 16-word state, compresses, XOR-folds to 8 words.
+╭─ blake3 : String → String
+╰─ let msgBytes = bytes ₀
+   # ₀=msgBytes ₁=str
+   in let msgLen = len ₀
+   # ₀=msgLen ₁=msgBytes
+   in let padded = blake3PadBlock ₁
+   # ₀=padded ₁=msgLen ₂=msgBytes
+   in let m = blockToWordsLE ₀ 0
+   # ₀=m ₁=padded ₂=msgLen ₃=msgBytes
+   # State init: [IV[0..7], IV[0..3], 0, 0, blockLen, flags=11]
+   in let state = [
+        index sha256H0 0, index sha256H0 1, index sha256H0 2, index sha256H0 3,
+        index sha256H0 4, index sha256H0 5, index sha256H0 6, index sha256H0 7,
+        index sha256H0 0, index sha256H0 1, index sha256H0 2, index sha256H0 3,
+        0, 0, ₂, 11
+      ]
+   # ₀=state ₁=m ₂=padded ₃=msgLen
+   in let final = blake3Compress ₀ ₁
+   # ₀=final ₁=state ₂=m
+   # XOR first 8 words with second 8 words
+   in let output = ⌿ (λ→ λ→
+     # ₁=acc ₀=i ₂=final
+     ₁ ⊕ [⊻ (index ₂ ₀) (index ₂ (₀ + 8))]
+   ) [] (ι 8)
+   # ₀=output
+   in wordsToHexLE ₀
+
+# ================================================================
+# Base64 (RFC 4648)
+# ================================================================
+
+let b64Alphabet = "ABCDEFGHIJKLMNOPQRSTUVWXYZabcdefghijklmnopqrstuvwxyz0123456789+/"
+
+# Encode 3 bytes → 4 base64 characters as a string.
+# ₂=b0 ₁=b1 ₀=b2
+╭─ b64EncodeTriple : I64 → I64 → I64 → String
+╰─ let n = bitor (bitor (shl ₂ 16) (shl ₁ 8)) ₀
+   # ₀=n ₁=b2 ₂=b1 ₃=b0
+   in let c0 = index b64Alphabet (bitand (shr ₀ 18) 63)
+   # ₀=c0 ₁=n
+   in let c1 = index b64Alphabet (bitand (shr ₁ 12) 63)
+   # ₀=c1 ₁=c0 ₂=n
+   in let c2 = index b64Alphabet (bitand (shr ₂ 6) 63)
+   # ₀=c2 ₁=c1 ₂=c0 ₃=n
+   in let c3 = index b64Alphabet (bitand ₃ 63)
+   # ₀=c3 ₁=c2 ₂=c1 ₃=c0
+   in toString ₃ ⧺ toString ₂ ⧺ toString ₁ ⧺ toString ₀
+
+# Base64-encode a byte array.
+╭─ base64Encode : [n]I64 → String
+╰─ let blen = len ₀
+   # ₀=blen ₁=data
+   in let fullTriples = ₀ / 3
+   # ₀=fullTriples ₁=blen ₂=data
+   in let remainder = ₁ % 3
+   # ₀=remainder ₁=fullTriples ₂=blen ₃=data
+   # Encode full 3-byte groups
+   in let bulk = ⌿ (λ→ λ→
+     # ₁=acc ₀=i ₂=remainder ₃=fullTriples ₄=blen ₅=data
+     let off = ₀ × 3
+     # ₀=off ₁=i ₂=acc ₃=remainder ₄=fullTriples ₅=blen ₆=data
+     in ₂ ⧺ b64EncodeTriple (index ₆ ₀) (index ₆ (₀ + 1)) (index ₆ (₀ + 2))
+   ) "" (ι ₁)
+   # ₀=bulk ₁=remainder ₂=fullTriples ₃=blen ₄=data
+   # Handle remainder
+   in if ₁ = 1
+      then let b0 = index ₄ (₃ - 1)
+           # ₀=b0 ₁=bulk ₂=remainder ₃=fullTriples ₄=blen ₅=data
+           in let n = shl ₀ 16
+           # ₀=n ₁=b0
+           in ₂ ⧺ toString (index b64Alphabet (bitand (shr ₀ 18) 63))
+              ⧺ toString (index b64Alphabet (bitand (shr ₀ 12) 63))
+              ⧺ "=="
+      else if ₁ = 2
+      then let b0 = index ₄ (₃ - 2)
+           # ₀=b0 ₁=bulk ₂=remainder ₃=fullTriples ₄=blen ₅=data
+           in let b1 = index ₅ (₄ - 1)
+           # ₀=b1 ₁=b0 ₂=bulk
+           in let n = bitor (shl ₁ 16) (shl ₀ 8)
+           # ₀=n ₁=b1 ₂=b0 ₃=bulk
+           in ₃ ⧺ toString (index b64Alphabet (bitand (shr ₀ 18) 63))
+              ⧺ toString (index b64Alphabet (bitand (shr ₀ 12) 63))
+              ⧺ toString (index b64Alphabet (bitand (shr ₀ 6) 63))
+              ⧺ "="
+      else ₀
+
+# Base64-encode a string (encodes its UTF-8 bytes).
+╭─ base64EncodeStr : String → String
+╰─ base64Encode (bytes ₀)
+
+# Base64 decode: maps ASCII byte → 6-bit value.
+╭─ b64DecodeVal : I64 → I64
+╰─ if ₀ ≥ 65 then if ₀ ≤ 90 then ₀ - 65 else
+     if ₀ ≥ 97 then if ₀ ≤ 122 then ₀ - 71 else 0 - 1 else 0 - 1
+   else if ₀ ≥ 48 then if ₀ ≤ 57 then ₀ + 4 else
+     if ₀ = 43 then 62 else if ₀ = 47 then 63 else 0 - 1
+   else 0 - 1
+
+# Base64-decode a string → byte array.
+╭─ base64Decode : String → [n]I64
+╰─ let raw = bytes ₀
+   # ₀=raw ₁=str
+   # Filter out '=' (61) and collect 6-bit values
+   in let vals = ⌿ (λ→ λ→
+     # ₁=acc ₀=byte ₂=raw
+     if ₀ = 61 then ₁ else ₁ ⊕ [b64DecodeVal ₀]
+   ) [] ₀
+   # ₀=vals ₁=raw
+   in let vlen = len ₀
+   # ₀=vlen ₁=vals
+   in let fullQuads = ₀ / 4
+   # ₀=fullQuads ₁=vlen ₂=vals
+   in let remainder = ₁ % 4
+   # ₀=remainder ₁=fullQuads ₂=vlen ₃=vals
+   # Decode full 4-value groups → 3 bytes each
+   in let bulk = ⌿ (λ→ λ→
+     # ₁=acc ₀=i ₂=remainder ₃=fullQuads ₄=vlen ₅=vals
+     let off = ₀ × 4
+     # ₀=off ₁=i ₂=acc ₃=remainder ₄=fullQuads ₅=vlen ₆=vals
+     in let n = bitor (bitor (bitor (shl (index ₆ ₀) 18) (shl (index ₆ (₀ + 1)) 12)) (shl (index ₆ (₀ + 2)) 6)) (index ₆ (₀ + 3))
+     # ₀=n ₁=off ₂=i ₃=acc
+     in ₃ ⊕ [bitand (shr ₀ 16) 255, bitand (shr ₀ 8) 255, bitand ₀ 255]
+   ) [] (ι ₁)
+   # ₀=bulk ₁=remainder ₂=fullQuads ₃=vlen ₄=vals
+   # Handle remainder (2 values → 1 byte, 3 values → 2 bytes)
+   in if ₁ = 2
+      then let n = bitor (shl (index ₄ (₃ - 2)) 18) (shl (index ₄ (₃ - 1)) 12)
+           # ₀=n ₁=bulk
+           in ₁ ⊕ [bitand (shr ₀ 16) 255]
+      else if ₁ = 3
+      then let n = bitor (bitor (shl (index ₄ (₃ - 3)) 18) (shl (index ₄ (₃ - 2)) 12)) (shl (index ₄ (₃ - 1)) 6)
+           # ₀=n ₁=bulk
+           in ₁ ⊕ [bitand (shr ₀ 16) 255, bitand (shr ₀ 8) 255]
+      else ₀
diff --git a/stdlib/list.goth b/stdlib/list.goth
index 9d30967..7988f7e 100644
--- a/stdlib/list.goth
+++ b/stdlib/list.goth
@@ -103,10 +103,10 @@
 ╰─ Σ ₀ / len ₀
 
 ╭─ minimum : [n]F → F
-╰─ min/ ₀
+╰─ ⌿ (λ→ λ→ if ₀ < ₁ then ₀ else ₁) (₀[0]) ₀
 
 ╭─ maximum : [n]F → F
-╰─ max/ ₀
+╰─ ⌿ (λ→ λ→ if ₀ > ₁ then ₀ else ₁) (₀[0]) ₀
 
 # Variance (population variance)
 ╭─ variance : [n]F → F
@@ -280,24 +280,9 @@
 ╭─ unsnoc : [n]α → ⟨[m]α, α⟩
 ╰─ ⟨take (len ₀ - 1) ₀, ₀[len ₀ - 1]⟩
 
-# ============ Singleton & Pair Operations ============
+# ============ Singleton Operations ============
+# Note: pair, fst, snd, bimap (mapPair) are in prelude.goth
 
 # Create singleton list
 ╭─ singleton : α → [1]α
 ╰─ [₀]
-
-# Create pair from two elements
-╭─ pair : α → β → ⟨α, β⟩
-╰─ ⟨₁, ₀⟩
-
-# Get first element of pair
-╭─ fst : ⟨α, β⟩ → α
-╰─ ₀.0
-
-# Get second element of pair
-╭─ snd : ⟨α, β⟩ → β
-╰─ ₀.1
-
-# Map over both elements of pair
-╭─ mapPair : (α → γ) → (β → δ) → ⟨α, β⟩ → ⟨γ, δ⟩
-╰─ ⟨₂ ₀.0, ₁ ₀.1⟩
diff --git a/stdlib/math.goth b/stdlib/math.goth
index 5bee5a2..d7f0eda 100644
--- a/stdlib/math.goth
+++ b/stdlib/math.goth
@@ -219,14 +219,7 @@ let lnTen = ln 10.0
 ╰─ 0.5 × ln ((1.0 + ₀) / (1.0 - ₀))
 
 # ============ Number Theory (Integer) ============
-
-# Check if even
-╭─ isEven : ℤ → Bool
-╰─ ₀ % 2 = 0
-
-# Check if odd
-╭─ isOdd : ℤ → Bool
-╰─ ₀ % 2 ≠ 0
+# Note: isEven, isOdd, isDivisibleBy are in prelude.goth
 
 # Check if divisible
 ╭─ divides : ℤ → ℤ → Bool
@@ -354,9 +347,7 @@ let lnTen = ln 10.0
 ╭─ maxI : ℤ → ℤ → ℤ
 ╰─ if ₁ > ₀ then ₁ else ₀
 
-# Clamp value to range [lo, hi]
-╭─ clamp : F → F → F → F
-╰─ if ₀ < ₂ then ₂ else if ₀ > ₁ then ₁ else ₀
+# Note: clamp (float) is in prelude.goth
 
 # Clamp integer to range
 ╭─ clampI : ℤ → ℤ → ℤ → ℤ
diff --git a/stdlib/option.goth b/stdlib/option.goth
index 446fbfa..a68eea5 100644
--- a/stdlib/option.goth
+++ b/stdlib/option.goth
@@ -3,311 +3,182 @@
 #
 # Option is encoded as a tuple ⟨Bool, α⟩ where:
 #   - ⟨⊤, value⟩ represents Some(value)
-#   - ⟨⊥, _⟩ represents None (second element is undefined/placeholder)
+#   - ⟨⊥, _⟩ represents None (payload is undefined; never read by correct code)
 #
-# This encoding allows pattern matching and works with the current
-# type system limitations around polymorphism.
+# All functions are generic — the evaluator is type-erased at runtime,
+# so a single `some` works for any value type. Type signatures use
+# α, β, γ as documentation; the checker passes them through.
 #
-# Convention: Functions ending in 'I' work with ⟨Bool, ℤ⟩
-#             Functions ending in 'F' work with ⟨Bool, F⟩
-#             Generic functions (where possible) have no suffix
-
-# ============ Type Aliases (Documentation) ============
-# OptionI = ⟨Bool, ℤ⟩   -- Option of integer
-# OptionF = ⟨Bool, F⟩   -- Option of float
-# OptionB = ⟨Bool, Bool⟩ -- Option of bool
+# None uses 0 as a dead placeholder. The payload of a None is never
+# observed by any function in this module.
 
 # ============ Constructors ============
 
-# Create Some value (integer)
-╭─ someI : ℤ → ⟨Bool, ℤ⟩
-╰─ ⟨⊤, ₀⟩
-
-# Create Some value (float)
-╭─ someF : F → ⟨Bool, F⟩
-╰─ ⟨⊤, ₀⟩
-
-# Create Some value (bool)
-╭─ someB : Bool → ⟨Bool, Bool⟩
+# Wrap a value as Some
+╭─ some : α → ⟨Bool, α⟩
 ╰─ ⟨⊤, ₀⟩
 
-# Create None (integer) - uses 0 as placeholder
-╭─ noneI : ⟨Bool, ℤ⟩
+# Create None (empty option)
+# Takes unit arg to force evaluation (type variable α would make
+# a bare constant look like a 1-arg function to the evaluator)
+╭─ none : ⟨⟩ → ⟨Bool, α⟩
 ╰─ ⟨⊥, 0⟩
 
-# Create None (float) - uses 0.0 as placeholder
-╭─ noneF : ⟨Bool, F⟩
-╰─ ⟨⊥, 0.0⟩
-
-# Create None (bool) - uses ⊥ as placeholder
-╭─ noneB : ⟨Bool, Bool⟩
-╰─ ⟨⊥, ⊥⟩
-
 # ============ Predicates ============
 
-# Check if option has a value (generic - works with any ⟨Bool, α⟩)
+# Check if option has a value
 ╭─ isSome : ⟨Bool, α⟩ → Bool
 ╰─ ₀.0
 
-# Check if option is empty (generic)
+# Check if option is empty
 ╭─ isNone : ⟨Bool, α⟩ → Bool
 ╰─ ¬(₀.0)
 
-# Integer-specific versions
-╭─ isSomeI : ⟨Bool, ℤ⟩ → Bool
-╰─ ₀.0
-
-╭─ isNoneI : ⟨Bool, ℤ⟩ → Bool
-╰─ ¬(₀.0)
-
-# Float-specific versions
-╭─ isSomeF : ⟨Bool, F⟩ → Bool
-╰─ ₀.0
-
-╭─ isNoneF : ⟨Bool, F⟩ → Bool
-╰─ ¬(₀.0)
-
 # ============ Extractors ============
 
-# Get value or default (integer)
-╭─ getOrElseI : ℤ → ⟨Bool, ℤ⟩ → ℤ
+# Get value or return default
+╭─ getOrElse : α → ⟨Bool, α⟩ → α
 ╰─ if ₀.0 then ₀.1 else ₁
 
-# Get value or default (float)
-╭─ getOrElseF : F → ⟨Bool, F⟩ → F
-╰─ if ₀.0 then ₀.1 else ₁
-
-# Get value or default (bool)
-╭─ getOrElseB : Bool → ⟨Bool, Bool⟩ → Bool
-╰─ if ₀.0 then ₀.1 else ₁
-
-# Unsafe get - assumes Some (integer)
-# Use only when you're certain the option is Some
-╭─ unsafeGetI : ⟨Bool, ℤ⟩ → ℤ
-╰─ ₀.1
-
-# Unsafe get - assumes Some (float)
-╭─ unsafeGetF : ⟨Bool, F⟩ → F
+# Get value (unsafe — assumes Some)
+╭─ unsafeGet : ⟨Bool, α⟩ → α
 ╰─ ₀.1
 
-# Get value or compute default (integer)
-╭─ getOrComputeI : (⟨⟩ → ℤ) → ⟨Bool, ℤ⟩ → ℤ
-╰─ if ₀.0 then ₀.1 else ₁ ⟨⟩
-
-# Get value or compute default (float)
-╭─ getOrComputeF : (⟨⟩ → F) → ⟨Bool, F⟩ → F
+# Get value or compute default lazily
+╭─ getOrCompute : (⟨⟩ → α) → ⟨Bool, α⟩ → α
 ╰─ if ₀.0 then ₀.1 else ₁ ⟨⟩
 
 # ============ Transformations ============
 
-# Map function over option (integer → integer)
-╭─ mapOptI : (ℤ → ℤ) → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
-╰─ if ₀.0 then ⟨⊤, ₁ ₀.1⟩ else ⟨⊥, 0⟩
-
-# Map function over option (float → float)
-╭─ mapOptF : (F → F) → ⟨Bool, F⟩ → ⟨Bool, F⟩
-╰─ if ₀.0 then ⟨⊤, ₁ ₀.1⟩ else ⟨⊥, 0.0⟩
-
-# Map function over option (integer → float)
-╭─ mapOptIF : (ℤ → F) → ⟨Bool, ℤ⟩ → ⟨Bool, F⟩
-╰─ if ₀.0 then ⟨⊤, ₁ ₀.1⟩ else ⟨⊥, 0.0⟩
-
-# Map function over option (float → integer)
-╭─ mapOptFI : (F → ℤ) → ⟨Bool, F⟩ → ⟨Bool, ℤ⟩
+# Map function over option
+╭─ mapOpt : (α → β) → ⟨Bool, α⟩ → ⟨Bool, β⟩
 ╰─ if ₀.0 then ⟨⊤, ₁ ₀.1⟩ else ⟨⊥, 0⟩
 
-# FlatMap / bind (integer)
-╭─ flatMapOptI : (ℤ → ⟨Bool, ℤ⟩) → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
+# FlatMap / monadic bind
+╭─ flatMapOpt : (α → ⟨Bool, β⟩) → ⟨Bool, α⟩ → ⟨Bool, β⟩
 ╰─ if ₀.0 then ₁ ₀.1 else ⟨⊥, 0⟩
 
-# FlatMap / bind (float)
-╭─ flatMapOptF : (F → ⟨Bool, F⟩) → ⟨Bool, F⟩ → ⟨Bool, F⟩
-╰─ if ₀.0 then ₁ ₀.1 else ⟨⊥, 0.0⟩
-
-# Filter option by predicate (integer)
-╭─ filterOptI : (ℤ → Bool) → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
+# Filter: keep Some only if predicate holds
+╭─ filterOpt : (α → Bool) → ⟨Bool, α⟩ → ⟨Bool, α⟩
 ╰─ if ₀.0 ∧ ₁ ₀.1 then ₀ else ⟨⊥, 0⟩
 
-# Filter option by predicate (float)
-╭─ filterOptF : (F → Bool) → ⟨Bool, F⟩ → ⟨Bool, F⟩
-╰─ if ₀.0 ∧ ₁ ₀.1 then ₀ else ⟨⊥, 0.0⟩
-
 # ============ Combining Options ============
 
-# Or else: return first if Some, else second (integer)
-╭─ orElseOptI : ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
-╰─ if ₁.0 then ₁ else ₀
-
-# Or else: return first if Some, else second (float)
-╭─ orElseOptF : ⟨Bool, F⟩ → ⟨Bool, F⟩ → ⟨Bool, F⟩
+# Return first if Some, else second
+╭─ orElseOpt : ⟨Bool, α⟩ → ⟨Bool, α⟩ → ⟨Bool, α⟩
 ╰─ if ₁.0 then ₁ else ₀
 
-# And then: return second if first is Some, else None (integer)
-╭─ andThenOptI : ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
+# Return second if first is Some, else None
+╭─ andThenOpt : ⟨Bool, α⟩ → ⟨Bool, β⟩ → ⟨Bool, β⟩
 ╰─ if ₁.0 then ₀ else ⟨⊥, 0⟩
 
-# Zip two options: Some only if both are Some (integer)
-╭─ zipOptI : ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩ → ⟨Bool, ⟨ℤ, ℤ⟩⟩
-╰─ if ₁.0 ∧ ₀.0 then ⟨⊤, ⟨₁.1, ₀.1⟩⟩ else ⟨⊥, ⟨0, 0⟩⟩
+# Zip: Some only if both are Some
+╭─ zipOpt : ⟨Bool, α⟩ → ⟨Bool, β⟩ → ⟨Bool, ⟨α, β⟩⟩
+╰─ if ₁.0 ∧ ₀.0 then ⟨⊤, ⟨₁.1, ₀.1⟩⟩ else ⟨⊥, 0⟩
 
-# Zip two options with function (integer)
-╭─ zipWithOptI : (ℤ → ℤ → ℤ) → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
+# Zip with combining function
+╭─ zipWithOpt : (α → β → γ) → ⟨Bool, α⟩ → ⟨Bool, β⟩ → ⟨Bool, γ⟩
 ╰─ if ₁.0 ∧ ₀.0 then ⟨⊤, ₂ ₁.1 ₀.1⟩ else ⟨⊥, 0⟩
 
-# ============ Conversion ============
+# ============ Folding ============
 
-# Convert to list (empty or singleton) - integer
-╭─ optToListI : ⟨Bool, ℤ⟩ → [n]ℤ
-╰─ if ₀.0 then [₀.1] else []
+# Fold: apply f to value if Some, else return default
+╭─ foldOpt : β → (α → β) → ⟨Bool, α⟩ → β
+╰─ if ₀.0 then ₁ ₀.1 else ₂
 
-# Convert to list (empty or singleton) - float
-╭─ optToListF : ⟨Bool, F⟩ → [n]F
+# ============ Conversion ============
+
+# Convert to list (empty or singleton)
+╭─ optToList : ⟨Bool, α⟩ → [n]α
 ╰─ if ₀.0 then [₀.1] else []
 
-# Convert list head to option - integer
-╭─ listHeadOptI : [n]ℤ → ⟨Bool, ℤ⟩
+# Convert list head to option
+╭─ listHeadOpt : [n]α → ⟨Bool, α⟩
 ╰─ if len ₀ > 0 then ⟨⊤, ₀[0]⟩ else ⟨⊥, 0⟩
 
-# Convert list head to option - float
-╭─ listHeadOptF : [n]F → ⟨Bool, F⟩
-╰─ if len ₀ > 0 then ⟨⊤, ₀[0]⟩ else ⟨⊥, 0.0⟩
-
-# Convert list last to option - integer
-╭─ listLastOptI : [n]ℤ → ⟨Bool, ℤ⟩
+# Convert list last to option
+╭─ listLastOpt : [n]α → ⟨Bool, α⟩
 ╰─ if len ₀ > 0 then ⟨⊤, ₀[len ₀ - 1]⟩ else ⟨⊥, 0⟩
 
-# Convert list last to option - float
-╭─ listLastOptF : [n]F → ⟨Bool, F⟩
-╰─ if len ₀ > 0 then ⟨⊤, ₀[len ₀ - 1]⟩ else ⟨⊥, 0.0⟩
-
-# ============ Safe Operations ============
-
-# Safe division (returns None on divide by zero) - integer
-╭─ safeDivI : ℤ → ℤ → ⟨Bool, ℤ⟩
-╰─ if ₀ = 0 then ⟨⊥, 0⟩ else ⟨⊤, ₁ / ₀⟩
-
-# Safe division - float
-╭─ safeDivF : F → F → ⟨Bool, F⟩
-╰─ if ₀ = 0.0 then ⟨⊥, 0.0⟩ else ⟨⊤, ₁ / ₀⟩
-
-# Safe modulo (returns None on divide by zero)
-╭─ safeModI : ℤ → ℤ → ⟨Bool, ℤ⟩
-╰─ if ₀ = 0 then ⟨⊥, 0⟩ else ⟨⊤, ₁ % ₀⟩
-
-# Safe square root (returns None for negative) - float
-╭─ safeSqrtF : F → ⟨Bool, F⟩
-╰─ if ₀ < 0.0 then ⟨⊥, 0.0⟩ else ⟨⊤, √₀⟩
-
-# Safe log (returns None for non-positive) - float
-╭─ safeLogF : F → ⟨Bool, F⟩
-╰─ if ₀ ≤ 0.0 then ⟨⊥, 0.0⟩ else ⟨⊤, ln ₀⟩
-
-# Safe array index - integer
-╭─ safeIndexI : ℤ → [n]ℤ → ⟨Bool, ℤ⟩
-╰─ if ₁ ≥ 0 ∧ ₁ < len ₀ then ⟨⊤, ₀[₁]⟩ else ⟨⊥, 0⟩
-
-# Safe array index - float
-╭─ safeIndexF : ℤ → [n]F → ⟨Bool, F⟩
-╰─ if ₁ ≥ 0 ∧ ₁ < len ₀ then ⟨⊤, ₀[₁]⟩ else ⟨⊥, 0.0⟩
-
-# ============ Folding ============
-
-# Fold option (integer)
-╭─ foldOptI : β → (ℤ → β) → ⟨Bool, ℤ⟩ → β
-╰─ if ₀.0 then ₁ ₀.1 else ₂
-
-# Fold option (float)
-╭─ foldOptF : β → (F → β) → ⟨Bool, F⟩ → β
-╰─ if ₀.0 then ₁ ₀.1 else ₂
-
 # ============ Boolean Checks ============
 
-# Check if option contains specific value (integer)
-╭─ containsOptI : ℤ → ⟨Bool, ℤ⟩ → Bool
+# Check if option contains specific value
+╭─ containsOpt : α → ⟨Bool, α⟩ → Bool
 ╰─ ₀.0 ∧ ₀.1 = ₁
 
-# Check if option contains specific value (float)
-╭─ containsOptF : F → ⟨Bool, F⟩ → Bool
-╰─ ₀.0 ∧ ₀.1 = ₁
-
-# Check if option value satisfies predicate (integer)
-╭─ existsOptI : (ℤ → Bool) → ⟨Bool, ℤ⟩ → Bool
+# Check if value satisfies predicate (false for None)
+╭─ existsOpt : (α → Bool) → ⟨Bool, α⟩ → Bool
 ╰─ ₀.0 ∧ ₁ ₀.1
 
-# Check if option value satisfies predicate (float)
-╭─ existsOptF : (F → Bool) → ⟨Bool, F⟩ → Bool
-╰─ ₀.0 ∧ ₁ ₀.1
-
-# Check if None or value satisfies predicate (integer)
-╭─ forallOptI : (ℤ → Bool) → ⟨Bool, ℤ⟩ → Bool
-╰─ ¬(₀.0) ∨ ₁ ₀.1
-
-# Check if None or value satisfies predicate (float)
-╭─ forallOptF : (F → Bool) → ⟨Bool, F⟩ → Bool
+# Check if None or value satisfies predicate
+╭─ forallOpt : (α → Bool) → ⟨Bool, α⟩ → Bool
 ╰─ ¬(₀.0) ∨ ₁ ₀.1
 
 # ============ Comparison ============
 
-# Compare two options (integer) - both must be same variant
-╭─ eqOptI : ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩ → Bool
+# Compare two options (equal if both None, or both Some with equal values)
+╭─ eqOpt : ⟨Bool, α⟩ → ⟨Bool, α⟩ → Bool
 ╰─ if ₁.0 ∧ ₀.0 then ₁.1 = ₀.1
    else if ¬(₁.0) ∧ ¬(₀.0) then ⊤
    else ⊥
 
-# Compare two options (float)
-╭─ eqOptF : ⟨Bool, F⟩ → ⟨Bool, F⟩ → Bool
-╰─ if ₁.0 ∧ ₀.0 then ₁.1 = ₀.1
-   else if ¬(₁.0) ∧ ¬(₀.0) then ⊤
-   else ⊥
+# ============ Safe Operations ============
+
+# Safe division (None on divide by zero)
+╭─ safeDiv : α → α → ⟨Bool, α⟩
+╰─ if ₀ = 0 then ⟨⊥, 0⟩ else ⟨⊤, ₁ / ₀⟩
+
+# Safe modulo (None on divide by zero)
+╭─ safeMod : ℤ → ℤ → ⟨Bool, ℤ⟩
+╰─ if ₀ = 0 then ⟨⊥, 0⟩ else ⟨⊤, ₁ % ₀⟩
+
+# Safe square root (None for negative)
+╭─ safeSqrt : F → ⟨Bool, F⟩
+╰─ if ₀ < 0.0 then ⟨⊥, 0⟩ else ⟨⊤, √₀⟩
+
+# Safe log (None for non-positive)
+╭─ safeLog : F → ⟨Bool, F⟩
+╰─ if ₀ ≤ 0.0 then ⟨⊥, 0⟩ else ⟨⊤, ln ₀⟩
+
+# Safe array index (None if out of bounds)
+╭─ safeIndex : ℤ → [n]α → ⟨Bool, α⟩
+╰─ if ₁ ≥ 0 ∧ ₁ < len ₀ then ⟨⊤, ₀[₁]⟩ else ⟨⊥, 0⟩
 
 # ============ Utility ============
 
-# Apply function if Some, do nothing if None (for side effects)
-╭─ forEachOptI : (ℤ → ⟨⟩) → ⟨Bool, ℤ⟩ → ⟨⟩
+# Apply function for side effect if Some
+╭─ forEachOpt : (α → ⟨⟩) → ⟨Bool, α⟩ → ⟨⟩
 ╰─ if ₀.0 then ₁ ₀.1 else ⟨⟩
 
 # Tap: apply function for side effect, return original option
-╭─ tapOptI : (ℤ → ⟨⟩) → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ⟩
+╭─ tapOpt : (α → ⟨⟩) → ⟨Bool, α⟩ → ⟨Bool, α⟩
 ╰─ if ₀.0 then let _ = ₁ ₀.1 in ₀ else ₀
 
 # ============ Creating Options from Conditions ============
 
-# Create Some if condition is true, else None (integer)
-╭─ whenI : Bool → ℤ → ⟨Bool, ℤ⟩
+# Some if condition true, else None
+╭─ when : Bool → α → ⟨Bool, α⟩
 ╰─ if ₁ then ⟨⊤, ₀⟩ else ⟨⊥, 0⟩
 
-# Create Some if condition is true, else None (float)
-╭─ whenF : Bool → F → ⟨Bool, F⟩
-╰─ if ₁ then ⟨⊤, ₀⟩ else ⟨⊥, 0.0⟩
-
-# Create Some if predicate passes, else None (integer)
-╭─ filterToOptI : (ℤ → Bool) → ℤ → ⟨Bool, ℤ⟩
+# Some if predicate passes, else None
+╭─ filterToOpt : (α → Bool) → α → ⟨Bool, α⟩
 ╰─ if ₁ ₀ then ⟨⊤, ₀⟩ else ⟨⊥, 0⟩
 
-# Create Some if predicate passes, else None (float)
-╭─ filterToOptF : (F → Bool) → F → ⟨Bool, F⟩
-╰─ if ₁ ₀ then ⟨⊤, ₀⟩ else ⟨⊥, 0.0⟩
-
-# Create Some if value is non-zero, else None (integer)
-╭─ nonZeroOptI : ℤ → ⟨Bool, ℤ⟩
+# Some if value is non-zero, else None
+╭─ nonZeroOpt : ℤ → ⟨Bool, ℤ⟩
 ╰─ if ₀ ≠ 0 then ⟨⊤, ₀⟩ else ⟨⊥, 0⟩
 
-# Create Some if value is positive, else None (integer)
-╭─ positiveOptI : ℤ → ⟨Bool, ℤ⟩
+# Some if value is positive, else None
+╭─ positiveOpt : ℤ → ⟨Bool, ℤ⟩
 ╰─ if ₀ > 0 then ⟨⊤, ₀⟩ else ⟨⊥, 0⟩
 
-# Create Some if value is non-negative, else None (integer)
-╭─ nonNegativeOptI : ℤ → ⟨Bool, ℤ⟩
+# Some if value is non-negative, else None
+╭─ nonNegativeOpt : ℤ → ⟨Bool, ℤ⟩
 ╰─ if ₀ ≥ 0 then ⟨⊤, ₀⟩ else ⟨⊥, 0⟩
 
 # ============ String Representation ============
 
-# Convert option to string for display (integer)
-╭─ showOptI : ⟨Bool, ℤ⟩ → String
-╰─ if ₀.0 then strConcat "Some(" (strConcat (toString ₀.1) ")")
-   else "None"
-
-# Convert option to string for display (float)
-╭─ showOptF : ⟨Bool, F⟩ → String
-╰─ if ₀.0 then strConcat "Some(" (strConcat (toString ₀.1) ")")
+# Convert option to display string
+╭─ showOpt : ⟨Bool, α⟩ → String
+╰─ if ₀.0 then "Some(" ⧺ toString ₀.1 ⧺ ")"
    else "None"
diff --git a/stdlib/prelude.goth b/stdlib/prelude.goth
index 4684383..704f38a 100644
--- a/stdlib/prelude.goth
+++ b/stdlib/prelude.goth
@@ -179,132 +179,10 @@
 ╭─ divMod : ℤ → ℤ → ⟨ℤ, ℤ⟩
 ╰─ ⟨₁ / ₀, ₁ % ₀⟩
 
-# ============ Float Operations ============
-
-# Double a number
-╭─ double : F → F
-╰─ ₀ × 2.0
-
-# Halve a number
-╭─ half : F → F
-╰─ ₀ / 2.0
-
-# Square a number
-╭─ square : F → F
-╰─ ₀ × ₀
-
-# Cube a number
-╭─ cube : F → F
-╰─ ₀ × ₀ × ₀
-
-# Negate a float
-╭─ negate : F → F
-╰─ 0.0 - ₀
-
-# Reciprocal (1/x)
-╭─ recip : F → F
-╰─ 1.0 / ₀
-
-# Absolute value (float)
-╭─ absF : F → F
-╰─ if ₀ < 0.0 then 0.0 - ₀ else ₀
-
-# Sign of float (-1.0, 0.0, or 1.0)
-╭─ signF : F → F
-╰─ if ₀ < 0.0 then -1.0
-   else if ₀ > 0.0 then 1.0
-   else 0.0
-
-# Linear interpolation: lerp t a b = a + t*(b-a)
-╭─ lerp : F → F → F → F
-╰─ ₁ + ₂ × (₀ - ₁)
-
-# Inverse lerp: what t gives this value between a and b?
-╭─ invLerp : F → F → F → F
-╰─ (₂ - ₁) / (₀ - ₁)
-
-# Smooth step (cubic interpolation)
-╭─ smoothstep : F → F → F → F
-╰─ let t = clamp ((₀ - ₂) / (₁ - ₂)) 0.0 1.0
-   in t × t × (3.0 - 2.0 × t)
-
-# ============ Rounding Operations ============
-
-# Floor (round toward negative infinity)
-╭─ floor : F → F
-╰─ ⌊₀⌋
-
-# Ceiling (round toward positive infinity)
-╭─ ceil : F → F
-╰─ ⌈₀⌉
-
-# Round to nearest integer
-╭─ round : F → F
-╰─ ⌊₀ + 0.5⌋
-
-# Truncate toward zero
-╭─ trunc : F → F
-╰─ if ₀ < 0.0 then ⌈₀⌉ else ⌊₀⌋
-
-# Fractional part
-╭─ frac : F → F
-╰─ ₀ - ⌊₀⌋
-
-# ============ Trigonometric Functions ============
-# Note: Built-in trig functions: sin, cos, tan, asin, acos, atan
-
-# Secant
-╭─ sec : F → F
-╰─ 1.0 / cos ₀
-
-# Cosecant
-╭─ csc : F → F
-╰─ 1.0 / sin ₀
-
-# Cotangent
-╭─ cot : F → F
-╰─ cos ₀ / sin ₀
-
-# Convert degrees to radians
-╭─ toRadians : F → F
-╰─ ₀ × π / 180.0
-
-# Convert radians to degrees
-╭─ toDegrees : F → F
-╰─ ₀ × 180.0 / π
-
-# ============ Exponential and Logarithmic ============
-# Note: Built-in: exp, ln, log₁₀, log₂, √
-
-# Power of 2
-╭─ pow2 : F → F
-╰─ 2.0 ^ ₀
-
-# Power of 10
-╭─ pow10 : F → F
-╰─ 10.0 ^ ₀
-
-# Square root (alias)
-╭─ sqrt : F → F
-╰─ √₀
-
-# Cube root
-╭─ cbrt : F → F
-╰─ ₀ ^ (1.0 / 3.0)
-
-# Natural logarithm (alias)
-╭─ log : F → F
-╰─ ln ₀
-
-# Logarithm base b
-╭─ logBase : F → F → F
-╰─ ln ₀ / ln ₁
-
-# Hyperbolic functions are built-in: sinh, cosh, tanh
-
 # ============ Array/List Basic Operations ============
-# Note: head, length, sum, product, mean, minimum, maximum
-# are defined in list.goth. Import that module for these.
+# Note: For math functions (floor, ceil, sqrt, trig, etc.)
+# use "stdlib/math.goth". For list operations (head, tail, etc.)
+# use "stdlib/list.goth".
 
 # Check if empty
 ╭─ isEmpty : [n]α → Bool
diff --git a/stdlib/random.goth b/stdlib/random.goth
new file mode 100644
index 0000000..2b1f349
--- /dev/null
+++ b/stdlib/random.goth
@@ -0,0 +1,124 @@
+# Goth Standard Library - Random Number Generation
+# Provides seeded PRNG via xorshift64 with state-passing pattern.
+#
+# Usage pattern:
+#   let seed = bytesToSeed (⧏ 8 "/dev/urandom")
+#   let ⟨v1, s1⟩ = randFloat seed
+#   let ⟨v2, s2⟩ = randFloat s1
+#
+# All RNG functions return ⟨value, nextSeed⟩ tuples for explicit
+# state threading. Use randFloats/randInts for bulk generation.
+#
+# Built-in primitives used:
+#   ⧏ (readBytes), bitxor/⊻, shl, shr, bitand, bitor
+#   fold/⌿, toFloat, toInt
+
+# ============ Seed Management ============
+
+# Convert 8 entropy bytes to a 64-bit seed value.
+# Combines bytes via shift-and-or into a single I64.
+# Input: [8]I64 array of byte values (0-255)
+# Output: I64 seed (64-bit)
+╭─ bytesToSeed : [8]I64 → I64
+╰─ bitand (⌿ (λ→ λ→ bitor (shl ₁ 8) ₀) 0 ₀) mask64
+
+# Create a seed from system entropy.
+# Reads 8 bytes from /dev/urandom and packs them into I64.
+╭─ entropy : () → I64
+╰─ bytesToSeed (⧏ 8 "/dev/urandom")
+
+# ============ Core PRNG: xorshift64 ============
+
+# Mask to 64 bits. Goth integers are i128; xorshift64 assumes
+# 64-bit state, so we mask after each transition.
+let mask64 = 18446744073709551615
+
+# Xorshift64 state transition.
+# Marsaglia (2003) xorshift with shifts 13, 7, 17.
+# Input: current state (I64, 64-bit range)
+# Output: next state (I64, 64-bit range)
+╭─ xorshift64 : I64 → I64
+╰─ let a = bitand (⊻ ₀ (shl ₀ 13)) mask64
+   in let b = ⊻ a (shr a 7)
+   in bitand (⊻ b (shl b 17)) mask64
+
+# ============ Uniform Random Values ============
+
+# Generate a uniform random float in [0, 1).
+# Uses xorshift64 and scales to [0, 1) by dividing by 2^53.
+# Returns ⟨float, nextSeed⟩.
+╭─ randFloat : I64 → ⟨F64, I64⟩
+╰─ let s1 = xorshift64 ₀
+   in let bits = bitand (if s1 < 0 then 0 - s1 else s1) 9007199254740991
+   in ⟨toFloat bits / 9007199254740992.0, s1⟩
+
+# Generate a uniform random float in [lo, hi).
+# ₂ = lo, ₁ = hi, ₀ = seed
+# Returns ⟨float, nextSeed⟩.
+╭─ randFloatRange : F64 → F64 → I64 → ⟨F64, I64⟩
+╰─ let ⟨u, s1⟩ = randFloat ₀
+   in ⟨₄ + u × (₃ - ₄), s1⟩
+
+# Generate a uniform random integer in [lo, hi] (inclusive).
+# ₂ = lo, ₁ = hi, ₀ = seed
+# Returns ⟨int, nextSeed⟩.
+╭─ randInt : I64 → I64 → I64 → ⟨I64, I64⟩
+╰─ let s1 = xorshift64 ₀
+   in let range = ₂ - ₃ + 1
+   in let val = ₄ + (if s1 < 0 then 0 - s1 else s1) % range
+   in ⟨val, s1⟩
+
+# Generate a random boolean with probability p of being true.
+# ₁ = probability (0.0 to 1.0), ₀ = seed
+# Returns ⟨bool, nextSeed⟩.
+╭─ randBool : F64 → I64 → ⟨Bool, I64⟩
+╰─ let ⟨u, s1⟩ = randFloat ₀
+   in ⟨u < ₃, s1⟩
+
+# ============ Normal Distribution (Box-Muller) ============
+
+# Generate a standard normal random value (mean=0, stddev=1).
+# Uses Box-Muller transform: z = √(-2 ln u1) × cos(2π u2)
+# Returns ⟨float, nextSeed⟩.
+╭─ randNormal : I64 → ⟨F64, I64⟩
+╰─ let ⟨u1, s1⟩ = randFloat ₀
+   in let ⟨u2, s2⟩ = randFloat s1
+   in let u1safe = if u1 < 0.000001 then 0.000001 else u1
+   in let z = √(0.0 - 2.0 × ln u1safe) × cos (2.0 × 3.14159265358979323846 × u2)
+   in ⟨z, s2⟩
+
+# Generate a normal random value with given mean and stddev.
+# ₂ = mean, ₁ = stddev, ₀ = seed
+# Returns ⟨float, nextSeed⟩.
+╭─ randGaussian : F64 → F64 → I64 → ⟨F64, I64⟩
+╰─ let ⟨z, s1⟩ = randNormal ₀
+   in ⟨₄ + ₃ × z, s1⟩
+
+# ============ Bulk Generation ============
+
+# Generate n uniform random floats in [0, 1).
+# ₁ = count, ₀ = seed
+# Returns ⟨[n]F64, nextSeed⟩.
+╭─ randFloats : I64 → I64 → ⟨[n]F64, I64⟩
+╰─ ⌿ (λ→ λ→ let ⟨v, s⟩ = randFloat (₁.1)
+             in ⟨₃.0 ⊕ [v], s⟩)
+     ⟨[], ₀⟩
+     (ι ₁)
+
+# Generate n uniform random integers in [lo, hi].
+# ₃ = lo, ₂ = hi, ₁ = count, ₀ = seed
+# Returns ⟨[n]I64, nextSeed⟩.
+╭─ randInts : I64 → I64 → I64 → I64 → ⟨[n]I64, I64⟩
+╰─ ⌿ (λ→ λ→ let ⟨v, s⟩ = randInt ₅ ₄ (₁.1)
+             in ⟨₃.0 ⊕ [v], s⟩)
+     ⟨[], ₀⟩
+     (ι ₁)
+
+# Generate n standard normal random values.
+# ₁ = count, ₀ = seed
+# Returns ⟨[n]F64, nextSeed⟩.
+╭─ randNormals : I64 → I64 → ⟨[n]F64, I64⟩
+╰─ ⌿ (λ→ λ→ let ⟨v, s⟩ = randNormal (₁.1)
+             in ⟨₃.0 ⊕ [v], s⟩)
+     ⟨[], ₀⟩
+     (ι ₁)
diff --git a/stdlib/result.goth b/stdlib/result.goth
index 74d03ec..c9ccc2b 100644
--- a/stdlib/result.goth
+++ b/stdlib/result.goth
@@ -5,378 +5,239 @@
 #   - ⟨⊤, value, _⟩ represents Ok(value)
 #   - ⟨⊥, _, error⟩ represents Err(error)
 #
-# The first element is the "isOk" flag:
-#   - .0 = ⊤ means success, .1 contains the value
-#   - .0 = ⊥ means failure, .2 contains the error
+# The first element (.0) is the "isOk" tag:
+#   ⊤ → success, .1 holds the value
+#   ⊥ → failure, .2 holds the error
 #
-# Convention: Functions use suffixes to indicate types:
-#   - II = Result with integer value, integer error
-#   - IF = Result with integer value, float error
-#   - IS = Result with integer value, string error
-#   - FI, FF, FS = float value variants
-#   - SI, SF, SS = string value variants
-
-# ============ Type Aliases (Documentation) ============
-# ResultII = ⟨Bool, ℤ, ℤ⟩      -- Result with int value, int error
-# ResultIS = ⟨Bool, ℤ, String⟩ -- Result with int value, string error
-# ResultFF = ⟨Bool, F, F⟩      -- Result with float value, float error
-# ResultFS = ⟨Bool, F, String⟩ -- Result with float value, string error
+# Unused slots hold 0 as a dead placeholder (never read by correct code).
+# All functions are generic — the evaluator is type-erased at runtime.
 
 # ============ Constructors ============
 
-# Create Ok result (integer value, integer error type)
-╭─ okII : ℤ → ⟨Bool, ℤ, ℤ⟩
+# Wrap a success value
+╭─ ok : α → ⟨Bool, α, β⟩
 ╰─ ⟨⊤, ₀, 0⟩
 
-# Create Err result (integer value type, integer error)
-╭─ errII : ℤ → ⟨Bool, ℤ, ℤ⟩
+# Wrap an error value
+╭─ err : β → ⟨Bool, α, β⟩
 ╰─ ⟨⊥, 0, ₀⟩
 
-# Create Ok result (integer value, string error type)
-╭─ okIS : ℤ → ⟨Bool, ℤ, String⟩
-╰─ ⟨⊤, ₀, ""⟩
-
-# Create Err result (integer value type, string error)
-╭─ errIS : String → ⟨Bool, ℤ, String⟩
-╰─ ⟨⊥, 0, ₀⟩
-
-# Create Ok result (float value, float error type)
-╭─ okFF : F → ⟨Bool, F, F⟩
-╰─ ⟨⊤, ₀, 0.0⟩
-
-# Create Err result (float value type, float error)
-╭─ errFF : F → ⟨Bool, F, F⟩
-╰─ ⟨⊥, 0.0, ₀⟩
-
-# Create Ok result (float value, string error type)
-╭─ okFS : F → ⟨Bool, F, String⟩
-╰─ ⟨⊤, ₀, ""⟩
-
-# Create Err result (float value type, string error)
-╭─ errFS : String → ⟨Bool, F, String⟩
-╰─ ⟨⊥, 0.0, ₀⟩
-
 # ============ Predicates ============
 
-# Check if result is Ok (generic)
+# Check if result is Ok
 ╭─ isOk : ⟨Bool, α, β⟩ → Bool
 ╰─ ₀.0
 
-# Check if result is Err (generic)
+# Check if result is Err
 ╭─ isErr : ⟨Bool, α, β⟩ → Bool
 ╰─ ¬(₀.0)
 
-# Type-specific versions
-╭─ isOkII : ⟨Bool, ℤ, ℤ⟩ → Bool
-╰─ ₀.0
-
-╭─ isErrII : ⟨Bool, ℤ, ℤ⟩ → Bool
-╰─ ¬(₀.0)
-
-╭─ isOkIS : ⟨Bool, ℤ, String⟩ → Bool
-╰─ ₀.0
-
-╭─ isErrIS : ⟨Bool, ℤ, String⟩ → Bool
-╰─ ¬(₀.0)
-
-╭─ isOkFF : ⟨Bool, F, F⟩ → Bool
-╰─ ₀.0
-
-╭─ isErrFF : ⟨Bool, F, F⟩ → Bool
-╰─ ¬(₀.0)
-
-╭─ isOkFS : ⟨Bool, F, String⟩ → Bool
-╰─ ₀.0
-
-╭─ isErrFS : ⟨Bool, F, String⟩ → Bool
-╰─ ¬(₀.0)
-
 # ============ Extractors ============
 
-# Get Ok value or default (integer/integer)
-╭─ unwrapOrII : ℤ → ⟨Bool, ℤ, ℤ⟩ → ℤ
+# Get Ok value or return default
+╭─ unwrapOr : α → ⟨Bool, α, β⟩ → α
 ╰─ if ₀.0 then ₀.1 else ₁
 
-# Get Ok value or default (integer/string)
-╭─ unwrapOrIS : ℤ → ⟨Bool, ℤ, String⟩ → ℤ
-╰─ if ₀.0 then ₀.1 else ₁
-
-# Get Ok value or default (float/float)
-╭─ unwrapOrFF : F → ⟨Bool, F, F⟩ → F
-╰─ if ₀.0 then ₀.1 else ₁
-
-# Get Ok value or default (float/string)
-╭─ unwrapOrFS : F → ⟨Bool, F, String⟩ → F
-╰─ if ₀.0 then ₀.1 else ₁
-
-# Get Err value or default (integer/integer)
-╭─ unwrapErrOrII : ℤ → ⟨Bool, ℤ, ℤ⟩ → ℤ
+# Get Err value or return default
+╭─ unwrapErrOr : β → ⟨Bool, α, β⟩ → β
 ╰─ if ₀.0 then ₁ else ₀.2
 
-# Get Err value or default (integer/string)
-╭─ unwrapErrOrIS : String → ⟨Bool, ℤ, String⟩ → String
-╰─ if ₀.0 then ₁ else ₀.2
-
-# Unsafe get Ok value (assumes Ok)
-╭─ unsafeUnwrapII : ⟨Bool, ℤ, ℤ⟩ → ℤ
-╰─ ₀.1
-
-╭─ unsafeUnwrapFF : ⟨Bool, F, F⟩ → F
+# Get Ok value (unsafe — assumes Ok)
+╭─ unsafeUnwrap : ⟨Bool, α, β⟩ → α
 ╰─ ₀.1
 
-# Unsafe get Err value (assumes Err)
-╭─ unsafeUnwrapErrII : ⟨Bool, ℤ, ℤ⟩ → ℤ
+# Get Err value (unsafe — assumes Err)
+╭─ unsafeUnwrapErr : ⟨Bool, α, β⟩ → β
 ╰─ ₀.2
 
-╭─ unsafeUnwrapErrIS : ⟨Bool, ℤ, String⟩ → String
-╰─ ₀.2
-
-# Get Ok value or compute default
-╭─ unwrapOrComputeII : (⟨⟩ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ℤ
+# Get Ok value or compute default lazily
+╭─ unwrapOrCompute : (⟨⟩ → α) → ⟨Bool, α, β⟩ → α
 ╰─ if ₀.0 then ₀.1 else ₁ ⟨⟩
 
-# Get Ok value or compute from error
-╭─ unwrapOrElseII : (ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ℤ
-╰─ if ₀.0 then ₀.1 else ₁ ₀.2
-
-╭─ unwrapOrElseIS : (String → ℤ) → ⟨Bool, ℤ, String⟩ → ℤ
+# Get Ok value or compute from the error
+╭─ unwrapOrElse : (β → α) → ⟨Bool, α, β⟩ → α
 ╰─ if ₀.0 then ₀.1 else ₁ ₀.2
 
 # ============ Transformations ============
 
-# Map function over Ok value (integer/integer → integer/integer)
-╭─ mapResII : (ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 then ⟨⊤, ₁ ₀.1, 0⟩ else ₀
-
-# Map function over Ok value (float/string → float/string)
-╭─ mapResFS : (F → F) → ⟨Bool, F, String⟩ → ⟨Bool, F, String⟩
-╰─ if ₀.0 then ⟨⊤, ₁ ₀.1, ""⟩ else ₀
-
-# Map function over Err value (integer/integer)
-╭─ mapErrII : (ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 then ₀ else ⟨⊥, 0, ₁ ₀.2⟩
+# Map function over Ok value
+╭─ mapRes : (α → γ) → ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩
+╰─ if ₀.0 then ⟨⊤, ₁ ₀.1, 0⟩ else ⟨⊥, 0, ₀.2⟩
 
-# Map function over Err value (integer/string)
-╭─ mapErrIS : (String → String) → ⟨Bool, ℤ, String⟩ → ⟨Bool, ℤ, String⟩
-╰─ if ₀.0 then ₀ else ⟨⊥, 0, ₁ ₀.2⟩
+# Map function over Err value
+╭─ mapErr : (β → γ) → ⟨Bool, α, β⟩ → ⟨Bool, α, γ⟩
+╰─ if ₀.0 then ⟨⊤, ₀.1, 0⟩ else ⟨⊥, 0, ₁ ₀.2⟩
 
-# Bimap: map over both Ok and Err
-╭─ bimapII : (ℤ → ℤ) → (ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Map over both Ok and Err
+╭─ bimapRes : (α → γ) → (β → δ) → ⟨Bool, α, β⟩ → ⟨Bool, γ, δ⟩
 ╰─ if ₀.0 then ⟨⊤, ₂ ₀.1, 0⟩ else ⟨⊥, 0, ₁ ₀.2⟩
 
-# FlatMap / bind (integer/integer)
-╭─ flatMapResII : (ℤ → ⟨Bool, ℤ, ℤ⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 then ₁ ₀.1 else ₀
+# FlatMap / monadic bind on Ok
+╭─ flatMapRes : (α → ⟨Bool, γ, β⟩) → ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩
+╰─ if ₀.0 then ₁ ₀.1 else ⟨⊥, 0, ₀.2⟩
 
-# FlatMap / bind (float/string)
-╭─ flatMapResFS : (F → ⟨Bool, F, String⟩) → ⟨Bool, F, String⟩ → ⟨Bool, F, String⟩
-╰─ if ₀.0 then ₁ ₀.1 else ₀
-
-# FlatMap over error
-╭─ flatMapErrII : (ℤ → ⟨Bool, ℤ, ℤ⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 then ₀ else ₁ ₀.2
+# FlatMap on Err
+╭─ flatMapErr : (β → ⟨Bool, α, γ⟩) → ⟨Bool, α, β⟩ → ⟨Bool, α, γ⟩
+╰─ if ₀.0 then ⟨⊤, ₀.1, 0⟩ else ₁ ₀.2
 
 # ============ Combining Results ============
 
-# Or else: return first if Ok, else second (integer/integer)
-╭─ orElseResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Return first if Ok, else second
+╭─ orElseRes : ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩
 ╰─ if ₁.0 then ₁ else ₀
 
 # Or else with function: compute alternative from error
-╭─ orElseWithII : (ℤ → ⟨Bool, ℤ, ℤ⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 then ₀ else ₁ ₀.2
+╭─ orElseWith : (β → ⟨Bool, α, γ⟩) → ⟨Bool, α, β⟩ → ⟨Bool, α, γ⟩
+╰─ if ₀.0 then ⟨⊤, ₀.1, 0⟩ else ₁ ₀.2
 
-# And then: sequence two results (integer/integer)
-╭─ andThenResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₁.0 then ₀ else ₁
+# Return second if first is Ok, else propagate first's error
+╭─ andThenRes : ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩ → ⟨Bool, γ, β⟩
+╰─ if ₁.0 then ₀ else ⟨⊥, 0, ₁.2⟩
 
-# And: combine two results, keep first Ok value
-╭─ andResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₁.0 ∧ ₀.0 then ₁ else if ¬(₁.0) then ₁ else ₀
+# And: both must be Ok, keep first's value
+╭─ andRes : ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩ → ⟨Bool, α, β⟩
+╰─ if ₁.0 ∧ ₀.0 then ₁ else if ¬(₁.0) then ₁ else ⟨⊥, 0, ₀.2⟩
 
-# Zip two results: Ok only if both are Ok
-╭─ zipResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ⟨ℤ, ℤ⟩, ℤ⟩
+# Zip: Ok only if both Ok, combining values into a pair
+╭─ zipRes : ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩ → ⟨Bool, ⟨α, γ⟩, β⟩
 ╰─ if ₁.0 ∧ ₀.0 then ⟨⊤, ⟨₁.1, ₀.1⟩, 0⟩
-   else if ¬(₁.0) then ⟨⊥, ⟨0, 0⟩, ₁.2⟩
-   else ⟨⊥, ⟨0, 0⟩, ₀.2⟩
+   else if ¬(₁.0) then ⟨⊥, 0, ₁.2⟩
+   else ⟨⊥, 0, ₀.2⟩
 
-# Zip with function
-╭─ zipWithResII : (ℤ → ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Zip with combining function
+╭─ zipWithRes : (α → γ → δ) → ⟨Bool, α, β⟩ → ⟨Bool, γ, β⟩ → ⟨Bool, δ, β⟩
 ╰─ if ₁.0 ∧ ₀.0 then ⟨⊤, ₂ ₁.1 ₀.1, 0⟩
    else if ¬(₁.0) then ⟨⊥, 0, ₁.2⟩
    else ⟨⊥, 0, ₀.2⟩
 
-# ============ Conversion ============
+# ============ Folding ============
 
-# Convert Result to Option (discards error)
-╭─ resToOptII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ⟩
-╰─ ⟨₀.0, ₀.1⟩
+# Fold: apply f to Ok value, or g to Err value
+╭─ foldRes : (α → γ) → (β → γ) → ⟨Bool, α, β⟩ → γ
+╰─ if ₀.0 then ₂ ₀.1 else ₁ ₀.2
+
+# ============ Conversion ============
 
-╭─ resToOptFS : ⟨Bool, F, String⟩ → ⟨Bool, F⟩
+# Discard error, convert to Option
+╭─ resToOpt : ⟨Bool, α, β⟩ → ⟨Bool, α⟩
 ╰─ ⟨₀.0, ₀.1⟩
 
-# Convert Option to Result (with error value for None)
-╭─ optToResII : ℤ → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Convert Option to Result, providing error for None
+╭─ optToRes : β → ⟨Bool, α⟩ → ⟨Bool, α, β⟩
 ╰─ if ₀.0 then ⟨⊤, ₀.1, 0⟩ else ⟨⊥, 0, ₁⟩
 
-╭─ optToResIS : String → ⟨Bool, ℤ⟩ → ⟨Bool, ℤ, String⟩
-╰─ if ₀.0 then ⟨⊤, ₀.1, ""⟩ else ⟨⊥, 0, ₁⟩
-
 # Swap Ok and Err
-╭─ swapResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+╭─ swapRes : ⟨Bool, α, β⟩ → ⟨Bool, β, α⟩
 ╰─ ⟨¬(₀.0), ₀.2, ₀.1⟩
 
 # Convert to list (empty or singleton with Ok value)
-╭─ resToListII : ⟨Bool, ℤ, ℤ⟩ → [n]ℤ
+╭─ resToList : ⟨Bool, α, β⟩ → [n]α
 ╰─ if ₀.0 then [₀.1] else []
 
-# ============ Safe Operations ============
-
-# Safe division (returns Err on divide by zero)
-╭─ safeDivResII : ℤ → ℤ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀ = 0 then ⟨⊥, 0, -1⟩ else ⟨⊤, ₁ / ₀, 0⟩
-
-╭─ safeDivResIS : ℤ → ℤ → ⟨Bool, ℤ, String⟩
-╰─ if ₀ = 0 then ⟨⊥, 0, "division by zero"⟩ else ⟨⊤, ₁ / ₀, ""⟩
-
-╭─ safeDivResFS : F → F → ⟨Bool, F, String⟩
-╰─ if ₀ = 0.0 then ⟨⊥, 0.0, "division by zero"⟩ else ⟨⊤, ₁ / ₀, ""⟩
-
-# Safe modulo
-╭─ safeModResIS : ℤ → ℤ → ⟨Bool, ℤ, String⟩
-╰─ if ₀ = 0 then ⟨⊥, 0, "modulo by zero"⟩ else ⟨⊤, ₁ % ₀, ""⟩
-
-# Safe square root
-╭─ safeSqrtResFS : F → ⟨Bool, F, String⟩
-╰─ if ₀ < 0.0 then ⟨⊥, 0.0, "sqrt of negative"⟩ else ⟨⊤, √₀, ""⟩
-
-# Safe log
-╭─ safeLogResFS : F → ⟨Bool, F, String⟩
-╰─ if ₀ ≤ 0.0 then ⟨⊥, 0.0, "log of non-positive"⟩ else ⟨⊤, ln ₀, ""⟩
-
-# Safe array index
-╭─ safeIndexResIS : ℤ → [n]ℤ → ⟨Bool, ℤ, String⟩
-╰─ if ₁ < 0 then ⟨⊥, 0, "negative index"⟩
-   else if ₁ ≥ len ₀ then ⟨⊥, 0, "index out of bounds"⟩
-   else ⟨⊤, ₀[₁], ""⟩
-
-╭─ safeIndexResFS : ℤ → [n]F → ⟨Bool, F, String⟩
-╰─ if ₁ < 0 then ⟨⊥, 0.0, "negative index"⟩
-   else if ₁ ≥ len ₀ then ⟨⊥, 0.0, "index out of bounds"⟩
-   else ⟨⊤, ₀[₁], ""⟩
-
-# ============ Folding ============
-
-# Fold result (integer/integer)
-╭─ foldResII : (ℤ → γ) → (ℤ → γ) → ⟨Bool, ℤ, ℤ⟩ → γ
-╰─ if ₀.0 then ₂ ₀.1 else ₁ ₀.2
-
-# Fold result (integer/string)
-╭─ foldResIS : (ℤ → γ) → (String → γ) → ⟨Bool, ℤ, String⟩ → γ
-╰─ if ₀.0 then ₂ ₀.1 else ₁ ₀.2
-
 # ============ Boolean Checks ============
 
 # Check if Ok contains specific value
-╭─ containsResII : ℤ → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ containsRes : α → ⟨Bool, α, β⟩ → Bool
 ╰─ ₀.0 ∧ ₀.1 = ₁
 
 # Check if Err contains specific error
-╭─ containsErrII : ℤ → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ containsErr : β → ⟨Bool, α, β⟩ → Bool
 ╰─ ¬(₀.0) ∧ ₀.2 = ₁
 
-╭─ containsErrIS : String → ⟨Bool, ℤ, String⟩ → Bool
-╰─ ¬(₀.0) ∧ strEq ₀.2 ₁
-
 # Check if Ok value satisfies predicate
-╭─ existsResII : (ℤ → Bool) → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ existsRes : (α → Bool) → ⟨Bool, α, β⟩ → Bool
 ╰─ ₀.0 ∧ ₁ ₀.1
 
 # Check if Err value satisfies predicate
-╭─ existsErrII : (ℤ → Bool) → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ existsErr : (β → Bool) → ⟨Bool, α, β⟩ → Bool
 ╰─ ¬(₀.0) ∧ ₁ ₀.2
 
 # Check if Err or Ok value satisfies predicate
-╭─ forallResII : (ℤ → Bool) → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ forallRes : (α → Bool) → ⟨Bool, α, β⟩ → Bool
 ╰─ ¬(₀.0) ∨ ₁ ₀.1
 
 # ============ Comparison ============
 
 # Compare two results
-╭─ eqResII : ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩ → Bool
+╭─ eqRes : ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩ → Bool
 ╰─ if ₁.0 ∧ ₀.0 then ₁.1 = ₀.1
    else if ¬(₁.0) ∧ ¬(₀.0) then ₁.2 = ₀.2
    else ⊥
 
-╭─ eqResIS : ⟨Bool, ℤ, String⟩ → ⟨Bool, ℤ, String⟩ → Bool
-╰─ if ₁.0 ∧ ₀.0 then ₁.1 = ₀.1
-   else if ¬(₁.0) ∧ ¬(₀.0) then strEq ₁.2 ₀.2
-   else ⊥
+# ============ Side Effects ============
 
-# ============ Iteration ============
-
-# Apply function if Ok (for side effects)
-╭─ forEachResII : (ℤ → ⟨⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨⟩
+# Apply function if Ok
+╭─ forEachRes : (α → ⟨⟩) → ⟨Bool, α, β⟩ → ⟨⟩
 ╰─ if ₀.0 then ₁ ₀.1 else ⟨⟩
 
-# Apply function if Err (for side effects)
-╭─ forEachErrII : (ℤ → ⟨⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨⟩
+# Apply function if Err
+╭─ forEachErr : (β → ⟨⟩) → ⟨Bool, α, β⟩ → ⟨⟩
 ╰─ if ₀.0 then ⟨⟩ else ₁ ₀.2
 
-# Tap: apply function for side effect, return original
-╭─ tapResII : (ℤ → ⟨⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Tap: side-effect on Ok value, return original
+╭─ tapRes : (α → ⟨⟩) → ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩
 ╰─ if ₀.0 then let _ = ₁ ₀.1 in ₀ else ₀
 
-# ============ Creating Results from Conditions ============
+# ============ Safe Operations ============
 
-# Create Ok if condition is true, else Err
-╭─ okIfII : Bool → ℤ → ℤ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₂ then ⟨⊤, ₁, 0⟩ else ⟨⊥, 0, ₀⟩
+# Safe division (Err with message on divide by zero)
+╭─ safeDivRes : α → α → ⟨Bool, α, String⟩
+╰─ if ₀ = 0 then ⟨⊥, 0, "division by zero"⟩ else ⟨⊤, ₁ / ₀, ""⟩
 
-╭─ okIfIS : Bool → ℤ → String → ⟨Bool, ℤ, String⟩
-╰─ if ₂ then ⟨⊤, ₁, ""⟩ else ⟨⊥, 0, ₀⟩
+# Safe modulo
+╭─ safeModRes : ℤ → ℤ → ⟨Bool, ℤ, String⟩
+╰─ if ₀ = 0 then ⟨⊥, 0, "modulo by zero"⟩ else ⟨⊤, ₁ % ₀, ""⟩
 
-# Create Ok if predicate passes
-╭─ filterToResII : (ℤ → Bool) → ℤ → ℤ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₂ ₁ then ⟨⊤, ₁, 0⟩ else ⟨⊥, 0, ₀⟩
+# Safe square root
+╭─ safeSqrtRes : F → ⟨Bool, F, String⟩
+╰─ if ₀ < 0.0 then ⟨⊥, 0, "sqrt of negative"⟩ else ⟨⊤, √₀, ""⟩
 
-╭─ filterToResIS : (ℤ → Bool) → ℤ → String → ⟨Bool, ℤ, String⟩
-╰─ if ₂ ₁ then ⟨⊤, ₁, ""⟩ else ⟨⊥, 0, ₀⟩
+# Safe log
+╭─ safeLogRes : F → ⟨Bool, F, String⟩
+╰─ if ₀ ≤ 0.0 then ⟨⊥, 0, "log of non-positive"⟩ else ⟨⊤, ln ₀, ""⟩
 
-# Ensure value satisfies predicate
-╭─ ensureII : (ℤ → Bool) → ℤ → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
-╰─ if ₀.0 ∧ ₂ ₀.1 then ₀ else ⟨⊥, 0, ₁⟩
+# Safe array index
+╭─ safeIndexRes : ℤ → [n]α → ⟨Bool, α, String⟩
+╰─ if ₁ < 0 then ⟨⊥, 0, "negative index"⟩
+   else if ₁ ≥ len ₀ then ⟨⊥, 0, "index out of bounds"⟩
+   else ⟨⊤, ₀[₁], ""⟩
 
-# ============ String Representation ============
+# ============ Creating Results from Conditions ============
 
-# Convert result to string for display
-╭─ showResII : ⟨Bool, ℤ, ℤ⟩ → String
-╰─ if ₀.0 then strConcat "Ok(" (strConcat (toString ₀.1) ")")
-   else strConcat "Err(" (strConcat (toString ₀.2) ")")
+# Ok if condition true, else Err
+╭─ okIf : Bool → α → β → ⟨Bool, α, β⟩
+╰─ if ₂ then ⟨⊤, ₁, 0⟩ else ⟨⊥, 0, ₀⟩
 
-╭─ showResIS : ⟨Bool, ℤ, String⟩ → String
-╰─ if ₀.0 then strConcat "Ok(" (strConcat (toString ₀.1) ")")
-   else strConcat "Err(" (strConcat ₀.2 ")")
+# Ok if predicate passes on value, else Err
+╭─ filterToRes : (α → Bool) → α → β → ⟨Bool, α, β⟩
+╰─ if ₂ ₁ then ⟨⊤, ₁, 0⟩ else ⟨⊥, 0, ₀⟩
 
-╭─ showResFS : ⟨Bool, F, String⟩ → String
-╰─ if ₀.0 then strConcat "Ok(" (strConcat (toString ₀.1) ")")
-   else strConcat "Err(" (strConcat ₀.2 ")")
+# Ensure Ok value satisfies predicate, else replace with Err
+╭─ ensure : (α → Bool) → β → ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩
+╰─ if ₀.0 ∧ ₂ ₀.1 then ₀ else ⟨⊥, 0, ₁⟩
 
 # ============ Error Handling Patterns ============
 
-# Try: run function, catch errors with handler
-╭─ tryII : (ℤ → ⟨Bool, ℤ, ℤ⟩) → (ℤ → ℤ) → ℤ → ℤ
+# Try: run function, recover from error with handler
+╭─ try : (α → ⟨Bool, β, γ⟩) → (γ → β) → α → β
 ╰─ let res = ₂ ₀
    in if res.0 then res.1 else ₁ res.2
 
-# Catch: recover from error with default
-╭─ catchII : ⟨Bool, ℤ, ℤ⟩ → ℤ → ℤ
+# Catch: unwrap Ok or return default on Err
+╭─ catch : ⟨Bool, α, β⟩ → α → α
 ╰─ if ₁.0 then ₁.1 else ₀
 
-# Recover: transform error to Ok
-╭─ recoverII : (ℤ → ℤ) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Recover: transform Err into Ok
+╭─ recover : (β → α) → ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩
 ╰─ if ₀.0 then ₀ else ⟨⊤, ₁ ₀.2, 0⟩
 
-# Inspect error without changing result
-╭─ inspectErrII : (ℤ → ⟨⟩) → ⟨Bool, ℤ, ℤ⟩ → ⟨Bool, ℤ, ℤ⟩
+# Inspect error for side effect without changing the result
+╭─ inspectErr : (β → ⟨⟩) → ⟨Bool, α, β⟩ → ⟨Bool, α, β⟩
 ╰─ if ₀.0 then ₀ else let _ = ₁ ₀.2 in ₀
+
+# ============ String Representation ============
+
+# Convert result to display string
+╭─ showRes : ⟨Bool, α, β⟩ → String
+╰─ if ₀.0 then "Ok(" ⧺ toString ₀.1 ⧺ ")"
+   else "Err(" ⧺ toString ₀.2 ⧺ ")"