The compilation ladder: source to typed IR

Source text descends a fixed ladder, and each rung hands the next a different artifact. core/src/lib.rs exposes the whole descent as two functions: compile (parse → elaborate) and compile_and_typecheck (parse → elaborate → typecheck → CompileOutcome).

• Text → tokens. The lexer reads characters into tokens with no context-dependent rules — there is one lexer, not the several a POSIX shell needs. (syntax)

• Tokens → flat surface AST. The parser builds a single flat Ast enum. The flatness is deliberate (ast-stays-flat): head classification (^name, ./x, ~/x, bare) happens here, but no desugaring does.

• Surface AST → CBPV IR. The elaborator is the one phase that knows about surface sugar. It enforces the command split by binding effectful sub-expressions to fresh temporaries (a binds accumulator folded into Comp::Bind chains), resolves command heads against lexical scope, and runs group_stmts first to find mutually recursive binding groups, which lower to an n-ary Rec with a projection per member. A statement sequence a; b is itself a binder — a to _. b — so a block is a right-nested chain of Binds and the top level is a list of Phrases (Define / Source / Run). What it emits carries no parser syntax (ir-pure-cbpv). (elaboration)

• IR → typed IR. Hindley–Milner inference annotates the Val / Comp tree (types). The checker is a transformation, annotate. It rebuilds the inferred tree once, carrying a demand at each position. A demand is a value read here, or a value discarded here. The rebuild returns an annotated tree carrying four verdicts.

  • Each top-level name-bind carries the generalised Scheme it inferred, closed against the empty environment so the scheme outlives the per-run unifier (session-scheme-continuity).
  • Each Pipeline carries one PipeYield: the checker grounds the last stage’s route, with every unification variable defaulted away, and writes down the answer — Last to report the helper’s returned value, Unit because a byte payload never crosses the process boundary. The route itself does not survive; every interior edge is a byte pipe allocated from position, so there is nothing per-stage to write (pipes-are-positional-byte-wires).
  • Each Pipeline also carries stage_types, one resolved value type per stage. Only the structural REPL’s typed spine reads a stage type.
  • The rebuild wraps a node in a Capture node wherever a value demand meets a payload route that grounds Bytes (output-capture-and-detachment).

  Generalisation happens at each Bind, along the SCC structure the elaborator already found. A non-recursive group generalises at its own binding point. A mutually recursive group stays monomorphic until its fixed point.

  A value demand reaches:

  • a Bind’s RHS, unless its pattern is a wildcard: a discarded statement is a wildcard binder, so its own value is discarded while the ambient demand flows on into the binder’s rest;
  • each arm of an If, a Case, a fallback chain, or a try;
  • the body of a force of a syntactic thunk.

  Every other position is a discard. A discarded value never wraps in Capture.

  A join needs one further rule for an arm that grounds None at type Unit, inside an otherwise byte-payload join. ArmWalk::Wrap (annotate.rs) wraps that whole arm in Capture. Its own payload then reads as the empty string. Its bytes still reach the outer stream as effect. The arm rebuilds at its own, ordinary discard demand inside the wrap.

  A scope’s arm is a Val, not a Comp. It may be opaque. An opaque arm needing a value payload η-expands through eta_expand_captured (annotate.rs) into { |e| capture (force $h e) }. The expansion is sound because a scope forces its arm exactly once and never returns it. The arm’s own identity is therefore never observed, so nothing can compare, print, or send the wrapper elsewhere.

  Demand propagation stops at a leaf, at an opaque force, and at an opaque scope arm. A case arm is never one of those stops: arms are syntax, so the demand walks into every one of them (case-is-syntax-try-is-not).

  This rung is the only source of Capture nodes, and it runs on every evaluated path: no route reaches the evaluator at all — the checker grounds every route here and leaves its verdict as syntax, never re-derived at runtime. A node inference never visited keeps the elaborator’s placeholder — Unit for a stage type. The verdict rides inside the comp; CompileOutcome is unchanged in shape. (typecheck)

Each run’s check is seeded from the live session — one SessionSchemes, the scope’s name→scheme map plus the alias arms’ schemes — so a binding made in one run enters the next run’s check at its inferred scheme rather than a fresh variable. The evaluator installs each top-level bind’s scheme next to its value, so the seed never drifts from the values it describes.

The prelude is baked once at build time as a schema-less postcard blob of this same IR, so any field added to Comp, Val, or Pattern invalidates every emitted blob — a hazard pinned with cargo:rerun-if-changed in one place, bake_prelude_to_out_dir (core/src/boot.rs), since the only encode site and the only decode site (BakedPrelude) live there together as the host-embedding seam (host-embedding-api). The bake runs the checker: it parses, elaborates, and hands the comp to bake_prelude (core/src/typecheck.rs), which serialises the annotated prelude and harvests its bind schemes from the same pass, so the baked list and a run’s installed schemes come from one harvest. The two blobs — annotated IR and scheme list — land in OUT_DIR; a host embeds them through the baked_prelude! macro into a BakedPrelude, decoded lazily on first use. The typed IR is then handed to the evaluator, which a host reaches only through the synchronous framed run doors (unify-turn-evaluation).

See also cbpv, types; map hub core. The formal account is docs/SPEC.md.