Phase 2: AD as an Effect — Index
The algebraic effect and handler infrastructure implementing reverse-mode automatic differentiation as an in-language construct. This specification defines the transition from a pure shape-typed functional language (Phase 1) to an effectful language supporting AD, mutation constraints, and control flow.
The sections
Scope, Milestones, and Exit Criteria — What Phase 2 delivers, broken into three internal milestones. The
AD-as-handlerProof of Concept (PoC) as the load-bearing validation step. Risks and abandonment criteria.Effect Handler Infrastructure — Compiler and runtime support for algebraic effects and handlers. Typing rules for effect rows (e.g.,
Tensor[dtype, shape] !{Random, State}), effect row subtyping/coercions, and stack/unwind execution semantics.Automatic Differentiation — Reverse-mode AD implemented as a language-level handler. The continuation-passing style (CPS) transform mapping, adjoint storage allocation, and registration of custom gradients via handlers.
Control Flow and Iteration — Structured control flow (
if,while) and loop iteration. Integration of dynamic branch tapes and checkpointing for backpropagation memory optimization.
Key commitments
The decisions that shape everything Phase 2 builds:
| Decision | Rationale |
|---|---|
| AD is a language-level effect handler | Eliminates tape-based compiler-internal magic; AD becomes a modular, user-extensible library transformation. |
| Algebraic effects with row polymorphism | Allows composition of orthogonal effects (Random + State + Exception) in any order, with precise compile-time tracking. |
| Linear/owned tensors by default | Prevents aliasing issues under mutation-aware AD, ensuring that values are sound at differentiation time. |
| Stochastic estimators as handlers | Converts the choice of gradient estimator (reparameterization vs. score-function) from an ad-hoc user choice to a composed handler concern. |
| Implicit/fixpoint definitions via IFT | Uses the Implicit Function Theorem (IFT) to solve a linear system rather than unrolling iterative solver loops. |
What Phase 2 does not include
Phase 2's scope is strictly bounded. The following are deferred to later phases:
- Sharding & distributed programming. Phase 3.
- Sparsity & MoE routing. Phase 4.
- Hardware capabilities & custom GPU tile kernels. Phase 5.
- Verified compilation passes (Lean 4 proofs). Phase 6 (though Phase 2 mechanized statements may exist).
- Surface syntax & tooling. Phase 7.
- Multi-GPU / multi-device runtime. Phase 3.
Suggested reading order
For a first pass: read 01-scope-milestones-exit-criteria.md to understand the target goals and exit conditions, followed by the planned sections once they are drafted.