Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation

Prerequisites. Direct starred prerequisites: Chapter 19 and chapter 133; chapter 31 supplies the indexed families. No later core chapter depends on this route.

A dot product takes two vectors and multiplies them componentwise before summing. In an ordinary functional language its type is $\mathsf{[}\mathsf{]}\mathsf{int}\to \mathsf{[}\mathsf{]}\mathsf{int}\to \mathsf{int}$, which says that both arguments are arrays of integers and nothing else. It does not say that the two lengths agree, so the componentwise multiplication has no static justification and a run-time check must decide the matter.

Change one feature. A $\mathsf{filter}$ returns the elements satisfying a predicate; its result length is not any expression the caller can write down, because it depends on the values in the input. A type that must name every length cannot type $\mathsf{filter}$ at all.

Change one more. A nested $\mathsf{map}$ over an array of arrays exposes two levels of parallelism, and a flat accelerator target must recover the inner level without changing the result. Whether that is possible depends on whether the inner arrays all have the same length — which is again a fact about sizes.

Three obstacles, one object: a type language in which sizes are expressions. This chapter freezes the language $F$ of Bailly, Henriksen and Elsman (2023), proves its soundness proposition at exactly the strength that paper states, and only then compares two implementations.

The frozen language $F$

The witness condition is the chapter’s first non-obvious clause and it is worth saying at once what it excludes. If a value had type $[fx]\tau$ for some function $f$, recovering $x$ from the value would require inverting $f$. Definition 139.2 does not let $x$ count as witnessed there, so no rule ever asks for that inversion.

Two clauses of definition 139.3 carry the design. t-app substitutes the argument into the result type, as in any dependent system. t-map does not: its side condition $x\notin \mathrm{fv}({\tau }^{\prime })$ forbids the element type from depending on the element, which is what keeps the result a regular array rather than a ragged one.

Value equivalence and substitution

Two closures are equivalent when they return equivalent values on the same argument and fail on the same arguments. The second half is what makes the relation usable in a semantics that models only successful executions.

Proof of Proposition 139.7 — Substitution preserves semantics

Proof. Clauses 1 and 2 are proved by mutual induction on the evaluation and size-checking derivations; the mutual induction is forced because d-coerce appeals to size checking and size checking appeals to evaluation in c-arr. The converses are proved by mutual induction on the structure of $e$ rather than on a derivation, because the hypothesis is about $e[e^{\prime }/x]$ and gives no derivation for $e$. The last clause follows from the first three. Equivalence rather than equality appears in the conclusion because substituting a term for a variable duplicates the term’s evaluation, and two evaluations of one closure need not produce syntactically identical environments. ◻

Calculating with sizes

The type language is now fixed; the following calculations expose one clause of it at a time.

Soundness

The array clause is where the relation stops being a syntactic predicate: it evaluates the size expression in $\rho$ and compares the result with the actual length. That is why the relation is indexed by a dynamic environment at all.

Proof of Proposition 139.13 — Dynamic size matching and checking

Proof. Clause 1 is by induction on $\tau$, following definition 139.2: the only clause contributing a witness is $[x]\tau$, and there the array’s length supplies $n$. Clause 2 is by induction on the structure of $\tau$. Clause 3 is by induction on the size-checking derivation, each of whose rules is the corresponding clause of definition 139.11. Clause 1 uses that arrays are nonempty: for an empty array every $\tau$ would satisfy $\rho \vDash v:[0]\tau$, while extracting a size from $[0][x]\tau$ would require the array’s first element. ◻

Proof of Theorem 139.15 — Soundness

Proof. By induction on the typing derivation, with proposition 139.14 for t-relax.

t-int, t-var. Immediate from definition 139.11 and $\rho \vDash \mathrm{\Gamma }$.

