What about arrays? After doing my little C-like DSEL in Haskell I started wondering if you could do arrays that look like C arrays too. It turns out you can, but I can't figure out a way to make it safe from certain runtime errors. Array indexing in C is written a[i], and this is legal syntax in Haskell too, so we're off to a good start. But to make it work we need a to be a function that takes a list and returns something. What should it return? It must be something that is both an l-value and an r-value. Just as I had a function auto to create a local variable, I'll have a function arr to make a local array. It will take the size of the array and then return a function that takes the index. For simplicity I'll make the index be an Int.

arr :: forall a . [E Int] -> E (forall v . [E Int] -> E' v a)

So now this type checks

atest = do {
    a <- arr[2];
    a[1] =: a[0] + 1;
  }

Now we just need the body of arr.

arr [s] = do
    s' <- runE s
    a <- newArray (0, s' - 1) undefined :: IO (IOArray Int a)
    let ix [i] = runE i
    return (\ is -> V (ix is >>= readArray a)
                      (\ x -> ix is >>= \ i -> writeArray a i x))

The arr function takes a list with one element, the size, and allocates an array (indexed from 0) with this size. It then returns a function that expects a singleton list with an index and returns the V constructor which I used for variables. For multidimensional arrays we can extend the arr function.

arr ss = do
    ss' <- mapM runE ss
    let sz = product ss'
        ix is = do
                    is' <- mapM runE is
                    when (length is' /= length ss') $ error "wrong number of indicies"
                    return $ foldr (\ (i, s) r -> r * s + i) 0 (zip is' ss')
    a <- newArray (0, product ss' - 1) undefined :: IO (IOArray Int a)
    return (\ is -> V (ix is >>= readArray a) (\ x -> ix is >>= \ i -> writeArray a i x))

The problem with both these definitions is that the number of indicies is checked dynamically rather than statically. To do it statically we'd have to be able to overload the syntax for list literals to use a type that keeps track of the number of elements.