packages feed

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 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