Emulate "static dependent types" in Haskell (if needed, with GHC extensions)
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))
开发者_C百科
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
-- ...
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…
精彩评论