fin 0.1 → 0.1.1

raw patch · 8 files changed

+259/−36 lines, 8 filesdep +QuickCheckdep ~basePVP ok

version bump matches the API change (PVP)

Dependencies added: QuickCheck

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• ChangeLog.md +9/−0
• fin.cabal +15/−10
• src/Data/Fin.hs +137/−3
• src/Data/Fin/Enum.hs +12/−12
• src/Data/Nat.hs +31/−1
• src/Data/Type/Nat.hs +44/−6
• src/Data/Type/Nat/LE.hs +6/−2
• src/Data/Type/Nat/LE/ReflStep.hs +5/−2

@@ -1,5 +1,14 @@ # Revision history for fin +## 0.1.1++- Add `isMin` and `isMax`+- Add `mirror`, `weakenRight1` and `weakenLeft1`+- Add `Mult2` and `DivMod2`+- Explicitly derive `Typeable SNat` and `Typeable LEProof`+- Derive `Typeable` for `Z` and `S` on GHC-7.8 explicitly+- Add `QuickCheck` instances for `Nat` and `Fin`+ ## 0.1  - Rename `Fin` constructors to `FZ` and `FS`.

@@ -1,8 +1,8 @@ cabal-version:      >=1.10 name:               fin-version:            0.1+version:            0.1.1 synopsis:           Nat and Fin: peano naturals and finite numbers-category:           Data, Dependent Types, Singletons+category:           Data, Dependent Types, Singletons, Math description:   This package provides two simple types, and some tools to work with them.   Also on type level as @DataKinds@.@@ -56,11 +56,18 @@ build-type:         Simple extra-source-files: ChangeLog.md tested-with:-  GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4+  GHC ==7.8.4+   || ==7.10.3+   || ==8.0.2+   || ==8.2.2+   || ==8.4.4+   || ==8.6.5+   || ==8.8.1  source-repository head   type:     git   location: https://github.com/phadej/vec.git+  subdir:   fin  library   exposed-modules:@@ -73,10 +80,11 @@     Data.Type.Nat.LT    build-depends:-      base      >=4.7     && <4.13-    , dec       >=0.0.3   && <0.1-    , deepseq   >=1.3.0.2 && <1.5-    , hashable  >=1.2.7.0 && <1.4+      base        >=4.7     && <4.14+    , dec         >=0.0.3   && <0.1+    , deepseq     >=1.3.0.2 && <1.5+    , hashable    >=1.2.7.0 && <1.4+    , QuickCheck  >=2.13.2  && <2.14    if !impl(ghc >=8.2)     build-depends: bifunctors >=5.5.3 && <5.6@@ -112,6 +120,3 @@    if !impl(ghc >=8.0)     buildable: False--  -- useful for development-  ghc-options:

