rose-ash/plans/idris-on-sx.md

# Idris-on-SX: dependent types as substrate stress test

The single most substrate-stretching language in the set. Dependent types unify the term and type universes — types may depend on values, normalisation becomes part of type-checking, decidable equality matters, totality has to be checked. **Idris 2** is the pragmatic choice: smaller than Agda, more accessible than Coq, designed for general programming rather than proof-only.

**The chisel:** *evidence*. Currently every typed guest in the set (OCaml, Haskell, Elm, Koka, Reasonml) lives in HM-or-rank-1 territory — types are simple-enough algebra. Dependent types force the substrate to think about *terms as evidence*: what does it mean for a value to *witness* a type? what's a normal form? when are two terms equal up to computation?

**What this exposes about the substrate:**
- Whether SX values can carry typing evidence efficiently, or whether a separate elaboration phase is required.
- Whether normalisation (beta, iota, delta) is fast enough at type-check time — implicates JIT, allocation, and frame management.
- Whether decidable equality of arbitrary values is reachable.
- Whether erasure (proofs deleted at runtime) can be expressed cleanly given SX's value model.
- Whether HM (lib/guest/typed/hm.sx) extends cleanly to bidirectional dependent inference, or whether they're genuinely different machinery.

**End-state goal:** **core Idris 2** — Pi types, indexed families, dependent pattern matching, totality checking, erasure, holes for interactive development. Not the full Idris 2 stdlib; a faithful core that runs idiomatic dependent programs.

## Ground rules
- Scope: `lib/idris/**` and `plans/idris-on-sx.md` only. Substrate gaps → `sx-improvements.md`, do not fix from this plan.
- Consumes from `lib/guest/`: `core/lex`, `core/pratt` (Idris has indentation but Pratt for ops), `core/match`, `layout/` (Idris is whitespace-sensitive), `typed/hm.sx` (as a starting point that gets extended).
- **Will propose** a new sub-layer `lib/guest/dependent/` — universes, conversion checking, normalisation, bidirectional elaboration. A second consumer is genuinely speculative for now; accept "second user TBD" until a Lean-fragment or Agda-fragment plan emerges.
- Branch: `loops/idris`. Standard worktree pattern.

## Architecture sketch

```
Idris source text
    │
    ▼
lib/idris/parser.sx        — Haskell-ish, layout-sensitive, type-level syntax
    │                        (consumes lib/guest/layout, lib/guest/pratt)
    ▼
lib/idris/elaborate.sx     — surface → core: implicit args, holes, do-notation
    │
    ▼
lib/idris/check.sx         — bidirectional dependent type-checker
    │                        infer / check modes, conversion via normalisation
    ▼
lib/idris/normalise.sx     — NbE (normalisation by evaluation): values are
    │                        semantic, neutral terms hold reflected applications
    ▼
lib/idris/runtime.sx       — erased terms run via standard SX evaluation;
                             constructors as tagged ADTs from sx-improvements
```

## Semantic mappings

| Idris construct | SX mapping |
|----------------|-----------|
| `(x : Nat) -> P x` | dependent function type — first-class `{:type :pi :name x :domain Nat :codomain (P x)}` |
| `\x => body` | `(fn (x) body)` — same as before |
| `data Vect : Nat -> Type -> Type` | indexed family — `define-type` extension carrying index |
| `Vect (S n) a` | applied type former — neutral term until index is ground |
| `case x of pat => e` | dependent pattern match — refines indices in branches |
| `(x : A) ** B x` | dependent pair — `{:type :sigma :name x :first A :second (B x)}` |
| `?hole` | unfilled term — type-checker reports goal type |
| `Refl : x = x` | propositional equality witness |
| `total` | totality check — termination + coverage |

## Roadmap

