Jeremy Gibbons at Lambda World 2017
APLicative Programming with Naperian Functors
Much of the expressive power of array-oriented languages such as Iverson’s APL and J comes from their implicit lifting of scalar operations to act on higher-ranked data, for example to add a value to each element of a vector, or to add two compatible matrices pointwise. It is considered a shape error to attempt to combine arguments of incompatible shape, such as a 3-vector with a 4-vector. APL and J are dynamically typed, so such shape errors are caught only at run-time. Recent work by Slepak et al develops a custom type system for an array-oriented language, statically ruling out such errors. I will show that such a custom language design is unnecessary: the requisite compatibility checks can already be captured in modern expressive type systems, as found for example in Haskell; moreover, generative type-driven programming can exploit that static type information constructively to automatically induce the appropriate liftings. I will also show that the structure of multi-dimensional data is inherently a matter of traversable Naperian applicative functors (and I will explain what this means).
Subscribe to the Lambda World YouTube channel to be updated when new videos are added.