source: doc/theses/mike_brooks_MMath/array.tex @ 8d76f2b

ADTast-experimentalenumpthread-emulationqualifiedEnum
Last change on this file since 8d76f2b was 8d76f2b, checked in by Michael Brooks <mlbrooks@…>, 2 years ago

Adding runtime bound checking for array subscripts and showing the optimizer removing them.

Adding draft thesis content on dependent types and bound checks.

  • Property mode set to 100644
File size: 30.5 KB
Line 
1\chapter{Array}
2
3\section{Features Added}
4
5The present work adds a type @array@ to the \CFA standard library~\cite{Cforall}.
6
7This 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.
8
9This section presents motivating examples of the new array type's usage, and follows up with definitions of the notations that appear.
10
11The 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.
12\lstinputlisting[language=CFA, firstline=50, lastline=59]{hello-array.cfa}
13Here, 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.
14
15The 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.
16
17A harness for this @f@ function shows how dynamic values are fed into the system.
18\lstinputlisting[language=CFA, firstline=100, lastline=119]{hello-array.cfa}
19Here, 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.
20
21The 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).
22
23The 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.
24
25The 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:
26\begin{lstlisting}
27  forall( dtype T  ) ...
28  forall( otype T  ) ...
29  forall( ztype(N) ) ...
30\end{lstlisting}
31
32The 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.
33
34
35
36In summary:
37
38\begin{tabular}{p{15em}p{20em}}
39  @ztype( N )@ & within a forall, declares the type variable @N@ to be a governed length \\[0.25em]
40  @Z( @ $e$ @ )@ & a type representing the value of $e$ as a governed length, where $e$ is a @size_t@-typed expression \\[0.25em]
41  @z( N )@ & an expression of type @size_t@, whose value is the governed length @N@ \\[0.25em]
42  @array( thing, N0, N1, ... )@
43  &  a type wrapping $\prod_i N_i$ adjacent occurrences of @thing@ objects
44\end{tabular}
45
46Unsigned 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.
47
48
49An 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.
50\lstinputlisting[language=CFA, firstline=150, lastline=155]{hello-array.cfa}
51As is common practice in C, the programmer is free to cast, to assert knownledge not shared with the type system.
52\lstinputlisting[language=CFA, firstline=200, lastline=202]{hello-array.cfa}
53
54Argument 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.
55\lstinputlisting[language=CFA, firstline=20, lastline=26]{hello-accordion.cfa}
56This 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.
57\lstinputlisting[language=CFA, firstline=50, lastline=57]{hello-accordion.cfa}
58In the example runs of a driver program, different offset values are navigated in the two cases.
59\lstinputlisting[language=CFA, firstline=100, lastline=115]{hello-accordion.cfa}
60The 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.''
61
62
63\section{Multidimensional implementation}
64\label{toc:mdimpl}
65
66
67TODO: introduce multidimensional array feature and approaches
68
69The new \CFA standard library @array@ datatype supports multidimensional uses more richly than the C array.  The new array's multimentsional interface and implementation, follows an array-of-arrays setup, meaning, like C's @float[n][m]@ type, one contiguous object, with coarsely-strided dimensions directly wrapping finely-strided dimensions.  This setup is in contrast with the pattern of array of pointers to other allocations representing a sub-array.  Beyond what C's 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.  C and C++ require a programmer with such a need to manage pointer/offset arithmetic manually.
70
71Examples are shown using a $5 \times 7$ float array, @a@, loaded with increments of $0.1$ when stepping across the length-7 finely-strided dimension shown on columns, and with increments of $1.0$ when stepping across the length-5 corsely-strided dimension shown on rows.
72\lstinputlisting[language=CFA, firstline=120, lastline=128]{hello-md.cfa}
73The memory layout of @a@ has strictly increasing numbers along its 35 contiguous positions.
74
75A trivial form of slicing extracts a contiguous inner array, within an array-of-arrays.  Like with 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.  This action first subscripts away the most coaresly strided dimensions, leaving a result that expects to be be subscripted by the more finely strided dimensions.
76\lstinputlisting[language=CFA, firstline=60, lastline=66]{hello-md.cfa}
77\lstinputlisting[language=CFA, firstline=140, lastline=140]{hello-md.cfa}
78
79This function declaration is asserting too much knowledge about its parameter @c@, for it to be usable for printing either a row slice or a column slice.  Specifically, declaring the parameter @c@ with type @array@ means that @c@ is contiguous.  However, the function does not use this fact.  For the function to do its job, @c@ need only be of a container type that offers a subscript operator (of type @ptrdiff_t@ $\rightarrow$ @float@), with governed length @N@.  The new-array library provides the trait @ix@, so-defined.  With it, the original declaration can be generalized, while still implemented with the same body, to the latter declaration:
80\lstinputlisting[language=CFA, firstline=40, lastline=44]{hello-md.cfa}
81\lstinputlisting[language=CFA, firstline=145, lastline=145]{hello-md.cfa}
82
83Nontrivial slicing, in this example, means passing a noncontiguous slice to @print1d@.  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 left ``not yet subscripted by a value,'' implementing the @ix@ trait, waiting for such a value.
84\lstinputlisting[language=CFA, firstline=150, lastline=151]{hello-md.cfa}
85
86The example has shown that @a[2]@ and @a[[2, all]]@ both refer to the same, ``2.*'' slice.  Indeed, the various @print1d@ calls under discussion access the entry with value 2.3 as @a[2][3]@, @a[[2,all]][3]@, and @a[[all,3]][2]@.  This design preserves (and extends) C array semantics by defining @a[[i,j]]@ to be @a[i][j]@ for numeric subscripts, but also for ``subscripting by all''.  That is:
87
88\begin{tabular}{cccccl}
89    @a[[2,all]][3]@  &  $=$  &  @a[2][all][3]@  & $=$  &  @a[2][3]@  & (here, @all@ is redundant)  \\
90    @a[[all,3]][2]@  &  $=$  &  @a[all][3][2]@  & $=$  &  @a[2][3]@  & (here, @all@ is effective)
91\end{tabular}
92
93Narrating progress through each of the @-[-][-][-]@ expressions gives, firstly, a definition of @-[all]@, and secondly, a generalization of C's @-[i]@.
94
95\noindent Where @all@ is redundant:
96
97\begin{tabular}{ll}
98    @a@  & 2-dimensional, want subscripts for coarse then fine \\
99    @a[2]@  & 1-dimensional, want subscript for fine; lock coarse = 2 \\
100    @a[2][all]@  & 1-dimensional, want subscript for fine \\
101    @a[2][all][3]@  & 0-dimensional; lock fine = 3
102\end{tabular}
103
104\noindent Where @all@ is effective:
105
106\begin{tabular}{ll}
107    @a@  & 2-dimensional, want subscripts for coarse then fine \\
108    @a[all]@  & 2-dimensional, want subscripts for fine then coarse \\
109    @a[all][3]@  & 1-dimensional, want subscript for coarse; lock fine = 3 \\
110    @a[all][3][2]@  & 0-dimensional; lock coarse = 2
111\end{tabular}
112
113The semantics of @-[all]@ is to dequeue from the front of the ``want subscripts'' list and re-enqueue at its back.  The semantics of @-[i]@ is to dequeue from the front of the ``want subscripts'' list and lock its value to be @i@.
114
115Contiguous arrays, and slices of them, are all realized by the same underlying parameterized type.  It includes stride information in its metatdata.  The @-[all]@ operation is a conversion from a reference to one instantiation, to a reference to another instantiation.  The running example's @all@-effective step, stated more concretely, is:
116
117\begin{tabular}{ll}
118    @a@       & : 5 of ( 7 of float each spaced 1 float apart ) each spaced 7 floats apart \\
119    @a[all]@  & : 7 of ( 5 of float each spaced 7 floats apart ) each spaced 1 float apart
120\end{tabular}
121
122\begin{figure}
123    \includegraphics{measuring-like-layout}
124    \caption{Visualization of subscripting by value and by \lstinline[language=CFA,basicstyle=\ttfamily]{all}, for \lstinline[language=CFA,basicstyle=\ttfamily]{a} of type \lstinline[language=CFA,basicstyle=\ttfamily]{array( float, Z(5), Z(7) )}. The horizontal dimension represents memory addresses while vertical layout is conceptual.}
125    \label{fig:subscr-all}
126\end{figure}
127
128\noindent While the latter description implies overlapping elements, Figure \ref{fig:subscr-all} shows that the overlaps only occur with unused spaces between elements.  Its depictions of @a[all][...]@ show the navigation of a memory layout with nontrivial strides, that is, with ``spaced \_ floats apart'' values that are greater or smaller than the true count of valid indeces times the size of a logically indexed element.  Reading from the bottom up, the expression @a[all][3][2]@ shows a float, that is masquerading as a @float[7]@, for the purpose of being arranged among its peers; five such occurrences form @a[all][3]@.  The tail of flatter boxes extending to the right of a poper element represents this stretching.  At the next level of containment, the structure @a[all][3]@ masquerades as a @float[1]@, for the purpose of being arranged among its peers; seven such occurrences form @a[all]@.  The verical staircase arrangement represents this compression, and resulting overlapping.
129
130The new-array library defines types and operations that ensure proper elements are accessed soundly in spite of the overlapping.  The private @arpk@ structure (array with explicit packing) is generic over these two types (and more): the contained element, what it is masquerading as.  This structure's public interface is the @array(...)@ construction macro and the two subscript operators.  Construction by @array@ initializes the masquerading-as type information to be equal to the contained-element information.  Subscrpting by @all@ rearranges the order of masquerading-as types to achieve, in genernal, 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 there element found there, in unmasked form.
131
132The @arpk@ structure and its @-[i]@ operator are thus defined as:
133\begin{lstlisting}
134forall( ztype(N),               // length of current dimension
135        dtype(S) | sized(S),    // masquerading-as
136        dtype E_im,             // immediate element, often another array
137        dtype E_base            // base element, e.g. float, never array
138      ) {
139    struct arpk {
140        S strides[z(N)];        // so that sizeof(this) is N of S
141    };
142
143    // expose E_im, stride by S
144    E_im & ?[?]( arpk(N, S, E_im, E_base) & a, ptrdiff_t i ) {
145        return (E_im &) a.strides[i];
146    }
147}
148\end{lstlisting}
149
150An instantion of the @arpk@ generic is given by the @array(E_base, N0, N1, ...)@ exapnsion, 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.
151
152Subscripting by @all@, to operate on nontrivial strides, is a dequeue-enqueue operation on the @E_im@ chain, which carries @S@ instatiations, intact, to new positions.  Expressed as an operation on types, this rotation is:
153\begin{eqnarray*}
154suball( arpk(N, S, E_i, E_b) ) & = & enq( N, S, E_i, E_b ) \\
155enq( N, S, E_b, E_b ) & = & arpk( N, S, E_b, E_b ) \\
156enq( N, S, arpk(N', S', E_i', E_b), E_b ) & = & arpk( N', S', enq(N, S, E_i', E_b), E_b )
157\end{eqnarray*}
158
159
160\section{Bound checks, added and removed}
161
162\CFA array subscripting is protected with runtime bound checks.  Having dependent typing causes the opimizer to remove more of these bound checks than it would without them.  This section provides a demonstration of the effect.
163
164The experiment compares the \CFA array system with the padded-room system [todo:xref] most typically exemplified by Java arrays, but also reflected in the C++ 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 C++ version to keep access to generated assembly code simple.
165
166As a control case, a simple loop (with no reused dimension sizes) is seen to get the same optimization treatment in both the \CFA and C++ 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 assemly, ready to catch an occurrence the mistake.
167
168TODO: paste source and assemby codes
169
170Incorporating 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.
171
172TODO: paste source codes
173
174
175
176
177
178\section{Comparison with other arrays}
179
180\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 that further helps guarantee statically the validity of every pointer deference.  These systems, therefore, ask the programmer to convince the typechecker that every pointer dereference is valid.  \CFA imposes the lighter-weight obligation, with the more limited guarantee, that initially-declared bounds are respected thereafter.
181
182\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.
183
184\subsction{Safety in a padded room}
185
186Java's array [todo:cite] is a straightforward example of assuring safety against undefined behaviour, at a cost of expressiveness for more applied properties.  Consider the array parameter declarations in:
187
188\begin{tabular}{rl}
189    C      &  @void f( size_t n, size_t m, float a[n][m] );@ \\
190    Java   &  @void f( float[][] a );@
191\end{tabular}
192
193Java's safety against undefined behaviour assures the callee that, if @a@ is non-null, then @a.length@ is a valid access (say, evaluating to the number $\ell$) and if @i@ is in $[0, \ell)$ then @a[i]@ is a valid access.  If a value of @i@ outside this range is used, a runtime error is guaranteed.  In these respects, C offers no guarantess at all.  Notably, the suggestion that @n@ is the intended size of the first dimension of @a@ is documentation only.  Indeed, many might prefer the technically equivalent declarations @float a[][m]@ or @float (*a)[m]@ as emphasizing the ``no guarantees'' nature of an infrequently used language feature, over using the opportunity to explain a programmer intention.  Moreover, even if @a[0][0]@ is valid for the purpose intended, C's basic infamous feature is the possibility of an @i@, such that @a[i][0]@ is not valid for the same purpose, and yet, its evaluation does not produce an error.
194
195Java's lack of expressiveness for more applied properties means these outcomes are possible:
196\begin{itemize}
197    \item @a[0][17]@ and @a[2][17]@ are valid accesses, yet @a[1][17]@ is a runtime error, because @a[1]@ is a null pointer
198    \item the same observation, now because @a[1]@ refers to an array of length 5
199    \item execution times vary, because the @float@ values within @a@ are sometimes stored nearly contiguously, and other times, not at all
200\end{itemize}
201C's array has none of these limitations, nor do any of the ``array language'' comparators discussed in this section.
202
203This Java level of safety and expressiveness is also exemplified in the C family, with the commonly given advice [todo:cite example], for C++ programmers to use @std::vector@ in place of the C++ language's array, which is essentially the C array.  The advice is that, while a vector is also more powerful (and quirky) than an arry, its capabilities include options to preallocate with an upfront size, to use an available bound-checked accessor (@a.at(i)@ in place of @a[i]@), to avoid using @push_back@, and to use a vector of vectors.  Used with these restrictions, out-of-bound accesses are stopped, and in-bound accesses never exercise the vector's ability to grow, which is to say, they never make the program slow to reallocate and copy, and they never invalidate the program's other references to the contained values.  Allowing this scheme the same referential integrity assumption that \CFA enjoys [todo:xref], this scheme matches Java's safety and expressiveness exactly.  [TODO: decide about going deeper; some of the Java expressiveness concerns have mitigations, up to even more tradeoffs.]
204
205\subsection{Levels of dependently typed arrays}
206
207The \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:
208\begin{itemize}
209    \item a \emph{zip}-style operation that consumes two arrays of equal length
210    \item a \emph{map}-style operation whose produced length matches the consumed length
211    \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
212\end{itemize}
213Across this field, this expressiveness is not just an avaiable 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.
214
215
216
217Dependent 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]
218
219Idris is a current, general-purpose dependently typed programming language.  Length checking is a common benchmark for full dependent type stystems.  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]
220
221POINTS:
222here is how our basic checks look (on a system that deosn't have to compromise);
223it can also do these other cool checks, but watch how I can mess with its conservativeness and termination
224
225Two current, state-of-the-art array languages, Dex\cite{arr:dex:long} and Futhark\cite{arr:futhark:tytheory}, offer 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 leightweight bounds-only analysis.  Like \CFA, their checks that are conservatively limited by forbidding arithmetic in the depended-upon expression.
226
227
228
229The 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. 
230
231Dex uses a novel conception of size, embedding its quantitative information completely into an ordinary type.
232
233Futhark and full-strength dependently typed lanaguages treat array sizes are ordinary values.  Futhark restricts these expressions syntactically to variables and constants, while a full-strength dependent system does not.
234
235CFA'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.
236
237\subsection{Static safety in C extensions}
238
239
240\section{Future Work}
241
242\subsection{Declaration syntax}
243
244\subsection{Range slicing}
245
246\subsection{With a module system}
247
248\subsection{With described enumerations}
249
250A project in \CFA's current portfolio will improve enumerations.  In the incumbent state, \CFA has C's enumerations, unmodified.  I will not discuss the core of this project, which has a tall mission already, to improve type safety, maintain appropriate C compatibility and offer more flexibility about storage use.  It also has a candidate stretch goal, to adapt \CFA's @forall@ generic system to communicate generalized enumerations:
251\begin{lstlisting}
252    forall( T | is_enum(T) )
253    void show_in_context( T val ) {
254        for( T i ) {
255            string decorator = "";
256            if ( i == val-1 ) decorator = "< ready";
257            if ( i == val   ) decorator = "< go"   ;
258            sout | i | decorator;
259        }
260    }
261    enum weekday { mon, tue, wed = 500, thu, fri };
262    show_in_context( wed );
263\end{lstlisting}
264with output
265\begin{lstlisting}
266    mon
267    tue < ready
268    wed < go
269    thu
270    fri
271\end{lstlisting}
272The details in this presentation aren't meant to be taken too precisely as suggestions for how it should look in \CFA.  But the example shows these abilities:
273\begin{itemize}
274    \item a built-in way (the @is_enum@ trait) for a generic routine to require enumeration-like information about its instantiating type
275    \item an implicit implementation of the trait whenever a user-written enum occurs (@weekday@'s declaration implies @is_enum@)
276    \item a total order over the enumeration constants, with predecessor/successor (@val-1@) available, and valid across gaps in values (@tue == 1 && wed == 500 && tue == wed - 1@)
277    \item a provision for looping (the @for@ form used) over the values of the type.
278\end{itemize}
279
280If \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.
281
282[TODO: indroduce Ada in the comparators]
283
284In Ada and Dex, an array is conceived as a function whose domain must satisfy only certain structural assumptions, while in C, C++, 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.
285
286This change of perspective also lets us remove ubiquitous dynamic bound checks.  [TODO: xref] discusses how automatically inserted bound checks can often be otimized 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 ubiquitious 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.
287
288[TODO, fix confusion:  Idris has this arrangement of checks, but still the natural numbers as the domain.]
289
290The 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.
291\begin{lstlisting}
292interface Ix n
293  get_size n : Unit -> Int
294  ordinal : n -> Int
295  unsafe_from_ordinal n : Int -> n
296\end{lstlisting}
297
298Dex 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 funciton.  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 dimensoned interpretations of ``size,'' this function requries the argument sizes to match, and it produces a result of the that size.
299
300The polymorphism plays out with the pointwise-difference routine advertizing 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
301\begin{lstlisting}
302instance {a b} [Ix a, Ix b] Ix (a & b)
303  get_size = \(). size a * size b
304  ordinal = \(i, j). (ordinal i * size b) + ordinal j
305  unsafe_from_ordinal = \o.
306    bs = size b
307    (unsafe_from_ordinal a (idiv o bs), unsafe_from_ordinal b (rem o bs))
308\end{lstlisting}
309and 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
310\begin{lstlisting}
311    img_trans :: (img_wd,img_ht)=>Real
312    img_trans.(i,j) = img.i.j
313    result = pairwise img_trans
314\end{lstlisting}
315[TODO: cite as simplification of example from https://openreview.net/pdf?id=rJxd7vsWPS section 4]
316
317In 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.
318
319\subsection{Retire pointer arithmetic}
Note: See TracBrowser for help on using the repository browser.