@@ -5,6 +5,7 @@ {-# LANGUAGE KindSignatures       #-} {-# LANGUAGE ScopedTypeVariables  #-} {-# LANGUAGE StandaloneDeriving   #-}+{-# LANGUAGE TypeOperators        #-} {-# LANGUAGE UndecidableInstances #-} -- | Finite numbers. --@@ -27,6 +28,7 @@     toNatural,     toInteger,     -- * Interesting+    mirror,     inverse,     universe,     inlineUniverse,@@ -36,9 +38,14 @@     boring,     -- * Plus     weakenLeft,+    weakenLeft1,     weakenRight,+    weakenRight1,     append,     split,+    -- * Min and max+    isMin,+    isMax,     -- * Aliases     fin0, fin1, fin2, fin3, fin4, fin5, fin6, fin7, fin8, fin9,     ) where@@ -48,14 +55,19 @@ import Data.Hashable      (Hashable (..)) import Data.List.NonEmpty (NonEmpty (..)) import Data.Proxy         (Proxy (..))+import Data.Type.Nat      (Nat (..)) import Data.Typeable      (Typeable) import GHC.Exception      (ArithException (..), throw) import Numeric.Natural    (Natural)-import Data.Type.Nat (Nat (..))  import qualified Data.List.NonEmpty as NE import qualified Data.Type.Nat      as N+import qualified Test.QuickCheck    as QC +-------------------------------------------------------------------------------+-- Type+-------------------------------------------------------------------------------+ -- | Finite numbers: @[0..n-1]@. data Fin (n :: Nat) where     FZ :: Fin ('S n)@@ -103,7 +115,7 @@     signum (FS FZ)     = FS FZ     signum (FS (FS _)) = FS FZ -    fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n)))+    fromInteger = unsafeFromNum . (`mod` N.reflectToNum (Proxy :: Proxy n))      n + m = fromInteger (toInteger n + toInteger m)     n * m = fromInteger (toInteger n * toInteger m)@@ -121,6 +133,28 @@     quotRem a b = (quot a b, 0)     quot a b = a * inverse b +-- | Mirror the values, 'minBound' becomes 'maxBound', etc.+--+-- >>> map mirror universe :: [Fin N.Nat4]+-- [3,2,1,0]+--+-- >>> reverse universe :: [Fin N.Nat4]+-- [3,2,1,0]+--+-- @since 0.1.1+--+mirror :: forall n. N.InlineInduction n => Fin n -> Fin n+mirror = getMirror (N.inlineInduction start step) where+    start :: Mirror 'Z+    start = Mirror id++    step :: forall m. N.InlineInduction m => Mirror m -> Mirror ('S m)+    step (Mirror rec) = Mirror $ \n -> case n of+        FZ   -> getMaxBound (N.inlineInduction (MaxBound FZ) (MaxBound . FS . getMaxBound))+        FS m -> weakenLeft1 (rec m)++newtype Mirror n = Mirror { getMirror :: Fin n -> Fin n }+ -- | Multiplicative inverse. -- -- Works for @'Fin' n@ where @n@ is coprime with an argument, i.e. in general when @n@ is prime.@@ -168,6 +202,39 @@     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ  -------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance (n ~ 'S m, N.SNatI m) => QC.Arbitrary (Fin n) where+    arbitrary = getArb $ N.induction (Arb (return FZ)) step where+        step :: forall p. N.SNatI p => Arb p -> Arb ('S p)+        step (Arb p) = Arb $ QC.frequency+            [ (1,                                 return FZ)+            , (N.reflectToNum (Proxy :: Proxy p), fmap FS p)+            ]++    shrink = shrink++shrink :: Fin n -> [Fin n]+shrink FZ      = []+shrink (FS FZ) = [FZ]+shrink (FS n)  = map FS (shrink n)++newtype Arb n = Arb { getArb :: QC.Gen (Fin ('S n)) }++instance QC.CoArbitrary (Fin n) where+    coarbitrary FZ     = QC.variant (0 :: Int)+    coarbitrary (FS n) = QC.variant (1 :: Int) . QC.coarbitrary n++instance (n ~ 'S m, N.SNatI m) => QC.Function (Fin n) where+    function = case N.snat :: N.SNat m of+        N.SZ -> QC.functionMap (\FZ -> ()) (\() -> FZ)+        N.SS -> QC.functionMap isMin       (maybe FZ FS)++-- TODO: https://github.com/nick8325/quickcheck/pull/283+-- newtype Fun b m = Fun { getFun :: (Fin ('S m) -> b) -> Fin ('S m) QC.:-> b }++------------------------------------------------------------------------------- -- Showing ------------------------------------------------------------------------------- @@ -286,7 +353,7 @@ newtype Universe  n = Universe  { getUniverse  :: [Fin n] } newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('S n)) } --- | @'Fin' 'N.Nat0'@ is inhabited.+-- | @'Fin' 'N.Nat0'@ is not inhabited. absurd :: Fin N.Nat0 -> b absurd n = case n of {} @@ -298,9 +365,74 @@ boring = FZ  -------------------------------------------------------------------------------+-- min and max+-------------------------------------------------------------------------------++-- | Return a one less.+--+-- >>> isMin (FZ :: Fin N.Nat1)+-- Nothing+--+-- >>> map isMin universe :: [Maybe (Fin N.Nat3)]+-- [Nothing,Just 0,Just 1,Just 2]+--+-- @since 0.1.1+--+isMin :: Fin ('S n) -> Maybe (Fin n)+isMin FZ     = Nothing+isMin (FS n) = Just n++-- | Return a one less.+--+-- >>> isMax (FZ :: Fin N.Nat1)+-- Nothing+--+-- >>> map isMax universe :: [Maybe (Fin N.Nat3)]+-- [Just 0,Just 1,Just 2,Nothing]+--+-- @since 0.1.1+--+isMax :: forall n. N.InlineInduction n => Fin ('S n) -> Maybe (Fin n)+isMax = getIsMax (N.inlineInduction start step) where+    start :: IsMax 'Z+    start = IsMax $ \_ -> Nothing++    step :: IsMax m -> IsMax ('S m)+    step (IsMax rec) = IsMax $ \n -> case n of+        FZ   -> Just FZ+        FS m -> fmap FS (rec m)++newtype IsMax n = IsMax { getIsMax :: Fin ('S n) -> Maybe (Fin n) }++------------------------------------------------------------------------------- -- Append & Split ------------------------------------------------------------------------------- +-- | >>> map weakenRight1 universe :: [Fin N.Nat5]+-- [1,2,3,4]+--+-- @since 0.1.1+weakenRight1 :: Fin n -> Fin ('S n)+weakenRight1 = FS++-- | >>> map weakenLeft1 universe :: [Fin N.Nat5]+-- [0,1,2,3]+--+-- @since 0.1.1+weakenLeft1 :: N.InlineInduction n => Fin n -> Fin ('S n)+weakenLeft1 = getWeaken1 (N.inlineInduction start step) where+    start :: Weaken1 'Z+    start = Weaken1 absurd++    step :: Weaken1 n -> Weaken1 ('S n)+    step (Weaken1 go) = Weaken1 $ \n -> case n of+        FZ    -> FZ+        FS n' -> FS (go n')++newtype Weaken1 n = Weaken1 { getWeaken1 :: Fin n -> Fin ('S n) }++-- | >>> map (weakenLeft (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])+-- [0,1,2] weakenLeft :: forall n m. N.InlineInduction n => Proxy m -> Fin n -> Fin (N.Plus n m) weakenLeft _ = getWeakenLeft (N.inlineInduction start step :: WeakenLeft m n) where     start :: WeakenLeft m 'Z@@ -313,6 +445,8 @@  newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) } +-- | >>> map (weakenRight (Proxy :: Proxy N.Nat2)) (universe :: [Fin N.Nat3])+-- [2,3,4] weakenRight :: forall n m. N.InlineInduction n => Proxy n -> Fin m -> Fin (N.Plus n m) weakenRight _ = getWeakenRight (N.inlineInduction start step :: WeakenRight m n) where     start = WeakenRight id

@@ -1,14 +1,14 @@-{-# LANGUAGE ConstraintKinds        #-}-{-# LANGUAGE DataKinds              #-}-{-# LANGUAGE DefaultSignatures      #-}-{-# LANGUAGE FlexibleContexts       #-}-{-# LANGUAGE FlexibleInstances      #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE PolyKinds              #-}-{-# LANGUAGE ScopedTypeVariables    #-}-{-# LANGUAGE TypeFamilies           #-}-{-# LANGUAGE TypeOperators          #-}-{-# LANGUAGE UndecidableInstances   #-}+{-# LANGUAGE ConstraintKinds       #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE PolyKinds             #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}+{-# LANGUAGE UndecidableInstances  #-} -- | -- -- This module is designed to be imported qualified:@@ -148,7 +148,7 @@  -- | Generic version of 'to'. gto :: (G.Generic a, GTo a) => Fin (GEnumSize a) -> a-gto = \x -> G.to $ gtoRep x id $ F.absurd+gto = \x -> G.to $ gtoRep x id F.absurd  -- | Constraint for the class that computes 'gto'. type GTo a = GToRep (G.Rep a)

@@ -1,4 +1,10 @@+{-# LANGUAGE CPP                #-} {-# LANGUAGE DeriveDataTypeable #-}++#if __GLASGOW_HASKELL__ < 710+{-# LANGUAGE DataKinds          #-}+{-# LANGUAGE StandaloneDeriving #-}+#endif -- | 'Nat' numbers. -- -- This module is designed to be imported qualified.@@ -23,6 +29,8 @@ import GHC.Exception   (ArithException (..), throw) import Numeric.Natural (Natural) +import qualified Test.QuickCheck as QC+ ------------------------------------------------------------------------------- -- Nat -------------------------------------------------------------------------------@@ -33,6 +41,11 @@ -- data Nat = Z | S Nat deriving (Eq, Ord, Typeable, Data) +#if __GLASGOW_HASKELL__ < 710+deriving instance Typeable 'Z+deriving instance Typeable 'S+#endif+ -- | 'Nat' is printed as 'Natural'. -- -- To see explicit structure, use 'explicitShow' or 'explicitShowsPrec'@@ -63,7 +76,7 @@     toInteger = cata 0 succ      quotRem _ Z = throw DivideByZero-    quotRem _ _ = error "un-implemented"+    quotRem _ _ = error "quotRam @Nat un-implemented"  {- TODO: make <= with witness instance Ix Nat where@@ -89,6 +102,23 @@  instance Hashable Nat where     hashWithSalt salt = hashWithSalt salt . toInteger++-------------------------------------------------------------------------------+-- QuickCheck+-------------------------------------------------------------------------------++instance QC.Arbitrary Nat where+    arbitrary = fmap fromNatural QC.arbitrarySizedNatural++    shrink Z     = []+    shrink (S n) = n : QC.shrink n++instance QC.CoArbitrary Nat where+    coarbitrary Z     = QC.variant (0 :: Int) +    coarbitrary (S n) = QC.variant (1 :: Int) . QC.coarbitrary n++instance QC.Function Nat where+    function = QC.functionIntegral  ------------------------------------------------------------------------------- -- Showing

@@ -1,5 +1,6 @@ {-# LANGUAGE CPP                  #-} {-# LANGUAGE DataKinds            #-}+{-# LANGUAGE DeriveDataTypeable   #-} {-# LANGUAGE EmptyCase            #-} {-# LANGUAGE GADTs                #-} {-# LANGUAGE KindSignatures       #-}@@ -45,6 +46,8 @@     -- * Arithmetic     Plus,     Mult,+    Mult2,+    DivMod2,     -- * Conversion to GHC Nat     ToGHC,     FromGHC,@@ -63,16 +66,26 @@     )  where  import Data.Function      (fix)-import Data.Nat import Data.Proxy         (Proxy (..))-import Data.Type.Equality-import Data.Type.Dec+import Data.Type.Dec      (Dec (..))+import Data.Type.Equality ((:~:) (..), TestEquality (..))+import Data.Typeable      (Typeable) import Numeric.Natural    (Natural)  import qualified GHC.TypeLits as GHC  import Unsafe.Coerce (unsafeCoerce) +#if !MIN_VERSION_base(4,11,0)+import Data.Type.Equality (type (==))+#endif++import Data.Nat++-- $setup+-- >>> :set -XTypeOperators -XDataKinds+-- >>> import Data.Type.Dec (decShow)+ ------------------------------------------------------------------------------- -- SNat -------------------------------------------------------------------------------@@ -81,6 +94,7 @@ data SNat (n :: Nat) where     SZ :: SNat 'Z     SS :: SNatI n => SNat ('S n)+  deriving (Typeable)  deriving instance Show (SNat p) @@ -338,6 +352,33 @@     Mult 'Z     m = 'Z     Mult ('S n) m = Plus m (Mult n m) +-- | Multiplication by two. Doubling.+--+-- >>> reflect (snat :: SNat (Mult2 Nat4))+-- 8+--+type family Mult2 (n :: Nat) :: Nat where+    Mult2 'Z     = 'Z+    Mult2 ('S n) = 'S ('S (Mult2 n))++-- | Division by two. 'False' is 0 and 'True' is 1 as a remainder.+--+-- >>> :kind! DivMod2 Nat7+-- DivMod2 Nat7 :: (Nat, Bool)+-- = '( 'S ('S ('S 'Z)), 'True)+--+-- >>> :kind! DivMod2 Nat4+-- DivMod2 Nat4 :: (Nat, Bool)+-- = '( 'S ('S 'Z), 'False)+--+type family DivMod2 (n :: Nat) :: (Nat, Bool) where+    DivMod2 'Z          = '( 'Z, 'False)+    DivMod2 ('S 'Z)     = '( 'Z, 'True)+    DivMod2 ('S ('S n)) = DivMod2' (DivMod2 n)++type family DivMod2' (p :: (Nat, Bool)) :: (Nat, Bool) where+    DivMod2' '(n, b) = '( 'S n, b)+ ------------------------------------------------------------------------------- -- Aliases -------------------------------------------------------------------------------@@ -425,6 +466,3 @@  retagMap :: (a -> b) -> Tagged n a -> Tagged m b retagMap f = Tagged . f . unTagged---- $setup--- >>> :set -XTypeOperators -XDataKinds

@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveDataTypeable    #-} {-# LANGUAGE EmptyCase             #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-}@@ -48,10 +49,12 @@     ) where  import Data.Type.Dec      (Dec (..), Decidable (..), Neg)-import Data.Type.Equality-import Data.Type.Nat+import Data.Type.Equality ((:~:) (..))+import Data.Typeable      (Typeable) import Data.Void          (absurd) +import Data.Type.Nat+ ------------------------------------------------------------------------------- -- Proof -------------------------------------------------------------------------------@@ -60,6 +63,7 @@ data LEProof n m where     LEZero :: LEProof 'Z m     LESucc :: LEProof n m -> LEProof ('S n) ('S m)+  deriving (Typeable)  deriving instance Show (LEProof n m) 

@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DeriveDataTypeable    #-} {-# LANGUAGE EmptyCase             #-} {-# LANGUAGE FlexibleContexts      #-} {-# LANGUAGE FlexibleInstances     #-}@@ -35,10 +36,11 @@     ) where  import Data.Type.Dec      (Dec (..), Decidable (..), Neg)-import Data.Type.Equality-import Data.Type.Nat+import Data.Type.Equality ((:~:) (..))+import Data.Typeable      (Typeable) import Data.Void          (absurd) +import Data.Type.Nat import qualified Data.Type.Nat.LE as ZeroSucc  -------------------------------------------------------------------------------@@ -49,6 +51,7 @@ data LEProof n m where     LERefl :: LEProof n n     LEStep :: LEProof n m -> LEProof n ('S m)+  deriving (Typeable)  deriving instance Show (LEProof n m)