Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Compiling with Arrays

David Richter, Timon Böhler, Pascal Weisenburger, Mira Mezini

TL;DR

This work introduces AiNF, an intermediate representation for array computations, grounded in a positively polarized view of types that treats arrays as positive function types. By translating a simple surface language Polara into AiNF, the authors achieve maximal loop fission and safe, schedule-free optimizations via typed partial evaluation and common subexpression elimination, all formalized and mechanized in Lean 4. The approach enables straightforward loop-invariant code motion and robust CSE across complex control flow, while ensuring termination and type preservation. The combination of a logical foundation with a practical array-centric IR promises more predictable optimization for array programs, with demonstrated benefits on dense layers, convolution, and Black-Scholes-style pipelines. The work also provides a path toward extending the language with automatic differentiation and probabilistic primitives, guided by the same formal guarantees.

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.

Compiling with Arrays

TL;DR

This work introduces AiNF, an intermediate representation for array computations, grounded in a positively polarized view of types that treats arrays as positive function types. By translating a simple surface language Polara into AiNF, the authors achieve maximal loop fission and safe, schedule-free optimizations via typed partial evaluation and common subexpression elimination, all formalized and mechanized in Lean 4. The approach enables straightforward loop-invariant code motion and robust CSE across complex control flow, while ensuring termination and type preservation. The combination of a logical foundation with a practical array-centric IR promises more predictable optimization for array programs, with demonstrated benefits on dense layers, convolution, and Black-Scholes-style pipelines. The work also provides a path toward extending the language with automatic differentiation and probabilistic primitives, guided by the same formal guarantees.

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.
Paper Structure (36 sections, 3 theorems, 2 equations, 7 figures, 1 table)

This paper contains 36 sections, 3 theorems, 2 equations, 7 figures, 1 table.

Table of Contents

  1. Introduction
  2. Contributions.
  3. Problem Statement
  4. AiNF, Polara, and Simplified Optimizations
  5. The Duality of Functions and Arrays
  6. Products as Positive and as Negative Types.
  7. Functions as Negative and Positive Types.
  8. Interpreting positive function types as arrays.
  9. Arrays Enable CSE.
  10. Lifting Branching into the Context
  11. Polara and AiNF by Example
  12. Dense Layer.
  13. Convolution.
  14. Black-Scholes.
  15. Simplifying Optimizations with AiNF
  16. ...and 21 more sections

Key Result

Theorem 1

Our optimization procedure is terminating and type preserving.

Figures (7)

  • Figure 1: Sample programs.
  • Figure 2: Generated AiNF.
  • Figure 3: Polara and AiNF
  • Figure 4: Polara's type system.
  • Figure 5: Typed partial evaluation.
  • ...and 2 more figures

Theorems & Definitions (3)

  • Theorem 1: Well-typedness of Optimization
  • Theorem 2: Well-typedness of Translation
  • Theorem 3: Maximal Fission