vector-heterogenous 0.0.2 → 0.1.0

raw patch · 2 files changed

+66/−19 lines, 2 files

Files

• src/Data/Vector/Heterogenous/HList.hs +65/−18
• vector-heterogenous.cabal +1/−1

@@ -16,23 +16,32 @@     -- * Heterogenous List     HList (..)     , HLength (..)+    , List2HList (..)          -- * Downcasting     , ConstraintBox (..)     , Downcast (..)          -- * Boxes-    , ShowBox-    , AnyBox+    , ShowBox (..)+    , AnyBox (..)          -- * Type functions     +    -- ** HList+    , HCons (..)+    , UnHList (..)+         -- ** Type Lists     , Distribute (..)     , Replicate (..)     , Map (..)     , Reverse (..)     , (:!) (..)+    , (++) (..)+    , ($) (..)+    , Concat (..)+    , Length (..)          -- ** Type Nats     , Nat1(..)@@ -92,6 +101,20 @@ instance (HLength (HList xs)) => HLength (HList (x ': xs)) where     hlength (x:::xs) = 1+hlength xs +-- | For construction from lists++class List2HList x xs where+    list2hlist :: [x] -> HList (x ': xs)+    +instance List2HList x '[] where+    list2hlist []       = error "List2HList x HNil: cannot append empty list"+    list2hlist (x:[])   = x:::HNil+    list2hlist _        = error "List2HList x HNil: too many elements in list"++instance (List2HList x xs) => List2HList x (x ': xs) where+    list2hlist []       = error "List2HList x HNil: cannot append empty list"+    list2hlist (x:xs)   = x:::(list2hlist xs)+ ------------------------------------------------------------------------------- -- downcasting HList -> [] @@ -131,33 +154,43 @@ ------------------------------------------------------------------------------- -- type functions ++type family HCons (x :: *) (xs :: *) :: *+type instance HCons x (HList xs) = HList (x ': xs)++type family UnHList (xs :: *) :: [a]+type instance UnHList (HList xs) = xs++---------------------------------------+ type family Distribute (xs::[a->b]) (t::a) :: [b] type instance Distribute '[] a = '[] type instance Distribute (x ': xs) a = (x a) ': (Distribute xs a) -type family Replicate (x::a) (n::Nat) :: [a]-type instance Replicate x n = Replicate1 x (ToNat1 n)-type family Replicate1 (x::a) (n::Nat1) :: [a]-type instance Replicate1 x Zero = '[]-type instance Replicate1 x (Succ n) = x ': (Replicate1 x n)+type family Replicate (n::Nat) (x::a) :: [a]+type instance Replicate n x = Replicate1 (ToNat1 n) x+type family Replicate1 (n::Nat1) (x::a) :: [a]+type instance Replicate1 Zero x = '[]+type instance Replicate1 (Succ n) x = x ': (Replicate1 n x)  type family Map (f :: a -> a) (xs::[a]) :: [a] type instance Map f '[] = '[] type instance Map f (x ': xs) = (f x) ': (Map f xs) -type family Length (xs::[a]) :: Nat-type instance Length '[] = 0-type instance Length (a ': xs) = 1 + (Length xs)+-- type family Length (xs::[a]) :: Nat+-- type instance Length '[] = 0+-- type instance Length (a ': xs) = 1 + (Length xs) -type family MoveR (xs::[a]) (ys::[a]) :: [a]-type instance MoveR '[] ys = ys-type instance MoveR (x ': xs) ys = MoveR xs (x ': ys)+type family Length (xs :: [a]) :: Nat+type instance Length xs = FromNat1 ( Length1 xs ) -type family Reverse (xs::[a]) :: [a]-type instance Reverse xs = MoveR xs '[]+type family Length1 (xs::[a]) :: Nat1+type instance Length1 '[] = Zero+type instance Length1 (x ': xs) = Succ (Length1 xs) -type family (xs::[a]) ++ (ys::[a]) :: [a]-type instance xs ++ ys = MoveR (Reverse xs) ys+type family Reverse (xs::[a]) :: [a]+type instance Reverse '[] = '[]+type instance Reverse (x ': xs) = Reverse xs ++ '[x]  type family (:!) (xs::[a]) (i::Nat) :: a type instance (:!) xs n = Index xs (ToNat1 n)@@ -166,13 +199,27 @@ type instance Index (x ': xs) Zero = x type instance Index (x ': xs) (Succ i) = Index xs i +type family ($) (f :: a -> b) (a :: a) :: b+type instance f $ a = f a+     +type family (xs :: [a]) ++ (ys :: [a]) :: [a]+type instance '[] ++ ys = ys+type instance (x ': xs) ++ ys = x ': (xs ++ ys)+     +type family Concat (xs :: [[a]]) :: [a]+type instance Concat '[] = '[]+type instance Concat (x ': xs) = x ++ Concat xs+ ---------------------------------------  data Nat1 = Zero | Succ Nat1  type family FromNat1 (n :: Nat1) :: Nat type instance FromNat1 Zero     = 0-type instance FromNat1 (Succ n) = 1 + FromNat1 n+type instance FromNat1 (Succ Zero) = 1+type instance FromNat1 (Succ (Succ Zero)) = 2+type instance FromNat1 (Succ (Succ (Succ Zero))) = 3+type instance FromNat1 (Succ (Succ (Succ (Succ Zero)))) = 4  type family ToNat1 (n :: Nat) :: Nat1 type instance ToNat1 0 = Zero

@@ -1,5 +1,5 @@ Name:                vector-heterogenous-Version:             0.0.2+Version:             0.1.0 Synopsis:            A type-safe library for vectors whose elements can be of any type, or any type satisfying some constraints Description:          Category:            Data, Data Structures