Creating Variable-Sized Arrays in Fortress
Fortress tries to capture as much bounds information about arrays as possible in the static type of the array. This yields a family of array types which look like:
| Array1[\E,b0,s0\] | a 1-D array of element type E with s0 elements starting from b0 |
| Array2[\E,b0,s0,b1,s1\] | a 2-D array of element type E with s0×s1 elements, origin (b0,b1) |
| Array3[\E,b0,s0,b1,s1,b2,s2\] | a 3-D array, as above |
Let call these array types with full bounds information. The format of the type arguments is always element type E first, followed by base index and size in the first dimension, followed by base index and size in the second dimension, and so forth.
Array types when you don't know the array bounds
There is one other type of interest in the Fortress array hierarchy: Array[\E,I\] is the type of arrays with elements E and indices I whose bounds are unknown. If you don't know your array's bounds at compile time, this is the type you will use to talk about that array. For example:
| Array[\RR64,ZZ32\] | a 1-D array of doubles with unknown bounds |
| Array[\Boolean, (ZZ32,ZZ32,ZZ32) \] | a 3-D array of objects of type Boolean with unknown bounds |
You create an Array using the array[\E\] factory:
| Factory call | Static result type | Dynamic type (see below) | description |
| array[\RR64\](m,n) | Array[\RR64, (ZZ32,ZZ32) \] | Array2[\RR64,0,m,0,n\] | a 0-based 2-D m×n array of doubles. |
| array[\Boolean\](n) | Array[\Boolean, ZZ32\] || Array1[\Boolean,0,''n'' \] || a 0-based 1-D array of booleans of length n`. |
The type Array[\E,I\] is a supertype of the various concrete array types whose bounds are known, shown at the top of the page. Thus, the first call to array above returns an instance of Array2[\RR64,...\] which is in turn an instance of Array[\RR64, (ZZ32,ZZ32)\]. The typechecker doesn't know at compile time what m and n to choose, though, because they are run-time values; so at compile time we must assume that the static type is the latter type.
Note that the type Array[\E,I\] has two static parameters, while the factory array[\E\] has only one (the element type). This is because not every index type I is legal; right now only ZZ32, (ZZ32,ZZ32), and (ZZ32,ZZ32,ZZ32) are accepted. We use overloading to determine the index type based on the size you specify when array is called.
Getting specific static bounds back from dynamically-sized arrays
Often, we'd like to use the more-specific bounds information obtained dynamically. Once we know the bounds information we can write fully bounds-checked code. There are two basic approaches:
- Use typecase: Sadly, this doesn't work at the moment because you can't bind static variables (like b0 and s0) in a typecase clause.
- Use function overloading: There's the version of this that works right now, and the version that is type-correct. Luckily, they're not too different. For example, let's say I create two m×n arrays:
Loading...
Getting specific bounds information using function overloading
Now I want to write a function which takes two identically-sized 2-D arrays. I can write it like this (here is a version which will work today):
But this is type-ambiguous, so we have to provide another overloading that handles the ambiguous cases. Since in general we can't prove statically that a random Array[\RR64,ZZ32\] and Array[\ZZ32,ZZ32\] have the same bounds, we're in effect using overloading to do the checking dynamically. Here is the other overloading:
Now, if the array sizes match dynamically, we will pick the more specific overloading; if they don't, we use the less specific overloading, which will fail.
Any bounds must be mentioned in the arguments
One thing we can't do is write a function like this one:
Here lo and size must somehow be existentially bound---that is, they should be picked by toStatic rather than plugged in at the call site. But there's no way to say that in Fortress (and it's a challenging but interesting problem with current type systems in other languages, too). The basic rule of thumb is this:
We can mention bounds on argument arrays; bounds on result arrays must be derived from bounds on argument arrays.
Specific bounds information using where clauses (does not work at present)
This is actually a bit problematic because it involves inferring parameters in one of the overloadings, and really we can see that the actual values of those parameters aren't available at compile time. What we should really be doing is using a where clause instead:
We're discussing adding binding forms to typecase, as well, since this involves a bit less heavy lifting at type-checking time to make things work out. But meanwhile techniques like the one shown here have been used to implement the internals of the array[\E\] factory itself. If you want to learn more, I encourage you to look at the code for array[\E\] in source:trunk/Library/FortressLibrary.fss. In there you'll see a bunch of trickery which uses overloading and type parameters to reify a dynamic ZZ32 as a static nat parameter.
