• Author and Context: Robert Schenck wrote this on June 17, 2024. He's a PhD student at DIKU and has worked on Futhark. AUTOMAP isn't in Futhark's master branch yet but a paper is in review and he'll give a talk at ARRAY24 on June 25th. He's looking for postdoc positions in type systems/functional programming/compilers.
• Motivation for AUTOMAP: To make mathematical code involving higher-dimensional arguments look closer to handwritten code by avoiding clutter from "administrative" maps. For example, to be able to write [1,2,3] + [4,5,6] instead of map2 (+) [1,2,3] [4,5,6].

• Examples of AUTOMAP:

  • Subtracting matrices: map2 (map2 (-)) [[1,2,3], [4,5,6], [7,8,9]] [[9,8,7], [6,5,4], [3,2,1]] or map (map (-)) [[1,2,3], [4,5,6], [7,8,9]] [[9,8,7], [6,5,4], [3,2,1]].
  • Adding a matrix and a vector: map (map (+)) [[1,2,3], [4,5,6], [7,8,9]] (rep [10,20,30]).
  • Applying a function to arguments of different ranks: map ((map f xss) (rep xss)) xss for a function f : []int -> [][]int -> int -> int and xss : [][]int.

• Challenges of Rank Polymorphism in Futhark:

  • Usually done dynamically in languages like NumPy and APL, but harder in statically-typed languages like Futhark as it needs to be decided during type checking without runtime information.
  • Futhark supports parametric polymorphism which complicates reasoning about how to insert maps and reps.
  • There are often many ways to insert maps and reps to make an application rank-correct, leading to ambiguity.

• Strategy for Handling Ambiguity:

  • Rule 1: An application can be mapped or repped but never both.
  • Rule 2: Minimize the number of inserted maps and reps.
  • When there are multiple minimal elaborations, the compiler signals an error and the programmer can choose or insert maps or reps manually.
• Finding Minimal Rank-Correct Elaborations: Traverse the program, generate constraints for each application to obtain a rank-correct program. For example, for f x, generate constraints like |a| = |c| (relaxed to rank equality), and handle rank differences with R and M variables. Accumulate these constraints during type checking and solve them to find the minimal assignment of rank variables.
• Solving the Constraints: Linearize the constraints using binary variables to enforce Rule 1. Transform the problem into an integer linear program (ILP) and solve it using an existing solver or an ILP algorithm.
• How AUTOMAP Works: For each top-level definition in a program: generate rank equality and Rule 1 constraints, transform into an ILP and solve. The solution tells the compiler how to insert the minimal number of maps and reps. Type check the transformed program and continue compilation.

Footnotes:

1. This is about ad-hoc polymorphism and adding a definition for vector addition.
2. Typed Remora demonstrates shape polymorphism at the type-level.
3. Delaying map and rep decisions until runtime has multiple drawbacks in a statically-typed language.