Spec 0020 — User-declared annotations: one typed definition, derived on every side

Status: approved and frozen 2026-10-04 (decisions in §0). Implementation follows spec 0015's merge; v1 scope is target: "operation" for user definitions (§0.4). Change this contract by editing this file explicitly. Nothing here supersedes spec 0015 (config + Extension + untyped @Annotate(name, args)), which is being built now; 0020 is the typed layer that 0015's primitives are the untyped floor of (§9). Builds on 0001, 0002, 0005, 0006, 0013 and 0019.

0. Operator decisions (2026-10-04)Copy Anchor Link

1. Tighten the five §1 divergences into one strict definition, as separate commits after the behaviour-preserving re-expression, each with its own fixture updates. 0013's source sugar stays explicit: Http.Contract.group/.success are A.sourceOptional (optional to write, required in Read), query is A.union(A.schema(), A.literal(true)). The strict forms: acceptedCredentials and principalKinds non-empty and unique everywhere (including group defaults); capability/capabilities entries non-empty strings; the runtime type is derived from the compiler schema, never the reverse.
2. Falsifier unchanged: all 18 interpreted built-ins re-expressed via define/implement with identical Collected, IR hash, generated bytes and diagnostics on every fixture (including the vendored mono-web declarations, built read-only through a throwaway config), type-equivalence tests on the 9 option types, and the import-graph gate — before any tightening.
3. Two-call define/implement split accepted.
4. v1 ships target: "operation" only for user definitions. The built-ins that attach to a class, group or model (Http.Group, PersistentModel) use internal targets ("class", "group", "model") that the public define type does not accept; they are reachable only through an internal defineBuiltin. Public "class"/"group"/"model" targets are a later spec.
5. Order: spec 0015 → this spec → spec 0019. 0019's S1 (lifters) is delivered here, as implement({ lift }).

1. Problem: every annotation is written three-to-five timesCopy Anchor Link

An annotation today exists as a runtime half (decorator, builder step, option type), a compiler half (a Schema that re-describes the same options plus an interpreter), and a frontend half (how its arguments lower from TypeScript). Nothing links them; they agree by convention.

Measured on main 5de7921:

Leaf option fields that are declared twice (runtime type and compiler Schema) for the builtins: Query/Command 3, Http.Contract 19, Http.Group 13, Http.Access 9, Http.Problems 4, PersistentModel 4, Foldkit.Command 2, Authorize 3 — 57 leaves, plus one string argument each for Http.Get/Post/Put/Patch/Delete, Rpc, Cli. "Http.Group" alone occurs at 15 sites in 5 files; "Http.Contract" at 9 in 5.

The copies already disagree where they should not (no test connects them):

Some of these are deliberate (source sugar expanded by 0013), but the intent lives nowhere. A user who writes an extension (0015) would multiply the problem: a decorator type, a Schema, a lowering rule that only the compiler owner can add.

Goal: one definition from which the decorator, the builder step, the frontend lowering, the decode, the IR contribution, the Effect writer and the lift recognizer are derived, each typed by the same Schema, with tsc, the Schema decoder and the generated-code typecheck as the three gates.

2. The definitionCopy Anchor Link

2.1 Two halves bound by one valueCopy Anchor Link

@effx/runtime must stay tiny and must never import the compiler (invariant: runtime decorators are no-ops/metadata, ADR 0001), yet application modules import the decorator. So a definition is two calls on one value:

// syntax half — imports only @effx/runtime; safe in application bundles
const RateLimit = Annotation.define({
  name: "app.RateLimit",               // literal type; namespaced; collision = EFFX1302
  target: "operation",                 // v1 public: "operation" only (§0.4); built-ins use internal class/group/model
  args: { perMinute: A.int({ min: 1 }), burst: A.optional(A.int({ min: 1 })) },
  cardinality: "one",                  // framework emits the duplicate diagnostic (code configurable)
  effect: { target: "endpoint", key: RateLimitPolicy },   // optional, §4: default Effect writer + static lift (data only)
})

// compiler half — imports @effx/compiler; never reachable from an application import
const rateLimit = Annotation.implement(RateLimit, {
  read?, analyze?, write?, lift?,     // all optional; each receives types derived from RateLimit
})
// effx.config.ts (spec 0015):  extensions: (b) => [...b, Annotation.extension("app", [rateLimit])]

define holds only data (name, target, args, cardinality, the optional Effect key) so it is a leaf, evaluation-safe module; implement holds the code. implement takes the definition value, so args types flow into read/write/lift by inference; there is no second place to repeat them. A single-call form (define({…, read, write, lift})) is rejected because it would put compiler code in every application import graph; the gate is a test that @effx/runtime's emitted import graph contains no @effx/compiler.

