Compiling with Arrays (Artifact)

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



PDF
Thumbnail PDF

Artifact Description

DARTS.10.2.18.pdf
  • Filesize: 0.52 MB
  • 7 pages

Document Identifiers

Author Details

David Richter
  • Technische Universität Darmstadt, Germany
Timon Böhler
  • Technische Universität Darmstadt, Germany
Pascal Weisenburger
  • University of St. Gallen, Switzerland
Mira Mezini
  • Technische Universität Darmstadt, Germany
  • The Hessian Center for Artificial Intelligence (hessian.AI), Darmstadt, Germany

Cite AsGet BibTex

David Richter, Timon Böhler, Pascal Weisenburger, and Mira Mezini. Compiling with Arrays (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 18:1-18:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)
https://doi.org/10.4230/DARTS.10.2.18

Artifact

Artifact Evaluation Policy

The artifact has been evaluated as described in the ECOOP 2024 Call for Artifacts and the ACM Artifact Review and Badging Policy.

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 (A_{i}NF), which relies on the formal logical foundation of the positive formulation for the array type to facilitate maximal loop fission and subsequent optimizations. A_{i}NF 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 A_{i}NF, establishing that the process terminates, preserves types, and produces maximally fissioned terms.

Subject Classification

ACM Subject Classification
  • Software and its engineering → Domain specific languages
Keywords
  • array languages
  • functional programming
  • domain-specific languages
  • normalization by evaluation
  • common subexpression elimination
  • polarity
  • positive function type
  • intrinsic types

Metrics

Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail