Hoas

Higher-Order Abstract Syntax layer that lets you write kernel terms using Nix lambdas for variable binding. The elaborate function compiles HOAS trees to de Bruijn indexed Tm terms.

Spec reference: kernel-spec.md §2.

Example

# Π(A:U₀). A → A
H.forall "A" (H.u 0) (A: H.forall "x" A (_: A))

Type Combinators

• nat, bool, unit, void — base types
• string, int_, float_, attrs, path, function_, any — primitive types
• listOf : Hoas → Hoas — List(elem)
• sum : Hoas → Hoas → Hoas — Sum(left, right)
• eq : Hoas → Hoas → Hoas → Hoas — Eq(type, lhs, rhs)
• u : Int → Hoas — Universe at level
• forall : String → Hoas → (Hoas → Hoas) → Hoas — Π-type (Nix lambda for body)
• sigma : String → Hoas → (Hoas → Hoas) → Hoas — Σ-type

Compound Types (Sugar)

• record : [{ name; type; }] → Hoas — nested Sigma (sorted fields)
• maybe : Hoas → Hoas — Sum(inner, Unit)
• variant : [{ tag; type; }] → Hoas — nested Sum (sorted tags)

Term Combinators

• lam : String → Hoas → (Hoas → Hoas) → Hoas — λ-abstraction
• let_ : String → Hoas → Hoas → (Hoas → Hoas) → Hoas — let binding
• zero, succ, true_, false_, tt, refl — intro forms
• nil, cons, pair, inl, inr — data constructors
• stringLit, intLit, floatLit, attrsLit, pathLit, fnLit, anyLit — primitive literals
• absurd, ann, app, fst_, snd_ — elimination/annotation

Eliminators

• ind — NatElim(motive, base, step, scrut)
• boolElim — BoolElim(motive, onTrue, onFalse, scrut)
• listElim — ListElim(elem, motive, onNil, onCons, scrut)
• sumElim — SumElim(left, right, motive, onLeft, onRight, scrut)
• j — J(type, lhs, motive, base, rhs, eq)

Elaboration

• elaborate : Int → Hoas → Tm — compile at given depth
• elab : Hoas → Tm — compile from depth 0

Convenience

• checkHoas : Hoas → Hoas → Tm|Error — elaborate type+term, type-check
• inferHoas : Hoas → { term; type; }|Error — elaborate and infer
• natLit : Int → Hoas — build S^n(zero)

Stack Safety

Binding chains (pi/lam/sigma/let), succ chains, and cons chains are elaborated iteratively via genericClosure — safe to 8000+ depth.