Design doc for #1882: Issue #1882 Design: Statically Checked Autograd - #1884
Design doc for #1882: Issue #1882 Design: Statically Checked Autograd#1884johnynek wants to merge 3 commits into
Conversation
Codecov Report✅ All modified and coverable lines are covered by tests. Please upload reports for the commit 09078f9 to get more accurate results. Additional details and impacted files@@ Coverage Diff @@
## main #1884 +/- ##
==========================================
Coverage 85.03% 85.03%
==========================================
Files 190 176 -14
Lines 46891 34485 -12406
Branches 11805 8636 -3169
==========================================
- Hits 39876 29326 -10550
+ Misses 7015 5159 -1856 ☔ View full report in Codecov by Sentry. 🚀 New features to boost your workflow:
|
|
|
||
| Add compiler rule: | ||
|
|
||
| `Diff[a] <:< (a -> Float64)` |
There was a problem hiding this comment.
explain how we would do this. This seems to be a new kind of judgement in Infer. It seems like we would have to do a new kind of subsumption check where we add a runtime call during on the subsumption judgement.
For instance, if are judging Diff[b] <:< (a -> Float64) we would check if a <:< b and then apply run_Diff to the Diff[b] value to get the a -> Float64. Or something like this?
Please be more explicit with how Infer needs to change.
There was a problem hiding this comment.
Updated the design doc with an explicit Infer plan in section Subsumption/coercion changes in Infer (explicit). It now specifies a new subsCheckRho2 case for Diff[b] <:< (a -> Float64), reducing through runType = b -> Float64, reusing existing function subsumption, and composing coercion by inserting run_Diff at runtime (coerce_fn(run_Diff(d))). It also states the contravariant consequence a <:< b through existing function rules.
| ### 3. Intrinsic typing rules | ||
|
|
||
| 1. `diff(e)` requires `e` to typecheck as `a -> Float64`. | ||
| 2. `diff(e)` runs a differentiability checker on typed `e`. |
There was a problem hiding this comment.
explain in more detail how this differentiability checker looks. Now, we only compile one package at a time, and the only things we read from imports are the exported names and exported types. How does this compose? Can you only call other Diff[a] inside and some intrinsics? I guess that's right, but explain how.
Can we handle some branching? What kind? Be explicit.
There was a problem hiding this comment.
Expanded Differentiability checker with a new subsection on composition under Bosatsu’s package model (imports only expose exported names/types). The doc now explicitly limits cross-package calls inside diff bodies to: local inspectable functions, known derivative-registry globals, or Diff-typed imported values. It also adds a concrete branching policy section: non-active conditions are allowed (with examples), active-input-dependent branch conditions are rejected in phase 1.
| 1. `Float64` | ||
| 2. Tuples recursively composed of `Float64` | ||
|
|
||
| `Array[Float64]` is explicitly deferred in this issue (see rollout/follow-up). Calls that attempt `diff` on unsupported domains fail with dedicated autograd type errors. |
There was a problem hiding this comment.
add more explanation why Array[Float64] is difficult. It's one of the most obvious use cases.
Also, what about data types that only have nested tuples inside:
struct Pair(p: (Float64, Float64))
could we handle recursions on these easily?
There was a problem hiding this comment.
Added a dedicated Why Array[Float64] is deferred section with concrete reasons (runtime shape handling, scatter-add accumulation, optimizer/lowering implications, and dynamic guards without shape types). Also added Product structs and recursive ADTs: non-recursive product structs like struct Pair(p: (Float64, Float64)) are called out as much easier (tuple-isomorphic tangent structure), while recursive ADTs remain out-of-scope in phase 1 due current recursion restrictions in diff bodies.
| run_Diff, | ||
| ) | ||
|
|
||
| struct Diff[a](run: a -> Float64, grad: a -> a) |
There was a problem hiding this comment.
I'm confused about how the type for grad is a -> a. Can you explain that in more detail and give examples with Float64 and tuples of Float64?
There was a problem hiding this comment.
Added a new Why grad has type a -> a subsection with explicit examples for Float64, (Float64, Float64), and nested tuples. The section now explains that gradient output mirrors the input product structure and shows representative signatures and sample partial-derivative interpretation.
| ```bosatsu | ||
| from Bosatsu/Num/Autograd import diff, grad | ||
|
|
||
| square = diff(x -> x * x) |
There was a problem hiding this comment.
what about cases where we want to have variables that aren't part of the differentiation? For instance we have a Bool and if true we have one function and if false another, but both of those functions are differentiable. This is a common case. How is this handled?
There was a problem hiding this comment.
Added explicit handling for non-differentiated control variables in Branching policy (explicit). The doc now distinguishes active vs non-active values and includes examples where a Bool controls which differentiable branch to use (choose/choose2) while still allowing differentiation with respect to float inputs. It also states that branch conditions depending on active differentiable inputs are rejected in phase 1.
…nd checker details
|
Addressed all five review comments by directly revising |
|
|
|
MergeXO feedback automation is blocked because the agent returned Action: request concrete file edits (or explicit |
1 participant
Design doc.
Refs #1882