t-app. Inverting d-app, the function evaluates to a closure $⟨x,e_0,{\rho }^{\prime }⟩$ and the argument to $v^{\prime }$, and ${\rho }^{\prime },x:v^{\prime }⊢e_0\Downarrow v$. The induction hypothesis at the function gives $\rho \vDash ⟨x,e_0,{\rho }^{\prime }⟩:(x:\tau )\to \mu$, and at the argument gives $\rho \vDash v^{\prime }:\tau$. Unfolding the closure clause of definition 139.11 at those data gives $\rho ,x:v^{\prime }\vDash v:\mu$, and clause 5 of proposition 139.7 converts that to $\rho \vDash v:\mu [e^{\prime }/x]$, which is the conclusion of t-app.

t-map. Inverting d-map, the array evaluates to $[v_1,\dots ,v_n]$ and each $v_i^{\prime }$ is the closure’s result on $v_i$. The induction hypothesis at $e_a$ gives $\rho ⊢e_s\Downarrow n$ and $\rho \vDash v_i:\tau$; the hypothesis at $e_f$ gives $\rho ,x:v_i\vDash v_i^{\prime }:{\tau }^{\prime }$, and $x\notin \mathrm{fv}({\tau }^{\prime })$ with proposition 139.12 strips the extra binding, giving $\rho \vDash v_i^{\prime }:{\tau }^{\prime }$. Hence $\rho \vDash [v_1^{\prime },\dots ,v_n^{\prime }]:[e_s]{\tau }^{\prime }$. Without the side condition the $n$ results would be related at $n$ different types and no array type would hold.

t-let. Inverting d-let, $e$ evaluates to $v$, the sizes $\bar{n}$ are extracted by dynamic size matching, and $e^{\prime }$ evaluates in the extended environment. The hypothesis at $e$ gives $\rho \vDash v:\mathrm{\exists }\bar{x}.\tau$; clause 2 of proposition 139.13 gives $\rho ,\bar{x}:\bar{n}\vDash v:\tau$, so the extended environment is related to the extended context and the hypothesis at $e^{\prime }$ applies. The side condition $\bar{x},y\notin \mathrm{fv}(\mu )$ and proposition 139.12 strip the extra bindings from the conclusion.

t-coerce. Inverting d-coerce gives $\rho ⊢v▹\tau$, and clause 3 of proposition 139.13 gives $\rho \vDash v:\tau$ directly — the induction hypothesis at $e$ is not needed.

The remaining rules are componentwise. ◻

System card: a production array compiler

Only now, with the proved core in hand, is it useful to look at an implementation. The following observations are about a particular compiler and are not theorems about $F$.

Second-order array combinators.

The source language offers $\mathsf{map}$, $\mathsf{reduce}$, $\mathsf{scan}$ and $\mathsf{filter}$ as primitives with fixed sequential meanings. Their sequential semantics is what the compiler is entitled to preserve; their parallel implementation is a choice made later.

Uniqueness and aliasing.

A parameter marked unique may be consumed, so its buffer can be updated in place. The analysis tracks which values may alias which, and rejects a program that uses a consumed value. This is a static discipline for in-place update in a pure language, and it is absent from $F$: definition 139.1 has no update and no uniqueness annotation.

Fusion and flattening.

Adjacent combinators are fused into one, and nested parallelism is flattened into flat parallelism. Each pass has an invariant that the compiler’s own type checker enforces. That a pass preserves that invariant is evidence of the kind discussed in chapter 133, and is not a semantic-preservation theorem.

Generated code.

The back end emits code for a parallel target. The boundary between the functional meaning of the source and the behaviour of the generated program is where floating-point associativity, scheduling and hardware behaviour enter, and none of them is modelled by $F$.

Bounded property analysis.

A restricted property language can express equivalence, range, injectivity, bijectivity, monotonicity, filtering and partitioning of array-producing expressions, and a bounded automatic analysis decides properties in that grammar. It is an analysis with a stated grammar, not a verifier.

Comparison card: eager memoized functions over index sets

Change one design decision at a time from the proved spine.

1. Replace “array indexed by a size” with “eagerly memoized function over a typed finite index set”. A table has type $i\Rightarrow a$ where $i$ is a type whose inhabitants are the legal indices. Where $F$ writes $[n]\tau$, this design writes $\mathsf{Fin}n\Rightarrow \tau$, and the index type may be a sum or a product rather than a prefix of the integers.

