  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.
