Let say that the type b is an instance of Monoid and for a fixed indices range of (v1,v2) :: (i,i) with i belonging to the type class Ix I want to define the corresponding Data.Array type to be a Monoid as well. How can this be done? Here, mempty should be the Array with entries mempty::b and also mappend for arrays should be the mappend-operation component-wise.
(For instance if i=(Int,Int) the type Data.Array i b represents of all (2 dimensional) matricies with different sizes (and different ranges of the index). Only for fixed size such a Monoid-declaration makes sense. Actually, I am interested in the vector-space case instead of Monoids, but Monoid already shows the difficulty. I have only a vague idea about dependent type but this seems to be a prototypical example for a situation in which individual types corresponding to the only a subset of the range of one parameter would be useful.)
A common way is to wrap a not-very-typed representation into a more typed one like this:
data Nat = Z | S Nat
newtype Vec (n :: Nat) a = Vec [a]
newtype Sized m (ns :: [Nat]) a = Sized { getArray :: Array (Vec m Int) a }
Here ns is a promoted (see Giving Haskell a Promotion) phantom (see Motivation behind Phantom Types?) value — a list of sizes of dimensions and m is the length of this list (promoted and phantom as well). So any array under the Sized wrapper is assumed to be a multidimensional matrix with ns representing its dimensions. The Monoid instance then looks like this:
instance (SingI m, SingI ns, Monoid a) => Monoid (Sized m ns a) where
mempty = listSized $ repeat mempty
Sized as `mappend` Sized bs = listSized $ zipWith mappend (elems as) (elems bs)
That SingI stuff is from the singletons library. Singletons allow to lift values to the type-level, so we can kinda emulate dependent types, and SingI allows to get lifted values back at the value level via the fromSing function. listSized is essentially listArray, but for arrays with statically known dimensions and hence it requires all those SingIs to be in scope. Here is its definition:
toInt :: Nat -> Int
toInt = go 0 where
go !a Z = a
go a (S n) = go (1 + a) n
vecBounds :: forall m (ns :: [Nat]). (SingI m) => Sing ns -> (Vec m Int, Vec m Int)
vecBounds singNs = (Vec $ replicate m 0, Vec ns') where
m = toInt $ fromSing (sing :: Sing m)
ns' = map (pred . toInt) $ fromSing singNs
listSized :: forall m (ns :: [Nat]) a. (SingI m, SingI ns) => [a] -> Sized m ns a
listSized = Sized . listArray (vecBounds (sing :: Sing ns))
vecBounds computes bounds for a given promoted list of sizes of dimensions. It returns a tuple which first component is the lowerest index which is always of the form [0,0..0] (there as many zeros as there are dimensions, i.e. m). The second component is the greatest index, so if you e.g. have a list of sizes of dimensions like [2, 1, 3] (represented as [S (S Z), S Z, S (S (S Z))]), then the maximum index is [1, 0, 2].
It only remains to provide an Ix instance for Vec n a which is a direct generalization of the product instances:
instance Ix a => Ix (Vec n a) where
range (Vec ns, Vec ms) = map Vec . sequence $ zipWith (curry range) ns ms
index (Vec ns, Vec ms) (Vec ps) = foldr (\(i, r) a -> i + r * a) 0 $
zipWith3 (\n m p -> (index (n, m) p, rangeSize (n, m))) ns ms ps
inRange (Vec ns, Vec ms) (Vec ps) = and $ zipWith3 (curry inRange) ns ms ps
And we can write some tests:
type M = S (S (S Z))
type Ns = [S (S Z), S Z, S (S (S Z))]
arr1 :: Sized M Ns (Sum Int)
arr1 = listSized $ map Sum [5,3,6,7,1,4]
arr2 :: Sized M Ns (Sum Int)
arr2 = listSized $ map Sum [8,2,9,7,3,6]
main = mapM_ (print . getArray) $ [arr1, arr2, arr1 `mappend` arr2 `mappend` mempty]
This prints
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 5}),(Vec [0,0,1],Sum {getSum = 6}),(Vec [0,0,2],Sum {getSum = 1}),(Vec [1,0,0],Sum {getSum = 3}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 4})]
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 8}),(Vec [0,0,1],Sum {getSum = 9}),(Vec [0,0,2],Sum {getSum = 3}),(Vec [1,0,0],Sum {getSum = 2}),(Vec [1,0,1],Sum {getSum = 7}),(Vec [1,0,2],Sum {getSum = 6})]
array (Vec [0,0,0],Vec [1,0,2]) [(Vec [0,0,0],Sum {getSum = 13}),(Vec [0,0,1],Sum {getSum = 15}),(Vec [0,0,2],Sum {getSum = 4}),(Vec [1,0,0],Sum {getSum = 5}),(Vec [1,0,1],Sum {getSum = 14}),(Vec [1,0,2],Sum {getSum = 10})]
I.e. elements were summed pointwise as required. And if you accidentally try to sum arrays with different dimensions, you'll get a type error:
type Ns = [S (S Z), S Z, S (S (S Z))]
type Ns' = [S (S (S Z)), S Z, S (S Z)]
arr1 :: Sized M Ns (Sum Int)
arr1 = listSized $ map Sum [5,3,6,7,1,4]
arr2 :: Sized M Ns' (Sum Int)
arr2 = listSized $ map Sum [8,2,9,7,3,6]
main = print . getArray $ arr1 `mappend` arr2
-- Couldn't match type 'S 'Z with 'Z …
-- Expected type: Sized M Ns (Sum Int)
-- Actual type: Sized M Ns' (Sum Int)
-- In the second argument of `mappend', namely `arr2'
-- In the first argument of `mappend', namely `arr1 `mappend` arr2'