Emulate "static dependent types" in Haskell (if needed, with GHC extensions)

Question

Assume that I have a type class Vec that implements the theory of, say, vector spaces over the rationals.

class Vec a where
    (+)  :: a -> a -> a
    zero :: a
    -- rest omitted

Now given a natural number n, I can easily construct an instance of Vec whose underlying type is the type of lists of rationals and which implements a vector space of dimension n. We take n = 3 in the following:

newtype RatList3 = RatList3 { list3 :: [Rational] }
instance Vec RatList3 where
    v + w = RatList3 (zipWith (Prelude.+) (list3 v) (list3 w))
    zero  = RatList3 (take 3 (repeat 0))

For another natural number, for example a calculated one, I can write

f :: Int -> Int
f x = x * x -- some complicated function
n :: Int
n = f 2
newtype RatListN = RatListN { listN :: [Rational] }
instance Vec RatListN where
    v + w = RatListN (zipWith (Prelude.+) (listN v) (listN w))
    zero  = RatListN (take n (repeat 0))

Now I have two types, one for vector spaces of dimension 3 and one for vector spaces of dimension n. However, if I want to put my instance declaration of the form instance Vec RatList? in a module where I don't know which n my main program eventually uses, I have a problem as the type RatList? doesn't know which n it belongs to.

To solve the problem, I tried to do something along the following lines:

class HasDim a where
    dim      :: Int

instance (HasDim a, Fractional a) => Vec [a] where
    v + w = ...
    zero  = take dim (repeat (fromRational 0))

-- in the main module
instance HasDim Rational where
    dim = n -- some integer

This doesn't work, of course, because dim in HasDim is independent of the type variable a and in instance (HasDim a) => Vec [a] it is not clear which type's dim to take. I tried to circumvent the first problem by introducing another type:

newtype Dim a = Dim { idim :: Int }

Then I can write

class HasDim a where
    dim      :: Dim a

However, it is not clear to me how to use this in instance (HasDim a) => Vec [a] where. Also my whole "solution" looks rather cumbersome to me, while the posed problem looks simple. (I think it is easy to code this with C++ templates.)

EDIT

I have excepted ephemient's answer because without the type arithmetic it solved my problem the way I wanted to. Just for information, my final solution is along the following lines:

class Vec a where
    zero :: a
    -- ...

n :: Int
n = 10

newtype RatListN = RatListN [Rational]

instance Vec RatListN where
    zero = RatListN . take n $ repeat 0
    -- ...

Have you looked at the vector-space package, http://hackage.haskell.org/package/vector-space? I think it implements exactly this. — John L, Mar 25 '11 at 08:37
@John: I have taken a look at the package you mentioned. I haven't found inside a construction like the one I am looking for. Further, the vector space class above is just for illustration, so I am not looking for a haskell implementation for vector spaces but for a general solution of my problem, namely parametrising instances by values (and not types). — Marc, Mar 25 '11 at 15:05
Perhaps there's some value looking at how the REPA library implements shape types: http://hackage.haskell.org/package/repa . Is there anything about your problem space requiring the parameterization be by value, rather than specialized types? — Carl, Mar 25 '11 at 17:08

score 2 · Accepted Answer · answered Mar 25 '11 at 17:52

This seems like a case where type arithmetic would get you some of what you want.

data Zero
data Succ a
type One = Succ Zero
type Two = Succ One
type Three = Succ Two
-- ...

class NumericType a where
    toNum :: (Num b) => a -> b
instance NumericType Zero where
    toNum = const 0
instance (NumericType a) => NumericType (Succ a) where
    toNum (Succ a) = toNum a + 1

data RatList a b = RatList { list :: [b] }
instance (NumericType a, Num b) => Vec (RatList a b) where
    zero = RatList . take (toNum (undefined :: a)) $ repeat 0

Now RatList Two Int and RatList Three Int are different types. On the other hand, this does prevent you from instantiating new dimensionalities at runtime…

Thanks for your answer. I had also thought about type arithmetic before. However, the n I would like to use is calculated by ordinary Haskell code and I don't want to lift the algorithm on the type level. In any case, your answer is nevertheless helpful to me as you have reminded me of the `undefined` construct. As soon as I have time to I will check whether the use of this can make my ideas work. — Marc, Mar 25 '11 at 18:58

Emulate "static dependent types" in Haskell (if needed, with GHC extensions)

1 Answers1

Linked