source: doc/theses/mike_brooks_MMath/array.tex@ e0350e0

\chapter{Array}
\label{c:Array}

Arrays in C are possibly the single most misunderstood and incorrectly used feature in the language, resulting in the largest proportion of runtime errors and security violations.
This chapter describes the new \CFA language and library features that introduce a length-checked array type, @array@, to the \CFA standard library~\cite{Cforall}.

Offering the @array@ type, as a distinct alternative to the C array, is consistent with \CFA's goal of backwards compatibility, \ie virtually all existing C (@gcc@) programs can be compiled by \CFA with only a small number of changes, similar to \CC (@g++@).
However, a few compatibility-breaking changes to the behaviour of the C array are necessary, both as an implementation convenience and to fix C's lax treatment of arrays.
Hence, the @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features, making it unnecessary to deal with every inherited complexity of the C array.


\section{Introduction}
\label{s:ArrayIntro}

The new \CFA array is declared by instantiating the generic @array@ type,
much like instantiating any other standard-library generic type (such as \CC @vector@),
though using a new style of generic parameter.
\begin{cfa}
@array( float, 99 )@ x;                                 $\C[2.5in]{// x contains 99 floats}$
\end{cfa}
Here, the arguments to the @array@ type are @float@ (element type) and @99@ (dimension).
When this type is used as a function parameter, the type-system requires the argument is a perfect match.
\begin{cfa}
void f( @array( float, 42 )@ & p ) {}   $\C{// p accepts 42 floats}$
f( x );                                                                 $\C{// statically rejected: type lengths are different, 99 != 42}$
test2.cfa:3:1 error: Invalid application of existing declaration(s) in expression.
Applying untyped:  Name: f ... to:  Name: x
\end{cfa}
Function @f@'s parameter expects an array with dimension 42, but the argument dimension 99 does not match.

A function can be polymorphic over @array@ arguments using the \CFA @forall@ declaration prefix.
\begin{cfa}
forall( T, @[N]@ )
void g( array( T, @N@ ) & p, int i ) {
        T elem = p[i];                                          $\C{// dynamically checked: requires 0 <= i < N}$
}
g( x, 0 );                                                              $\C{// T is float, N is 99, dynamic subscript check succeeds}$
g( x, 1000 );                                                   $\C{// T is float, N is 99, dynamic subscript check fails}$
Cforall Runtime error: subscript 1000 exceeds dimension range [0,99) $for$ array 0x555555558020.
\end{cfa}
Function @g@ takes an arbitrary type parameter @T@ and an unsigned integer \emph{dimension} @N@.
The dimension represents a to-be-determined number of elements, managed by the type system, where 0 represents an empty array.
The type system implicitly infers @float@ for @T@ and @99@ for @N@.
Furthermore, the runtime subscript @x[0]@ (parameter @i@ being @0@) in @g@ is valid because 0 is in the dimension range $[0,99)$ for argument @x@.
The call @g( x, 1000 )@ is also accepted at compile time.
However, the subscript, @x[1000]@, generates a runtime error, because @1000@ is outside the dimension range $[0,99)$ of argument @x@.
In general, the @forall( ..., [N] )@ participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and within a function.
The syntactic form is chosen to parallel other @forall@ forms:
\begin{cfa}
forall( @[N]@ ) ...     $\C{// dimension}$
forall( T ) ...         $\C{// value datatype}$
forall( T & ) ...       $\C{// opaque datatype}$
\end{cfa}
% The notation @array(thing, N)@ is a single-dimensional case, giving a generic type instance.

The generic @array@ type is comparable to the C array type, which \CFA inherits from C.
Their runtime characteristics are often identical, and some features are available in both.
For example, assume a caller has an argument that instantiates @N@ with 42.
\begin{cfa}
forall( [N] )
void f( ... ) {
        float x1[@N@];                                          $\C{// C array, no subscript checking}$
        array(float, N) x2;                                     $\C{// \CFA array, subscript checking}\CRT$
}
\end{cfa}
Both of the stack declared array variables, @x1@ and @x2@, have 42 elements, each element being a @float@.
The two variables have identical size and layout, with no additional ``bookkeeping'' allocations or headers.
The C array, @x1@, has no subscript checking, while \CFA array, @x2@, does.
Providing this explicit generic approach requires a significant extension to the \CFA type system to support a full-feature, safe, efficient (space and time) array-type, which forms the foundation for more complex array forms in \CFA.
In all following discussion, ``C array'' means types like @x1@ and ``\CFA array'' means types like @x2@.

A future goal is to provide the new @array@ features with syntax approaching C's (declaration style of @x1@).
Then, the library @array@ type could be removed, giving \CFA a largely uniform array type.
At present, the C-syntax @array@ is only partially supported, so the generic @array@ is used exclusively in the thesis.

My contributions in this chapter are:
\begin{enumerate}[leftmargin=*]
\item A type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@.
\item Provide a dimension/subscript-checked array-type in the \CFA standard library, where the array's length is statically managed and dynamically valued.
\item Provide argument/parameter passing safety for arrays and subscript safety.
\item Identify the interesting specific abilities available by the new @array@ type.
\item Where there is a gap concerning this feature's readiness for prime-time, identification of specific workable improvements that are likely to close the gap.
\end{enumerate}


\begin{comment}
\section{Dependent Typing}

General dependent typing allows a type system to encode arbitrary predicates, \eg behavioural specifications for functions, which is an anti-goal for my work.
Firstly, this application is strongly associated with pure functional languages,
where a characterization of the return value (giving it a precise type, generally dependent upon the parameters)
is a sufficient postcondition.
In an imperative language like C and \CFA, it is also necessary to discuss side effects, for which an even heavier formalism, like separation logic, is required.
Secondly, TODO: bash Rust.
TODO: cite the crap out of these claims.
\end{comment}


\section{Features Added}

This section shows more about using the \CFA array and dimension parameters, demonstrating syntax and semantics by way of motivating examples.
As stated, the core capability of the new array is tracking all dimensions within the type system, where dynamic dimensions are represented using type variables.

By declaring type variables at the front of object declarations, an array dimension is lexically referenceable where it is needed.
For example, a declaration can share one length, @N@, among a pair of parameters and return type, meaning the input arrays and return array are the same length.
\lstinput{10-17}{hello-array.cfa}
Function @f@ does a pointwise comparison of its two input arrays, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated @bool@ array.
The dynamic allocation of the @ret@ array uses the library @alloc@ function,
\begin{cfa}
forall( T & | sized(T) )
T * alloc() {
        return @(T *)@malloc( @sizeof(T)@ );
}
\end{cfa}
which captures the parameterized dimension information implicitly within its @sizeof@ determination, and casts the return type.
Note, @alloc@ only sees the whole type for its @T@, @array(bool, N)@, where this type's size is a computation based on @N@.
This example illustrates how the new @array@ type plugs into existing \CFA behaviour by implementing necessary \emph{sized} assertions needed by other types.
(\emph{sized} implies a concrete \vs abstract type with a runtime-available size, exposed as @sizeof@.)
As a result, there is significant programming safety by making the size accessible and implicit, compared with C's @calloc@ and non-array supporting @memalign@, which take an explicit length parameter not managed by the type system.

\begin{figure}
\lstinput{30-43}{hello-array.cfa}
\lstinput{45-48}{hello-array.cfa}
\caption{\lstinline{f} Example}
\label{f:fExample}
\end{figure}

\VRef[Figure]{f:fExample} shows an example using function @f@, illustrating how dynamic values are fed into the @array@ type.
Here, the dimension of arrays @x@, @y@, and @result@ is specified from a command-line value, @dim@, and these arrays are allocated on the stack.
Then the @x@ array is initialized with decreasing values, and the @y@ array with amounts offset by constant @0.005@, giving relative differences within tolerance initially and diverging for later values.
The program main is run (see figure bottom) with inputs @5@ and @7@ for sequence lengths.
The loops follow the familiar pattern of using the variable @dim@ to iterate through the arrays.
Most importantly, the type system implicitly captures @dim@ at the call of @f@ and makes it available throughout @f@ as @N@.
The example shows @dim@ adapting into a type-system managed length at the declarations of @x@, @y@, and @result@, @N@ adapting in the same way at @f@'s loop bound, and a pass-thru use of @dim@ at @f@'s declaration of @ret@.
Except for the lifetime-management issue of @result@, \ie explicit @free@, this program has eliminated both the syntactic and semantic problems associated with C arrays and their usage.
The result is a significant improvement in safety and usability.

In summary:
\begin{itemize}[leftmargin=*]
\item
@[N]@ within a @forall@ declares the type variable @N@ to be a managed length.
\item
@N@ can be used in an expression with type @size_t@ within the function body.
\item
The value of an @N@-expression is the acquired length, derived from the usage site, \ie generic declaration or function call.
\item
@array( thing, N0, N1, ... )@ is a multi-dimensional type wrapping $\prod_i N_i$ adjacent occurrences of @thing@-typed objects.
\end{itemize}

\VRef[Figure]{f:TemplateVsGenericType} shows @N@ is not the same as a @size_t@ declaration in a \CC \lstinline[language=C++]{template}.
\begin{enumerate}[leftmargin=*]
\item
The \CC template @N@ can only be a compile-time value, while the \CFA @N@ may be a runtime value.
\item
\CC does not allow a template function to be nested, while \CFA lets its polymorphic functions to be nested.
Hence, \CC precludes a simple form of information hiding.
\item
\label{p:DimensionPassing}
The \CC template @N@ must be passed explicitly at the call, unless @N@ has a default value, even when \CC can deduct the type of @T@.
The \CFA @N@ is part of the array type and passed implicitly at the call.
% fixed by comparing to std::array
% mycode/arrr/thesis-examples/check-peter/cs-cpp.cpp, v2
\item
\CC cannot have an array of references, but can have an array of @const@ pointers.
\CC has a (mistaken) belief that references are not objects, but pointers are objects.
In the \CC example, the arrays fall back on C arrays, which have a duality with references with respect to automatic dereferencing.
The \CFA array is a contiguous object with an address, which can be stored as a reference or pointer.
% not really about forall-N vs template-N
% any better CFA support is how Rob left references, not what Mike did to arrays
% https://stackoverflow.com/questions/1164266/why-are-arrays-of-references-illegal
% https://stackoverflow.com/questions/922360/why-cant-i-make-a-vector-of-references
\item
\label{p:ArrayCopy}
C/\CC arrays cannot be copied, while \CFA arrays can be copied, making them a first-class object (although array copy is often avoided for efficiency).
% fixed by comparing to std::array
% mycode/arrr/thesis-examples/check-peter/cs-cpp.cpp, v10
\end{enumerate}
The \CC template @array@ type mitigates points \VRef[]{p:DimensionPassing} and \VRef[]{p:ArrayCopy}, but it is also trying to accomplish a similar mechanism to \CFA @array@.

\begin{figure}
\begin{tabular}{@{}l@{\hspace{20pt}}l@{}}
\begin{c++}

@template< typename T, size_t N >@
void copy( T ret[@N@], T x[@N@] ) {
        for ( int i = 0; i < N; i += 1 ) ret[i] = x[i];
}
int main() {

        int ret[10], x[10];
        for ( int i = 0; i < 10; i += 1 ) x[i] = i;
        @copy<int, 10 >( ret, x );@
        for ( int i = 0; i < 10; i += 1 )
                cout << ret[i] << ' ';
        cout << endl;
}
\end{c++}
&
\begin{cfa}
int main() {
        @forall( T, [N] )@              // nested function
        void copy( array( T, @N@ ) & ret, array( T, @N@ ) & x ) {
                for ( i; N ) ret[i] = x[i];
        }

        const int n = promptForLength();
        array( int, n ) ret, x;
        for ( i; n ) x[i] = i;
        @copy( ret,  x );@
        for ( i; n )
                sout | ret[i] | nonl;
        sout | nl;
}
\end{cfa}
\end{tabular}
\caption{\lstinline{N}-style parameters, for \CC template \vs \CFA generic type }
\label{f:TemplateVsGenericType}
\end{figure}

Just as the first example in \VRef[Section]{s:ArrayIntro} shows a compile-time rejection of a length mismatch,
so are length mismatches stopped when they involve dimension parameters.
While \VRef[Figure]{f:fExample} shows successfully calling a function @f@ expecting two arrays of the same length,
\begin{cfa}
array( bool, N ) & f( array( float, N ) &, array( float, N ) & );
\end{cfa}
a static rejection occurs when attempting to call @f@ with arrays of differing lengths.
\lstinput[tabsize=1]{70-74}{hello-array.cfa}
When the argument lengths themselves are statically unknown,
the static check is conservative and, as always, \CFA's casting lets the programmer use knowledge not shared with the type system.
\begin{tabular}{@{\hspace{0.5in}}l@{\hspace{1in}}l@{}}
\lstinput{90-97}{hello-array.cfa}
&
\lstinput{110-117}{hello-array.cfa}
\end{tabular}

\noindent
This static check's full rules are presented in \VRef[Section]{s:ArrayTypingC}.

Orthogonally, the \CFA array type works within generic \emph{types}, \ie @forall@-on-@struct@.
The same argument safety and the associated implicit communication of array length occurs.
Preexisting \CFA allowed aggregate types to be generalized with type parameters, enabling parameterizing of element types.
This has been extended to allow parameterizing by dimension.
Doing so gives a refinement of C's ``flexible array member''~\cite[\S~6.7.2.1.18]{C11}.
\begin{cfa}
struct S {
        ...
        double d []; // incomplete array type => flexible array member
} * s = malloc( sizeof( struct S ) + sizeof( double [10] ) );
\end{cfa}
which creates a VLA of size 10 @double@s at the end of the structure.
A C flexible array member can only occur at the end of a structure;
\CFA allows length-parameterized array members to be nested at arbitrary locations, with intervening member declarations.
\lstinput{10-15}{hello-accordion.cfa}
The structure has course- and student-level metatdata (their respective field names) and a position-based preferences' matrix.
Its layout has the starting offset of @studentIds@ varying according to the generic parameter @C@, and the offset of @preferences@ varying according to both generic parameters.

\VRef[Figure]{f:checkExample} shows a program main using @School@ and results with different array sizes.
The @school@ variable holds many students' course-preference forms.
It is on the stack and its initialization does not use any casting or size arithmetic.
Both of these points are impossible with a C flexible array member.
When heap allocation is preferred, the original pattern still applies.
\begin{cfa}
School( classes, students ) * sp = alloc();
\end{cfa}
This ability to avoid casting and size arithmetic improves safety and usability over C flexible array members.
Finally, inputs and outputs are given at the bottom for different sized schools.
The example program prints the courses in each student's preferred order, all using the looked-up display names.

\begin{figure}
\begin{cquote}
\lstinput{50-55}{hello-accordion.cfa}
\lstinput{90-98}{hello-accordion.cfa}
\ \\
@$ cat school1@
\lstinput{}{school1}

@$ ./a.out < school1@
\lstinput{}{school1.out}

@$ cat school2@
\lstinput{}{school2}

@$ ./a.out < school2@
\lstinput{}{school2.out}
\end{cquote}

\caption{\lstinline{School} Example, Input and Output}
\label{f:checkExample}
\end{figure}

When a function operates on a @School@ structure, the type system handles its memory layout transparently.
\lstinput{30-37}{hello-accordion.cfa}
In the example, function @getPref@ returns, for the student at position @is@, what is the position of their @pref@\textsuperscript{th}-favoured class?


\section{Dimension Parameter Implementation}

The core of the preexisting \CFA compiler already had the ``heavy equipment'' needed to provide the feature set just reviewed (up to bugs in cases not yet exercised).
To apply this equipment in tracking array lengths, I encoded a dimension (array's length) as a type.
The type in question does not describe any data that the program actually uses at runtime.
It simply carries information through intermediate stages of \CFA-to-C lowering.
And this type takes a form such that, once \emph{it} gets lowered, the result does the right thing.
This new dimension type, encoding the array dimension within it, is the first limited \newterm{dependent type}~\cite{DependentType} added to the \CFA type-system and is used at appropriate points during type resolution.

Furthermore, the @array@ type itself is really ``icing on the cake.''
Presenting its full version is deferred until \VRef[Section]{s:ArrayMdImpl}
(where added complexity needed for multiple dimensions is considered).
But simplifications close enough for the present discussion are:
\begin{cfa}
forall( [N] )
struct array_1d_float {
        float items[N];
};
forall( T, [N] )
struct array_1d_T {
        T items[N];
};
\end{cfa}
These two structure patterns, plus a subscript operator, is all that @array@ provides.
My main work is letting a programmer define such a structure (one whose type is parameterized by @[N]@) and functions that operate on it (these being similarly parameterized).

The repurposed heavy equipment is
\begin{itemize}[leftmargin=*]
\item
        Resolver provided values for a used declaration's type-system variables, gathered from type information in scope at the usage site.
\item
        The box pass, encoding information about type parameters into ``extra'' regular parameters/arguments on declarations and calls.
        Notably, it conveys the size of a type @foo@ as a @__sizeof_foo@ parameter, and rewrites the @sizeof(foo)@ expression as @__sizeof_foo@, \ie a use of the parameter.
\end{itemize}

The rules for resolution had to be restricted slightly, in order to achieve important refusal cases.
This work is detailed in \VRef[Section]{s:ArrayTypingC}.
However, the resolution--boxing scheme, in its preexisting state, was already equipped to work on (desugared) dimension parameters.
The following discussion explains the desugaring and how correctly lowered code results.

A simpler structure, and a toy function on it, demonstrate what is needed for the encoding.
\begin{cfa}
forall( [@N@] ) { $\C{// [1]}$
        struct thing {};
        void f( thing(@N@) ) { sout | @N@; } $\C{// [2], [3]}$
}
int main() {
        thing( @10@ ) x;  f( x );  $\C{// prints 10, [4]}$
        thing( @100@ ) y;  f( y );  $\C{// prints 100}$
}
\end{cfa}
This example has:
\begin{enumerate}[leftmargin=*]
\item
        The symbol @N@ being declared as a type variable (a variable of the type system).
\item
        The symbol @N@ being used to parameterize a type.
\item
        The symbol @N@ being used as an expression (value).
\item
        A value like 10 being used as an argument to the parameter @N@.
\end{enumerate}
The chosen solution is to encode the value @N@ \emph{as a type}, so items 1 and 2 are immediately available for free.
Item 3 needs a way to recover the encoded value from a (valid) type (and to reject invalid types occurring here).
Item 4 needs a way to produce a type that encodes the given value.

Because the box pass handles a type's size as its main datum, the encoding is chosen to use it.
The production and recovery are then straightforward.
\begin{itemize}[leftmargin=*]
\item
        The value $n$ is encoded as a type whose size is $n$.
\item
        Given a dimension expression $e$, produce an internal type @char[@$e$@]@ to represent it.
        If $e$ evaluates to $n$ then the encoded type has size $n$.
\item
        Given a type $T$ (produced by these rules), recover the value that it represents with the expression @sizeof(@$T$@)@.
        If $T$ has size $n$ then the recovery expression evaluates to $n$.
\end{itemize}

This desugaring is applied in a translation step before the resolver.
The ``validate'' pass hosts it, along with several other canonicalizing and desugaring transformations (the pass's name notwithstanding).
The running example is lowered to:
\begin{cfa}
forall( @N *@ ) { $\C{// [1]}$
        struct thing {};
        void f( thing(@N@) ) { sout | @sizeof(N)@; } $\C{// [2], [3]}$
}
int main() {
        thing( @char[10]@ ) x;  f( x );  $\C{// prints 10, [4]}$
        thing( @char[100]@ ) y;  f( y );  $\C{// prints 100}$
}
\end{cfa}
Observe:
\begin{enumerate}[leftmargin=*]
\item
        @N@ is now declared to be a type.
        It is declared to be \emph{sized} (by the @*@), meaning that the box pass shall do its @sizeof(N)@$\rightarrow$@__sizeof_N@ extra parameter and expression translation.
\item
        @thing(N)@ is a type; the argument to the generic @thing@ is a type (type variable).
\item
        The @sout...@ expression (being an application of the @?|?@ operator) has a second argument that is an ordinary expression.
\item
        The type of variable @x@ is another @thing(-)@ type; the argument to the generic @thing@ is a type (array type of bytes, @char[@$e$@]@).
\end{enumerate}

From this point, preexisting \CFA compilation takes over lowering it the rest of the way to C.
Here the result shows only the relevant changes of the box pass (as informed by the resolver), leaving the rest unadulterated:
\begin{cfa}
// [1]
void f( size_t __sizeof_N, @void *@ ) { sout | @__sizeof_N@; } $\C{// [2], [3]}$
int main() {
        struct __conc_thing_10 {} x;  f( @10@, &x );  $\C{// prints 10, [4]}$
        struct __conc_thing_100 {} y;  f( @100@, &y );  $\C{// prints 100}$
}
\end{cfa}
Observe:
\begin{enumerate}[leftmargin=*]
\item
        The type parameter @N@ is gone.
\item
        The type @thing(N)@ is (replaced by @void *@, but thereby effectively) gone.
\item
        The @sout...@ expression (being an application of the @?|?@ operator) has a regular variable (parameter) usage for its second argument.
\item
        Information about the particular @thing@ instantiation (value 10) is moved, from the type, to a regular function-call argument.
\end{enumerate}
At the end of the desugaring and downstream processing, the original C idiom of ``pass both a length parameter and a pointer'' has been reconstructed.
In the programmer-written form, only the @thing@ is passed.
The compiler's action produces the more complex form, which if handwritten, would be error-prone.

At the compiler front end, the parsing changes AST schema extensions and validation rules for enabling the sugared user input.
\begin{itemize}[leftmargin=*]
\item
        Recognize the form @[N]@ as a type-variable declaration within a @forall@.
\item
        Have the new brand of type-variable, \emph{Dimension}, in the AST form of a type-variable, to represent one parsed from @[-]@.
\item
        Allow a type variable to occur in an expression.  Validate (after parsing) that only dimension-branded type-variables are used here.
\item
        Allow an expression to occur in type-argument position.  Brand the resulting type argument as a dimension.
\item
        Validate (after parsing), on a generic-type usage, \eg the type part of the declaration
        \begin{cfa}
        array_1d( foo, bar ) x;
        \end{cfa}
        \vspace*{-10pt}
        that the brands on the generic arguments match the brands of the declared type variables.
        Here, that @foo@ is a type and @bar@ is a dimension.
\end{itemize}


\section{Typing of C Arrays}
\label{s:ArrayTypingC}

Essential in giving a guarantee of accurate length is the compiler's ability to reject a program that presumes to mishandle length.
By contrast, most discussion so far deals with communicating length, from one party who knows it, to another willing to work with any given length.
For scenarios where the concern is a mishandled length, the interaction is between two parties who both claim to know something about it.

C and \CFA can check when working with two static values.
\begin{cfa}
enum { n = 42 };
float x[@n@];   // or just 42
float (*xp1)[@42@] = &x;    // accept
float (*xp2)[@999@] = &x;   // reject
warning: initialization of 'float (*)[999]' from incompatible pointer type 'float (*)[42]'
\end{cfa}
When a variable is involved, C and \CFA take two different approaches.
Today's C compilers accept the following without warning.
\begin{cfa}
static const int n = 42;
float x[@n@];
float (* xp)[@999@] = &x; $\C{// should be static rejection here}$
(*xp)[@500@]; $\C{// in "bound"?}$
\end{cfa}
Here, the array @x@ has length 42, while a pointer to it (@xp@) claims length 999.
So, while the subscript of @xp@ at position 500 is out of bound with its referent @x@,
the access appears in-bound of the type information available on @xp@.
In fact, length is being mishandled in the previous step, where the type-carried length information on @x@ is not compatible with that of @xp@.

In \CFA, I choose to reject this C example at the point where the type-carried length information on @x@ is not compatible with that of @xp@, and correspondingly, its array counterpart at the same location:
\begin{cfa}
static const int n = 42;
array( float, @n@ ) x;
array( float, @999@ ) * xp = &x; $\C{// static rejection here}$
(*xp)[@500@]; $\C{// runtime check passes}$
\end{cfa}
The way the \CFA array is implemented, the type analysis for this case reduces to a case similar to the earlier C version.
The \CFA compiler's compatibility analysis proceeds as:
\begin{itemize}[parsep=0pt]
\item
        Is @array( float, 999 )@ type-compatible with @array( float, n )@?
\item
        Is desugared @array( float, char[999] )@ type-compatible with desugared @array( float, char[n] )@?
%               \footnote{
%               Here, \lstinline{arrayX} represents the type that results from desugaring the \lstinline{array} type into a type whose generic parameters are all types.
%               This presentation elides the noisy fact that \lstinline{array} is actually a macro for something bigger;
%               the reduction to \lstinline{char [-]} still proceeds as sketched.}
\item
        Is internal type @char[999]@ type-compatible with internal type @char[n]@?
\end{itemize}
The answer is false because, in general, the value of @n@ is unknown at compile time, and hence, an error is raised.
For safety, it makes sense to reject the corresponding C case, which is a non-backwards compatible change.
There are two mitigations for this incompatibility.

First, a simple recourse is available in a situation where @n@ is \emph{known} to be 999 by using a cast.
\begin{cfa}
float (* xp)[999] = @(float (*)[999])@&x;
\end{cfa}
The cast means the programmer has accepted blame.
Moreover, the cast is ``eye candy'' marking where the unchecked length knowledge is used.
Therefore, a program being onboarded to \CFA requires some upgrading to satisfy the \CFA rules (and arguably become clearer), without giving up its validity to a plain C compiler.
Second, the incompatibility only affects types like pointer-to-array, which are infrequently used in C.
The more common C idiom for aliasing an array is to use a pointer-to-first-element type, which does not participate in the \CFA array's length checking.\footnote{
        Notably, the desugaring of the \lstinline{array} type avoids letting any \lstinline{-[-]} type decay,
        in order to preserve the length information that powers runtime bound-checking.}
Therefore, the need to upgrade legacy C code is low.
Finally, if this incompatibility is a problem onboarding C programs to \CFA, it is should be possible to change the C type check to a warning rather than an error, acting as a \emph{lint} of the original code for a missing type annotation.

To handle two occurrences of the same variable, more information is needed, \eg, this is fine,
\begin{cfa}
int n = 42;
float x[@n@];
float (*xp)[@n@] = x;   // accept
\end{cfa}
where @n@ remains fixed across a contiguous declaration context.
However, intervening dynamic statement cause failures.
\begin{cfa}
int n = 42;
float x[@n@];
@n@ = 999; // dynamic change
float (*xp)[@n@] = x;   // reject
\end{cfa}
However, side-effects can occur in a contiguous declaration context.
\begin{cquote}
\setlength{\tabcolsep}{20pt}
\begin{tabular}{@{}ll@{}}
\begin{cfa}
// compile unit 1
extern int @n@;
extern float g();
void f() {
        float x[@n@] = { g() };
        float (*xp)[@n@] = x;   // reject
}
\end{cfa}
&
\begin{cfa}
// compile unit 2
int @n@ = 42;
void g() {
        @n@ = 99;
}


\end{cfa}
\end{tabular}
\end{cquote}
The issue here is that knowledge needed to make a correct decision is hidden by separate compilation.
Even within a translation unit, static analysis might not be able to provide all the information.
However, if the example uses @const@, the check is possible.
\begin{cquote}
\setlength{\tabcolsep}{20pt}
\begin{tabular}{@{}ll@{}}
\begin{cfa}
// compile unit 1
extern @const@ int n;
extern float g();
void f() {
        float x[n] = { g() };
        float (*xp)[n] = x;   // reject
}
\end{cfa}
&
\begin{cfa}
// compile unit 2
@const@ int n = 42;
void g() {
        @n = 99@; // allowed
}


\end{cfa}
\end{tabular}
\end{cquote}

In summary, the new rules classify expressions into three groups:
\begin{description}
\item[Statically Evaluable]
        Expressions for which a specific value can be calculated (conservatively) at compile-time.
        A preexisting \CFA compiler module defines which literals, enumerators, and expressions qualify and evaluates them.
\item[Dynamic but Stable]
        The value of a variable declared as @const@, including a @const@ parameter.
\item[Potentially Unstable]
        The catch-all category.  Notable examples include:
        any function-call result, @float x[foo()]@, the particular function-call result that is a pointer dereference, @void f(const int * n)@ @{ float x[*n]; }@, and any use of a reference-typed variable.
\end{description}
Within these groups, my \CFA rules are:
\begin{itemize}[leftmargin=*]
\item
        Accept a Statically Evaluable pair, if both expressions have the same value.
        Notably, this rule allows a literal to match with an enumeration value, based on the value.
\item
        Accept a Dynamic but Stable pair, if both expressions are written out the same, \eg refers to the same variable declaration.
\item
        Otherwise, reject.
        Notably, reject all pairs from the Potentially Unstable group and all pairs that cross groups.
\end{itemize}
The traditional C rules are:
\begin{itemize}[leftmargin=*]
\item
        Reject a Statically Evaluable pair, if the expressions have two different values.
\item
        Otherwise, accept.
\end{itemize}
\VRef[Figure]{f:DimexprRuleCompare} gives a case-by-case comparison of the consequences of these rule sets.
It demonstrates that the \CFA false alarms occur in the same cases as C treats unsafe.
It also shows that C-incompatibilities only occur in cases that C treats unsafe.

\begin{figure}
        \newcommand{\falsealarm}{{\color{blue}\small{*}}}
        \newcommand{\allowmisuse}{{\color{red}\textbf{!}}}

        \begin{tabular}{@{}l@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c@{\hspace{8pt}}c@{\hspace{16pt}}c}
         & \multicolumn{2}{c}{\underline{Values Equal}}
         & \multicolumn{2}{c}{\underline{Values Unequal}} 
         & \\
        \textbf{Case}                                & C      & \CFA                & C                      & \CFA    & Compat. \\
        Both Statically Evaluable, Same Symbol       & Accept & Accept              &                        &         & \cmark \\
        Both Statically Evaluable, Different Symbols & Accept & Accept              & Reject                 & Reject  & \cmark \\
        Both Dynamic but Stable, Same Symbol         & Accept & Accept              &                        &         & \cmark \\
        Both Dynamic but Stable, Different Symbols   & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
        Both Potentially Unstable, Same Symbol       & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark \\
        Any other grouping, Different Symbol         & Accept & Reject\,\falsealarm & Accept\,\allowmisuse   & Reject  & \xmark
        \end{tabular}

        \medskip
        \noindent\textbf{Legend}
        \begin{itemize}[leftmargin=*]
        \item
                Each row gives the treatment of a test harness of the form
                \begin{cfa}
                float x[ expr1 ];
                float (*xp)[ expr2 ] = &x;
                \end{cfa}
                \vspace*{-10pt}
                where \lstinline{expr1} and \lstinline{expr2} are meta-variables varying according to the row's Case.
                Each row's claim applies to other harnesses too, including,
                \begin{itemize}[leftmargin=*]
                \item
                        calling a function with a parameter like \lstinline{x} and an argument of the \lstinline{xp} type,
                \item
                        assignment in place of initialization,
                \item
                        using references in place of pointers, and
                \item
                        for the \CFA array, calling a polymorphic function on two \lstinline{T}-typed parameters with \lstinline{&x}- and \lstinline{xp}-typed arguments.
                \end{itemize}
        \item
                Each case's claim is symmetric (swapping \lstinline{expr1} with \lstinline{expr2} has no effect),
                even though most test harnesses are asymmetric.
        \item
                The table treats symbolic identity (Same/Different on rows)
                apart from value equality (Equal/Unequal on columns).
                \begin{itemize}[leftmargin=*]
                \item
                        The expressions \lstinline{1}, \lstinline{0+1} and \lstinline{n}
                        (where \lstinline{n} is a variable with value 1),
                        are all different symbols with the value 1.
                \item
                        The column distinction expresses ground truth about whether an omniscient analysis should accept or reject.
                \item
                        The row distinction expresses the simple static factors used by today's analyses.
                \end{itemize}
        \item
                Accordingly, every Reject under Values Equal is a false alarm (\falsealarm),
                while every Accept under Values Unequal is an allowed misuse (\allowmisuse).
        \end{itemize}

        \caption{Case comparison for array type compatibility, given pairs of dimension expressions.}
        \label{f:DimexprRuleCompare}
\end{figure}

\begin{comment}
Given that the above check
\begin{itemize}
        \item
        Is internal type @char[999]@ type-compatible with internal type @char[n]@?
\end{itemize}
answers false, discussion turns to how I got the \CFA compiler to produce this answer.
In its preexisting form, the type system had a buggy approximation of the C rules.
To implement the new \CFA rules, I added one further step.
\begin{itemize}
        \item
                Is @999@ compatible with @n@?
\end{itemize}
This question applies to a pair of expressions, where the earlier question applies to types.
An expression-compatibility question is a new addition to the \CFA compiler, and occurs in the context of dimension expressions, and possibly enumerations assigns, which must be unique.

% TODO: ensure these compiler implementation matters are treated under \CFA compiler background: type unification, cost calculation, GenPoly.

The relevant technical component of the \CFA compiler is the standard type-unification within the type resolver.
\begin{cfa}
example
\end{cfa}
I added rules for continuing this unification into expressions that occur within types.
It is still fundamentally doing \emph{type} unification because it is participating in binding type variables, and not participating in binding any variables that stand in for expression fragments (for there is no such sort of variable in \CFA's analysis.)
An unfortunate fact about the \CFA compiler's preexisting implementation is that type unification suffers from two forms of duplication.

In detail, the first duplication has (many of) the unification rules stated twice.
As a result, my additions for dimension expressions are stated twice.
The extra statement of the rules occurs in the @GenPoly@ module, where concrete types like @array( int, 5 )@\footnote{
        Again, the presentation is simplified
        by leaving the \lstinline{array} macro unexpanded.}
are lowered into corresponding C types @struct __conc_array_1234@ (the suffix being a generated index).
In this case, the struct's definition contains fields that hardcode the argument values of @float@ and @5@.
The next time an @array( -, - )@ concrete instance is encountered, it checks if the previous @struct __conc_array_1234@ is suitable for it.
Yes, for another occurrence of @array( int, 5 )@;
no, for examples like @array( int, 42 )@ or @array( rational(int), 5 )@.
In the first example, it must reject the reuse hypothesis for a dimension-@5@ and a dimension-@42@ instance.

The second duplication has unification (proper) being invoked at two stages of expression resolution.
As a result, my added rule set needs to handle more cases than the preceding discussion motivates.
In the program
\begin{cfa}
void @f@( double ); // overload 
forall( T & ) void @f@( T & ); // overload 
void g( int n ) {
        array( float, n + 1 ) x;
        f(x);   // overloaded
}
\end{cfa}
when resolving a function call to @g@, the first unification stage compares the type @T@ of the parameter with @array( float, n + 1 )@, of the argument.
\PAB{TODO: finish.}

The actual rules for comparing two dimension expressions are conservative.
To answer, ``yes, consider this pair of expressions to be matching,''
is to imply, ``all else being equal, allow an array with length calculated by $e_1$
to be passed to a function expecting a length-$e_2$ array.''\footnote{
        TODO: Deal with directionality, that I'm doing exact-match, no ``at least as long as,'' no subtyping.
        Should it be an earlier scoping principle?  Feels like it should matter in more places than here.}
So, a ``yes'' answer must represent a guarantee that both expressions evaluate the
same result, while a ``no'' can tolerate ``they might, but we're not sure'',
provided that practical recourses are available
to let programmers express better knowledge.
The new rule-set in the current release is, in fact, extremely conservative.
I chose to keep things simple,
and allow future needs to drive adding additional complexity, within the new framework.

For starters, the original motivating example's rejection is not based on knowledge that the @xp@ length of (the literal) 999 is value-unequal to the (obvious) runtime value of the variable @n@, which is the @x@ length.
Rather, the analysis assumes a variable's value can be anything, and so there can be no guarantee that its value is 999.
So, a variable and a literal can never match.

TODO: Discuss the interaction of this dimension hoisting with the challenge of extra unification for cost calculation
\end{comment}

The conservatism of the new rule set can leave a programmer needing a recourse, when needing to use a dimension expression whose stability argument is more subtle than current-state analysis.
This recourse is to declare an explicit constant for the dimension value.
Consider these two dimension expressions, whose uses are rejected by the blunt current-state rules:
\begin{cfa}
void f( int @&@ nr, @const@ int nv ) {
        float x[@nr@];
        float (*xp)[@nr@] = &x;   // reject: nr varying (no references)
        float y[@nv + 1@];
        float (*yp)[@nv + 1@] = &y;   // reject: ?+? unpredictable (no functions)
}
\end{cfa}
Yet, both dimension expressions are reused safely.
The @nr@ reference is never written, not volatile meaning no implicit code (load) between declarations, and control does not leave the function between the uses.
As well, the build-in @?+?@ function is predictable.
To make these cases work, the programmer must add the follow constant declarations (cast does not work):
\begin{cfa}
void f( int & nr, const int nv ) {
        @const int nx@ = nr;
        float x[nx];
        float (*xp)[nx] = & x;   // accept
        @const int ny@ = nv + 1;
        float y[ny];
        float (*yp)[ny] = & y;   // accept
}
\end{cfa}
The result is the originally intended semantics,
achieved by adding a superfluous ``snapshot it as of now'' directive.

The snapshot trick is also used by the \CFA translation, though to achieve a different outcome.
Rather obviously, every array must be subscriptable, even a bizarre one:
\begin{cfa}
array( float, @rand(10)@ ) x;
x[@0@];  // 10% chance of bound-check failure
\end{cfa}
Less obvious is that the mechanism of subscripting is a function call, which must communicate length accurately.
The bound-check above (callee logic) must use the actual allocated length of @x@, without mistakenly reevaluating the dimension expression, @rand(10)@.
Adjusting the example to make the function's use of length more explicit:
\begin{cfa}
forall( T * )
void f( T * x ) { sout | sizeof( *x ); }
float x[ rand(10) ];
f( x );
\end{cfa}
Considering that the partly translated function declaration is, loosely,
\begin{cfa}
void f( size_t __sizeof_T, void * x ) { sout | __sizeof_T; }
\end{cfa}
the translation calls the dimension argument twice:
\begin{cfa}
float x[ rand(10) ];
f( rand(10), &x );
\end{cfa}
The correct form is:
\begin{cfa}
size_t __dim_x = rand(10);
float x[ __dim_x ];
f( __dim_x, &x );
\end{cfa}
Dimension hoisting already existed in the \CFA compiler.
But its was buggy, particularly with determining, ``Can hoisting the expression be skipped here?'', for skipping this hoisting is clearly desirable in some cases.
For example, when a programmer has already hoisted to perform an optimization to prelude duplicate code (expression) and/or expression evaluation.
In the new implementation, these cases are correct, harmonized with the accept/reject criteria.


\section{Multidimensional Array Implementation}
\label{s:ArrayMdImpl}

A multidimensional array implementation has three relevant levels of abstraction, from highest to lowest, where the array occupies \emph{contiguous memory}.
\begin{enumerate}[leftmargin=*]
\item
Flexible-stride memory:
this model has complete independence between subscripting ordering and memory layout, offering the ability to slice by (provide an index for) any dimension, \eg slice a plane, row, or column, \eg @c[3][*][*]@, @c[3][4][*]@, @c[3][*][5]@.
\item
Fixed-stride memory:
this model binds the first subscript and the first memory layout dimension, offering the ability to slice by (provide an index for) only the coarsest dimension, @m[row][*]@ or @c[plane][*][*]@, \eg slice only by row (2D) or plane (3D).
After which, subscripting and memory layout are independent.
\item
Explicit-displacement memory:
this model has no awareness of dimensions just the ability to access memory at a distance from a reference point (base-displacement addressing), \eg @x + 23@ or @x[23}@ $\Rightarrow$ 23rd element from the start of @x@.
A programmer must manually build any notion of dimensions using other tools;
hence, this style is not offering multidimensional arrays \see{\VRef[Figure]{f:FixedVariable} right example}.
\end{enumerate}

There is some debate as to whether the abstraction point ordering above goes $\{1, 2\} < 3$, rather than my numerically-ordering.
That is, styles 1 and 2 are at the same abstraction level, with 3 offering a limited set of functionality.
I chose to build the \CFA style-1 array upon a style-2 abstraction.
(Justification of the decision follows, after the description of the design.)

Style 3 is the inevitable target of any array implementation.
The hardware offers this model to the C compiler, with bytes as the unit of displacement.
C offers this model to its programmer as pointer arithmetic, with arbitrary sizes as the unit.
Casting a multidimensional array as a single-dimensional array/pointer, then using @x[i]@ syntax to access its elements, is still a form of pointer arithmetic.

Now stepping into the implementation of \CFA's new type-1 multidimensional arrays in terms of C's existing type-2 multidimensional arrays, it helps to clarify that even the interface is quite low-level.
A C/\CFA array interface includes the resulting memory layout.
The defining requirement of a type-2 system is the ability to slice a column from a column-finest matrix.
The required memory shape of such a slice is fixed, before any discussion of implementation.
The implementation presented here is how the \CFA array-library wrangles the C type system, to make it do memory steps that are consistent with this layout while not affecting legacy C programs.
% TODO: do I have/need a presentation of just this layout, just the semantics of -[all]?

The new \CFA standard-library @array@-datatype supports richer multidimensional features than C.
The new array implementation follows C's contiguous approach, \ie @float [r][c]@, with one contiguous object subscripted by coarsely-strided dimensions directly wrapping finely-strided dimensions.
Beyond what C's array type offers, the new array brings direct support for working with a noncontiguous array slice, allowing a program to work with dimension subscripts given in a non-physical order.

The following examples use the matrix declaration @array( float, 5, 7 ) m@, loaded with values incremented by $0.1$, when stepping across the length-7 finely-strided column dimension, and stepping across the length-5 coarsely-strided row dimension.
\par
\mbox{\lstinput{121-126}{hello-md.cfa}}
\par\noindent
The memory layout is 35 contiguous elements with strictly increasing addresses.

A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays.
As for the C array, a lesser-dimensional array reference can be bound to the result of subscripting a greater-dimensional array by a prefix of its dimensions, \eg @m[2]@, giving the third row.
This action first subscripts away the most coarsely strided dimensions, leaving a result that expects to be subscripted by the more finely strided dimensions, \eg @m[2][3]@, giving the value @2.3@.
The following is an example slicing a row.
\lstinput{60-64}{hello-md.cfa}
\lstinput[aboveskip=0pt]{140-140}{hello-md.cfa}

However, function @print1d@ is asserting too much knowledge about its parameter @r@ for printing either a row slice or a column slice.
Specifically, declaring the parameter @r@ with type @array@ means that @r@ is contiguous, which is unnecessarily restrictive.
That is, @r@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@) with managed length @N@.
The new-array library provides the trait @ar@, so-defined.
With it, the original declaration can be generalized with the same body.
\lstinput{43-44}{hello-md.cfa}
\lstinput[aboveskip=0pt]{145-145}{hello-md.cfa}
The nontrivial slicing in this example now allows passing a \emph{noncontiguous} slice to @print1d@, where the new-array library provides a ``subscript by all'' operation for this purpose.
In a multi-dimensional subscript operation, any dimension given as @all@ is a placeholder, \ie ``not yet subscripted by a value'', waiting for such a value, implementing the @ar@ trait.
\lstinput{150-151}{hello-md.cfa}

The example shows @x[2]@ and @x[[2, all]]@ both refer to the same, ``2.*'' slice.
Indeed, the various @print1d@ calls under discussion access the entry with value @2.3@ as @x[2][3]@, @x[[2,all]][3]@, and @x[[all,3]][2]@.
This design preserves (and extends) C array semantics by defining @x[[i,j]]@ to be @x[i][j]@ for numeric subscripts, but also for ``subscripting by all''.
That is:
\begin{cquote}
\begin{tabular}{@{}cccccl@{}}
@x[[2,all]][3]@ & $\equiv$      & @x[2][all][3]@  & $\equiv$    & @x[2][3]@  & (here, @all@ is redundant)  \\
@x[[all,3]][2]@ & $\equiv$      & @x[all][3][2]@  & $\equiv$    & @x[2][3]@  & (here, @all@ is effective)
\end{tabular}
\end{cquote}

Narrating progress through each of the @-[-][-][-]@\footnote{
The first ``\lstinline{-}'' is a variable expression and the remaining ``\lstinline{-}'' are subscript expressions.}
expressions gives, firstly, a definition of @-[all]@, and secondly, a generalization of C's @-[i]@.
Where @all@ is redundant:
\begin{cquote}
\begin{tabular}{@{}ll@{}}
@x@  & 2-dimensional, want subscripts for coarse then fine \\
@x[2]@  & 1-dimensional, want subscript for fine; lock coarse == 2 \\
@x[2][all]@  & 1-dimensional, want subscript for fine \\
@x[2][all][3]@  & 0-dimensional; lock fine == 3
\end{tabular}
\end{cquote}
Where @all@ is effective:
\begin{cquote}
\begin{tabular}{@{}ll@{}}
@x@  & 2-dimensional, want subscripts for coarse then fine \\
@x[all]@  & 2-dimensional, want subscripts for fine then coarse \\
@x[all][3]@  & 1-dimensional, want subscript for coarse; lock fine == 3 \\
@x[all][3][2]@  & 0-dimensional; lock coarse == 2
\end{tabular}
\end{cquote}
The semantics of @-[all]@ is to dequeue from the front of the ``want subscripts'' list and re-enqueue at its back.
For example, in a two dimensional matrix, this semantics conceptually transposes the matrix by reversing the subscripts.
The semantics of @-[i]@ is to dequeue from the front of the ``want subscripts'' list and lock its value to be @i@.

Contiguous arrays, and slices of them, are all represented by the same underlying parameterized type, which includes stride information in its metatdata.
The \lstinline{-[all]} operation takes subscripts, \eg @x[2][all]@, @x[all][3]@, \etc, and converts (transposes) from the base reference @x[all]@ to a specific reference of the appropriate form.
The running example's @all@-effective step, stated more concretely, is:
\begin{cquote}
\begin{tabular}{@{}ll@{}}
@x@       & : 5 of ( 7 of @float@ each spaced 1 @float@ apart ) each spaced 7 @floats@ apart \\
@x[all]@  & : 7 of ( 5 of @float@ each spaced 7 @float@s apart ) each spaced 1 @float@ apart
\end{tabular}
\end{cquote}

\begin{figure}
\includegraphics{measuring-like-layout}
\caption{Visualization of subscripting by value and by \lstinline[language=CFA]{all}, for \lstinline{x} of type \lstinline{array( float, 5, 7 )} understood as 5 rows by 7 columns.
The horizontal layout represents contiguous memory addresses while the vertical layout is conceptual.
The vertical shaded band highlights the location of the targeted element, 2.3.
Any such vertical slice contains various interpretations of a single address.}
\label{fig:subscr-all}
\end{figure}

\VRef[Figure]{fig:subscr-all} shows one element (in the white band) accessed two different ways: as @x[2][3]@ and as @x[all][3][2]@.
In both cases, subscript 2 selects from the coarser dimension (rows of @x@),
while subscript 3 selects from the finer dimension (columns of @x@).
The figure illustrates the value of each subexpression, comparing how numeric subscripting proceeds from @x@, \vs from @x[all]@.
Proceeding from @x@ gives the numeric indices as coarse then fine, while proceeding from @x[all]@ gives them fine then coarse.
These two starting expressions, which are the example's only multidimensional subexpressions
(those that received zero numeric indices so far), are illustrated with vertical steps where a \emph{first} numeric index would select.

The figure's presentation offers an intuition answer to: What is an atomic element of @x[all]@?
From there, @x[all]@ itself is simply a two-dimensional array, in the strict C sense, of these building blocks.
An atom (like the bottommost value, @x[all][3][2]@), is the contained value (in the square box)
and a lie about its size (the left diagonal above it, growing upward).
An array of these atoms (like the intermediate @x[all][3]@) is just a contiguous arrangement of them, done according to their size;
call such an array a column.
A column is almost ready to be arranged into a matrix;
it is the \emph{contained value} of the next-level building block, but another lie about size is required.
At first, an atom needs to be arranged as if it were bigger, but now a column needs to be arranged as if it is smaller (the left diagonal above it, shrinking upward).
These lying columns, arranged contiguously according to their size (as announced) form the matrix @x[all]@.
Because @x[all]@ takes indices, first for the fine stride, then for the coarse stride, it achieves the requirement of representing the transpose of @x@.
Yet every time the programmer presents an index, a C-array subscript is achieving the offset calculation.

In the @x[all]@ case, after the finely strided subscript is done (column 3 is selected),
the locations referenced by the coarse subscript options (rows 0..4) are offset by 3 floats,
compared with where analogous rows appear when the row-level option is presented for @x@.
For example, in \lstinline{x[all]}, the shaded band and its immediate values to the left touches atoms 2.3, 2.0, 2.1, 2.2, 1.4, 1.5 and 1.6.
But only the atom 2.3 is storing its value there.
The rest are lying about (conflicting) claims on this location, but never exercising these alleged claims.

Lying is implemented as casting.
The arrangement just described is implemented in the structure @arpk@.
This structure uses one type in its internal field declaration and offers a different type as the return of its subscript operator.
The field within is a plain-C array of the fictional type, which is 7 floats long for @x[all][3][2]@ and 1 float long for @x[all][3]@.
The subscript operator presents what is really inside, by casting to the type below the left diagonal of the lie.

%  Does x[all] have to lie too?  The picture currently glosses over how it it advertises a size of 7 floats.  I'm leaving that as an edge case benignly misrepresented in the picture.  Edge cases only have to be handled right in the code.

Casting, overlapping, and lying are unsafe.
The mission is to implement a style-1 feature in the type system for safe use by a programmer.
The offered style-1 system is allowed to be internally unsafe,
just as C's implementation of a style-2 system (upon a style-3 system) is unsafe within, even when the programmer is using it without casts or pointer arithmetic.
Having a style-1 system relieves the programmer from resorting to unsafe pointer arithmetic when working with noncontiguous slices.

% PAB: repeat from previous paragraph.
% The choice to implement this style-1 system upon C's style-2 arrays, rather than its style-3 pointer arithmetic, reduces the attack surface of unsafe code.
% My casting is unsafe, but I do not do any pointer arithmetic.
% When a programmer works in the common-case style-2 subset (in the no-@[all]@ top of \VRef[Figure]{fig:subscr-all}), my casts are identities, and the C compiler is doing its usual displacement calculations.
% If I had implemented my system upon style-3 pointer arithmetic, then this common case would be circumventing C's battle-hardened displacement calculations in favour of my own.

% \noindent END: Paste looking for a home

The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping.
The @arpk@ structure and its @-[i]@ operator are defined as:
\begin{cfa}
forall(
        [N],                                    $\C{// length of current dimension}$
        S & | sized(S),                 $\C{// masquerading-as}$
        Timmed &,                               $\C{// immediate element, often another array}$
        Tbase &                                 $\C{// base element, \eg float, never array}$
) { // distribute forall to each element
        struct arpk {
                S strides[N];           $\C{// so that sizeof(this) is N of S}$
        };
        // expose Timmed, stride by S
        static inline Timmed & ?[?]( arpk( N, S, Timmed, Tbase ) & a, long int i ) {
                subcheck( a, i, 0, N );
                return (Timmed &)a.strides[i];
        }
}
\end{cfa}
The private @arpk@ structure (array with explicit packing) is generic over four types: dimension length, masquerading-as, ...
This structure's public interface is hidden behind the @array(...)@ macro and the subscript operator.
Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information.
Subscripting by @all@ rearranges the order of masquerading-as types to achieve, in general, nontrivial striding.
Subscripting by a number consumes the masquerading-as size of the contained element type, does normal array stepping according to that size, and returns the element found there, in unmasked form.

An instantiation of the @arpk@ generic is given by the @array( E_base, N0, N1, ... )@ expansion, which is @arpk( N0, Rec, Rec, E_base )@, where @Rec@ is @array( E_base, N1, ... )@.
In the base case, @array( E_base )@ is just @E_base@.
Because this construction uses the same value for the generic parameters @S@ and @E_im@, the resulting layout has trivial strides.

Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instantiations, intact, to new positions.
Expressed as an operation on types, this rotation is:
\begin{eqnarray*}
suball( arpk(N, S, E_i, E_b) ) & = & enq( N, S, E_i, E_b ) \\
enq( N, S, E_b, E_b ) & = & arpk( N, S, E_b, E_b ) \\
enq( N, S, arpk(N', S', E_i', E_b), E_b ) & = & arpk( N', S', enq(N, S, E_i', E_b), E_b )
\end{eqnarray*}


\section{Bound Checks, Added and Removed}

\CFA array subscripting is protected with runtime bound checks.
The array dependent-typing provides information to the C optimizer allowing it remove many of the bound checks.
This section provides a demonstration of the effect.

The experiment compares the \CFA array system with the padded-room system [TODO:xref] most typically exemplified by Java arrays, but also reflected in the \CC pattern where restricted vector usage models a checked array.
The essential feature of this padded-room system is the one-to-one correspondence between array instances and the symbolic bounds on which dynamic checks are based.
The experiment compares with the \CC version to keep access to generated assembly code simple.

As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and \CC versions.
When the programmer treats the array's bound correctly (making the subscript ``obviously fine''), no dynamic bound check is observed in the program's optimized assembly code.
But when the bounds are adjusted, such that the subscript is possibly invalid, the bound check appears in the optimized assembly, ready to catch an occurrence the mistake.

TODO: paste source and assembly codes

Incorporating reuse among dimension sizes is seen to give \CFA an advantage at being optimized.
The case is naive matrix multiplication over a row-major encoding.

TODO: paste source codes


\section{Array Lifecycle}

An array, like a structure, wraps subordinate objects.
Any object type, like @string@, can be an array element or structure member.
A consequence is that the lifetime of the container must match with its subordinate objects: all elements and members must be initialized/uninitialized implicitly as part of the container's allocation/deallocation.
Modern programming languages implicitly perform these operations via a type's constructor and destructor.
Therefore, \CFA must assure that an array's subordinate objects' lifetime operations are called.
Preexisting \CFA mechanisms achieve this requirement, but with poor performance.
Furthermore, advanced array users need an exception to the basic mechanism, which does not occur with other aggregates.
Hence, arrays introduce subtleties in supporting an element's lifecycle.

The preexisting \CFA support for contained-element lifecycle is based on recursive occurrences of the object-type (otype) pseudo-trait.
A type is an otype, if it provides a default (parameterless) constructor, copy constructor, assignment operator, and destructor (like \CC).
For a structure with otype members, the compiler implicitly generates implementations of the four otype functions for the outer structure.
Then the generated default constructor for the outer structure calls the default constructor for each member, and the other otype functions work similarly.
For a member that is a C array, these calls occur in a loop for each array element, which even works for VLAs.
This logic works the same, whether the member is a concrete type (that happens to be an otype) or if the member is a polymorphic type asserted to be an otype (which is implicit in the syntax, @forall(T)@).
The \CFA array has the simplified form (similar to one seen before):
\begin{cfa}
forall( T * )   // non-otype element, no lifecycle functions
// forall( T )  // otype element, lifecycle functions asserted
struct array5 {
        T __items[ 5 ];
};
\end{cfa}
Being a structure with a C-array member, the otype-form declaration @T@ causes @array5( float )@ to be an otype too.
But this otype-recursion pattern has a performance issue.
\VRef[Figure]{f:OtypeRecursionBlowup} shows the steps to find lifecycle functions, under the otype-recursion pattern, for a cube of @float@:
\begin{cfa}
array5( array5( array5( float ) ) )
\end{cfa}
The work needed for the full @float@-cube is 256 leaves.
Then the otype-recursion pattern generates helper functions and thunks that are exponential in the number of dimensions.
Anecdotal experience is annoyingly slow compile time at three dimensions and unusable at four.

%array5(T) offers
%1 parameterless ctor, which asks for T to have
%       1 parameterless ctor
%       2 copy ctor
%       3 asgt
%       4 dtor
%2 copy ctor, which asks for T to have
%       1 parameterless ctor
%       2 copy ctor
%       3 asgt
%       4 dtor
%3 asgt, which asks for T to have
%       1 parameterless ctor
%       2 copy ctor
%       3 asgt
%       4 dtor
%4 dtor, which asks for T to have
%       1 parameterless ctor
%       2 copy ctor
%       3 asgt
%       4 dtor

\begin{figure}
\centering
\setlength{\tabcolsep}{20pt}
\begin{tabular}{@{}lll@{}}
\begin{cfa}[deletekeywords={default}]
float offers
1 default ctor
2 copy ctor
3 assignment
4 dtor
























\end{cfa}
&
\begin{cfa}[deletekeywords={default}]
array5( float ) has
1 default ctor, using float$'$s
        1 default ctor
        2 copy ctor
        3 assignment
        4 dtor
2 copy ctor, using float$'$s
        1 default ctor
        2 copy ctor
        3 assignment
        4 dtor
3 assignment, using float$'$s
        1 default ctor
        2 copy ctor
        3 assignment
        4 dtor
4 dtor, using float$'$s
        1 default ctor
        2 copy ctor
        3 assignment
        4 dtor








\end{cfa}
&
\begin{cfa}[deletekeywords={default}]
array5( array5( float ) ) has
1 default ctor, using array5( float )
        1 default ctor, using float$'$s
                1 default ctor
                2 copy ctor
                3 assignment
                4 dtor
        2 copy ctor, using float$'$s
                1 default ctor
                2 copy ctor
                3 assignment
                4 dtor
        3 assignment, using float$'$s
                1 default ctor
                2 copy ctor
                3 assignment
                4 dtor
        4 dtor, using float$'$s
                1 default ctor
                2 copy ctor
                3 assignment
                4 dtor
2 copy ctor, using array5( float )
        ... 4 children, 16 leaves
3 assignment, using array5( float )
        ... 4 children, 16 leaves
4 dtor, using array5( float )
        ... 4 children, 16 leaves
(64 leaves)
\end{cfa}
\end{tabular}
\caption{Exponential thunk generation under the otype-recursion pattern.
        Each time one type's function (\eg ctor) uses another type's function, the \CFA compiler generates a thunk, to capture the used function's dependencies, presented according to the using function's need.
        So, each non-leaf line represents a generated thunk and every line represents a search request for the resolver to find a satisfying function.}
\label{f:OtypeRecursionBlowup}
\end{figure}

The issue is that the otype-recursion pattern uses more assertions than needed.
For example, @array5( float )@'s default constructor has all four lifecycle assertions about the element type, @float@.
However, it only needs @float@'s default constructor, as the other operations are never used.
Current work by the \CFA team aims to improve this situation.
Therefore, I had to construct a workaround.

My workaround moves from otype (value) to dtype (pointer) with a default-constructor assertion, where dtype does not generate any constructors but the assertion claws back the default otype constructor.
\begin{cquote}
\setlength{\tabcolsep}{10pt}
\begin{tabular}{@{}ll@{}}
\begin{cfa}
// autogenerated for otype-recursion:
forall( T )
void ?{}( array5( T ) & this ) {
        for ( i; 5 ) { ( this[i] ){}; }
}
forall( T )
void ?{}( array5( T ) & this, array5( T ) & src ) {
        for ( i; 5 ) { ( this[i] ){ src[i] }; }
}
forall( T )
void ^?{}( array5( T ) & this ) {
        for ( i; 5 ) { ^( this[i] ){}; }
}
\end{cfa}
&
\begin{cfa}
// lean, bespoke:
forall( T* | { void @?{}( T & )@; } )
void ?{}( array5( T ) & this ) {
        for ( i; 5 ) { ( this[i] ){}; }
}
forall( T* | { void @?{}( T &, T )@; } )
void ?{}( array5( T ) & this, array5( T ) & src ) {
        for ( i; 5 ) { ( this[i] ){ src[i] }; }
}
forall( T* | { void @?{}( T & )@; } )
void ^?{}( array5(T) & this ) {
        for (i; 5) { ^( this[i] ){}; }
}
\end{cfa}
\end{tabular}
\end{cquote}
Moreover, the assignment operator is skipped, to avoid hitting a lingering growth case.
Temporarily skipping assignment is tolerable because array assignment is not a common operation.
With this solution, the critical lifecycle functions are available, with linear growth in thunk creation for the default constructor.

Finally, the intuition that a programmer using an array always wants the elements' default constructor called \emph{automatically} is simplistic.
Arrays exist to store different values at each position.
So, array initialization needs to let the programmer provide different constructor arguments to each element.
\begin{cfa}
thread worker { int id; };
void ?{}( worker & ) = void; // remove default constructor
void ?{}( worker &, int id );
array( worker, 5 ) ws = @{}@; // rejected; but desire is for no initialization yet
for ( i; 5 ) (ws[i]){ @i@ }; // explicitly initialize each thread, giving id
\end{cfa}
Note the use of the \CFA explicit constructor call, analogous to \CC's placement-@new@.
This call is where initialization is desired, and not at the declaration of @ws@.
The attempt to initialize from nothing (equivalent to dropping @= {}@ altogether) is invalid because the @worker@ type removes the default constructor.
The @worker@ type is designed this way to work with the threading system.
A thread type forks a thread at the end of each constructor and joins with it at the start of each destructor.
But a @worker@ cannot begin its forked-thread work without knowing its @id@.
Therefore, there is a conflict between the implicit actions of the builtin @thread@ type and a user's desire to defer these actions.

Another \CFA feature for providing C backwards compatibility, at first seem viable for initializing the array @ws@, though on closer inspection is not.
C initialization without a constructor is specified with \lstinline|@=|, \eg \lstinline|array(worker, 5) ws @= {}| ignores all \CFA lifecycle management and uses C empty initialization.
This option does achieve the desired semantics on the construction side.
But on destruction side, the desired semantics is for implicit destructor calls to continue, to keep the join operation tied to lexical scope.
C initialization disables \emph{all} implicit lifecycle management, but the goal is to disable only the implicit construction.

To fix this problem, I enhanced the \CFA standard library to provide the missing semantics, available in either form:
\begin{cfa}
array( @uninit@(worker), 5 ) ws1;
array( worker, 5) ws2 = { @delay_init@ };
\end{cfa}
Both cause the @ws@-construction-time implicit call chain to stop before reaching a @worker@ constructor, while leaving the implicit destruction calls intact.
Two forms are available, to parallel the development of this feature in \uCpp~\cite{uC++}.
Originally \uCpp offered only the @ws1@ form, using the class-template @uNoCtor@ equivalent to \CFA's @uninit@.
More recently, \uCpp was extended with the declaration macro, @uArray@, with usage similar to the @ws2@ case.
Based on experience piloting @uArray@ as a replacement of @uNoCtor@, it should be possible to remove the first option.

% note to Mike, I have more fragments on some details available in push24\fragments\uNoCtor.txt

\section{Array Comparison}


\subsection{Rust}

A Rust array is a set of mutable or immutable (@const@) contiguous objects of the same type @T@, where the compile-time dimension(s) is part of the type signature @[T; dimension]@.
\begin{rust}
let val = 42;
let mut ia: [usize; 5] = [val; 5];      $\C{// mutable, repeated initialization [42, 42, 42, 42, 42]}$
let fval = 42.2;
let fa: [f64; 5] = [1.2, fval, 5.6, 7.3, 9.1];  $\C{// immutable, individual initialization}$
\end{rust}
Initialization is required even if the  array is subsequently initialized.
Rust arrays are not VLAs, but the compile-time length can be queried using member @len()@.
Arrays can be assigned and passed to parameters by value or reference, if and only if, the type and dimension match, meaning a different function is needed for each array size.

Array iteration is by a range or array variable.
\begin{rust}
for i in @0..ia.len()@ { print!("{:?} ", ia[i] ); }  $\C{// 42 42 42 42 42}$
for fv in @fa@ { print!("{:?} ", fv ); }  $\C{// 1.2 42.2 5.6 7.3 9.1}$
for i in 0..=1 { ia[i] = i; }    $\C{// mutable changes}$
for iv in ia { print!("{:?} ", iv ); }  $\C{// 0 1 42 42 42}$
\end{rust}
An array can be assigned and printed as a set.
\begin{rust}
ia = @[5; 5]@;   println!( "{:?} {:?}", @ia@, ia.len() );       $\C{// [5, 5, 5, 5, 5] 5}$
ia = @[1, 2, 3, 4, 5]@;   println!( "{:?} {:?}", @ia@, ia.len() );      $\C{// [1, 2, 3, 4, 5] 5}$
\end{rust}

Multi-dimensional arrays use nested dimensions, resulting in columns before rows.
Here the outer array is a length @ROWS@ array whose elements are @f64@ arrays of length @COLS@ each.
\begin{cquote}
\setlength{\tabcolsep}{10pt}
\begin{tabular}{@{}ll@{}}
\begin{rust}
const ROWS: usize = 4;   const COLS: usize = 6;
let mut fmatrix: [[f64; @COLS@]; @ROWS@] = [[0.; @COLS@]; @ROWS@];
for r in 0 .. ROWS {
        for c in 0 .. COLS {  fmatrix[r][c] = r as f64 + c as f64;  }  }
\end{rust}
&
\begin{rust}
[ 0.0, 1.0, 2.0, 3.0, 4.0, 5.0 ]
[ 1.0, 2.0, 3.0, 4.0, 5.0, 6.0 ]
[ 2.0, 3.0, 4.0, 5.0, 6.0, 7.0 ]
[ 3.0, 4.0, 5.0, 6.0, 7.0, 8.0 ]
\end{rust}
\end{tabular}
\end{cquote}

Slices borrow a section of an array (subarray) and have type @&[T]@.
A slice has a dynamic size and does not implicitly coerce to an array.
\begin{rust}
println!( "{:?}", @&ia[0 .. 3]@ ); $\C{// fixed bounds, [1, 2, 3]}$
println!( "{:?}", @&ia[ia.len() - 2 .. ia.len()@] ); $\C{// variable bounds, [4, 5]}$
println!( "{:?}", @&ia[ia.len() - 2 .. ]@ ); $\C{// drop upper bound, [4, 5]}$
println!( "{:?}", @&ia[.. ia.len() - 2 ]@ ); $\C{// drop lower bound, [1, 2, 3]}$
println!( "{:?}", @&ia[..]@ ); $\C{// drop both bound, [1, 2, 3, 4, 5]}$
\end{rust}
A multi-dimensional slice can only borrow subrows because a slice requires contiguous memory.
Here columns 2--4 are sliced from row 3.
\begin{rust}
let mut slice2: &[f64] = &fmatrix[3][@2 ..= 4@];
println!( "{:?}", slice2 );  $\C{// [5.0, 6.0, 7.0]}$
\end{rust}
Here row 2 is sliced from the sub-matrix formed from rows 1--3.
\begin{rust}
slice2 = &fmatrix[@1 ..= 3@][1];
println!( "{:?}", slice2 );  $\C{// [3.0, 4.0, 5.0, 6.0, 7.0, 8.0]}$
\end{rust}
A slice can be explicitly converted into an array or reference to an array.
\begin{rust}
let slice: &[f64];
slice = &fa[0 ..= 1]; $\C{// create slice, [1.2, 42.2]}$
let mut fa2: [f64; 2] = @<[f64; 2]>::try_from( slice ).unwrap()@; $\C{// convert slice to array, [1.2, 42.2]}$
fa2 = @(& fa[2 ..= 3]).try_into().unwrap()@; $\C{// convert slice to array, [5.6, 7.3]}$
\end{rust}

The @vec@ macro (using @Vec@ type) provides dynamically-size dynamically-growable arrays of arrays only using the heap (\CC @vector@ type).
\begin{cquote}
\setlength{\tabcolsep}{10pt}
\begin{tabular}{@{}ll@{}}
\multicolumn{1}{c}{Rust} &\multicolumn{1}{c}{\CC} \\
\begin{rust}
let (rows, cols) = (4, 6);
let mut matrix = vec![vec![0; cols]; rows];
...     matrix[r][c] = r + c; // fill matrix
\end{rust}
&
\begin{c++}
int rows = 4, cols = 6;
vector<vector<int>> matrix( rows, vector<int>(cols) );
...     matrix[r][c] = r + c; // fill matrix}
\end{c++}
\end{tabular}
\end{cquote}
A dynamically-size array is sliced the same as a fixed-size one.
\begin{rust}
let mut slice3: &[usize] = &matrix[3][2 ..= 4]; $\C{// [5, 6, 7]}$
slice3 = &matrix[1 ..= 3][1]; $\C{// [2, 3, 4, 5, 6, 7]}$
\end{rust}
Finally, to mitigate the restriction of matching array dimensions between argument and parameter types, it is possible for a parameter to be a slice.
\begin{rust}
fn zero( arr: @& mut [usize]@ ){
        for i in 0 .. arr.len() { arr[i] = 0; }
}
zero( & mut ia[0..5] ); // arbitrary sized slice
zero( & mut ia[0..3] );
\end{rust}
Or write a \emph{generic} function taking an array of fixed-element type and any size.
\begin{rust}
fn aprint<@const N: usize@>( arg: [usize; N] ) {
        for r in 0 .. arg.len() {   print!( "{} ", arg[r] );   }
}
aprint( ia );
\end{rust}


\subsection{Java}

Java arrays are references, so multi-dimension arrays are arrays-of-arrays \see{\VRef{toc:mdimpl}}.
For each array, Java implicitly storages the array dimension in a descriptor, supporting array length, subscript checking, and allowing dynamically-sized array-parameter declarations.
\begin{cquote}
\begin{tabular}{rl}
C      &  @void f( size_t n, size_t m, float x[n][m] );@ \\
Java   &  @void f( float x[][] );@
\end{tabular}
\end{cquote}
However, in the C prototype, the parameters @n@ and @m@ are manually managed, \ie there is no guarantee they match with the argument matrix for parameter @x@.
\VRef[Figure]{f:JavaVsCTriangularMatrix} compares a triangular matrix (array-of-arrays) in dynamically safe Java to unsafe C.
Each dynamically sized row in Java stores its dimension, while C requires the programmer to manage these sizes explicitly (@rlnth@).
All subscripting is Java has bounds checking, while C has none.
Both Java and C require explicit null checking, otherwise there is a runtime failure.

\begin{figure}
\setlength{\tabcolsep}{15pt}
\begin{tabular}{ll@{}}
\begin{java}
int m[][] = {  // triangular matrix
        new int [4],
        new int [3],
        new int [2],
        new int [1],
        null
};

for ( int r = 0; r < m.length; r += 1 ) {
        if ( m[r] == null ) continue;
        for ( int c = 0; c < m[r].length; c += 1 ) {
                m[r][c] = c + r; // subscript checking
        }

}

for ( int r = 0; r < m.length; r += 1 ) {
        if ( m[r] == null ) {
                System.out.println( "null row" );
                continue;
        }
        for ( int c = 0; c < m[r].length; c += 1 ) {
                System.out.print( m[r][c] + " " );
        }
        System.out.println();

}
\end{java}
&
\begin{cfa}
int * m[5] = {  // triangular matrix
        calloc( 4, sizeof(int) ),
        calloc( 3, sizeof(int) ),
        calloc( 2, sizeof(int) ),
        calloc( 1, sizeof(int) ),
        NULL
};
int rlnth = 4;
for ( int r = 0; r < 5; r += 1 ) {
        if ( m[r] == NULL ) continue;
        for ( int c = 0; c < rlnth; c += 1 ) {
                m[r][c] = c + r; // no subscript checking
        }
        rlnth -= 1;
}
rlnth = 4;
for ( int r = 0; r < 5; r += 1 ) {
        if ( m[r] == NULL ) {
                printf( "null row\n" );
                continue;
        }
        for ( int c = 0; c < rlnth; c += 1 ) {
                printf( "%d ", m[r][c] );
        }
        printf( "\n" );
        rlnth -= 1;
}
\end{cfa}
\end{tabular}
\caption{Java (left) \vs C (right) Triangular Matrix}
\label{f:JavaVsCTriangularMatrix}
\end{figure}

The downside of the arrays-of-arrays approach is performance due to pointer chasing versus pointer arithmetic for a contiguous arrays.
Furthermore, there is the cost of managing the implicit array descriptor.
It is unlikely that a JIT can dynamically rewrite an arrays-of-arrays form into a contiguous form.


\subsection{\CC}

Because C arrays are difficult and dangerous, the mantra for \CC programmers is to use @std::vector@ in place of the C array.
While the vector size can grow and shrink dynamically, \vs a fixed-size dynamic size with VLAs, the cost of this extra feature is mitigated by preallocating the maximum size (like the VLA) at the declaration (one dynamic call) to avoid using @push_back@.
\begin{c++}
vector< vector< int > > m( 5, vector<int>(8) ); // initialize size of 5 x 8 with 6 dynamic allocations
\end{c++}
Multidimensional arrays are arrays-of-arrays with associated costs.
Each @vector@ array has an array descriptor contain the dimension, which allows bound checked using @x.at(i)@ in place of @x[i]@.
Used with these restrictions, out-of-bound accesses are caught, and in-bound accesses never exercise the vector's ability to grow, preventing costly reallocate and copy, and never invalidate references to contained values.
This scheme matches Java's safety and expressiveness exactly, but with the inherent costs.


\subsection{Levels of Dependently Typed Arrays}

\CFA's array is the first lightweight application of dependently-typed bound tracking to an extension of C.
Other extensions of C that apply dependently-typed bound tracking are heavyweight, in that the bound tracking is part of a linearly-typed ownership-system, which further helps guarantee statically the validity of every pointer deference.
These systems, therefore, ask the programmer to convince the type checker that every pointer dereference is valid.
\CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter.

\CFA's array is also the first extension of C to use its tracked bounds to generate the pointer arithmetic implied by advanced allocation patterns.
Other bound-tracked extensions of C either forbid certain C patterns entirely, or address the problem of \emph{verifying} that the user's provided pointer arithmetic is self-consistent.
The \CFA array, applied to accordion structures [TOD: cross-reference] \emph{implies} the necessary pointer arithmetic, generated automatically, and not appearing at all in a user's program.

The \CFA array and the field of ``array language'' comparators all leverage dependent types to improve on the expressiveness over C and Java, accommodating examples such as:
\begin{itemize}[leftmargin=*]
\item a \emph{zip}-style operation that consumes two arrays of equal length
\item a \emph{map}-style operation whose produced length matches the consumed length
\item a formulation of matrix multiplication, where the two operands must agree on a middle dimension, and where the result dimensions match the operands' outer dimensions
\end{itemize}
Across this field, this expressiveness is not just an available place to document such assumption, but these requirements are strongly guaranteed by default, with varying levels of statically/dynamically checked and ability to opt out.
Along the way, the \CFA array also closes the safety gap (with respect to bounds) that Java has over C.

Dependent type systems, considered for the purpose of bound-tracking, can be full-strength or restricted.
In a full-strength dependent type system, a type can encode an arbitrarily complex predicate, with bound-tracking being an easy example.
The tradeoff of this expressiveness is complexity in the checker, even typically, a potential for its nontermination.
In a restricted dependent type system (purposed for bound tracking), the goal is to check helpful properties, while keeping the checker well-behaved; the other restricted checkers surveyed here, including \CFA's, always terminate.
[TODO: clarify how even Idris type checking terminates]

Idris is a current, general-purpose dependently typed programming language.
Length checking is a common benchmark for full dependent type systems.
Here, the capability being considered is to track lengths that adjust during the execution of a program, such as when an \emph{add} operation produces a collection one element longer than the one on which it started.
[TODO: finish explaining what Data.Vect is and then the essence of the comparison]

POINTS:
here is how our basic checks look (on a system that does not have to compromise);
it can also do these other cool checks, but watch how I can mess with its conservativeness and termination

Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer novel contributions concerning similar, restricted dependent types for tracking array length.
Unlike \CFA, both are garbage-collected functional languages.
Because they are garbage-collected, referential integrity is built-in, meaning that the heavyweight analysis, that \CFA aims to avoid, is unnecessary.
So, like \CFA, the checking in question is a lightweight bounds-only analysis.
Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression.



The Futhark work discusses the working language's connection to a lambda calculus, with typing rules and a safety theorem proven in reference to an operational semantics.
There is a particular emphasis on an existential type, enabling callee-determined return shapes.


Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type.

Futhark and full-strength dependently typed languages treat array sizes are ordinary values.
Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.

\CFA's hybrid presentation, @forall( [N] )@, has @N@ belonging to the type system, yet has no instances.
Belonging to the type system means it is inferred at a call site and communicated implicitly, like in Dex and unlike in Futhark.
Having no instances means there is no type for a variable @i@ that constrains @i@ to be in the range for @N@, unlike Dex, [TODO: verify], but like Futhark.

If \CFA gets such a system for describing the list of values in a type, then \CFA arrays are poised to move from the Futhark level of expressiveness, up to the Dex level.

[TODO: introduce Ada in the comparators]

In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, \CC, Java, Futhark and \CFA today, the domain is a prefix of the natural numbers.
The generality has obvious aesthetic benefits for programmers working on scheduling resources to weekdays, and for programmers who prefer to count from an initial number of their own choosing.

This change of perspective also lets us remove ubiquitous dynamic bound checks.
[TODO: xref] discusses how automatically inserted bound checks can often be optimized away.
But this approach is unsatisfying to a programmer who believes she has written code in which dynamic checks are unnecessary, but now seeks confirmation.
To remove the ubiquitous dynamic checking is to say that an ordinary subscript operation is only valid when it can be statically verified to be in-bound (and so the ordinary subscript is not dynamically checked), and an explicit dynamic check is available when the static criterion is impractical to meet.

[TODO, fix confusion:  Idris has this arrangement of checks, but still the natural numbers as the domain.]

The structural assumptions required for the domain of an array in Dex are given by the trait (there, ``interface'') @Ix@, which says that the parameter @n@ is a type (which could take an argument like @weekday@) that provides two-way conversion with the integers and a report on the number of values.
Dex's @Ix@ is analogous the @is_enum@ proposed for \CFA above.
\begin{cfa}
interface Ix n
get_size n : Unit -> Int
ordinal : n -> Int
unsafe_from_ordinal n : Int -> n
\end{cfa}

Dex uses this foundation of a trait (as an array type's domain) to achieve polymorphism over shapes.
This flavour of polymorphism lets a function be generic over how many (and the order of) dimensions a caller uses when interacting with arrays communicated with this function.
Dex's example is a routine that calculates pointwise differences between two samples.
Done with shape polymorphism, one function body is equally applicable to a pair of single-dimensional audio clips (giving a single-dimensional result) and a pair of two-dimensional photographs (giving a two-dimensional result).
In both cases, but with respectively dimensioned interpretations of ``size,'' this function requires the argument sizes to match, and it produces a result of the that size.

The polymorphism plays out with the pointwise-difference routine advertising a single-dimensional interface whose domain type is generic.
In the audio instantiation, the duration-of-clip type argument is used for the domain.
In the photograph instantiation, it's the tuple-type of $ \langle \mathrm{img\_wd}, \mathrm{img\_ht} \rangle $.
This use of a tuple-as-index is made possible by the built-in rule for implementing @Ix@ on a pair, given @Ix@ implementations for its elements
\begin{cfa}
instance {a b} [Ix a, Ix b] Ix (a & b)
get_size = \(). size a * size b
ordinal = \(i, j). (ordinal i * size b) + ordinal j
unsafe_from_ordinal = \o.
bs = size b
(unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
\end{cfa}
and by a user-provided adapter expression at the call site that shows how to indexing with a tuple is backed by indexing each dimension at a time
\begin{cfa}
img_trans :: (img_wd,img_ht)=>Real
img_trans.(i,j) = img.i.j
result = pairwise img_trans
\end{cfa}
[TODO: cite as simplification of example from https://openreview.net/pdf?id=rJxd7vsWPS section 4]

In the case of adapting this pattern to \CFA, my current work provides an adapter from ``successively subscripted'' to ``subscripted by tuple,'' so it is likely that generalizing my adapter beyond ``subscripted by @ptrdiff_t@'' is sufficient to make a user-provided adapter unnecessary.

\subsection{Static Safety in C Extensions}


\section{Future Work}

\subsection{Array Syntax}

An important goal is to recast @array(...)@ syntax into C-style @[]@.
The proposal (which is partially implemented) is an alternate dimension and subscript syntax.
C multi-dimension and subscripting syntax uses multiple brackets.
\begin{cfa}
int m@[2][3]@;  // dimension
m@[0][1]@ = 3;  // subscript
\end{cfa}
Leveraging this syntax, the following (simpler) syntax should be intuitive to C programmers with only a small backwards compatibility issue.
\begin{cfa}
int m@[2, 3]@;  // dimension
m@[0, 1]@ = 3;  // subscript
\end{cfa}
However, the new subscript syntax is not backwards compatible, as @0, 1@ is a comma expression.
Interestingly, disallowed the comma expression in this context eliminates an unreported error: subscripting a matrix with @m[i, j]@ instead of @m[i][j]@, which selects the @j@th row not the @i, j@ element.
Hence, a comma expression in this context is rare.
Finally, it is possible to write @m[(i, j)]@ in the new syntax to achieve the equivalent of the old @m[i, j]@.
Note, the new subscript syntax can easily be internally lowered to @[-][-]...@ and handled as regular subscripting.
The only ambiguity with C syntax is for a single dimension array, where the syntax for old and new are the same.
\begin{cfa}
int m[2@,@];  // single dimension
m[0] = 3;  // subscript
\end{cfa}
The solution for the dimension is to use a terminating comma to denote a new single-dimension array.
This syntactic form is also used for the (rare) singleton tuple @[y@{\color{red},}@]@.
The extra comma in the dimension is only mildly annoying, and acts as eye-candy differentiating old and new arrays.
The subscript operator is not an issue as overloading selects the correct single-dimension operation for old/new array types.
The ultimately goal is to replace all C arrays with \CFA arrays, establishing a higher level of safety in C programs, and eliminating the need for the terminating comma.


\subsection{Range Slicing}

\subsection{With a Module System}


\subsection{Retire Pointer Arithmetic}


\begin{comment}
\section{\texorpdfstring{\CFA}{Cforall}}

XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX \\
moved from background chapter \\
XXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXXX \\

Traditionally, fixing C meant leaving the C-ism alone, while providing a better alternative beside it.
(For later:  That's what I offer with array.hfa, but in the future-work vision for arrays, the fix includes helping programmers stop accidentally using a broken C-ism.)

\subsection{\texorpdfstring{\CFA}{Cforall} Features Interacting with Arrays}

Prior work on \CFA included making C arrays, as used in C code from the wild,
work, if this code is fed into @cfacc@.
The quality of this this treatment was fine, with no more or fewer bugs than is typical.

More mixed results arose with feeding these ``C'' arrays into preexisting \CFA features.

A notable success was with the \CFA @alloc@ function,
which type information associated with a polymorphic return type
replaces @malloc@'s use of programmer-supplied size information.
\begin{cfa}
// C, library
void * malloc( size_t );
// C, user
struct tm * el1 = malloc( sizeof(struct tm) );
struct tm * ar1 = malloc( 10 * sizeof(struct tm) );

// CFA, library
forall( T * ) T * alloc();
// CFA, user
tm * el2 = alloc();
tm (*ar2)[10] = alloc();
\end{cfa}
The alloc polymorphic return compiles into a hidden parameter, which receives a compiler-generated argument.
This compiler's argument generation uses type information from the left-hand side of the initialization to obtain the intended type.
Using a compiler-produced value eliminates an opportunity for user error.

TODO: fix in following: even the alloc call gives bad code gen: verify it was always this way; walk back the wording about things just working here; assignment (rebind) seems to offer workaround, as in bkgd-cfa-arrayinteract.cfa

Bringing in another \CFA feature, reference types, both resolves a sore spot of the last example, and gives a first example of an array-interaction bug.
In the last example, the choice of ``pointer to array'' @ar2@ breaks a parallel with @ar1@.
They are not subscripted in the same way.
\begin{cfa}
ar1[5];
(*ar2)[5];
\end{cfa}
Using ``reference to array'' works at resolving this issue.  TODO: discuss connection with Doug-Lea \CC proposal.
\begin{cfa}
tm (&ar3)[10] = *alloc();
ar3[5];
\end{cfa}
The implicit size communication to @alloc@ still works in the same ways as for @ar2@.

Using proper array types (@ar2@ and @ar3@) addresses a concern about using raw element pointers (@ar1@), albeit a theoretical one.
TODO xref C standard does not claim that @ar1@ may be subscripted,
because no stage of interpreting the construction of @ar1@ has it be that ``there is an \emph{array object} here.''
But both @*ar2@ and the referent of @ar3@ are the results of \emph{typed} @alloc@ calls,
where the type requested is an array, making the result, much more obviously, an array object.

The ``reference to array'' type has its sore spots too.
TODO see also @dimexpr-match-c/REFPARAM_CALL@ (under @TRY_BUG_1@)

TODO: I fixed a bug associated with using an array as a T.  I think.  Did I really?  What was the bug?
\end{comment}