Shape-Constrained Array Programming with Size-Dependent Types

Explore a 43-minute video presentation from the FHPNC 2023 conference that introduces a dependent type system for enforcing array-size consistency in ML-style functional array languages. Delve into the innovative approach that aims to ensure shape-consistency at compile time while allowing complex transformations on array shapes, without the typical complexities associated with dependently typed languages. Learn how sizes can be arbitrary expressions with syntactical equality, fitting naturally into a scheme interpreting size-polymorphic functions as having implicit arguments. Discover the system's ability to automate book-keeping for tracking existential sizes, such as in array filtering scenarios. Gain insights into the formalization of a substantial subset of the presented type system, its soundness proof, and discussions on adapting it for real-world implementation, including type inference, within the Futhark programming language. Presented by Lubin Bailly, Troels Henriksen, and Martin Elsman from ENS, France, and the University of Copenhagen, Denmark, this talk offers valuable knowledge for those interested in type systems, parallel programming, and functional programming.

[FHPNC'23] Shape-Constrained Array Programming with Size-Dependent Types