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. At of this writing (and this is expected to change) 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

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, you will be creating one of these. For example:

Array[\RR64,ZZ32\]	a 1-D array of doubles with unknown bounds
Array[\Mumble, (ZZ32,ZZ32,ZZ32) \]	a 3-D array of objects of type Mumble with unknown bounds

You create an Array using the array[\E\] factory:

array[\RR64\](m,n)

creates a 0-based 2-D m×n array of doubles.

This is a supertype of the various concrete array types whose bounds are known, shown at the top of the page. The above call to array will return an instance of Array2[\RR64,m,n\] 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, so at compile time we only know that the static type is the latter type.

The next trick is to "unwrap" the more specific type. Once we know the type, we know the bounds information and we can write fully bounds-checked code. There are two basic approaches:

1. 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.

2. 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:

     a1 = array[\RR64\](m,n).fill(0)
     a2 = array[\ZZ32\](m,n).fill(1)
     f(a1,a2)
   

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 with today's interpreter):

  f[\nat r, nat c\]( f: Array2[\RR64, r, c\], i: Array2[\ZZ32, r, c\] ) = do
    ... (* I can assume the sizes of these arrays are statically known to be r×c *)
  end

But this is type-ambiguous, so we have to provide another overloading which 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:

  f[\nat r, nat c\](f: Array[\RR64, (ZZ32, ZZ32)\], i: Array2[\ZZ32, (ZZ32, ZZ32)\])=
      fail("Array sizes do not match dynamically.")

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.

This is actually a bit problematic because it involves inferring useless parameters in one of the overloadings, which become useful in the other one, 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:

  f( f: Array2[\RR64, r, c\], i: Array2[\ZZ32, r, c\] ) where { nat r, nat c } = do
    ... (* I can assume the sizes of these arrays are statically known to be rxc *)
  end

  f( f: Array[\RR64, (ZZ32, ZZ32)\], i: Array2[\ZZ32, (ZZ32, ZZ32)\] ) =
      fail("Array sizes do not match dynamically.")

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 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.

One thing we can't do is write a function like this one:

  toStatic( f: Array[\RR64, ZZ32\] ): Array1[\RR64,lo,size\]

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).

---

Return to the Fortress How Tos