Ignore:
Timestamp:
Dec 11, 2023, 1:48:43 PM (4 months ago)
Author:
Michael Brooks <mlbrooks@…>
Branches:
master
Children:
77d46c7
Parents:
dab9fb93
Message:

Recent thesis writing

File:
1 edited

Legend:

Unmodified
Added
Removed
  • doc/theses/mike_brooks_MMath/array.tex

    rdab9fb93 r40ab446  
    11\chapter{Array}
     2
     3\section{Introduction}
     4
     5This chapter describes my contribution of language and library features that provide a length-checked array type, as in:
     6
     7\begin{lstlisting}
     8    array(float, 99) x;    // x contains 99 floats
     9
     10    void f( array(float, 42) & a ) {}
     11    f(x);                  // statically rejected: types are different
     12
     13    forall( T, [N] )
     14    void g( array(T, N) & a, int i ) {
     15        T elem = a[i];     // dynamically checked: requires 0 <= i < N
     16    }
     17    g(x, 0);               // T is float, N is 99, succeeds
     18    g(x, 1000);            // T is float, N is 99, dynamic check fails
     19\end{lstlisting}
     20
     21This example first declares @x@ a variable, whose type is an instantiation of the generic type named @array@, with arguments @float@ and @99@.
     22Next, 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.
     23Next, 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.
     24Because @g@ accepts any length of array; the type system accepts the calls' passing @x@ to @g@, inferring that this length is 99.
     25Just 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.
     26In 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@$.
     27
     28The type @array@, as seen above, comes from my additions to the \CFA standard library.
     29It is very similar to the built-in array type, which \CFA inherits from C.
     30Its runtime characteristics are often identical, and some features are available in both.
     31
     32\begin{lstlisting}
     33    forall( [N] )
     34    void declDemo() {
     35        float a1[N];         // built-in type ("C array")
     36        array(float, N) a2;  // type from library
     37    }
     38\end{lstlisting}
     39
     40If 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@.
     41The two variables have identical size and layout; they both encapsulate 42-float stack allocations, no heap allocations, and no further "bookkeeping" allocations/header.
     42Having the @array@ library type (that of @a2@) is a tactical measure, an early implementation that offers full feature support.
     43A 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.
     44In present state, the built-in array has partial support for the new features.
     45The fully-featured library type is used exclusively in introductory examples; feature support and C compatibility are revisited in sec TODO.
     46
     47Offering the @array@ type, as a distinct alternative from the the C array, is consistent with \CFA's extension philosophy (TODO xref background) to date.
     48A 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.
     49
     50The @array@ type is an opportunity to start from a clean slate and show a cohesive selection of features.
     51A clean slate was an important starting point because it meant not having to deal with every inherited complexity introduced in TODO xref background-array.
     52
     53
     54My contributions are
     55\begin{itemize}
     56    \item a type system enhancement that lets polymorphic functions and generic types be parameterized by a numeric value: @forall( [N] )@
     57    \item [TODO: general parking...]
     58    \item identify specific abilities brought by @array@
     59    \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
     60\end{itemize}
     61
     62
     63
     64\section{Definitions and design considerations}
     65
     66\subsection{Dependent typing}
     67
     68
    269
    370
Note: See TracChangeset for help on using the changeset viewer.