AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming

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.

Authors

Institutions

Publication Details

Journal
Proceedings of the ACM on Programming Languages
Published
2024-10-08
DOI
https://doi.org/10.1145/3689774
Citations
1
Primary Topic
Logic, programming, and type systems
Type
article
Field-Weighted Citation Impact
0.35
Controls
|||
ALL TIME
JAN
FEB
MAR
APR
MAY
JUN
JUL
AUG
SEP
OCT
article

AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming

Magnus Madsen, Troels Henriksen, Robert Schenck, Martin Elsman et al.
1 citations
Proceedings of the ACM on Programming Languages
Logic, programming, and type systems
0.35
article

AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming

Magnus Madsen, Troels Henriksen, Robert Schenck, Martin Elsman, Nikolaj Hey Hinnerskov
article en
1 citations

Abstract

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.

Proceedings of the ACM on Programming LanguagesVol. 8(OOPSLA2)
University of Copenhagen (DK), Aarhus University (DK)
Openalex Percentile: Top 33%
Logic, programming, and type systems
0.35
AI Navigator

Ask Laika to Summarize, Analyze, and Connect papers live on the map.

Summarize Papers & Methodologies

Extract key findings, datasets, and comparative methods across publications.

Benchmark Rankings & Visual Analytics

Rank top research institutions, authors, funders, topics, and journals by Field-Weighted Citation Impact (FWCI) and paper volume with instant charts.

Connect Distant Disciplines

Bridge topological clusters on the map to find hidden collaborative intersections.

AUTOMAP: Inferring Rank-Polymorphic Function Applications with Integer Linear Programming — Magnus Madsen, Troels Henriksen, et al. · Proceedings of the ACM on Programming Languages (2024) | TGRS Research Map | TGRS