Annotation.define returns a callable. Calling it produces an applied annotation, which is both a TC39 decorator and a builder argument:

@RateLimit({ perMinute: 60 })                                   // decorator (target "operation": a static method)
static list() { … }

Operation.query({ … }).with(RateLimit({ perMinute: 60 })).http.get("/x").declare()   // builder step

At runtime an applied annotation records exactly { name, args: [live] } — the record @Annotate(name, args) of spec 0015 records — so the two syntaxes (spec 0002's "one meaning, two syntaxes") and the untyped primitive agree by construction. OperationBuilder.with is the one new builder method (typed Applied<_, "operation">); the builtin steps (.http.get, .errors, …) are generated or hand-kept sugar over the same mechanism (§3).

2.2 The args algebra: statically lowerable by constructionCopy Anchor Link

ADR 0001: the compiler never executes application modules, so every argument must be recoverable from the source text. The frontend already lowers a closed set (spec 0002 table + lower.ts). args is therefore not an arbitrary Schema but a closed combinator set A whose members each have a fixed lowering, an Encoded form (what the frontend produces: AnnotationArg), a Read type (what read receives) and a Live type (what the user writes; tsc checks it):

Derived constructors. A taggedUnion exposes its cases as typed constructors (Capability.one("x") ≡ { _tag: "One", capability: "x" }; zero-field cases are values). The frontend lowers a call/value whose static type carries the brand ~effx/Annotation/Constructor with a literal tag — the current eight special names become derived, not special-cased. This also accepts Schema.TaggedUnion cases (X.cases.One.make({…}), which mono-web already writes) and Data.taggedEnum constructors, because both expose a literal tag type. The 0013 addendum's "resolve the root symbol to @effx/runtime, including renamed imports" becomes "resolve to a branded constructor".

Rejected, at define time, with EFFX1301 naming the JSON path and node kind: Schema.Class/Opaque, Declaration nodes other than the ref markers, Date, BigInt, Symbol, Undefined-as-value, Unknown/Any/Object (use A.json), suspend, and any Transformation that changes shape (NumberFromString, transform, transformOrFail) — the value written in source would not be the value read sees. Allowed: refinement checks (isInt, isMinLength, isUnique, custom makeFilter): they run after lowering inside decodeResult, in compiler (extension) code, never in the application. Because the algebra is the only way to build args, the check only fires for A.fromSchema; everything else is correct by construction. define is total: it returns the definition plus diagnostics; the extension loader reports them as errors (invariant 11) and refuses to register it.

Schema-directed lowering replaces name-directed lowering: the frontend receives a lowering plan per annotation name (plain data derived from args, no ts), walks the TypeScript expression and the plan together, and produces AnnotationArg. The 16 SymbolContexts collapse into A.symbol({check}) positions. An expression the plan cannot lower is the existing EFFX1102 with location. The frontend recognizes a call as an applied annotation by the brand ~effx/Annotation/Applied on the callee's return type (same detect-by-shape, never by name rule as SCHEMA_TYPE_ID), reads name from its literal type, and looks the plan up; an unknown name keeps EFFX1101.

2.3 What each half derivesCopy Anchor Link

Per-definition laws (Annotation.laws(def, universe), derived, property-based): (a) decode(lower(print(x))) = x for x generated from args; (b) decorator and builder spellings lower to identical Collected (spec 0005 "syntax law"); (c) with an Effect writer, lift(write(read(x))) = x (spec 0019 L2 for this annotation). They run in the extension author's own test suite.

3. Can every builtin be re-expressed? (the falsifier)Copy Anchor Link

Claim to falsify: all builtin annotations can be rebuilt with define/implement with byte-identical IR, semantic hashes, generated files and diagnostics. Feasibility by what each needs beyond args → Contribution (analysis from the sources named in §1; not yet implemented):

So all 18 interpreted names are plain definitions; the 19th, builder-only Http.In, is not an annotation reading itself but an association rewritten by a pass. Gates that make the claim falsifiable, in order:

1. Type equivalence: for each of the nine option types, expectTypeOf<Live<D.args>>().toEqualTypeOf<HandWrittenOptions>(), with the §1 divergences preserved one-for-one (A.sourceOptional, A.union(schema, literal(true))). Tightening (§0.1) is a later, separate commit per divergence, each with updated fixtures; it is a recorded behaviour change, never a side effect of the re-expression.
2. Collected identity: every existing frontend fixture (users, rc116, group association, tagged access, content colon actions, Profile twin) produces byte-identical Collected under schema-directed lowering.
3. IR identity: canonical IR and semanticHash equal for all fixtures and for the vendored mono-web declarations (Profile ea8695d9…, plus Directory and SocialEvents as rebuilt by the same compiler).
4. Generated bytes equal; diagnostics equal in code, severity and location — messages that embed schemaError.message (EFFX1102) depend on the Schema structure, so the derived schema must be structurally the same tuple/struct nesting (Schema.Tuple([Options])) or the message change is declared.
5. Import graph: @effx/runtime bundles no @effx/compiler; a user definition module imports only the runtime.

Order: derive the runtime option types from the existing compiler Schemas first (kills the 57-leaf duplication, no behaviour change), then lowering plans, then decorators/builders, then implement.

4. Hypothesis: could an annotation just be an Effect Context key?Copy Anchor Link

Verified against the installed Effect 4.0.0 (node_modules/effect/src):

• Context.Key<I, S> / Context.Service<I, S>()("id"); HttpApiEndpoint.annotate<I,S>(key: Context.Key<I,S>, value: NoInfer<S>) and annotateMerge(ctx) (http-api/HttpApiEndpoint.ts:236,256); the same pair exists on HttpApiGroup, HttpApi, Rpc, RpcGroup, cli/Command, Workflow, Activity, ai/Tool, cluster/Entity (grep annotateMerge).
• OpenAPI's own annotations are keys: OpenApi.Identifier/Title/Description/Summary/Deprecated/Override/Transform are Context.Service classes (http-api/OpenApi.ts:42-170); OpenApi.annotations({…}) builds one Context from them.
• Context has no public enumeration: its public surface is get/getOption/getOrElse/getOrUndefined/merge/omit/pick/make/add; the entry map exists only as mapUnsafe. A reader must therefore be handed the keys it wants.
• Schema has the analogous typed hook: Schema.annotate({…}) extended by module augmentation of Schema.Annotations.Annotations, read back with Schema.resolveAnnotations.
• mono-web already uses exactly this: AccessSpecAnnotation = Context.Service<AccessSpec>(…), annotateAccessSpec(endpoint, spec) = endpoint.annotateMerge(accessSpecAnnotations(spec)), and reflectAccessSpec = Context.getOption(endpoint.annotations, AccessSpecAnnotation). Http.Access is a hand-built instance of "annotation = typed key + app annotator".

Conclusion: a typed key is the right default writer and default static lift for annotations that attach to an Effect object, and the wrong definition: the definition must exist before any Effect value does and must cover non-Effect targets, so args + target stay primary and effect is an optional clause. The "reader for free" holds only in the weak sense above (check-time reflection and static source lift), not as a source→IR reader.

5. Macro framingCopy Anchor Link

(Row contents are general knowledge of those systems, not re-verified for this document.) What effx takes: C#/Java's closed constant-argument algebra, Rust's typed-args-as-a-library layer, and C#'s writers only add files. What it keeps from its own invariants: AOT-only, decorator = contribution to IR (never behaviour), generated code is ordinary Effect, and a writer never rewrites user source: it emits generated files, or fragments inside a generated file (endpointAnnotations slot, §6), nothing else.

6. Writer contractCopy Anchor Link

write?:
  | Generator                                              // free: IR → files (today's contract)
  | Annotation.Fragment<Def>   // { slot: "endpoint" | "group" | "root" | "rpc" | "command",
                               //   code: (data, item) => Code }   // Code = Effect annotate/annotateMerge fragments

The HTTP/Rpc/CLI built-in generators expose fragment slots (seam S2 in 0019 makes them term-producing); a fragment is appended after the generator's own .annotateMerge chain in declaration order of the extension list, deterministically. Code is built from Print.ref(SymbolRef), Print.literal(json) and the Arg printer, so every import is a real, resolved import and unused undefined is never emitted. The default fragment for effect: { key } is .annotate(key, <printed Read>).

7. Type-safety story, end to endCopy Anchor Link

 declaration site        tsc              Live<args>            decorator/builder param types; a wrong literal is a tsc error
 frontend lowering       plan from args   EFFX1102 + location   expression the algebra cannot lower; never silently dropped
 decode                  Schema (args)    Read<args>            the SAME schema; malformed ⇒ EFFX1102 (existing)
 IR                      Extension.data   Schema.decode         dataOf(def, ir, op) typed in analyses and generators
 writer                  Print(args)      tsc on generated file generated `annotate(key, value)` checked against Context.Key shape (NoInfer<S>)
 lift                    same plan        same Schema           .annotate(K, expr) → Read; spec 0019 L2 holds per definition

Three independent gates (tsc, the Schema decoder, tsc on generated code) check three representations of one args value; nothing is checked by convention.

8. Worked example: @RateLimit (documentation only)Copy Anchor Link

// src/rate-limit.ts — application module (syntax half)
import { Context } from "effect";
import { A, Annotation } from "@effx/runtime";

export class RateLimitPolicy extends Context.Service<
  RateLimitPolicy,
  {
    readonly perMinute: number;
    readonly burst?: number;
  }
>()("app/RateLimit") {} // literal id: the lift matches this string

export const RateLimit = Annotation.define({
  name: "app.RateLimit",
  target: "operation",
  args: { perMinute: A.int({ min: 1 }), burst: A.optional(A.int({ min: 1 })) },
  cardinality: "one",
  effect: { target: "endpoint", key: RateLimitPolicy }, // default writer + default static lift
});

// src/users.ts — use (typed by tsc; lowered without evaluation)
export class Users {
  @Query({ name: "users.list", input: ListInput, success: UserList })
  @Http.Get("/users")
  @RateLimit({ perMinute: 60 })
  static list(input: ListInput) {
    /* … */
  }

  // @RateLimit({ perMinute: "60" })  // tsc error: string is not assignable to number (shape is tsc's job)
  // @RateLimit({ perMinute: 0 })     // tsc accepts (Live is `number`); decode rejects `min: 1` ⇒ EFFX1102
  // @RateLimit({ perMinute: n })     // tsc accepts; frontend: `n` is not a literal ⇒ EFFX1102
}

// effx/rate-limit.ext.ts — compiler half (config module only; never imported by the app)
import { Annotation, error, warning } from "@effx/compiler";
import { RateLimit, RateLimitPolicy } from "../src/rate-limit";

export const rateLimit = Annotation.implement(RateLimit, {
  // `read` omitted: IR gets Extension node ext:app/app.RateLimit/<op>, data = { perMinute, burst? }
  analyze: ({ operationsWith }) =>
    operationsWith(RateLimit).flatMap(({ operation, args, exposures }) => [
      ...(exposures.every((e) => e.transport._tag !== "http")
        ? [error("EFFX9001", `${operation.name}: @RateLimit needs an HTTP exposure`)]
        : []),
      ...(args.perMinute > 10_000
        ? [
            warning(
              "EFFX9002",
              `${operation.name}: perMinute ${args.perMinute} is effectively unlimited`,
            ),
          ]
        : []),
    ]),
});

Generated http.ts (only the new fragment shown):

HttpApiEndpoint.get("users.list", "/users", {/* … */})
  .annotateMerge(OpenApi.annotations({ identifier: "users.list" }))
  .annotate(RateLimitPolicy, { perMinute: 60 }); // tsc: checked against the service shape

App-owned reader (hand-written, typed): Context.getOption(endpoint.annotations, RateLimitPolicy) inside the middleware layer that builds its limiter from HttpApi.reflect. Lift (0019): .annotate(RateLimitPolicy, { perMinute: 60 }) on a hand-written endpoint is recognized because RateLimitPolicy's declaration carries the literal id "app/RateLimit" equal to rateLimit.effect.key.key, and { perMinute: 60 } lowers with the same plan, giving @RateLimit({ perMinute: 60 }).

9. Relationship to spec 0015 and migrationCopy Anchor Link

No 0015 decision needs revisiting: config loading, the trust boundary (one evaluated user module: the config, plus what it imports) and the curated @effx/compiler surface are orthogonal. The one rule for 0015's implementation: treat Interpreter as an implementation detail of an extension, not a contract extension authors must write, so deriving it later is not a break. Trust boundary, stated precisely: the CLI evaluates the config and what it imports, which now includes each extension's definition module (needed for the typed value, the lowering plan and effect.key). It still never evaluates an application program module (operations, schemas, handlers, services). To keep that true, a definition module must be a leaf: its static import closure may contain only effect, @effx/* and other definition modules; the frontend checks this on the TypeScript program and reports EFFX1306. RateLimitPolicy in §8 is a Context.Service class declared in the definition module for that reason.

10. Diagnostics (reserved EFFX13xx)Copy Anchor Link

11. Seams and non-goalsCopy Anchor Link

Seams (compiler/frontend/runtime owners): Annotation.define/A in @effx/runtime (new, replaces the per-annotation parts of Annotation.ts/decorators.ts/builder.ts); Annotation.implement/extension/dataOf/laws in @effx/compiler; SourceFrontend.analyze(project, { plans }); fragment slots in the HTTP/Rpc/CLI generators (shared with 0019 S2); Extension.expand for 0013; a branded Applied/Constructor type convention.

Non-goals: new builtin semantics; letting a definition run application code at compile time; IR v3 (a definition's data shape change needs a data migration story — open question: version field on data, mirroring migrate for the core IR); rewriting user source in any writer; Cedar/leases; multi-file definitions loaded by specifier (config loading stays 0015's).

Former open questions are decided in §0 (tightening: separate commits after identity; two-call split: accepted; v1 target: operation only). Still open: a version field on IR data for definition-data migrations.