From b4f988cb1490ed31ab225323b33448667b8578c0 Mon Sep 17 00:00:00 2001 From: Tom Smeding Date: Mon, 26 Jan 2026 23:37:55 +0100 Subject: Multihot cotangents WIP (doesn't work) The idea is sound but for a smaller source language. Notes also in Obsidian, but the theory so far is that dropping support for nested arrays makes this possible, although making the result type-safe (i.e. not have partial functions in a bunch of places) would require making the lack of nested array support explicit in the embedded type system, i.e. have Accelerate-like stratification. The point is that multihots can be added heterogeneously using plusSparseS but not homogeneously with EPlus or plusSparse, because the indices might differ between the summands. Thus as long as we never need to homogeneously sum multihot cotangents, we're golden. Now the crucial observation is that we only need plus to be homogeneous on array elements. So if array elements cannot themselves be arrays, i.e. we drop support for nested arrays, no homogeneous plus of multihot array cotangents is needed, and we can have static multihots. --- src/CHAD/AST/UnMonoid.hs | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/CHAD/AST/UnMonoid.hs') diff --git a/src/CHAD/AST/UnMonoid.hs b/src/CHAD/AST/UnMonoid.hs index d3cad25..1a66cdf 100644 --- a/src/CHAD/AST/UnMonoid.hs +++ b/src/CHAD/AST/UnMonoid.hs @@ -212,6 +212,11 @@ accumulateSparse topty topsp arg accum = case (topty, topsp) of (EIdx ext (evar (IS IZ)) (EVar ext tn IZ)) (\w prj idx val -> accum (WPop (WPop w)) (SAPArrIdx prj) (EPair ext (EVar ext tn (w @> IZ)) idx) val)) $ ENil ext + (SMTArr _ t, SpArrIdx s) -> + eunPair arg $ \w1 e1 e2 -> + elet (accumulateSparse t s e2 + (\w prj idx val -> accum (w .> w1) (SAPArrIdx prj) (EPair ext (weakenExpr w e1) idx) val)) $ + ENil ext acPrjCompose :: SAIDense dense -- cgit v1.2.3-70-g09d2