kind-integer 0.3 → 0.4

raw patch · 4 files changed

+128/−18 lines, 4 filesdep +singletonsdep −ghc-primPVP ok

version bump matches the API change (PVP)

Dependencies added: singletons

Dependencies removed: ghc-prim

API changes (from Hackage documentation)

Files

• CHANGELOG.md +19/−0
• kind-integer.cabal +3/−2
• lib/KindInteger.hs +62/−16
• test/Main.hs +44/−0

@@ -1,3 +1,22 @@+# Version 0.4++* COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion` consider+  `N 0` and `P 0` to be different.++* BREAKING CHANGE: The `Integer` inside `SInteger`s is not automatically+  normalized anymore. This is so that `SDecide`, `TestEquality` and+  `TestCoercion` behave as expected, treating `N 0` and `P 0` differently.+  This is mostly an internal change, but it can be observed in the `Show`+  instance for `SInteger`, for example.++* Added role annotations to `SInteger`.++* Add dependency on `singletons` so that we can give a `Sing` and `SDecide`+  instances for type-level `Integer`s.++* Export `fromSInteger'`, `eqIntegerRep`.++ # Version 0.3  * COMPILER ASSISTED BREAKING CHANGE: Renamed `Mod` to `Rem`, `DivMod` to

@@ -1,6 +1,6 @@ cabal-version: 2.4 name: kind-integer-version: 0.3+version: 0.4 license: BSD-3-Clause license-file: LICENSE extra-source-files: README.md CHANGELOG.md@@ -28,6 +28,7 @@     DataKinds     MultiWayIf     NoStarIsType+    RoleAnnotations     PatternSynonyms     TypeFamilies     TypeOperators@@ -35,8 +36,8 @@  library   import: basic+  build-depends: singletons   hs-source-dirs: lib-  build-depends: ghc-prim   exposed-modules: KindInteger  test-suite test

