Limitations of the type system

This section discusses in some detail some of limitations of the type systems from Chapter 3. Some of the limitations where pointed out in Section 4.1.

4.2.1 Representation of Matrices

As already mentioned in Section 4.1.4, matrices pose a challenge for the type systems. Before we go into details about the problems with the type systems, we quickly review the basic strategies for representing matrices (or in general, multi-dimensional arrays) using single-dimensional arrays. One strategy is to represent matrices as arrays of arrays. That is, we represent a matrix with Nrows andMcolumns as an array of sizeNwhere each element is a pointer to a row: an array of size Mas illustrated in Figure 4.7(a). Alternatively, we can use an array of size Mwhere each element is a pointer to a column: an array of size N. Another strategy is to flatten the matrix into just one array.

That is, we represent a matrix with N rows and M columns as an array of sizeN·M. Again, when we flatten the matrix we can either put the elements in row major order, as illustrated in Figure 4.7(c), or in column major order as illustrated in Figure 4.7(d).

In thematrix_multexample from Section 4.1.4 we saw that in the baseline type system the regfile type:

[ i0 : fix xarray(n) xarray(m) ]

specifies that the registeri0contains a pointer to a matrix withnrows and mcolumns represented as an array of fixed-point arrays.

When we try to translate this type using the extended type system we run into problems. Our first attempt might be the following store type and regfile type:

XMEM[ p1 -> fix [n], p2 -> xptr(p1, 0) [m] ] [ i0 : xptr(p2, 0) ]

However this is not the type of a matrix where each element occupies one distinct memory location. Instead it is the type of a matrix where all the rows are shared, as illustrated in Figure 4.7(b). Notice, that with the baseline

0,0 0,1

1,0 1,1

2,0 2,1

(a) Array of arrays, row major

x,0 x,1

(b) Array of arrays, shared

0,0 0,1 1,0 1,1 2,0 2,1

(c) Flattened, row major (C layout)

0,0 1,0 2,0 0,1 1,1 2,1

(d) Flattened, column major (Fortran layout)

Figure 4.7: Different representations of matrices

type system it is impossible to distinguish between the two representations in Figure 4.7(a) and Figure 4.7(b). One way to fix the extended type system is to introduce existential types over location variables in the style of Walker [53]. If we had existential types over location variables, then we could write the type of a matrix with nrows andmcolumns represented as an array of fixed-point arrays as the following store type and regfile type:

XMEM[ p1 -> (? p . XMEM[ p -> fix [n]] xptr(p, 0)) [m] ] [ i0 : xptr(p1, 0) ]

(where the question mark is used as ASCII notation for existential quan-tification). Here the regfile type says that i0 contains the pointer p1 into X memory, and the store type says that starting at locationp1there is a block ofmpointers, all distinct and different fromp1, and each pointing to a block of n fixed-point numbers. However, it is not straightforward to introduce existential quantification over location variables, and if we are not careful it is easy to introduce type unsoundness. I go into more detail about how to extend the type system with existential quantification over location variables in Section 6.1.2.

None of our type systems can handle matrices in the flattened represen-tation because of the limirepresen-tations of Presburger arithmetic. In the baseline type system, if the registeri0contains a pointer to a matrix withnrows and m columns represented as a single array of fixed-point numbers we would write the regfile type:

[i0 : fix xarray(n*m) ]

This looks promising, but the index expression denoting the length of the array is not a representable expression in Presburger arithmetic, because we multiply two variables. Similarly, in the extended type system we would write the store type and regfile type as:

XMEM[ p1 -> fix [n*m] ] [ i0 : xptr(p1, 0) ]

which suffers from the same problem.

The problem only occurs when both the number of rows and the number of columns are not statically known. For example, if we know that there are three rows andmcolumns. Then, in the baseline type system, we can write the regfile type:

[ i0 : fix xarray(3*m) ]

which is expressible in Presburger arithmetic. In the extended type system we have more choices. We could write the store type and regfile type as:

XMEM[ p1 -> fix [m] @ fix[m] @ fix[m]]

[ i0 : fix xptr(p1, 0) ] or

XMEM[ p1 -> fix [3*m]]

[ i0 : fix xptr(p1, 0) ]

which are equivalent, and both types only contain index expressions which are representable in Presburger arithmetic.

We might argue that in resource constrained embedded software with-out dynamic memory allocation, all dimensions are always statically known, hence the problems described in this section are of no concern. This is a weak argument, however, because we want to be able to type check a procedure without knowing all the places where it is called. And we want library func-tions likematrix_multto work with different, perhaps dynamically decided, dimensions. Section 6.1.2 discusses other extensions to the type systems.

4.2.2 Size of Type Annotations

It is apparent from the examples shown in this chapter that the type annota-tions can get large and somewhat unmanageable to write by hand. The two main reasons for the size of the type annotations are:

• Lack of abstraction. The type annotations form a partial specification of the meaning of assembler code. Hence, due to the explicit and low level nature of assembler code, the type annotations also need to be quite explicit.

• Repetition. As we have seen, large parts of the type annotations are repetitions of types already given. One remedy for this problem may be to introduce syntax for type names to allow type abbreviations in some form.

4.2.3 Type rules not general enough

As noted in Section 3.5 and in Section 4.1.5 the lack of sum types is some-times cumbersome when we want to make the types less precise. The trouble typically occurs when we want to unify types stemming from different con-trol flows. In Section 3.5 we had to make a more complicated and specialised

1 multi_swap:

2 (r, s, a, b)

3 {n : int, m : int, t : int

4 | n > 0

5 /\ (n = 2*m ==> t = 0)

6 /\ (n = 2*m + 1 ==> t = 1) }

7 [ i0 : int(n),

8 x0 : a,

9 y0 : b,

10 dsp : r,

11 csp : [ i0 : int(n),

12 x0 : choose(t, a, b),

13 y0 : choose(t, b, a),

14 dsp : r,

15 csp : s] :: s

16 ]

Figure 4.8: Type annotations formulti_swapusingchoose-types.

typing rule fordo-loops and in Section 4.1.5 we had to settle for less general type annotations.

If we introduce something like thechoose-types of DTAL, suggested by Xi and Harper [55], we can write a more general type for the entry-point of the multi_swapprocedure from Section 4.1.5. Figure 4.8 shows the more general polymorphic type for multi_swap. Butchoose-types are not enough if we want to type-check multi_swapwith the more general type. The (do) rule only accommodates a substitution over index variables, not type variables.

This can be fixed, but the fix requires the type variable context, ∆, to be threaded through all typing rules.