[codex] Add advanced effects guide

docs/guides/advanced-effects.md

@@ -0,0 +1,170 @@
+---
+title: Advanced Effects
+description: Designing open dotted effect names, callback forwarding, and policy boundaries in soundscript.
+---
+
+This guide is for library authors and teams that want to design their own effect taxonomies, not
+just consume the standard `fails` / `suspend` / `mut` / `host` umbrellas.
+
+The canonical surface still lives in the main repo annotation spec. This guide is about how to use
+that surface well.
+
+## Mental model
+
+The current effect system is built from four pieces:
+
+- open dotted effect names such as `fails.rejects`, `host.node.fs`, and `host.browser.dom`
+- prefix containment, so ancestors overlap descendants
+- declaration summaries through `add` and `forward`
+- negative contracts through `forbid`
+
+That means effect design is mostly about naming and boundaries. The checker itself is generic over
+effect names; it does not need hardcoded knowledge of your application-level effect families.
+
+## The standard core versus library tags
+
+The standardized semantic core is:
+
+- `fails`
+- `fails.throws`
+- `fails.rejects`
+- `suspend`
+- `suspend.await`
+- `suspend.yield`
+- `mut`
+- `host`
+- `host.io`
+- `host.random`
+- `host.time`
+- `host.system`
+- `host.ffi`
+
+Everything else is library or platform space. Common examples already used in bundled declarations
+include:
+
+- `host.node.fs`
+- `host.node.process`
+- `host.browser.dom`
+- `host.browser.message`
+
+The core names are about broad semantics. The dotted tags are where you encode platform or
+application-specific policy boundaries.
+
+## When you should actually write effect annotations
+
+Most ordinary bodyful soundscript code should not need them.
+
+In the current model, start from this default:
+
+- bodyful functions should rely on inference
+- generated declarations should project that inferred summary outward
+- explicit effect annotations are mainly for real declaration frontiers and intentionally
+  effect-transforming higher-order surfaces
+
+That means:
+
+- a normal bodyful wrapper over other soundscript code usually needs no annotation
+- a facade over ambient globals or foreign declarations usually does need an explicit declaration
+  summary
+- a higher-order wrapper only needs explicit `forward` / `rewrite` / `handle` when inference does
+  not already recover the intended public summary
+
+The shipped `sts:*` stdlib now follows that rule. Its remaining explicit effects are on host
+facades such as `sts:fetch`, `sts:text`, and `sts:url`, not on ordinary bodyful helper code.
+
+## Prefix containment matters
+
+Containment is by prefix, not by broad "same family" intuition.
+
+These overlap:
+
+- `host` and `host.io`
+- `host` and `host.browser.dom`
+- `fails` and `fails.rejects`
+- `suspend` and `suspend.await`
+
+These do not overlap:
+
+- `host.io` and `host.db.query`
+- `host.node.fs` and `host.browser.dom`
+- `fails.throws` and `host.io`
+
+That distinction is the key tool for modeling practical policies.
+
+## Forwarding, rewrite, and handle
+
+`forward` brings callback effects into a declaration summary.
+
+```ts
+// #[effects(forward: [callback])]
+declare function map<T, U>(
+  values: readonly T[],
+  callback: (value: T) => U,
+): readonly U[];
+```
+
+`rewrite` changes the forwarded effect names before they are merged.
+
+```ts
+// #[effects(
+//   add: [suspend.await],
+//   forward: [{ from: callback, rewrite: [{ from: fails, to: fails.rejects }] }],
+// )]
+declare function toPromise<T>(callback: () => T): Promise<T>;
+```
+
+`handle` discharges forwarded effects after rewriting.
+
+```ts
+// #[effects(forward: [{ from: action, handle: [fails] }])]
+declare function resultOf<T>(action: () => T): T | Error;
+```
+
+The evaluation order is always:
+
+1. resolve the forwarded callable summary
+2. apply rewrites in array order
+3. apply handled-effect removal
+4. union the result into the containing summary
+
+## Designing taxonomies for policy boundaries
+
+The main design constraint today is that `forbid` is subtractive only. There is no allow-list or
+"all except ..." operator.
+
+The main design constraint today is that `forbid` is subtractive only. There is no allow-list or
+"all except ..." operator.
+
+That means some intuitive policy shapes are *not* directly representable.
+
+In particular, this does not work as an honest transitive rule:
+
+- forbid `host.io`
+- but still allow database queries implemented with lower-level `host.io`
+
+If a real query implementation performs network or file I/O, then its summary still contains
+`host.io`. Adding a more specific tag does not erase the underlying effect. Effects describe what
+happened, not why it happened.
+
+So the practical naming rule is:
+
+- use dotted tags to classify and document boundaries honestly
+- do not expect effects alone to express purpose-based exceptions over the same transitive behavior
+- if a policy needs "DB I/O allowed, other I/O forbidden", that requires a different abstraction
+  model than the current effect system
+
+## Practical recommendations
+
+- Use the standard core for broad semantics.
+- Add dotted library tags for platform or subsystem ownership.
+- Put stable declaration-frontier summaries directly on declarations.
+- Prefer inference first for bodyful code; add callable-level `add` only to classify or widen a
+  callable honestly, never to restate what inference already knows.
+- Reserve `unknown: [direct]` for boundaries that are intentionally opaque today.
+- Use `forward` only when the body or summary really needs help expressing a higher-order boundary.
+- Do not rely on effects alone for purpose-based authority policies such as transaction-only DB access.
+
+## See also
+
+- [Annotation Spec](../reference/annotation-spec.md)
+- [Errors and Failures](./errors-and-failures.md)

