type-unary 0.0.0 → 0.1.0
raw patch · 2 files changed
+113/−89 lines, 2 files
Files
- src/TypeUnary/Vec.hs +112/−88
- type-unary.cabal +1/−1
src/TypeUnary/Vec.hs view
@@ -35,7 +35,7 @@ , vec1, vec2, vec3, vec4 , un1, un2, un3, un4 , get0, get1, get2, get3- , get, swizzle+ , get, swizzle, split ) where import Prelude hiding (foldr,sum)@@ -43,7 +43,7 @@ -- #include "Typeable.h" import Control.Applicative (Applicative(..),liftA2,(<$>))-import Data.Foldable (Foldable(..),sum)+import Data.Foldable (Foldable(..),toList,sum) import Data.Traversable (Traversable(..)) import Data.Maybe (isJust) -- import Data.Typeable@@ -240,32 +240,77 @@ -} +{--------------------------------------------------------------------+ Instances for standard classes+--------------------------------------------------------------------}++instance Eq a => Eq (Vec n a) where+ ZVec == ZVec = True+ a :< as == b :< bs = a==b && as==bs++instance Ord a => Ord (Vec n a) where+ ZVec `compare` ZVec = EQ+ (a :< as) `compare` (b :< bs) =+ case a `compare` b of+ LT -> LT+ GT -> GT+ EQ -> as `compare` bs++instance Show a => Show (Vec n a) where+ show v = "elemsV " ++ show (toList v)+ instance Functor (Vec n) where fmap _ ZVec = ZVec fmap f (a :< u) = f a :< fmap f u +instance IsNat n => Applicative (Vec n) where+ pure = pureV+ (<*>) = applyV --- | @n@ a vector length.-class {- Typeable n => -} IsNat n where- nat :: Nat n- pureV :: a -> Vec n a- elemsV :: [a] -> Vec n a- peekV :: Storable a => Ptr a -> IO (Vec n a)- pokeV :: Storable a => Ptr a -> Vec n a -> IO ()+applyV :: Vec n (a -> b) -> Vec n a -> Vec n b+ZVec `applyV` ZVec = ZVec+(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs) -{---- TODO: remove all but nat from the class. Define the rest outside of the--- class by using nat. Then break this module into Nat and Vec. For instance,+-- Without -fno-warn-incomplete-patterns above,+-- the previous two instances lead to warnings about non-exhaustive+-- pattern matches, although the other possibilities+-- are type-incorrect. According to SLPJ:+-- +-- The overlap warning checker simply doesn't take account of GADTs.+-- There's a long-standing project suggestion to fix this:+-- http://hackage.haskell.org/trac/ghc/wiki/ProjectSuggestions .+-- Perhaps a good GSoc project. -pureV :: IsNat n => a -> Vec n a-pureV = pureN nat+instance Foldable (Vec n) where+ foldr _ b ZVec = b+ foldr h b (a :< as) = a `h` foldr h b as -pureN :: Nat n -> a -> Vec n a-pureN Zero _ = ZVec-pureN (Succ n) a = a :< pureN n a--}+instance Traversable (Vec n) where+ traverse _ ZVec = pure ZVec+ traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as) +instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where+ { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate } +instance (IsNat n, Num a) => VectorSpace (Vec n a) where+ type Scalar (Vec n a) = Vec1 a+ (*^) (s :< ZVec) = fmap (s *)++instance (IsNat n, Num a) => InnerSpace (Vec n a) where+ -- u <.> v = vec1 (sum (liftA2 (*) u v))+ (<.>) = (result.result) (vec1 . sum) (liftA2 (*))++instance (IsNat n, Storable a) => Storable (Vec n a) where+ sizeOf = const (fromIntegral (natToZ (nat :: Nat n))+ * sizeOf (undefined :: a))+ alignment = const (alignment (undefined :: a))+ peek = peekV . castPtr+ poke = pokeV . castPtr++{--------------------------------------------------------------------+ IsNat+--------------------------------------------------------------------}+ instance IsNat Z where nat = Zero pureV _ = ZVec@@ -292,36 +337,9 @@ -- succPtr :: forall a. Storable a => Ptr a -> Ptr a -- succPtr p = p `plusPtr` sizeOf (undefined :: a) - -- TODO: Optimize peekV, pokeV. For instance, unroll the loop in the -- dictionary, remove the sizeOf dependence on @a@. -applyV :: Vec n (a -> b) -> Vec n a -> Vec n b-ZVec `applyV` ZVec = ZVec-(f :< fs) `applyV` (x :< xs) = f x :< (fs `applyV` xs)--instance IsNat n => Applicative (Vec n) where- pure = pureV- (<*>) = applyV---- Without -fno-warn-incomplete-patterns above,--- the previous two instances lead to warnings about non-exhaustive--- pattern matches, although the other possibilities--- are type-incorrect. According to SLPJ:--- --- The overlap warning checker simply doesn't take account of GADTs.--- There's a long-standing project suggestion to fix this:--- http://hackage.haskell.org/trac/ghc/wiki/ProjectSuggestions .--- Perhaps a good GSoc project.--instance Foldable (Vec n) where- foldr _ b ZVec = b- foldr h b (a :< as) = a `h` foldr h b as--instance Traversable (Vec n) where- traverse _ ZVec = pure ZVec- traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as)- infixl 1 <+> -- | Concatenation of vectors (<+>) :: Vec m a -> Vec n a -> Vec (m :+: n) a@@ -336,6 +354,28 @@ -- TODO: Try reimplementing many Vec functions via foldr. Warning: some -- (most?) will fail because they rely on a polymorphic combining function. +-- | @n@ a vector length.+class {- Typeable n => -} IsNat n where+ nat :: Nat n+ pureV :: a -> Vec n a+ elemsV :: [a] -> Vec n a+ peekV :: Storable a => Ptr a -> IO (Vec n a)+ pokeV :: Storable a => Ptr a -> Vec n a -> IO ()++-- Convert from vector to list via Data.Foldable.toList++{-+-- TODO: remove all but nat from the class. Define the rest outside of the+-- class by using nat. Then break this module into Nat and Vec. For instance,++pureV :: IsNat n => a -> Vec n a+pureV = pureN nat++pureN :: Nat n -> a -> Vec n a+pureN Zero _ = ZVec+pureN (Succ n) a = a :< pureN n a+-}+ -- Convenient nicknames type Vec0 = Vec N0@@ -386,24 +426,7 @@ un4 :: Vec4 a -> (a,a,a,a) un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d) - {--------------------------------------------------------------------- Vector space instances---------------------------------------------------------------------}--instance (IsNat n, Num a) => AdditiveGroup (Vec n a) where- { zeroV = pure 0; (^+^) = liftA2 (+) ; negateV = fmap negate }--instance (IsNat n, Num a) => VectorSpace (Vec n a) where- type Scalar (Vec n a) = Vec1 a- (*^) (s :< ZVec) = fmap (s *)--instance (IsNat n, Num a) => InnerSpace (Vec n a) where- -- u <.> v = vec1 (sum (liftA2 (*) u v))- (<.>) = (result.result) (vec1 . sum) (liftA2 (*))---{-------------------------------------------------------------------- Extract elements --------------------------------------------------------------------} @@ -443,32 +466,33 @@ t3 = swizzle t2 t1 -} ---{--------------------------------------------------------------------- Some instances. More in Type.hs---------------------------------------------------------------------}--instance Eq a => Eq (Vec n a) where- ZVec == ZVec = True- a :< as == b :< bs = a==b && as==bs--instance Ord a => Ord (Vec n a) where- ZVec `compare` ZVec = EQ- (a :< as) `compare` (b :< bs) =- case a `compare` b of- LT -> LT- GT -> GT- EQ -> as `compare` bs+-- | Split a vector+split :: IsNat n => Vec (n :+: m) a -> (Vec n a, Vec m a)+split = split' nat +split' :: Nat n -> Vec (n :+: m) a -> (Vec n a, Vec m a)+split' Zero v = (ZVec, v)+split' (Succ n) (a :< as) = (a :< bs, cs)+ where+ (bs,cs) = split' n as -{--------------------------------------------------------------------- Storage---------------------------------------------------------------------}+-- For instance,+-- +-- *TypeUnary.Vec> split (pure 3) :: (Vec7 Int, Vec4 Int)+-- (elemsV [3,3,3,3,3,3,3],elemsV [3,3,3,3])+-- +-- Note that 'pure 3' was inferred to have type 'Vec11 Int'. -instance (IsNat n, Storable a) => Storable (Vec n a) where- sizeOf = const (fromIntegral (natToZ (nat :: Nat n))- * sizeOf (undefined :: a))- alignment = const (alignment (undefined :: a))- peek = peekV . castPtr- poke = pokeV . castPtr+-- I'd like to define take & drop similarly, e.g.,+--+-- take :: IsNat n => Vec (n :+: m) a -> Vec n a+-- take = fst . split+-- +-- However,+-- +-- Could not deduce ((n :+: m0) ~ (n :+: m))+-- from the context (IsNat n)+-- bound by the type signature for+-- TypeUnary.Vec.take :: IsNat n => Vec (n :+: m) a -> Vec n a+-- at /Users/conal/Haskell/type-unary/src/TypeUnary/Vec.hs:488:1-18+-- NB: `:+:' is a type function, and may not be injective
type-unary.cabal view
@@ -1,5 +1,5 @@ Name: type-unary-Version: 0.0.0+Version: 0.1.0 Cabal-Version: >= 1.2 Synopsis: Type-level and typed unary natural numbers, vectors, inequality proofs Category: Data