type-unary 0.3.0 → 0.3.2
raw patch · 3 files changed
+35/−29 lines, 3 filesdep +newtype-genericsdep −newtypedep ~basePVP: major bump suggested
API removals or changes: PVP suggests a major version bump
Dependencies added: newtype-generics
Dependencies removed: newtype
Dependency ranges changed: base
API changes (from Hackage documentation)
- TypeUnary.Nat: SLess :: m :<: n -> S m :<: S n
- TypeUnary.Nat: Succ :: Nat n -> Nat (S n)
- TypeUnary.Nat: ZLess :: Z :<: S n
- TypeUnary.Nat: Zero :: Nat Z
- TypeUnary.Nat: data (:<:) m n
- TypeUnary.Nat: instance ((n TypeUnary.TyNat.:+: TypeUnary.TyNat.Z) ~ n) => TypeUnary.Nat.PlusZero n
- TypeUnary.Vec: (:<) :: a -> Vec n a -> Vec (S n) a
- TypeUnary.Vec: ZVec :: Vec Z a
- TypeUnary.Vec: instance Control.Newtype.Newtype (TypeUnary.Vec.Vec (TypeUnary.TyNat.S n) a) (a, TypeUnary.Vec.Vec n a)
- TypeUnary.Vec: instance Control.Newtype.Newtype (TypeUnary.Vec.Vec TypeUnary.TyNat.Z a) ()
+ TypeUnary.Nat: [SLess] :: m :<: n -> S m :<: S n
+ TypeUnary.Nat: [Succ] :: IsNat n => Nat n -> Nat (S n)
+ TypeUnary.Nat: [ZLess] :: Z :<: S n
+ TypeUnary.Nat: [Zero] :: Nat Z
+ TypeUnary.Nat: data m (:<:) n
+ TypeUnary.Nat: instance (n TypeUnary.TyNat.:+: TypeUnary.TyNat.Z) ~ n => TypeUnary.Nat.PlusZero n
+ TypeUnary.Vec: [:<] :: a -> Vec n a -> Vec (S n) a
+ TypeUnary.Vec: [ZVec] :: Vec Z a
+ TypeUnary.Vec: infixl 1 <+>
+ TypeUnary.Vec: instance Control.Newtype.Generics.Newtype (TypeUnary.Vec.Vec (TypeUnary.TyNat.S n) a)
+ TypeUnary.Vec: instance Control.Newtype.Generics.Newtype (TypeUnary.Vec.Vec TypeUnary.TyNat.Z a)
- TypeUnary.Nat: induction :: p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> (forall n. IsNat n => Dict (p n))
+ TypeUnary.Nat: induction :: forall p. p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n))) -> (forall n. IsNat n => Dict (p n))
- TypeUnary.Nat: natMul :: Nat m -> Nat n -> Nat (m :*: n)
+ TypeUnary.Nat: natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
- TypeUnary.Nat: unIndex :: (Num a, Enum a) => Index m -> a
+ TypeUnary.Nat: unIndex :: Num a => Index m -> a
- TypeUnary.Vec: iota :: (IsNat n, Num a, Enum a) => Vec n a
+ TypeUnary.Vec: iota :: (IsNat n, Num a) => Vec n a
Files
- src/TypeUnary/Nat.hs +2/−2
- src/TypeUnary/Vec.hs +31/−23
- type-unary.cabal +2/−4
src/TypeUnary/Nat.hs view
@@ -1,7 +1,7 @@ {-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-} {-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE ScopedTypeVariables #-} -- PlusZero Experiment {-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP #-}@@ -247,7 +247,7 @@ -- TODO: Consider removing the Nat n field, since it's computable from -- IsNat n or n :<: lim. -unIndex :: (Num a, Enum a) => Index m -> a+unIndex :: Num a => Index m -> a unIndex (Index _ j) = natToZ j instance Eq (Index lim) where
src/TypeUnary/Vec.hs view
@@ -114,11 +114,11 @@ -} -cant :: String -> a-cant str = error $ str ++ ": GHC doesn't know this case can't happen."+-- cant :: String -> a+-- cant str = error $ str ++ ": GHC doesn't know this case can't happen." -cantV :: String -> a-cantV str = cant (str ++ " on Vec")+-- cantV :: String -> a+-- cantV str = cant (str ++ " on Vec") {-------------------------------------------------------------------- Instances for standard classes@@ -127,13 +127,13 @@ instance Eq a => Eq (Vec n a) where ZVec == ZVec = True a :< as == b :< bs = a==b && as==bs- _ == _ = cantV "(==)"+-- _ == _ = cantV "(==)" instance Ord a => Ord (Vec n a) where ZVec `compare` ZVec = EQ (a :< as) `compare` (b :< bs) = (a `compare` b) `mappend` (as `compare` bs)- _ `compare` _ = cantV "compare"+-- _ `compare` _ = cantV "compare" -- Equivalently, -- @@ -168,6 +168,12 @@ -- if the code generation uses Pretty instead of Show. -- The Monoid instance uses a standard recipe for applicative functors.++#if MIN_VERSION_base(4,11,0)+instance (IsNat n, Semigroup a) => Semigroup (Vec n a) where+ (<>) = liftA2 (<>)+#endif+ instance (IsNat n, Monoid a) => Monoid (Vec n a) where mempty = pure mempty mappend = liftA2 mappend@@ -227,7 +233,7 @@ joinV :: Vec n (Vec n a) -> Vec n a joinV ZVec = ZVec joinV ((a :< _) :< vs) = a :< joinV (tailV <$> vs)-joinV _ = cant "joinV"+-- joinV _ = cant "joinV" instance Foldable (Vec n) where foldMap _ ZVec = mempty@@ -239,11 +245,13 @@ traverse f (a :< as) = liftA2 (:<) (f a) (traverse f as) {-# INLINE traverse #-} -instance Newtype (Vec Z a) () where+instance Newtype (Vec Z a) where+ type O (Vec Z a) = () pack () = ZVec unpack ZVec = () -instance Newtype (Vec (S n) a) (a,Vec n a) where+instance Newtype (Vec (S n) a) where+ type O (Vec (S n) a) = (a,Vec n a) pack = uncurry (:<) unpack = unConsV @@ -253,7 +261,7 @@ instance (IsNat n, Num a) => VectorSpace (Vec n a) where type Scalar (Vec n a) = Vec1 a (*^) (s :< ZVec) = fmap (s *)- (*^) _ = cantV "(*^)"+-- (*^) _ = cantV "(*^)" instance (IsNat n, Num a) => InnerSpace (Vec n a) where -- u <.> v = vec1 (sum (liftA2 (*) u v))@@ -299,7 +307,7 @@ pokeV' Zero _ ZVec = return () pokeV' (Succ n) p (a :< as) = do poke p a pokeV' n (p `plusPtr` sizeOf a) as-pokeV' _ _ _ = cant "pokeV"+-- pokeV' _ _ _ = cant "pokeV" -- -- Experiment toward simplifying away the plusPtr calls. -- succPtr :: forall a. Storable a => Ptr a -> Ptr a@@ -323,7 +331,7 @@ -- Convert from vector to list via Data.Foldable.toList -- | Vector of ints from 0 to n-1. Named for APL iota operation (but 0 based).-iota :: (IsNat n, Num a, Enum a) => Vec n a+iota :: (IsNat n, Num a) => Vec n a iota = unIndex <$> indices @@ -376,22 +384,22 @@ -- | Extract element un1 :: Vec1 a -> a un1 (a :< ZVec) = a-un1 _ = cant "un1"+-- un1 _ = cant "un1" -- | Extract elements un2 :: Vec2 a -> (a,a) un2 (a :< b :< ZVec) = (a,b)-un2 _ = cant "un2"+-- un2 _ = cant "un2" -- | Extract elements un3 :: Vec3 a -> (a,a,a) un3 (a :< b :< c :< ZVec) = (a,b,c)-un3 _ = cant "un3"+-- un3 _ = cant "un3" -- | Extract elements un4 :: Vec4 a -> (a,a,a,a) un4 (a :< b :< c :< d :< ZVec) = (a,b,c,d)-un4 _ = cant "un4"+-- un4 _ = cant "un4" -- TODO: consider this notation: --@@ -411,7 +419,7 @@ get :: Index n -> Vec n a -> a get (Index ZLess Zero ) (a :< _) = a get (Index (SLess p) (Succ m)) (_ :< as) = get (Index p m) as-get _ _ = cant "get"+-- get _ _ = cant "get" get0 :: Vec (N1 :+: n) a -> a -- ^ Get first element get1 :: Vec (N2 :+: n) a -> a -- ^ Get second element@@ -427,7 +435,7 @@ update :: Index n -> (a -> a) -> Vec n a -> Vec n a update (Index ZLess Zero ) f (a :< as) = f a :< as update (Index (SLess p) (Succ m)) f (a :< as) = a :< update (Index p m) f as-update _ _ _ = cantV "update"+-- update _ _ _ = cantV "update" -- | Replace a vector element, taking a proof that the index is within bounds. set :: Index n -> a -> Vec n a -> Vec n a@@ -464,7 +472,7 @@ flattenV' :: Nat n -> Vec n (Vec m a) -> Vec (n :*: m) a flattenV' Zero _ = ZVec flattenV' (Succ n') (v :< vs') = v <+> flattenV' n' vs'-flattenV' _ _ = error "flattenV': GHC doesn't know this case can't happen."+-- flattenV' _ _ = error "flattenV': GHC doesn't know this case can't happen." -- | Chunk a vector into a vector of vectors (a 2D array) chunkV :: (IsNat n, IsNat m) => Vec (n :*: m) a -> Vec n (Vec m a)@@ -473,7 +481,7 @@ chunkV' :: IsNat m => Nat n -> Vec (n :*: m) a -> Vec n (Vec m a) chunkV' Zero ZVec = ZVec chunkV' (Succ n) as = v :< chunkV' n as' where (v,as') = split as-chunkV' _ _ = cant "chunkV"+-- chunkV' _ _ = cant "chunkV" -- | Swizzling. Extract multiple elements simultaneously. swizzle :: Vec n (Index m) -> Vec m a -> Vec n a@@ -493,7 +501,7 @@ split' (Succ n) (a :< as) = (a :< bs, cs) where (bs,cs) = split' n as-split' _ _ = cantV "split"+-- split' _ _ = cantV "split" -- For instance, -- @@ -650,14 +658,14 @@ zipWithV :: (a -> b -> c) -> Vec n a -> Vec n b -> Vec n c zipWithV _ ZVec ZVec = ZVec zipWithV f (a :< as) (b :< bs) = f a b :< zipWithV f as bs-zipWithV _ _ _ = cant "zipWithV"+-- zipWithV _ _ _ = cant "zipWithV" -- | Unzip one vector into two. Like 'liftA2', but the former requires -- @IsNat n@. zipWithV3 :: (a -> b -> c -> d) -> Vec n a -> Vec n b -> Vec n c -> Vec n d zipWithV3 _ ZVec ZVec ZVec = ZVec zipWithV3 f (a :< as) (b :< bs) (c :< cs) = f a b c :< zipWithV3 f as bs cs-zipWithV3 _ _ _ _ = cant "zipWithV3"+-- zipWithV3 _ _ _ _ = cant "zipWithV3" -- | Unzip a vector of pairs into a pair of vectors unzipV :: Vec n (a,b) -> (Vec n a, Vec n b)
type-unary.cabal view
@@ -1,5 +1,5 @@ Name: type-unary-Version: 0.3.0+Version: 0.3.2 Cabal-Version: >= 1.6 Synopsis: Type-level and typed unary natural numbers, inequality proofs, vectors@@ -27,7 +27,7 @@ Extensions: Build-Depends: base >=4 && < 5 , constraints- , newtype >= 0.2+ , newtype-generics , ty >= 0.1.5 , vector-space , applicative-numbers@@ -37,5 +37,3 @@ TypeUnary.Vec ghc-options: -Wall-- ghc-prof-options: -prof -auto-all