docs/reference/annotation-spec.md

@@ -32,6 +32,7 @@ Rules:
 
 Builtin directives:
 
+- `effects`
 - `extern`
 - `interop`
 - `newtype`
@@ -53,6 +54,7 @@ compiler-only magic. See [Macros](./macros.md) for the authoring model and suppo
 
 ## Where each one attaches
 
+- `#[effects(...)]` attaches to callable declarations and callable type members, plus function-valued parameters for parameter-local negative contracts
 - `#[interop]` attaches to import boundaries
 - `#[extern]` attaches to local ambient runtime declarations
 - `#[variance(...)]` attaches to generic interfaces and type aliases
@@ -74,9 +76,53 @@ That matters because teams can:
 
 Today, only these builtin forms take arguments:
 
+- `// #[effects(...)]`
 - `// #[variance(...)]`
 - `// #[value(deep: true)]`
 
+## `#[effects(...)]`
+
+`effects` is the builtin effect-summary and effect-contract annotation.
+
+Supported fields:
+
+- `add`
+- `forbid`
+- `forward`
+- `unknown`
+
+Rules:
+
+- effect names are open dotted identifiers such as `fails.rejects`, `host.io`, `host.node.fs`, and `host.browser.dom`
+- `forward` must use parameter-rooted callable references or `{ from, rewrite?, handle? }` objects
+- `unknown` currently only supports `unknown: [direct]`
+- bodyful local callables may use `add`, `forbid`, and `forward`
+- bodyful `add` is monotonic: it unions with inferred effects and never hides inferred lower-level behavior
+- declaration-only callable surfaces use `add`, `forward`, and optionally `unknown`
+- function-valued parameters use `forbid` only
+- overload signatures with an implementation sibling must stay effect-unannotated
+- there is no allow-list or "all except ..." surface in `#[effects(...)]`
+- transitive effects stay honest, so policies like "allow database I/O but forbid other I/O" are not representable today without a different abstraction model
+
+Most ordinary bodyful soundscript code should rely on inference alone. Explicit callable-level
+`add` and `forward` are mainly for declaration frontiers and for the cases where you intentionally
+widen or transform the honest inferred surface.
+
+Quick example:
+
+```ts
+// #[effects(
+//   add: [suspend.await],
+//   forward: [{ from: callback, rewrite: [{ from: fails, to: fails.rejects }] }],
+// )]
+declare function toPromise<T>(callback: () => T): Promise<T>;
+```
+
+For the full current surface and semantics, see the canonical repo spec and the advanced guide:
+
+- [Advanced Effects](../guides/advanced-effects.md)
+- [`docs/annotation-spec.md` in the soundscript repo](https://github.com/soundscript-lang/soundscript/blob/main/docs/annotation-spec.md)
+
 ## `#[value]`
 
 Supported forms:
@@ -115,7 +161,7 @@ interface Reader<T> {
 The current annotation system does **not** include:
 
 - parser-level `#[...]` syntax
-- parameter annotations
+- arbitrary parameter annotations, except for `#[effects(...)]` on function-valued parameters
 - type-parameter annotations
 - arbitrary type-expression macros
 
@@ -125,6 +171,7 @@ soundscript keeps TypeScript parser syntax. The annotation system is intentional
 
 ## See also
 
+- [Advanced Effects](../guides/advanced-effects.md)
 - [Newtypes and Value Classes](./newtypes-and-value-classes.md)
 - [Variance Contracts](./variance-contracts.md)
 - [Macros](./macros.md)

sidebars.ts

@@ -33,6 +33,7 @@ const sidebars: SidebarsConfig = {
       type: 'category',
       label: 'How-to Guides',
       items: [
+        'guides/advanced-effects',
         'guides/tooling-and-js-target',
         'guides/ci-and-editor-setup',
         'guides/publishing-packages',