Typed Metaprogramming and Hygienic Elaboration

Definition 116.1 — Scoped identifiers and occurrence identity¶

Fix disjoint countable sets of atoms, raw binder tokens $\beta$, raw reference tokens $\omega$, expanded origin tokens $o$, and scope stamps. Every raw syntax tree uses each binder token at most once. This global uniqueness condition is part of raw well-formedness, even when two binders lie in disjoint subtrees or at different staging levels. A raw binder is written $a^{\beta }$. Every raw reference is written $a_{\beta }^{\omega }$: its stable token is $\omega$, and its lexical target is the particular binder token $\beta$, not the printed atom $a$. Thus in $\lambda a^{{\beta }_0}.\lambda a^{{\beta }_1}.a_{{\beta }_0}^{\omega }$, the reference still targets ${\beta }_0$ despite the intervening binder named $a$.

An expanded binding is a triple $(a,S_b,o)$, where $S_b$ is a finite scope set. An origin environment $\mathrm{\Xi }$ is a finite partial map $o\mapsto (a,S_b)$. Its entry is a candidate for a scoped reference $a^{S_r}$ when $S_b\subseteq S_r$. The partial operation ${\mathsf{resolve}}_{\mathrm{\Xi }}(a^{S_r})$ selects the origin of the unique candidate maximal by inclusion. It is undefined when there is no candidate or when two distinct candidates are maximal. Expanded references retain their raw token $\omega$ or carry the marker $\mathsf{new}(o_t)$ naming a declared target origin $o_t$.

Definition 116.2 — Raw and scoped syntax¶

Raw terms are trees with typed binders $$r::=a_{\beta }^{\omega }\mid \lambda (a^{\beta }:A).r\mid rr\mid \mathsf{quote}(r)\mid \mathsf{splice}(r)\mid m(r_1,\dots ,r_k).$$ Scoped terms have the same constructors but every identifier is a scoped identifier and every reference resolves by definition 116.1. A syntax object is a scoped term together with its phase number. Raw syntax has no scoped-binding claim, but it is well formed only when its binder tokens are pairwise distinct and each lexical target $\beta$ on a reference names the unique enclosing binder carrying $\beta$. Scoped syntax records enough data to check the corresponding expanded binding claim. Every source-typing and expansion judgment below ranges only over well-formed raw syntax.

Definition 116.3 — Provenance on scoped syntax¶

A transformer package $P$ partitions its nodes into copies substituted from named input nodes and newly constructed nodes. For an introduction stamp $i$, ${\mathsf{mark}}_i(P)=h$ copies every substituted node byte-for-byte and adds $i$ to every constructed identifier. Every constructed binder $a^S[o;\mathsf{new}(o)]$ has its own origin. Every free constructed reference is marked $\mathsf{new}(o_t)$, where $o_t$ is either such a constructed origin or an origin exported by the transformer-definition environment $D$. The latter records an origin environment ${\mathrm{\Xi }}_D$ for its exports.

The judgment $D;\mathrm{\Xi }⊢h\mathsf{prov}$ is defined by structural recursion on scoped syntax. At a copied source reference $a^S[o;\mathsf{src}(\omega )]$, it requires ${\mathsf{resolve}}_{\mathrm{\Xi }}(a^S)=o$. At a constructed reference $a^S[o;\mathsf{new}(o_t)]$, it requires ${\mathsf{resolve}}_{\mathrm{\Xi }\cup {\mathrm{\Xi }}_D}(a^S)=o=o_t$ and requires $o_t$ to be a constructed origin in scope or an origin exported by $D$. At a transformer-created binder $\lambda (a^S[o;\mathsf{new}(o)]:A).h_0$, it checks $h_0$ under $\mathrm{\Xi },o\mapsto (a,S)$. A binder marked $\mathsf{src}(\beta )$ extends $\mathrm{\Xi }$ by the same clause. Applications check both subterms under $\mathrm{\Xi }$, and quotation and splicing check their subterm under $\mathrm{\Xi }$. Thus the origin environment is extended under every binder that a transformer creates; checking only free references is not the provenance judgment. Finally, the judgment requires every copied node to be unchanged. It fails on an unresolved, ambiguous, or mismatched reference, and it rejects duplicate binder origins.

Definition 116.4 — Hygienic expansion with provenance¶

The scoped expansion environment $\overline{E}$ is a finite stack of records $\beta \mapsto (a,S_b,o)$. Lookup is by binder token, so shadowing an atom does not overwrite an older record. Its origin projection is ${\pi }_o(\overline{E})(\beta )=o$, and its origin environment is $\mathrm{\Xi }(\overline{E})(o)=(a,S_b)$. These two projections are not source typing environments. Let $L$ be the lexical scopes on the node being expanded and let $U$ be the finite set of stamps already used. Write $\mathrm{Scopes}(D,\overline{E},r)$ for the finite set of stamps occurring in $D$, $\overline{E}$, and $r$. An expansion judgment is well formed only when $\mathrm{Scopes}(D,\overline{E},r)\subseteq U$; the vector form uses the union of the component scope sets. The judgment $$D;\overline{E};n;L;U⊢r⟼h▹U^{\prime }$$ is the least relation generated by the following rules. Argument vectors are expanded left to right by the two rules

