packages feed

fin 0.0.3 → 0.1

raw patch · 6 files changed

+102/−90 lines, 6 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

- Data.Fin: [S] :: Fin n -> Fin ( 'S n)
- Data.Fin: [Z] :: Fin ( 'S n)
+ Data.Fin: [FS] :: Fin n -> Fin ( 'S n)
+ Data.Fin: [FZ] :: Fin ( 'S n)

Files

ChangeLog.md view
@@ -1,5 +1,10 @@ # Revision history for fin +## 0.1++- Rename `Fin` constructors to `FZ` and `FS`.+  Now you can have both `Nat` and `Fin` imported unqualified in a single module.+ ## 0.0.3  - Add `Data.Type.Nat.LE`, `Data.Type.Nat.LT` and `Data.Type.Nat.LE.ReflStep`
fin.cabal view
@@ -1,6 +1,6 @@ cabal-version:      >=1.10 name:               fin-version:            0.0.3+version:            0.1 synopsis:           Nat and Fin: peano naturals and finite numbers category:           Data, Dependent Types, Singletons description:
src/Data/Fin.hs view
@@ -8,7 +8,13 @@ {-# LANGUAGE UndecidableInstances #-} -- | Finite numbers. ----- This module is designed to be imported qualified.+-- This module is designed to be imported as+--+-- @+-- import Data.Fin (Fin (..))+-- import qualified Data.Fin as Fin+-- @+-- module Data.Fin (     Fin (..),     cata,@@ -45,14 +51,15 @@ 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  -- | Finite numbers: @[0..n-1]@.-data Fin (n :: N.Nat) where-    Z :: Fin ('N.S n)-    S :: Fin n -> Fin ('N.S n)+data Fin (n :: Nat) where+    FZ :: Fin ('S n)+    FS :: Fin n -> Fin ('S n)   deriving (Typeable)  -------------------------------------------------------------------------------@@ -77,7 +84,7 @@ -- *** Exception: divide by zero -- ... ----- >>> signum (Z :: Fin N.Nat1)+-- >>> signum (FZ :: Fin N.Nat1) -- 0 -- -- >>> signum (3 :: Fin N.Nat4)@@ -92,9 +99,9 @@ instance N.SNatI n => Num (Fin n) where     abs = id -    signum Z         = Z-    signum (S Z)     = S Z-    signum (S (S _)) = S Z+    signum FZ          = FZ+    signum (FS FZ)     = FS FZ+    signum (FS (FS _)) = FS FZ      fromInteger = unsafeFromNum . (`mod` (N.reflectToNum (Proxy :: Proxy n))) @@ -140,22 +147,22 @@ instance N.SNatI n => Enum (Fin n) where     fromEnum = go where         go :: Fin m -> Int-        go Z     = 0-        go (S n) = succ (go n)+        go FZ     = 0+        go (FS n) = succ (go n)      toEnum = unsafeFromNum -instance (n ~ 'N.S m, N.SNatI m) => Bounded (Fin n) where-    minBound = Z+instance (n ~ 'S m, N.SNatI m) => Bounded (Fin n) where+    minBound = FZ     maxBound = getMaxBound $ N.induction-        (MaxBound Z)-        (MaxBound . S . getMaxBound)+        (MaxBound FZ)+        (MaxBound . FS . getMaxBound) -newtype MaxBound n = MaxBound { getMaxBound :: Fin ('N.S n) }+newtype MaxBound n = MaxBound { getMaxBound :: Fin ('S n) }  instance NFData (Fin n) where-    rnf Z     = ()-    rnf (S n) = rnf n+    rnf FZ     = ()+    rnf (FS n) = rnf n  instance Hashable (Fin n) where     hashWithSalt salt = hashWithSalt salt . cata (0 :: Integer) succ@@ -167,19 +174,19 @@ -- | 'show' displaying a structure of 'Fin'. -- -- >>> explicitShow (0 :: Fin N.Nat1)--- "Z"+-- "FZ" -- -- >>> explicitShow (2 :: Fin N.Nat3)--- "S (S Z)"+-- "FS (FS FZ)" -- explicitShow :: Fin n -> String explicitShow n = explicitShowsPrec 0 n ""  -- | 'showsPrec' displaying a structure of 'Fin'. explicitShowsPrec :: Int -> Fin n -> ShowS-explicitShowsPrec _ Z     = showString "Z"-explicitShowsPrec d (S n) = showParen (d > 10)-    $ showString "S "+explicitShowsPrec _ FZ     = showString "FZ"+explicitShowsPrec d (FS n) = showParen (d > 10)+    $ showString "FS "     . explicitShowsPrec 11 n  -------------------------------------------------------------------------------@@ -190,12 +197,12 @@ cata :: forall a n. a -> (a -> a) -> Fin n -> a cata z f = go where     go :: Fin m -> a-    go Z = z-    go (S n) = f (go n)+    go FZ = z+    go (FS n) = f (go n)  -- | Convert to 'Nat'. toNat :: Fin n -> N.Nat-toNat = cata N.Z N.S+toNat = cata Z S  -- | Convert from 'Nat'. --@@ -207,13 +214,13 @@ -- fromNat :: N.SNatI n => N.Nat -> Maybe (Fin n) fromNat = appNatToFin (N.induction start step) where-    start :: NatToFin 'N.Z+    start :: NatToFin 'Z     start = NatToFin $ const Nothing -    step :: NatToFin n -> NatToFin ('N.S n)+    step :: NatToFin n -> NatToFin ('S n)     step (NatToFin f) = NatToFin $ \n -> case n of-        N.Z   -> Just Z-        N.S m -> fmap S (f m)+        Z   -> Just FZ+        S m -> fmap FS (f m)  newtype NatToFin n = NatToFin { appNatToFin :: N.Nat -> Maybe (Fin n) } @@ -224,16 +231,16 @@ -- | Convert from any 'Ord' 'Num'. unsafeFromNum :: forall n i. (Num i, Ord i, N.SNatI n) => i -> Fin n unsafeFromNum = appUnsafeFromNum (N.induction start step) where-    start :: UnsafeFromNum i 'N.Z+    start :: UnsafeFromNum i 'Z     start = UnsafeFromNum $ \n -> case compare n 0 of         LT -> throw Underflow         EQ -> throw Overflow         GT -> throw Overflow -    step :: UnsafeFromNum i m -> UnsafeFromNum i ('N.S m)+    step :: UnsafeFromNum i m -> UnsafeFromNum i ('S m)     step (UnsafeFromNum f) = UnsafeFromNum $ \n -> case compare n 0 of-        EQ -> Z-        GT -> S (f (n - 1))+        EQ -> FZ+        GT -> FS (f (n - 1))         LT -> throw Underflow  newtype UnsafeFromNum i n = UnsafeFromNum { appUnsafeFromNum :: i -> Fin n }@@ -248,17 +255,17 @@ -- [0,1,2] universe :: N.SNatI n => [Fin n] universe = getUniverse $ N.induction (Universe []) step where-    step :: Universe n -> Universe ('N.S n)-    step (Universe xs) = Universe (Z : map S xs)+    step :: Universe n -> Universe ('S n)+    step (Universe xs) = Universe (FZ : map FS xs)  -- | Like 'universe' but 'NonEmpty'. -- -- >>> universe1 :: NonEmpty (Fin N.Nat3) -- 0 :| [1,2]-universe1 :: N.SNatI n => NonEmpty (Fin ('N.S n))-universe1 = getUniverse1 $ N.induction (Universe1 (Z :| [])) step where-    step :: Universe1 n -> Universe1 ('N.S n)-    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))+universe1 :: N.SNatI n => NonEmpty (Fin ('S n))+universe1 = getUniverse1 $ N.induction (Universe1 (FZ :| [])) step where+    step :: Universe1 n -> Universe1 ('S n)+    step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs))  -- | 'universe' which will be fully inlined, if @n@ is known at compile time. --@@ -266,18 +273,18 @@ -- [0,1,2] inlineUniverse :: N.InlineInduction n => [Fin n] inlineUniverse = getUniverse $ N.inlineInduction (Universe []) step where-    step :: Universe n -> Universe ('N.S n)-    step (Universe xs) = Universe (Z : map S xs)+    step :: Universe n -> Universe ('S n)+    step (Universe xs) = Universe (FZ : map FS xs)  -- | >>> inlineUniverse1 :: NonEmpty (Fin N.Nat3) -- 0 :| [1,2]-inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('N.S n))-inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (Z :| [])) step where-    step :: Universe1 n -> Universe1 ('N.S n)-    step (Universe1 xs) = Universe1 (NE.cons Z (fmap S xs))+inlineUniverse1 :: N.InlineInduction n => NonEmpty (Fin ('S n))+inlineUniverse1 = getUniverse1 $ N.inlineInduction (Universe1 (FZ :| [])) step where+    step :: Universe1 n -> Universe1 ('S n)+    step (Universe1 xs) = Universe1 (NE.cons FZ (fmap FS xs))  newtype Universe  n = Universe  { getUniverse  :: [Fin n] }-newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('N.S n)) }+newtype Universe1 n = Universe1 { getUniverse1 :: NonEmpty (Fin ('S n)) }  -- | @'Fin' 'N.Nat0'@ is inhabited. absurd :: Fin N.Nat0 -> b@@ -288,7 +295,7 @@ -- >>> boring -- 0 boring :: Fin N.Nat1-boring = Z+boring = FZ  ------------------------------------------------------------------------------- -- Append & Split@@ -296,20 +303,20 @@  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 'N.Z+    start :: WeakenLeft m 'Z     start = WeakenLeft absurd -    step :: WeakenLeft m p -> WeakenLeft m ('N.S p)+    step :: WeakenLeft m p -> WeakenLeft m ('S p)     step (WeakenLeft go) = WeakenLeft $ \n -> case n of-        Z    -> Z-        S n' -> S (go n')+        FZ    -> FZ+        FS n' -> FS (go n')  newtype WeakenLeft m n = WeakenLeft { getWeakenLeft :: Fin n -> Fin (N.Plus n m) }  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-    step (WeakenRight go) = WeakenRight $ \x -> S $ go x+    step (WeakenRight go) = WeakenRight $ \x -> FS $ go x  newtype WeakenRight m n = WeakenRight { getWeakenRight :: Fin m -> Fin (N.Plus n m) } @@ -338,13 +345,13 @@ -- split :: forall n m. N.InlineInduction n => Fin (N.Plus n m) -> Either (Fin n) (Fin m) split = getSplit (N.inlineInduction start step) where-    start :: Split m 'N.Z+    start :: Split m 'Z     start = Split Right -    step :: Split m p -> Split m ('N.S p)+    step :: Split m p -> Split m ('S p)     step (Split go) = Split $ \x -> case x of-        Z    -> Left Z-        S x' -> bimap S id $ go x'+        FZ    -> Left FZ+        FS x' -> bimap FS id $ go x'  newtype Split m n = Split { getSplit :: Fin (N.Plus n m) -> Either (Fin n) (Fin m) } @@ -352,24 +359,24 @@ -- Aliases ------------------------------------------------------------------------------- -fin0 :: Fin (N.Plus N.Nat0 ('N.S n))-fin1 :: Fin (N.Plus N.Nat1 ('N.S n))-fin2 :: Fin (N.Plus N.Nat2 ('N.S n))-fin3 :: Fin (N.Plus N.Nat3 ('N.S n))-fin4 :: Fin (N.Plus N.Nat4 ('N.S n))-fin5 :: Fin (N.Plus N.Nat5 ('N.S n))-fin6 :: Fin (N.Plus N.Nat6 ('N.S n))-fin7 :: Fin (N.Plus N.Nat7 ('N.S n))-fin8 :: Fin (N.Plus N.Nat8 ('N.S n))-fin9 :: Fin (N.Plus N.Nat9 ('N.S n))+fin0 :: Fin (N.Plus N.Nat0 ('S n))+fin1 :: Fin (N.Plus N.Nat1 ('S n))+fin2 :: Fin (N.Plus N.Nat2 ('S n))+fin3 :: Fin (N.Plus N.Nat3 ('S n))+fin4 :: Fin (N.Plus N.Nat4 ('S n))+fin5 :: Fin (N.Plus N.Nat5 ('S n))+fin6 :: Fin (N.Plus N.Nat6 ('S n))+fin7 :: Fin (N.Plus N.Nat7 ('S n))+fin8 :: Fin (N.Plus N.Nat8 ('S n))+fin9 :: Fin (N.Plus N.Nat9 ('S n)) -fin0 = Z-fin1 = S fin0-fin2 = S fin1-fin3 = S fin2-fin4 = S fin3-fin5 = S fin4-fin6 = S fin5-fin7 = S fin6-fin8 = S fin7-fin9 = S fin8+fin0 = FZ+fin1 = FS fin0+fin2 = FS fin1+fin3 = FS fin2+fin4 = FS fin3+fin5 = FS fin4+fin6 = FS fin5+fin7 = FS fin6+fin8 = FS fin7+fin9 = FS fin8
src/Data/Fin/Enum.hs view
@@ -28,8 +28,8 @@ import Prelude hiding (Enum (..))  import Data.Bifunctor (bimap)-import Data.Fin       (Fin)-import Data.Nat       (Nat)+import Data.Fin       (Fin (..))+import Data.Nat       (Nat (..)) import Data.Proxy     (Proxy (..)) import GHC.Generics   ((:+:) (..), M1 (..), U1 (..), V1) @@ -106,7 +106,7 @@     EnumSizeRep (a :+: b )   n = EnumSizeRep a (EnumSizeRep b n)     EnumSizeRep V1           n = n     EnumSizeRep (M1 _d _c a) n = EnumSizeRep a n-    EnumSizeRep U1           n = 'N.S n+    EnumSizeRep U1           n = 'S n     -- No instance for K1 or :*:  -------------------------------------------------------------------------------@@ -139,8 +139,8 @@     gfromSkip _ n = n  instance GFromRep U1 where-    gfromRep U1 _ = F.Z-    gfromSkip _ n = F.S n+    gfromRep U1 _ = FZ+    gfromSkip _ n = FS n  ------------------------------------------------------------------------------- -- To@@ -166,5 +166,5 @@     gtoRep n _ k = k n  instance GToRep U1 where-    gtoRep F.Z     s _ = s U1-    gtoRep (F.S n) _ k = k n+    gtoRep FZ     s _ = s U1+    gtoRep (FS n) _ k = k n
src/Data/Type/Nat/LE/ReflStep.hs view
@@ -124,9 +124,8 @@  -- | \(\forall n\, m\, p : \mathbb{N}, n \le m \to m \le p \to n \le p \) leTrans :: LEProof n m -> LEProof m p -> LEProof n p-leTrans LERefl     q          = q-leTrans p          LERefl     = p-leTrans (LEStep p) (LEStep q) = LEStep $ leTrans p $ leStepL q+leTrans p LERefl     = p+leTrans p (LEStep q) = LEStep $ leTrans p q  -- | \(\forall n\, m : \mathbb{N}, \neg (n \le m) \to 1 + m \le n \) leSwap :: forall n m. (SNatI n, SNatI m) => Neg (LEProof n m) -> LEProof ('S m) n
test/Inspection.hs view
@@ -6,6 +6,7 @@ {-# OPTIONS_GHC -O -fplugin Test.Inspection.Plugin #-} module Main (main) where +import Data.Fin           (Fin (..)) import Data.Function      (fix) import Data.Proxy         (Proxy (..)) import Data.Tagged        (Tagged (..), retag)@@ -51,9 +52,9 @@ lhsEnum = E.gfrom  rhsEnum :: Ordering' -> F.Fin N.Nat3-rhsEnum LT' = F.Z-rhsEnum EQ' = F.S F.Z-rhsEnum GT' = F.S (F.S F.Z)+rhsEnum LT' = FZ+rhsEnum EQ' = FS FZ+rhsEnum GT' = FS (FS FZ)  inspect $ 'lhsEnum ==- 'rhsEnum