kind-integer 0.4 → 0.5

raw patch · 4 files changed

+79/−45 lines, 4 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• CHANGELOG.md +11/−0
• kind-integer.cabal +1/−1
• lib/KindInteger.hs +39/−26
• test/Main.hs +28/−18

@@ -1,3 +1,14 @@+# Version 0.5++* COMPILER ASSISTED BREAKING CHANGE: `integerVal`, `someIntegerVal`,+  `fromSInteger` and `withSomeSInteger` now deal with `KindInteger`'s+  `Integer`s, rather than `Prelude`'s `Integer`s.++* COMPILER ASSISTED BREAKING CHANGE: Removed `fromSInteger'`.++* Added `SingI` and `SingKind` instances.++ # Version 0.4  * COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion` consider

@@ -1,6 +1,6 @@ cabal-version: 2.4 name: kind-integer-version: 0.4+version: 0.5 license: BSD-3-Clause license-file: LICENSE extra-source-files: README.md CHANGELOG.md

@@ -34,7 +34,6 @@   , SInteger   , pattern SInteger   , fromSInteger-  , fromSInteger'   , withSomeSInteger   , withKnownInteger @@ -83,8 +82,7 @@  -------------------------------------------------------------------------------- --- | Type-level version of 'P.Integer', only ever used as a /kind/--- for 'P' and 'N'+-- | Type-level version of 'P.Integer', mostly used as a /kind/ for 'P' and 'N'. -- -- * A positive number /+x/ is represented as @'P' x@. --@@ -102,11 +100,16 @@ -- at the term-level is so that you embed it in larger data-types (for example, -- the "KindRational" module from the -- [@kind-rational@](https://hackage.haskell.org/package/kind-rational)--- library embeds this 'I.Integer' in its 'KindRational.Rational' type)+-- library embeds this 'I.Integer' in its 'KindRational.Rational' type).+-- Contrary to "Prelude"'s 'P.Integer', "KindInteger"'s 'Integer' preserves+-- the internal distinction between @'P' 0@ and @'N' 0@, this is why functions+-- such as 'fromSInteger' prefer to use "KindInteger"'s 'Integer' rather+-- than "Prelude"'s 'P.Integer'. data Integer   = P_ Natural   | N_ Natural +-- | Note that @'P' 0 '==' 'N' 0@. instance Eq Integer where   a == b = toPrelude a P.== toPrelude b @@ -194,19 +197,21 @@ instance L.KnownNat x => KnownInteger (N x) where   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 -> toPrelude x+-- | Term-level "KindRational" 'Integer' representation of the type-level+-- 'Integer' @i@.+integerVal :: forall i proxy. KnownInteger i => proxy i -> Integer+integerVal _ = case integerSing :: SInteger i of UnsafeSInteger x -> x  -- | This type represents unknown type-level 'Integer'. data SomeInteger = forall n. KnownInteger n => SomeInteger (Proxy n) --- | Convert a term-level 'P.Integer' into an unknown type-level 'Integer'.-someIntegerVal :: P.Integer -> SomeInteger-someIntegerVal i = withSomeSInteger i (\(si :: SInteger i) ->-                   withKnownInteger si (SomeInteger @i Proxy))+-- | Convert a term-level "KindInteger" 'Integer' into an unknown+-- type-level 'Integer'.+someIntegerVal :: Integer -> SomeInteger+someIntegerVal i = withSomeSInteger i $ \(si :: SInteger i) ->+                   withKnownInteger si (SomeInteger @i Proxy) +-- | Note that @'P' 0 '==' 'N' 0@. instance Eq SomeInteger where   SomeInteger x == SomeInteger y = integerVal x P.== integerVal y @@ -526,21 +531,15 @@   testCoercion = decideCoercion   {-# INLINE testCoercion #-} --- | Return the term-level "Prelude" 'P.Integer' number corresponding to @i@--- in a @'SInteger' i@ value.-fromSInteger :: SInteger i -> P.Integer-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' #-}+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+-- Note that this is not the same as '(P.==)'. Use '(P.==)' unless you -- know what you are doing. eqIntegerRep :: Integer -> Integer -> Bool eqIntegerRep (N_ l) (N_ r) = l P.== r@@ -554,17 +553,31 @@   :: forall i rep (r :: TYPE rep). SInteger i -> (KnownInteger i => r) -> r withKnownInteger = withDict @(KnownInteger i) --- | Convert a 'P.Integer' number into an @'SInteger' n@ value, where @n@ is a--- fresh type-level 'Integer'.+-- | Convert a "KindIiteger" 'Integer' number into an @'SInteger' n@ value,+-- where @n@ is a fresh type-level 'Integer'. withSomeSInteger-  :: forall rep (r :: TYPE rep). P.Integer -> (forall n. SInteger n -> r) -> r-withSomeSInteger n k = k (UnsafeSInteger (fromPrelude n))+  :: forall rep (r :: TYPE rep). Integer -> (forall n. SInteger n -> r) -> r+withSomeSInteger n k = k (UnsafeSInteger n) -- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats" {-# NOINLINE withSomeSInteger #-}  --------------------------------------------------------------------------------  type instance Sing = SInteger++instance KnownInteger i => SingI (i :: Integer) where+  sing = integerSing+  {-# INLINE sing #-}++-- | 'Demote' refers to "KindInteger"'s 'Integer' rather than "Prelude"'s+-- 'Integer' so that the 'SInteger''s internal representation is preserved.+-- Use 'toPrelude' and 'fromPrelude' as necessary.+instance SingKind Integer where+  type Demote Integer = Integer+  fromSing = fromSInteger+  {-# INLINE fromSing #-}+  toSing i = withSomeSInteger i SomeSing+  {-# INLINE toSing #-}  -- | 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