Single terms are generated by the following six rules.

Here $C(P)$ is the finite set of origins on constructed binders. The two fresh choices therefore name the finite sets they avoid: $i$ avoids the threaded stamp set $U_k$, and every member of $C(P)$ avoids $F_P$. The transformer table stores an arity and an executable partial meta-function, not a trusted typing theorem. If it diverges or produces a package that fails $\mathsf{prov}$, then Exp-Macro has no derivation.

Definition 116.6 — Staged typing¶

A staged context contains declarations $x:A@n$. The judgment $\mathrm{\Gamma }{⊢}_{n}e:A$ means that $e$ is available at phase $n$. In addition to the ordinary typed lambda-calculus rules at a fixed phase, the calculus has

There is no rule that uses $x:A@n$ directly at phase $n+1$.

Definition 116.7 — Source typing¶

A source context $\mathrm{\Gamma }$ maps source origins to declarations $A@n$, and the source environment $E_0$ maps binder tokens to source origins. In particular, $E_0$ is not the scoped stack $\overline{E}$ and is not the expanded-origin projection ${\pi }_o(\overline{E})$. A macro signature $M$ records only an intended arity and source type $M(m)=(A_1,\dots ,A_k;A;n)$; it is not evidence that the executable transformer respects that type. Write $E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}r:A$. The ordinary variable, lambda, application, quotation, splice, and macro rules are

The first premise of Src-Macro checks a source call against its declared interface. It deliberately says nothing about the transformer output; that output is checked independently after expansion.

Definition 116.9 — Source–scoped compatibility¶

Let $\hat{\mathrm{\Gamma }}$ map expanded origins to declarations. The judgment $${\mathsf{Compat}}_{\rho }(E_0;\mathrm{\Gamma };\overline{E};\hat{\mathrm{\Gamma }})$$ holds when $\rho :\mathrm{dom}\mathrm{\Gamma }\to \mathrm{dom}\hat{\mathrm{\Gamma }}$ is a bijection satisfying both of the following clauses:

1. $\mathrm{dom}{E}_0=\mathrm{dom}\overline{E}$, $\mathrm{dom}\mathrm{\Gamma }=\mathrm{ran}{E}_0$, and $\mathrm{dom}\hat{\mathrm{\Gamma }}=\mathrm{dom}\mathrm{\Xi }(\overline{E})$. If $E_0(\beta )=o_s$ and $\overline{E}(\beta )=(a,S,o_h)$, then $\rho (o_s)=o_h={\pi }_o(\overline{E})(\beta )$;

2. for every $o_s\in \mathrm{dom}\mathrm{\Gamma }$, $\hat{\mathrm{\Gamma }}(\rho (o_s))=\mathrm{\Gamma }(o_s)$.

Thus $\rho$ records an origin renaming, not an equality between source and expanded origins. For vectors, the judgments $E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}\overrightarrow{r}:\overrightarrow{A}$ and $\hat{\mathrm{\Gamma }}{⊢}_n\overrightarrow{h}:\overrightarrow{A}$ mean that the corresponding judgment holds componentwise.

Definition 116.11 — Checked macro expansion¶

A call $m(\overrightarrow{r})$ with $M(m)=(\overrightarrow{A};A;n)$ is accepted relative to $E_0,\mathrm{\Gamma },\overline{E},\hat{\mathrm{\Gamma }}$ only when there is a bijection $\rho$ such that $${\mathsf{Compat}}_{\rho }(E_0;\mathrm{\Gamma };\overline{E};\hat{\mathrm{\Gamma }}),E_0;\mathrm{\Gamma }{⊢}_n^{\mathsf{src}}\overrightarrow{r}:\overrightarrow{A},$$ and expansion derives $$D;\overline{E};n;L;U⊢m(\overrightarrow{r})⟼h▹U^{\prime }.$$ The ordinary staged checker then independently derives $\hat{\mathrm{\Gamma }}{⊢}_{n}h:A$, and the accepted output must satisfy $D;\mathrm{\Xi }(\overline{E})⊢h\mathsf{prov}$. The target judgment is deliberately under $\hat{\mathrm{\Gamma }}$, not the source-origin context $\mathrm{\Gamma }$. Neither the target derivation nor provenance is stored in $D$, and neither is inferred from the macro signature.

Definition 116.12 — Checked command expansion¶

A generated declaration contains a fresh global name $c$, a closed type $A$, and a term $t$. The command expander may propose the declaration only after hygienic expansion and staged checking. The environment is extended by $c:A$ only when the ordinary kernel independently checks $\cdot ⊢t:A$. Name freshness is checked against the finite global signature.