Emulate "static dependent types" in Haskell (optionally with GHC extensions)

Question

Suppose I have a class of type Vec that implements the theory of, say, vector spaces over rational ones.

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

Now, given the natural number n, I can easily build an instance of Vec whose base type is the type of rational lists and which implements a vector space of dimension n. 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 fx = 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 instance Vec RatList? declaration on an instance Vec RatList? into a module where I don’t know which one my main program ultimately uses, do I have a problem since the type is RatList? doesn't know which n belongs.

To solve the problem, I tried to do something in 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 does not work, of course, because dim in HasDim is independent of a variable of type a and in instance (HasDim a) => Vec [a] it is not clear which type of dim to take. I tried to work around the first problem by introducing a different 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 “solution” looks rather cumbersome for me, and the problem posed looks simple. (I think it is easy to code using C ++ templates.)

EDIT

I ruled out the ephemeral answer, because without arithmetic like, he solved my problem the way I wanted. For information only, my final decision consists of 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 -- ... 

Answer 1

This is similar to the case when the type of arithmetic will provide you with 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 ab = RatList { list :: [b] } instance (NumericType a, Num b) => Vec (RatList ab) 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 not allow you to create new measurements at runtime ...