AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
summary
Automatic insertion of maps and replicates makes rank-polymorphic calls type-check by encoding per-application rank choices as integer variables and solving a global integer linear programming problem to minimize total mappings. The system produces an explicit elaboration that a compiler can type-check; a prototype in a statically-typed array language and a Futhark implementation compiles benchmarks with correct outputs but incurs about a 2.5× compile slowdown while ILP solving remains practical.
AI-written summary · about
chapters (9)
- 0:00AUTOMAP intro
- 1:04Rank polymorphism
- 2:50Map and rep
- 4:16Rank-correct elaboration
- 7:46Type variables
- 9:55Rank inference
- 12:02Solving constraints with Integer Linear Programming
- 13:47Fuar implementation
- 14:52Summary
related talks
25mAUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming
15mScaling Optimization Over Uncertainty via Compilation
36mRank-Polymorphism for Shape-Guided Blocking
26mMechanical Proofs in an Array-Combinator Language
23mBetter Defunctionalization through Lambda Set Specialization
30mLayout Polymorphism: Using static computation to allow efficient polymorphism over...
08mCompiling pattern matching to in-place modifications
14mMicroKanren in J
