The type checker that can wait

"No" and "not yet" are different answers, and a type checker that files both under the same exception will reject correct programs for arriving in the wrong order. The toy below does exactly that. One queue step supplies f's type and another checks a call to f; run them in one order and you get a core term, swap them and you get an error about a fact that was ten lines from being known.

let fType: Type | undefined;const solveF = () => {  fType = arrow(nat, nat);};const checkCall = () => {  if (!fType) throw new Error("f has no function type yet");  return apply(variable("f"), numeral(3), fType);};run([checkCall, solveF]); // errorrun([solveF, checkCall]); // core application at Nat

What the checker wants is a third outcome. When the context cannot yet decide a required fact, the computation should hold on to the obligation and resume once somebody supplies the missing type — without inventing an answer, and without giving up.

The split matters because only one of the two cases is a real rejection. If f is already known at type Nat, the call is wrong and no amount of rescheduling will save it. An absent type is another thing entirely, since later constraints may pin down exactly the function type the call needs, and a checker that throws on absence is rejecting programs it merely has not finished learning about.

Elaboration fills the missing core#

This scheduling problem is elaboration's daily work. Proof assistants let you write id 3 while the kernel insists on @id Nat 3, and somebody has to find that Nat.

surface: id 3core:    @id Nat 3

Bidirectional typing splits the traffic: some terms synthesize a type outward, others check against a type flowing inward. Application is where the order becomes visible.

The result type may mention the argument just checked. Any step can hit a fact the context does not hold yet, so waiting has to preserve both the obligation and the partial term around it.

Waiting composes#

Bidirectional Elaborators à la Carte specifies elaboration in a dependently typed monadic DSL. The TypeScript sketch below keeps only the operational outline, which is already worth a look.

type Elab<A> =  | { tag: "done"; value: A }  | { tag: "wait"; resume: (context: Context) => Elab<A> }  | { tag: "error"; message: string };function bind<A, B>(  job: Elab<A>,  next: (value: A) => Elab<B>,): Elab<B> {  if (job.tag === "done") return next(job.value);  if (job.tag === "error") return job;  return {    tag: "wait",    resume: context => bind(job.resume(context), next),  };}

Read the wait branch of bind. A suspended job gets wrapped in a new suspension whose resume runs the original job under the richer context and then binds the remainder again — so the entire rest of the computation waits along with its earliest blocked step. Errors still cut through immediately, and finished values flow on as if nothing had happened.

The part my sketch cannot show is why waiting is safe. A suspended computation may be resumed after metavariables have been solved and the context has grown, and the term it produces then has to agree with what the partial computation already committed to. The paper carries that burden with a presheaf model and dependent indexing: the DSL cannot produce an ill-typed core term, and elaboration is stable under substitution and judgmental equality. The TypeScript union is an intuition for the control flow, nothing more.

That guarantee is precisely what a homemade promise pile lacks. Swapping the toy's exception for a callback would postpone the decision, but postponing proves nothing about whether reordered checks still mean the same typed term.

The locked lever stays visible#

The paper abstracts over normal forms and conversion checking and then extracts a concrete elaborator from the algebra, which makes it a foundation rather than a settled production tool. Fine by me — the foundation is the part that usually gets hand-waved.

In the opening queue, checkCall reaches for a locked lever and throws. The suspended version keeps its hand on the lever: the request for f's type rides along inside the result, and when solveF finally supplies Nat → Nat, the same obligation moves and the application receives its Nat. Signal boxes solved this by making wrong-order lever pulls mechanically impossible; the elaborator settles for making the order stop mattering.