source: doc/theses/mike_brooks_MMath/content/array/features/sec.tex @ 8e819a9

The present work adds a type @array@ to the \CFA standard library.

This array's length is statically governed and dynamically valued.  This static governance achieves argument safety and suggests a path to subscript safety as future work (TODO: cross reference).  In present state, this work is a runtime libray accessed through a system of macros, while section [TODO: discuss C conexistence] discusses a path for the new array type to be accessed directly by \CFA's array syntax, replacing the lifted C array that this syntax currently exposes.

This section presents motivating examples of the new array type's usage, and follows up with definitions of the notations that appear.

The core of the new array governance is tracking all array lengths in the type system.  Dynamically valued lengths are represented using type variables.  The stratification of type variables preceding object declarations makes a length referenceable everywhere that it is needed.  For example, a declaration can share one length, @N@, among a pair of parameters and the return.
\lstinputlisting[language=C, firstline=50, lastline=59]{hello-array.cfa}
Here, the function @f@ does a pointwise comparison, checking if each pair of numbers is within half a percent of each other, returning the answers in a newly allocated bool array.

The array type uses the parameterized length information in its @sizeof(-)@ determination, illustrated in the example's call to @alloc@.  That call requests an allocation of type @array(bool, N)@, which the type system deduces from the left-hand side of the initialization, into the return type of the @alloc@ call.  Preexesting \CFA behaviour is leveraged here, both in the return-type-only polymorphism, and the @sized(T)@-aware standard-library @alloc@ routine.  The new @array@ type plugs into this behaviour by implementing the @sized@/@sizeof(-)@ assertion to have the intuitive meaning.  As a result, this design avoids an opportunity for programmer error by making the size/length communication to a called routine implicit, compared with C's @calloc@ (or the low-level \CFA analog @aalloc@) which take an explicit length parameter not managed by the type system.

A harness for this @f@ function shows how dynamic values are fed into the system.
\lstinputlisting[language=C, firstline=100, lastline=119]{hello-array.cfa}
Here, the @a@ sequence is loaded with decreasing values, and the @b@ sequence with amounts off by a constant, giving relative differences within tolerance at first and out of tolerance later.  The driver program is run with two different inputs of sequence length.

The loops in the driver follow the more familiar pattern of using the ordinary variable @n@ to convey the length.  The type system implicitly captures this value at the call site (@main@ calling @f@) and makes it available within the callee (@f@'s loop bound).

The two parts of the example show @Z(n)@ adapting a variable into a type-system governed length (at @main@'s declarations of @a@, @b@, and @result@), @z(N)@ adapting in the opposite direction (at @f@'s loop bound), and a passthru use of a governed length (at @f@'s declaration of @ret@.)  It is hoped that future language integration will allow the macros @Z@ and @z@ to be omitted entirely from the user's notation, creating the appearance of seamlessly interchanging numeric values with appropriate generic parameters.

The macro-assisted notation, @forall...ztype@, participates in the user-relevant declaration of the name @N@, which becomes usable in parameter/return declarations and in the function body.  So future language integration only sweetens this form and does not seek to elimimate the declaration.  The present form is chosen to parallel, as closely as a macro allows, the existing forall forms:
\begin{lstlisting}
  forall( dtype T  ) ...
  forall( otype T  ) ...
  forall( ztype(N) ) ...
\end{lstlisting}

The notation @array(thing, N)@ is also macro-assisted, though only in service of enabling multidimensional uses discussed further in section \ref{toc:mdimpl}.  In a single-dimensional case, the marco expansion gives a generic type instance, exactly like the original form suggests.



In summary:

\begin{tabular}{p{15em}p{20em}}
  @ztype( N )@ & within a forall, declares the type variable @N@ to be a governed length \\[0.25em]
  @Z( @ $e$ @ )@ & a type representing the value of $e$ as a governed length, where $e$ is a @size_t@-typed expression \\[0.25em]
  @z( N )@ & an expression of type @size_t@, whose value is the governed length @N@ \\[0.25em]
  @array( thing, N0, N1, ... )@
  &  a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects
\end{tabular}

Unsigned integers have a special status in this type system.  Unlike how C++ allows @template< size_t N, char * msg, typename T >...@ declarations, this system does not accommodate values of any user-provided type.  TODO: discuss connection with dependent types.


An example of a type error demonstrates argument safety.  The running example has @f@ expecting two arrays of the same length.  A compile-time error occurs when attempting to call @f@ with arrays whose lengths may differ.
\lstinputlisting[language=C, firstline=150, lastline=155]{hello-array.cfa}
As is common practice in C, the programmer is free to cast, to assert knownledge not shared with the type system.
\lstinputlisting[language=C, firstline=200, lastline=202]{hello-array.cfa}

Argument safety, and the associated implicit communication of length, work with \CFA's generic types too.  As a structure can be defined over a parameterized element type, so can it be defined over a parameterized length.  Doing so gives a refinement of C's ``flexible array member'' pattern, that allows nesting structures with array members anywhere within other structures.
\lstinputlisting[language=C, firstline=20, lastline=26]{hello-accordion.cfa}
This structure's layout has the starting offest of @cost_contribs@ varying in @Nclients@, and the offset of @total_cost@ varying in both generic paramters.  For a function that operates on a @request@ structure, the type system handles this variation transparently.
\lstinputlisting[language=C, firstline=50, lastline=57]{hello-accordion.cfa}
In the example runs of a driver program, different offset values are navigated in the two cases.
\lstinputlisting[language=C, firstline=100, lastline=115]{hello-accordion.cfa}
The output values show that @summarize@ and its caller agree on both the offsets (where the callee starts reading @cost_contribs@ and where the callee writes @total_cost@).  Yet the call site still says just, ``pass the request.''