2. Replace bulk combinators with pointful nested indexing. A $\mathsf{map}$ becomes a comprehension over the index set, and the programmer writes the element expression rather than a function to be mapped.

3. Add fine-grained effect rows for the operations that behave like mutation. A table built by writing its entries needs an effect; the row records which region is written.

4. Isolate associative accumulation as its own effect. An accumulator whose combining operation is associative may be split and recombined.

5. Calculate one reduction or histogram with that accumulator, showing the reordering argument for that example.

Limits and seminar

The frozen source for the formal core is Bailly, Henriksen and Elsman (2023): definition 139.1, definition 139.2, definition 139.3, definition 139.4, definition 139.6, definition 139.11 are its Figures 1–7, and proposition 139.7, proposition 139.12, proposition 139.13, proposition 139.14 and theorem 139.15 are its Propositions 3.4, 3.5, 3.6–3.8, 3.9 and 3.10, at their exact statements. The 2021 precursor is used only where signatures coincide. Section 139.5 reports the implementation observations of the compiler papers, the thesis and the bounded property analysis; section 139.6 reports the typed-index, effect and accumulation design of its own source. No theorem is transferred from an implementation to $F$, or from $F$ to an implementation.

Five boundaries. Theorem 139.15 is conditioned on a successful evaluation, by remark 139.16, and is neither progress nor termination. Arrays are nonempty, and proposition 139.13 uses that. Size equality is syntactic, so example 139.9 needs a coercion with a run-time check where a solver would not. Uniqueness, in-place update, fusion, flattening and code generation are outside $F$ entirely, and remark 139.17 lists the five statements that are not proved. Finally, the printed formal syntax is $F$; any presentation-only notation used in an example must elaborate to it by an explicit translation with its own preservation lemma, and similar notation is not enough.

[4]

Suggested first pass.

None of these problems is a prerequisite for a later chapter. Begin with exercise 139.6, then complete exercise 139.9.

Exercise 139.6¶

★★☆ Derive the type of $\mathsf{zip}nab$ in example 139.8 step by step, naming the rule at each node, and then show that replacing $b$ by an array of declared length $m$ leaves no derivation. Identify the exact premise that fails.

Referenced from 3 locations

• Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation

Exercise 139.7¶

★★★ t-relax may be applied at any point, so a program has many typing derivations. Show that any two derivations of the same program give types that differ only in size information, and give two derivations of one program whose types are not syntactically equal.

Referenced from 2 locations

• Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation

Exercise 139.8¶

★★★ Admit empty arrays into definition 139.1. Show that clause 1 of proposition 139.13 becomes false, by exhibiting a value, a type and a witnessed variable for which no size can be extracted. Then propose the smallest change to definition 139.4 that restores it, and say what it costs at run time.

Referenced from 2 locations

• Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation

Exercise 139.9 — Practical: size-dependent checker and evaluator¶

★★★ Practical project.arr-size-checker Complete project arr-size-checker. Implement, for the frozen core of definition 139.1, (i) the typing rules of definition 139.3 including t-map’s side condition, t-let’s witness condition and t-coerce, (ii) the big-step evaluator of definition 139.4 with dynamic size matching and dynamic size checking, and (iii) the witness function of definition 139.2. The invariant the implementation must maintain is theorem 139.15 on every accepted input: whenever the checker accepts $e$ at $\mu$ and the evaluator produces $v$, the value must satisfy the size constraints $\mu$ names. Exclude empty arrays and failure propagation: either would be a separately proved extension beyond theorem 139.15. The frozen core has no $\mathsf{filter}$ and no recursion, so produce the escaping size of example 139.10 by relaxing a known size into an existential and unpacking it; record that this is weaker than a computation whose result length is genuinely unknown. The named cases print

dot-product: 32
mismatched-zip: rejected
unpacked-length: 3
unwitnessed-size: rejected
map-ragged: rejected

The checker is independent evidence for the frozen core; it does not prove theorem 139.15, implements none of section 139.5 or section 139.6, and — by remark 139.16 — says nothing about programs whose evaluation fails.

Referenced from 3 locations

• Typed Functional Array Languages: Shapes, Uniqueness, and Parallel Compilation