Shape-Constrained Array Programming with Size-Dependent Types
summary
A dependent-type extension enforces array-size consistency in an ML-style data-parallel language and is implemented in the Futhark compiler; sizes are arbitrary expressions, treated by syntactic size equality so most checks unify at compile time and remaining mismatches use dynamic casts. Existential sizes (e.g. filter results) are tracked and repacked automatically — automated existential bookkeeping — a large subset is formalized and proved sound, and the implementation integrates with existing code with few changes.
AI-written summary · about
chapters (33)
- 0:00Shape-constrained array programming intro
- 1:06Fuar compiler and array context
- 2:31Dynamically typed arrays challenges
- 3:55Dependent types and size programming
- 5:22Fuar size types examples
- 7:07Dot product and matrix multiplication
- 9:44Iota function and size constraints
- 10:27Explicit size arithmetic
- 11:50Concatenation and size polymorphism
- 13:15Regular arrays and rank polymorphism
- 14:42Irregular arrays and errors
- 15:47Dynamic errors and escape hatches
- 16:08Fuar unification-based type checking
- 17:40Syntactic unification limits
- 19:01Unflatten and split reshaping
- 21:08Runtime checks and type casts
- 22:55Compile-time vs runtime sizes
- 24:02Size compatibility constraints
- 25:25Size types allowed expressions
- 26:50Filter function existential sizes
- 29:18Unpacking existential sizes
- 29:40Type system formalization
- 31:06Empty arrays and shapes
- 32:28Fuar limitations non-termination
- 33:15Mechanization and future work
- 33:35Summary
- 33:57Questions and discussion on existential types
- 35:22Static vs dynamic trade-offs
- 36:47Explicit parameters vs checks
- 37:31Unification interpreter interaction
- 38:35Higher-order unification
- 39:17Reshaping functions memory
- 41:50Split function behavior
related talks
34mFunctional Programming + Dependent Types ≡ Verified Linear..
25mLinear Types with Dynamic Multiplicities in Dependent Type Theory (Functional Pearl)
21mGraded Monoids for Dependently Typed Array Programming
45mAPLicative Programming with Naperian Functors
25mIs Sized Typing for Coq Practical?
41mPrograms and Proofs — Dependent Typing as a Way to Structure Your Code
22mScale By The Bay 2018 Unconference: Gabriel Claramunt
36mConcrete Functional Programming