# Changeset 40ab446 for doc/theses/mike_brooks_MMath/array.tex

Ignore:
Timestamp:
Dec 11, 2023, 1:48:43 PM (4 months ago)
Branches:
master
Children:
77d46c7
Parents:
dab9fb93
Message:

Recent thesis writing

File:
1 edited

### Legend:

Unmodified
 rdab9fb93 \chapter{Array} \section{Introduction} This chapter describes my contribution of language and library features that provide a length-checked array type, as in: \begin{lstlisting} array(float, 99) x;    // x contains 99 floats void f( array(float, 42) & a ) {} f(x);                  // statically rejected: types are different forall( T, [N] ) void g( array(T, N) & a, int i ) { T elem = a[i];     // dynamically checked: requires 0 <= i < N } g(x, 0);               // T is float, N is 99, succeeds g(x, 1000);            // T is float, N is 99, dynamic check fails \end{lstlisting} This example first declares @x@ a variable, whose type is an instantiation of the generic type named @array@, with arguments @float@ and @99@. Next, it declares @f@ as a function that expects a length-42 array; the type system rejects the call's attempt to pass @x@ to @f@, because the lengths do not match. Next, the @forall@ annotation on function @g@ introduces @T@ as a familiar type parameter and @N@ as a \emph{dimension} parameter, a new feature that represents a count of elements, as managed by the type system. Because @g@ accepts any length of array; the type system accepts the calls' passing @x@ to @g@, inferring that this length is 99. Just as the caller's code does not need to explain that @T@ is @float@, the safe capture and communication of the value @99@ occurs without programmer involvement. In the case of the second call (which passes the value 1000 for @i@), within the body of @g@, the attempt to subscript @a@ by @i@ fails with a runtime error, since $@i@ \nless @N@$. The type @array@, as seen above, comes from my additions to the \CFA standard library. It is very similar to the built-in array type, which \CFA inherits from C. Its runtime characteristics are often identical, and some features are available in both. \begin{lstlisting} forall( [N] ) void declDemo() { float a1[N];         // built-in type ("C array") array(float, N) a2;  // type from library } \end{lstlisting} If a caller instantiates @N@ with 42, then both locally-declared array variables, @a1@ and @a2@, become arrays of 42 elements, each element being a @float@. The two variables have identical size and layout; they both encapsulate 42-float stack allocations, no heap allocations, and no further "bookkeeping" allocations/header. Having the @array@ library type (that of @a2@) is a tactical measure, an early implementation that offers full feature support. A future goal (TODO xref) is to port all of its features into the built-in array type (that of @a1@); then, the library type could be removed, and \CFA would have only one array type. In present state, the built-in array has partial support for the new features. The fully-featured library type is used exclusively in introductory examples; feature support and C compatibility are revisited in sec TODO. Offering the @array@ type, as a distinct alternative from the the C array, is consistent with \CFA's extension philosophy (TODO xref background) to date. A few compatibility-breaking changes to the behaviour of the C array were also made, both as an implementation convenience, and as justified fixes to C's lax treatment. The @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features. A clean slate was an important starting point because it meant not having to deal with every inherited complexity introduced in TODO xref background-array. My contributions are \begin{itemize} \item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@ \item [TODO: general parking...] \item identify specific abilities brought by @array@ \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{itemize} \section{Definitions and design considerations} \subsection{Dependent typing}