### Phase 1 — Parser + layout
- [ ] Lexer/parser via `lib/guest/lex` + `lib/guest/pratt`.
- [ ] Layout via `lib/guest/layout` — Idris uses indentation similar to Haskell.
- [ ] Type signatures `name : Type`, function definitions with multiple clauses.
- [ ] Tests in `lib/idris/tests/parse.sx`.

### Phase 2 — Untyped evaluator (sanity check)
- [ ] Strip types entirely; run programs as untyped lambda calculus + ADTs.
- [ ] Goal: factorial, list ops, recursive datatypes work without type-checking.
- [ ] Confirms the runtime story before tackling the type checker.

### Phase 3 — Bidirectional simply-typed checking + universes
- [ ] Hierarchy of universes `Type 0 : Type 1 : Type 2 : ...`.
- [ ] Check mode (push expected type), infer mode (synthesise type).
- [ ] Variable / lambda / application / annotation rules.
- [ ] Tests: simple programs that succeed/fail type-check.

### Phase 4 — Pi types + dependent functions
- [ ] Pi as a first-class type former.
- [ ] Application instantiates the codomain at the argument value.
- [ ] Conversion check: are two types equal up to normalisation?
- [ ] Implement NbE — values are either canonical (constructors, functions) or neutral (stuck applications); conversion compares via reify.
- [ ] Tests: `id : (a : Type) -> a -> a`, `const`, `flip`.

### Phase 5 — Indexed families + dependent pattern matching
- [ ] `data Vect : Nat -> Type -> Type` — constructors carry index.
- [ ] Pattern match refines indices in branches (`Cons` case has `n = S k`).
- [ ] Coverage check (incomplete matches reported).
- [ ] Tests: `head : Vect (S n) a -> a` (rejects empty vectors at compile time).

### Phase 6 — Totality / termination
- [ ] Termination checker: structural recursion, sized types or call graphs.
- [ ] Productivity for codata.
- [ ] `total` / `partial` annotations.
- [ ] Tests: recursive programs that pass / fail termination.

### Phase 7 — Erasure
- [ ] Mark proof-only arguments as erased.
- [ ] Runtime evaluation skips erased subterms.
- [ ] Tests: vector head runs at the speed of list head (proof argument deleted).

### Phase 8 — Holes + interactive development
- [ ] `?name` produces a hole with reported goal type.
- [ ] Tactic-like elaboration step (small set: `intro`, `apply`, `case-split`).
- [ ] Tests: develop a program by progressive hole-filling.

### Phase 9 — Propose `lib/guest/dependent/`
- [ ] Identify reusable universe machinery, conversion-checking framework, NbE infrastructure.
- [ ] Hold off on extraction until a second consumer (Lean-fragment, Agda-fragment) is plausible.

## lib/guest feedback loop

**Consumes:** `core/lex`, `core/pratt`, `core/match`, `layout/`, `typed/hm.sx` (as starting point).

**Stresses substrate:** value normalisation cost (every type-check step normalises); decidable equality across closures; whether ADT primitive (`define-type` from sx-improvements Phase 3) handles indexed families.

**May propose:** `lib/guest/dependent/` sub-layer — universes, NbE, conversion checking, bidirectional elaboration. Speculative second consumer until Lean/Agda-fragment plans materialise.

**What it teaches:** whether SX's substrate scales to type-level computation. Most languages have a clean separation: types are static, terms are dynamic. Idris collapses them. If SX can host this in <5000 lines, the substrate is genuinely paradigm-agnostic. If it can't, "paradigm-agnostic" was overclaiming.

## References
- Brady, "Type-Driven Development with Idris" (Manning, 2017).
- Idris 2 source: https://github.com/idris-lang/Idris2
- Coquand & Dybjer "An Algorithm for Type-Checking Dependent Types" (NbE foundations).
- Christiansen, "Functional Programming in Lean" (cleanest exposition of bidirectional dependent checking).

## Progress log
_(awaiting completion of Kernel-on-SX or substrate ADT primitive maturity, whichever happens first)_

## Blockers
_(speculative — main risk is substrate normalisation cost)_