How to annotate STArray types?

Albert Y. C. Lai, trebla [at] vex [dot] net

When we use STArrays in the ST monad, we have to provide some type annotations, but what to provide is elusive. For example, this code fragment leads to type errors:

 a
slow_head xs = runST imperative_head
    where
    imperative_head =
        do { a <- newListArray (1, length xs) xs
           ; readArray a 1
           }
]]>

The type checker needs our help with more type annotations. The primary question is how to do it minimally and elegantly. (The secondary question is why it is so difficult.)

Solution

Here is a way: we will need just one type annotation, and it is for an array function - in this example I choose newListArray, though in general readArray, getElems, etc., are also good candidates. I choose the construction function rather than an access function because it is nearest to the beginning and it is slightly more stable over code change.

There are many variations. The most basic one:

 (i,i) -> [e] -> ST s (STArray s i e)) (1, n) xs
]]>

If you don't like in-situ annotations to be lengthy, you can move it elsewhere. Define a type synonym:

 STA s i e) (1, n) xs

...

type STA s i e = (i,i) -> [e] -> ST s (STArray s i e)
]]>

or a function synonym with the desired type annotation:

 (i,i) -> [e] -> ST s ((STArray s) i e)
newListArrayST = newListArray
]]>

Next, the type variables i and e can be replaced by concrete types according to the actual code if we desire. For example, in the above, i can be replaced by Int (and the constraint (Ix i)=> removed), as it ends up being instantiated to the type of length xs, which is Int anyway. Although not applicable to this example, if you also know what e must be, you can replace that too.

Discussion of the Dilemma

If you have time, we now reflect on why the type checker needs our help and why it is picky on the help we provide. It is a series of unfortunate events.

Most of the time we use overloaded operations from the MArray class for our STArrays, including array construction. Therefore all the type checker sees is we are writing general MArray code. But eventually we round it up with runST, and then someone has to choose a concrete array type (to make a long technical story short). In the absence of a functional dependency from the ST monad to any array type, we have to choose and specify one. And now the fun begins.

If we broke the code into several functions, some for constructing arrays and some for taking in arrays, that would expose the array type in the function types, and we could easily annotate those. The code would look like:

 ST s (STArray s Int e)
        make xs = newListArray (1, length xs) xs
        use :: STArray s Int e -> ST s e
        use a = readArray a 1
]]>

However, sometimes we prefer to keep it as one function in which we construct an array, use it, and discard it. Then the array type is not exposed in the type of the function. The next place to annotate would be at construction or mention of the array:

But the type variables s and e would cause troubles. To see this, let us look at a complete function and its type signature:

 ST s e   -- inferred or annotated, does not matter
    f xs =
        do { a <- newListArray (1, length xs) xs
           ; readArray (a :: STArray s Int e) 1   -- different s,e
           }
]]>

As explained in the Haskell 98 Report, Section 4.4.1, the two occurrences of s would not be unified; similarly for e. (In some cases, we can replace e by a concrete type, and that part of the problem disappears. But there is always s.) One way to yell at the type checker "they are the same s!" is to use an explicit forall:

 ST s e
    f xs =
        do { a <- newListArray (1, length xs) xs
           ; readArray (a :: STArray s Int e) 1   -- same s,e
           }
]]>

The forall quantifier extends the scope of type variables to the whole function; inside this scope all s's are the same. This is a solution, but forall is an extension to Haskell, and sometimes we prefer not to use it (e.g., it requires a compiler flag that also turns on a million other extensions, and we prefer not to turn on a million extensions just to use this one). Furthermore, this venue is not available in case we prefer to write the do-block inline rather than as a named definition, i.e.,

slow_head xs = runST ( do { ... } )   -- nowhere to insert "forall s"

So finally we turn to the functions used to construct or access the array. Annotating a function or name defined elsewhere is less tricky than annotating other expressions (again to make a long technical story short). In this case, as long as our annotation is equivalent to or more specific than the declared type of the function, it is fine.


I have more Haskell Notes and Examples