@@ -34,6 +34,7 @@   , SInteger   , pattern SInteger   , fromSInteger+  , fromSInteger'   , withSomeSInteger   , withKnownInteger @@ -54,6 +55,7 @@     -- * Comparisons   , CmpInteger   , cmpInteger+  , eqIntegerRep      -- * Extra   , type (==?), type (==), type (/=?), type (/=)@@ -63,15 +65,17 @@ import Control.Exception qualified as Ex import Data.Bits import Data.Proxy+import Data.Singletons+import Data.Singletons.Decide import Data.Type.Bool (If) import Data.Type.Coercion-import Data.Type.Equality (TestEquality(..), (:~:)(..))+import Data.Type.Equality (TestEquality(..)) import Data.Type.Ord import GHC.Base (WithDict(..))+import GHC.Exts (TYPE, Constraint) import GHC.Real qualified as P import GHC.Show (appPrec, appPrec1) import GHC.TypeLits qualified as L-import GHC.Types (TYPE, Constraint) import Numeric.Natural (Natural) import Prelude hiding (Integer, (==), (/=), div, rem) import Prelude qualified as P@@ -179,15 +183,21 @@  -- | Positive numbers and zero. instance L.KnownNat x => KnownInteger (P x) where-  integerSing = UnsafeSInteger (L.natVal (Proxy @x))+  integerSing = UnsafeSInteger (P_ (fromInteger (L.natVal (Proxy @x))))  -- | Negative numbers and zero.+--+-- Implementation note: Notice that @'N' 0@ will not be 'Normalize'd to+-- @'P' 0@. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'+-- behave as expected. If you want a 'Normalize'd 'SInteger', then use+-- @'integerSing' \@('Normalize' i)@. instance L.KnownNat x => KnownInteger (N x) where-  integerSing = UnsafeSInteger (negate (L.natVal (Proxy @x)))+  integerSing = UnsafeSInteger (N_ (fromInteger (L.natVal (Proxy @x))))  -- | Term-level 'P.Integer' representation of the type-level 'Integer' @i@. integerVal :: forall i proxy. KnownInteger i => proxy i -> P.Integer-integerVal _ = case integerSing :: SInteger i of UnsafeSInteger x -> x+integerVal _ = case integerSing :: SInteger i of+                 UnsafeSInteger x -> toPrelude x  -- | This type represents unknown type-level 'Integer'. data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n)@@ -464,7 +474,8 @@ --------------------------------------------------------------------------------  -- | Singleton type for a type-level 'Integer' @i@.-newtype SInteger (i :: Integer) = UnsafeSInteger P.Integer+newtype SInteger (i :: Integer) = UnsafeSInteger Integer+type role SInteger representational  -- | A explicitly bidirectional pattern synonym relating an 'SInteger' to a -- 'KnownInteger' constraint.@@ -499,22 +510,44 @@  instance Show (SInteger i) where   showsPrec p (UnsafeSInteger i) = showParen (p > appPrec) $-    showString "SInteger @" .-    showsPrec appPrec1 (fromPrelude i)+    showString "SInteger @" . showsPrecTypeLit appPrec1 i +-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@+-- are not equal types, even if they are treated equally elsewhere in+-- "KindInteger". instance TestEquality SInteger where-  testEquality (UnsafeSInteger x) (UnsafeSInteger y)-    | x P.== y  = Just (unsafeCoerce Refl)-    | otherwise = Nothing+  testEquality = decideEquality+  {-# INLINE testEquality #-} +-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@+-- are not equal types, even if they are treated equally elsewhere in+-- "KindInteger". instance TestCoercion SInteger where-  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)+  testCoercion = decideCoercion+  {-# INLINE testCoercion #-} --- | Return the term-level 'P.Integer' number corresponding to @i@ in--- a @'SInteger' i@ value.+-- | Return the term-level "Prelude" 'P.Integer' number corresponding to @i@+-- in a @'SInteger' i@ value. fromSInteger :: SInteger i -> P.Integer-fromSInteger (UnsafeSInteger i) = i+fromSInteger (UnsafeSInteger i) = toPrelude i+{-# INLINE fromSInteger #-} +-- | Return the term-level "KindInteger" 'Integer' number corresponding to @i@+-- in a @'SInteger' i@ value.+fromSInteger' :: SInteger i -> Integer+fromSInteger' (UnsafeSInteger i) = i+{-# INLINE fromSInteger' #-}++-- | Whether the internal representation of the 'Integer's are equal.+--+-- Note that this is not the same as '(==)'. Use '(==)' unless you+-- know what you are doing.+eqIntegerRep :: Integer -> Integer -> Bool+eqIntegerRep (N_ l) (N_ r) = l P.== r+eqIntegerRep (P_ l) (P_ r) = l P.== r+eqIntegerRep _      _      = False+{-# INLINE eqIntegerRep #-}+ -- | Convert an explicit @'SInteger' i@ value into an implicit -- @'KnownInteger' i@ constraint. withKnownInteger@@ -525,9 +558,22 @@ -- fresh type-level 'Integer'. withSomeSInteger   :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r-withSomeSInteger n k = k (UnsafeSInteger n)+withSomeSInteger n k = k (UnsafeSInteger (fromPrelude n)) -- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats" {-# NOINLINE withSomeSInteger #-}++--------------------------------------------------------------------------------++type instance Sing = SInteger++-- | Note that this checks for type equality. That is, @'P' 0@ and @'N' 0@+-- are not equal types, even if they are treated equally elsewhere in+-- "KindInteger".+instance SDecide Integer where+  UnsafeSInteger l %~ UnsafeSInteger r =+    case eqIntegerRep l r of+      True  -> Proved (unsafeCoerce Refl)+      False -> Disproved (\Refl -> error "SDecide.Integer")  -------------------------------------------------------------------------------- 

@@ -9,6 +9,7 @@ import Data.List qualified as List import Data.Maybe import Data.Ratio as P+import Data.Type.Equality (TestEquality(..)) import Data.Type.Ord (type (<=)) import GHC.Exts (Constraint) import Prelude hiding (Integer)@@ -366,6 +367,49 @@       in readMaybe @P.Integer str             == fmap (\(K.SomeInteger p) -> K.integerVal p)                     (readMaybe @K.SomeInteger str)++  , assert "TestEquality +0 +0" $+     isJust (testEquality (K.SInteger @(P 0)) (K.SInteger @(P 0)))+  , assert "TestEquality -0 -0" $+     isJust (testEquality (K.SInteger @(N 0)) (K.SInteger @(N 0)))+  , assert "TestEquality +0 -0" $+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(N 0)))+  , assert "TestEquality -0 +0" $+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(P 0)))+  , assert "TestEquality +0 +1" $+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(P 1)))+  , assert "TestEquality +0 -1" $+     isNothing (testEquality (K.SInteger @(P 0)) (K.SInteger @(N 1)))+  , assert "TestEquality -0 +1" $+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(P 1)))+  , assert "TestEquality -0 -1" $+     isNothing (testEquality (K.SInteger @(N 0)) (K.SInteger @(N 1)))+  , assert "TestEquality +1 +0" $+     isNothing (testEquality (K.SInteger @(P 1)) (K.SInteger @(P 0)))+  , assert "TestEquality +1 -0" $+     isNothing (testEquality (K.SInteger @(P 1)) (K.SInteger @(N 0)))+  , assert "TestEquality -1 +0" $+     isNothing (testEquality (K.SInteger @(N 1)) (K.SInteger @(P 0)))+  , assert "TestEquality -1 -0" $+     isNothing (testEquality (K.SInteger @(N 1)) (K.SInteger @(N 0)))++  , assert "Show Integer +0" $+     "0" == show (K.fromSInteger (K.SInteger @(P 0)))+  , assert "Show Integer -0" $+     "0" == show (K.fromSInteger (K.SInteger @(N 0)))+  , assert "Show Integer +1" $+     "1" == show (K.fromSInteger (K.SInteger @(P 1)))+  , assert "Show Integer -1" $+     "-1" == show (K.fromSInteger (K.SInteger @(N 1)))++  , assert "Show SInteger +0" $+     "SInteger @(P 0)" == show (K.SInteger @(P 0))+  , assert "Show SInteger -0" $+     "SInteger @(N 0)" == show (K.SInteger @(N 0))+  , assert "Show SInteger +1" $+     "SInteger @(P 1)" == show (K.SInteger @(P 1))+  , assert "Show SInteger -1" $+     "SInteger @(N 1)" == show (K.SInteger @(N 1))    ] <> testsDivRem