一句话：提出用整数线性规划自动推断静态类型数组语言中的 map 与 replicate，兼顾动态数组语言体验与静态类型保证。
动态类型数组语言（如 Python、APL、Matlab）会把标量运算提升到数组并复制标量以适配应用，但这种便利在静态类型语言中通常缺失。本文提出一种自动推断 map 与 replicate 操作的机制，其类型系统支持参数多态、高阶函数和顶层 let-泛化，并利用整数线性规划寻找使程序能展开为良类型程序所需的最少操作。作者论证该推断系统为程序员提供有用且符合直觉的保证，展示若干理论性质，并在静态类型数组语言 Futhark 中实现了该机制。
Dynamically typed array languages such as Python, APL, and Matlab lift scalar operations to arrays and replicate scalars to fit applications. We present a mechanism for automatically inferring map and replicate operations in a statically-typed language in a way that resembles the programming experience of a dynamically-typed language while preserving the static typing guarantees. Our type system—which supports parametric polymorphism, higher-order functions, and top-level let-generalization—makes use of integer linear programming in order to find the minimum number of operations needed to elaborate to a well-typed program. We argue that the inference system provides useful and unsurprising guarantees to the programmer. We demonstrate important theoretical properties of the mechanism and report on the implementation of the mechanism in the statically-typed array programming language Futhark.
@article{0001HHME24,
title = {AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming},
author = {Robert Schenck and Nikolaj Hey Hinnerskov and Troels Henriksen and Magnus Madsen and Martin Elsman},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {OOPSLA2},
year = {2024},
doi = {10.1145/3689774}
}