Structuring Arrays with Algebraic Shapes
summary
A new array calculus called Star gives arrays structured shapes and indices as records and variants with structural subtyping, so indexing errors are prevented by richer types rather than size arithmetic; broadcasting computes the least common subshape and elementwise ops use that result. The paper shows progress/preservation (except for raw integer bounds), demonstrates a clearer padding implementation using product/concatenation shapes, reports a prototype using algebraic subtyping and sketches type inference, and proposes erasure/monomorphization for performant codegen.
AI-written summary · about
chapters (15)
- 0:00Introduction
- 1:03Array type challenges
- 3:52Labeled array axes
- 5:17Star calculus
- 7:43Product and concatenation
- 9:28Broadcasting with shapes
- 11:39Padding example
- 14:02Formal Star development
- 16:52Subtyping rules
- 18:40Type safety
- 20:21Design limitations
- 22:30Performance
- 24:15Future directions
- 24:56Conclusion
- 26:20Q&A
related talks
38mA Ray of Hope: Array Programming for the 21st Century
01h 02mThe Shapes of Multi-Dimensional Arrays
32mImmutable Arrays Help Mutating Arrays More Efficiently
15mCompilation of Sparse Array Programming Models
43muarray - Efficient and Generic Array Computation
36mAlgebraic DataTypes in Scala. Where is the algebra? What other algebras are there?
58mFunctional Array Funhouse Intensive - Part 2 of 5
20mCompiling Structured Tensor Algebra