@@ -1,53 +0,0 @@
1−{-# LANGUAGE BangPatterns #-}
2−{-# LANGUAGE DataKinds #-}
3−{-# LANGUAGE GADTs #-}
4−{-# LANGUAGE KindSignatures #-}
5−{-# LANGUAGE ScopedTypeVariables #-}
6−{-# LANGUAGE StandaloneDeriving #-}
7−{-# LANGUAGE TypeOperators #-}
8−{-# LANGUAGE TypeFamilies #-}
9−{-# LANGUAGE PolyKinds #-}
10−
11−module Grenade.Core.Vector (
12− Vector
13− , vectorZip
14− , vecToList
15− , mkVector
16− ) where
17−
18−import Data.Proxy
19−import GHC.TypeLits
20−
21−-- | A more specific Tagged type, ensuring that a list
22−-- is equal to the Nat value.
23−newtype Vector (n :: Nat) a = Vector [a]
24−
25−instance Foldable (Vector n) where
26− foldr f b (Vector as) = foldr f b as
27−
28−instance KnownNat n => Traversable (Vector n) where
29− traverse f (Vector as) = mkVector <$> traverse f as
30−
31−instance Functor (Vector n) where
32− fmap f (Vector as) = Vector (fmap f as)
33−
34−instance Show a => Show (Vector n a) where
35− showsPrec d = showsPrec d . vecToList
36−
37−instance Eq a => Eq (Vector n a) where
38− (Vector as) == (Vector bs) = as == bs
39−
40−mkVector :: forall n a. KnownNat n => [a] -> Vector n a
41−mkVector as
42− = let du = fromIntegral . natVal $ (undefined :: Proxy n)
43− la = length as
44− in if du == la
45− then Vector as
46− else error $ "Error creating staticly sized Vector of length: " ++
47− show du ++ " list is of length:" ++ show la
48−
49−vecToList :: Vector n a -> [a]
50−vecToList (Vector as) = as
51−
52−vectorZip :: (a -> b -> c) -> Vector n a -> Vector n b -> Vector n c
53−vectorZip f (Vector as) (Vector bs) = Vector (zipWith f as bs)