TypeNat 0.4.0.1 → 0.5.0.0

raw patch · 4 files changed

+37/−16 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Data/TypeNat/Fin.hs +9/−3
• Data/TypeNat/Nat.hs +1/−0
• Data/TypeNat/Vect.hs +25/−11
• TypeNat.cabal +2/−2

@@ -18,6 +18,7 @@   , ix10    , safeIndex+  , safeUpdate    , module Data.TypeNat.Nat @@ -43,6 +44,11 @@ ix10 = FS ix9  -- | Safely index a Vect.-safeIndex :: Vect a n -> Fin n -> a-safeIndex (VCons a _) FZ = a-safeIndex (VCons _ v) (FS x) = safeIndex v x+safeIndex :: Fin n -> Vect n a -> a+safeIndex FZ (VCons a _) = a+safeIndex (FS x) (VCons _ v) = safeIndex x v++-- | Safely update a Vect.+safeUpdate :: Fin n -> (a -> a) -> Vect n a -> Vect n a+safeUpdate FZ f (VCons x rest) = VCons (f x) rest+safeUpdate (FS fs) f (VCons x rest) = VCons x (safeUpdate fs f rest)

@@ -34,6 +34,7 @@ import Data.Proxy import GHC.Exts (Constraint) +-- | Natural numbers data Nat = Z | S Nat  instance Eq Nat where

@@ -20,43 +20,57 @@ import Data.TypeNat.Nat  -- | Nat-indexed list, where the nat determines the length.-data Vect :: * -> Nat -> * where-  VNil :: Vect a Z-  VCons :: a -> Vect a n -> Vect a (S n)+data Vect :: Nat -> * -> * where+  VNil :: Vect Z a+  VCons :: a -> Vect n a -> Vect (S n) a -deriving instance Eq t => Eq (Vect t n)-deriving instance Show t => Show (Vect t n)+deriving instance Eq a => Eq (Vect n a)+deriving instance Show a => Show (Vect n a) +instance Functor (Vect n) where+    fmap = vectMap++instance Foldable (Vect n) where+    foldr f b vect = case vect of+        VNil -> b+        VCons x rest -> f x (foldr f b rest)++instance Traversable (Vect n) where+    traverse f vect = case vect of+        VNil -> pure VNil+        VCons x rest -> VCons <$> f x <*> traverse f rest+ -- | A kind of fmap for Vect.-vectMap :: (a -> b) -> Vect a n -> Vect b n+vectMap :: (a -> b) -> Vect n a -> Vect n b vectMap f vect = case vect of   VNil -> VNil   VCons x v -> VCons (f x) (vectMap f v)  -- | VCons to the end of a Vect.-vectSnoc :: a -> Vect a n -> Vect a (S n)+vectSnoc :: a -> Vect n a -> Vect (S n) a vectSnoc x vect = case vect of   VNil -> VCons x VNil   VCons y v -> VCons y (vectSnoc x v) -showVect :: Show a => Vect a l -> String+-- | Show a Vect.+showVect :: Show a => Vect l a -> String showVect VNil = "VNil" showVect (VCons x xs) = show x ++ " , " ++ showVect xs  -- | Drop the length index from a Vect, giving a typical list.-vectToList :: Vect a n -> [a]+vectToList :: Vect n a -> [a] vectToList v = case v of   VNil -> []   VCons x xs -> x : vectToList xs  -- | Used to implement listToVect through natRecursion. newtype MaybeVect a n = MV {-    unMV :: Maybe (Vect a n)+    unMV :: Maybe (Vect n a)   }  -- | Try to produce a Vect from a list. The nat index must be fixed somehow, --   perhaps with the help of ScopedTypeVariables.-listToVect:: IsNat n => [a] -> Maybe (Vect a n)+listToVect:: IsNat n => [a] -> Maybe (Vect n a) listToVect = unMV . listToVect'    where

@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/  name:                TypeNat-version:             0.4.0.1+version:             0.5.0.0 synopsis:            Some Nat-indexed types for GHC -- description:          homepage:            https://github.com/avieth/TypeNat@@ -31,6 +31,6 @@                      , TypeFamilies                      , KindSignatures -  build-depends:       base >=4.7 && < 4.9+  build-depends:       base >=4.7 && < 4.11   -- hs-source-dirs:         default-language:    Haskell2010