@@ -308,28 +308,33 @@    , assert "integerVal . someIntegerVal == id" $     flip all [-5 .. 5] $ \a ->-      case K.someIntegerVal a of-        K.SomeInteger pa ->-          a == K.integerVal pa+      let a' = K.fromPrelude a+      in case K.someIntegerVal a' of+           K.SomeInteger pa ->+             a' == K.integerVal pa    , assert "sameIntegerVal a a" $     flip all [-5 .. 5] $ \a ->-      case K.someIntegerVal a of-        K.SomeInteger pa ->-          isJust (K.sameInteger pa pa)+      let a' = K.fromPrelude a+      in case K.someIntegerVal a' of+           K.SomeInteger pa ->+             isJust (K.sameInteger pa pa)    , assert "sameIntegerVal a a'" $     flip all [-5 .. 5] $ \a ->-      case (K.someIntegerVal a, K.someIntegerVal a) of-        (K.SomeInteger pa1, K.SomeInteger pa2) ->-          isJust (K.sameInteger pa1 pa2)+      let a' = K.fromPrelude a+      in case (K.someIntegerVal a', K.someIntegerVal a') of+           (K.SomeInteger pa1, K.SomeInteger pa2) ->+             isJust (K.sameInteger pa1 pa2)    , assert "sameIntegerVal a b" $     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->-      case (K.someIntegerVal a, K.someIntegerVal b) of-        (K.SomeInteger pa, K.SomeInteger pb)-          | a == b    -> isJust    (K.sameInteger pa pb)-          | otherwise -> isNothing (K.sameInteger pa pb)+      let a' = K.fromPrelude a+          b' = K.fromPrelude b+      in case (K.someIntegerVal a', K.someIntegerVal b') of+           (K.SomeInteger pa, K.SomeInteger pb)+             | a == b    -> isJust    (K.sameInteger pa pb)+             | otherwise -> isNothing (K.sameInteger pa pb)    , assert "Eq fromPrelude" $     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->@@ -351,21 +356,26 @@    , assert "Eq SomeInteger" $     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->-      (a == b) == (K.someIntegerVal a == K.someIntegerVal b)+      let a' = K.fromPrelude a+          b' = K.fromPrelude b+      in (a == b) == (K.someIntegerVal a' == K.someIntegerVal b')    , assert "Ord SomeInteger" $     flip all (liftA2 (,) [-5 .. 5] [-5 .. 5])$ \(a, b) ->-      (a `compare` b) == (K.someIntegerVal a `compare` K.someIntegerVal b)+      compare a b ==+         compare (K.someIntegerVal (K.fromPrelude a))+                 (K.someIntegerVal (K.fromPrelude b))    , assert "Show SomeInteger" $-    flip all [-5 .. 5] $ \i ->-      show i == show (K.someIntegerVal i)+    flip all [-5 .. 5] $ \a ->+      let a' = K.fromPrelude a+      in show a == show (K.someIntegerVal a')    , assert "Read SomeInteger" $     flip all [-5 .. 5] $ \i ->       let str = show (i :: P.Integer)       in readMaybe @P.Integer str-            == fmap (\(K.SomeInteger p) -> K.integerVal p)+            == fmap (\(K.SomeInteger p) -> K.toPrelude (K.integerVal p))                     (readMaybe @K.SomeInteger str)    , assert "TestEquality +0 +0" $