ADR-0002: Binding-Time Judgment
Status: accepted
Date: 2026-07-25
Context
P1 needs a sound distinction between information known to the specializer and dynamic residual input. Treating specialization as an unchecked optimizer hint would permit static computations to depend on dynamic data or perform hidden effects.
Options considered
| Option | Benefit | Cost |
|---|---|---|
| Compiler heuristic only | Simple surface | No sound staging contract |
Static<T> as runtime type | Explicit | Pollutes runtime type identity |
| Checked staging judgment | Formal and erasable | Adds a second analysis judgment |
Decision
Use:
Γs ; Γd ⊢ expression : T @ b ! effects
b ::= Static | Dynamic
Static ≤ Dynamicjoin is an operation, not a binding-time constructor. static and dynamic
annotations constrain inference. Specialization budgets and version policy are
compiler policy and do not change runtime semantics.
Static evaluation is pure by default and cannot depend on dynamic input.
Rationale
- The two-point lattice is sufficient for the first projection.
- Ordinary type equality stays independent of staging.
- The verifier can reject unsound or forged binding-time evidence.
- Partially static domains can be added later without destabilizing P1.
Trade-offs
- Static shape/type/tag knowledge is initially represented internally rather than as a rich public lattice.
- Some useful compile-time operations must residualize until capabilities are designed.
Consequences
IO, FFI, clocks, randomness, environment variables, and external state do not run during reproducible default specialization.
Revisit trigger
Add richer partially static domains only after P1 evidence shows repeated residual overhead that the two-point lattice cannot remove safely.