Compiling with Arrays
Journal
Proceedings of the 38th European Conference on Object-Oriented Programming (ECOOP)
Series
Leibniz International Proceedings in Informatics (LIPIcs); 313
ISSN
1868-8969
ISBN
978-3-95977-341-6
Type
conference paper
Date Issued
2024-07
Author(s)
Abstract
Linear algebra computations are foundational for neural networks and machine learning, often handled through arrays. While many functional programming languages feature lists and recursion, arrays in linear algebra demand constant-time access and bulk operations. To bridge this gap, some languages represent arrays as (eager) functions instead of lists. In this paper, we connect this idea to a formal logical foundation by interpreting functions as the usual negative types from polarized type theory, and arrays as the corresponding dual positive version of the function type. Positive types are defined to have a single elimination form whose computational interpretation is pattern matching. Just like (positive) product types bind two variables during pattern matching, (positive) array types bind variables with multiplicity during pattern matching. We follow a similar approach for Booleans by introducing conditionally-defined variables. The positive formulation for the array type enables us to combine typed partial evaluation and common subexpression elimination into an elegant algorithm whose result enjoys a property we call maximal fission, which we argue can be beneficial for further optimizations. For this purpose, we present the novel intermediate representation indexed administrative normal form (AiNF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. AiNF is normal with regard to commuting conversion for both let-bindings and for-loops, leading to flat and maximally fissioned terms. We mechanize the translation and normalization from a simple surface language to AiNF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.
Keywords
2012 ACM Subject Classification Software and its engineering → Domain specific languages phrases array languages
functional programming
domain-specific languages
normalization by evaluation
common subexpression elimination
polarity
positive function type
intrinsic types
Publisher
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Publisher place
Dagstuhl, Germany
Start page
33:1
End page
33:24
Pages
24
File(s)![Thumbnail Image]()
open.access
Name
2024_Compiling-with-Arrays.pdf
Size
1 MB
Format
Adobe PDF
Checksum (MD5)
d22f9c64e48bf0cf56cda32d6a41623d