WG211/M16Gibbons

Jerermy Gibbons: APLicative Programming with Naperian Functors

A lot 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. But it is 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 static type system for an array-oriented language. We show here 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, and moreover, generative type-driven programming can use that static type information constructively to automatically induce the appropriate liftings. We show also that the structure of multi-dimensional data is inherently a matter of Naperian applicative functors - lax monoidal functors, with strength, commutative up to isomorphism under composition.