kind-rational 0.2 → 0.3

raw patch · 4 files changed

+149/−36 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-rational.cabal +3/−2
• lib/KindRational.hs +73/−34
• test/Main.hs +54/−0

@@ -1,9 +1,28 @@+# Version 0.3++* COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion`+  don't `Normalize` inputs before making a decision anymore.++* BREAKING CHANGE: The `Rational` inside `SRational` is not automatically+  normalized anymore. This is so that `SDecide`, `TestEquality` and+  `TestCoercion` behave as expected, treating `1/2` differently than `2/4`,+  for example. This is mostly an internal change, but it can be observed in+  the `Show` instance for `SRational`, for example.++* Added role annotations to `SRational`.++* Add dependency on `singletons` so that we can give a `Sing` and `SDecide`+  instances for type-level `Rational`s.++* Export `fromSRational'`.+ # Version 0.2  * COMPILER ASSISTED BREAKING CHANGE: Removed `Mod`, `DivMod`, `mod`, `divMod`.  * COMPILER ASSISTED BREAKING CHANGE: Renamed `Dif` to `Rem`, `DivDif` to   `DivRem`, `mod` to `rem`, `divDif` to `divRem`.+  # Version 0.1 

@@ -1,6 +1,6 @@ cabal-version: 2.4 name: kind-rational-version: 0.2+version: 0.3 license: BSD-3-Clause license-file: LICENSE extra-source-files: README.md CHANGELOG.md@@ -26,11 +26,13 @@   build-depends:     base ==4.*,     kind-integer >=0.2,+    singletons,   default-extensions:     DataKinds     NoStarIsType     LambdaCase     PatternSynonyms+    RoleAnnotations     TypeFamilies     TypeOperators     ViewPatterns@@ -38,7 +40,6 @@ library   import: basic   hs-source-dirs: lib-  build-depends: ghc-prim   exposed-modules: KindRational  test-suite test

@@ -1,3 +1,4 @@+{-# LANGUAGE StrictData #-} {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE UndecidableSuperClasses #-} @@ -39,6 +40,7 @@   , SRational   , pattern SRational   , fromSRational+  , fromSRational'   , withSomeSRational   , withKnownRational @@ -67,6 +69,7 @@     -- * Comparisons   , CmpRational   , cmpRational+  , eqRationalRep      -- * Extra     --@@ -74,21 +77,22 @@   , type (==?), type (==), type (/=?), type (/=)   ) --}   where--import qualified Control.Exception as Ex+import Control.Exception qualified as Ex import Control.Monad 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.Read qualified as Read import GHC.Real qualified as P (Ratio(..), (%)) import GHC.Show (appPrec, appPrec1) import GHC.TypeLits qualified as L import GHC.TypeNats qualified as N-import GHC.Types (TYPE, Constraint) import KindInteger (Integer, N, P) import KindInteger (type (==?), type (==), type (/=?), type (/=)) import KindInteger qualified as I@@ -128,14 +132,14 @@     -- or 'fromPrelude' instead.     --     -- * At the type-level, safely construct a 'Rational' using '/'.+    --+    -- * We keep the numerator and denominator unnormalized because we use them+    -- to implement 'SDecide', 'TestEquality' and 'TestCoercion'. Even if “1/2”+    -- and “2/4” mean the same, in 'SDecide' and friends we treat them as the+    -- different types that they are.     I.Integer :% Natural -num :: Rational -> I.Integer-num (n :% _) = n--den :: Rational -> Natural-den (_ :% d) = d-+-- | Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\). instance Eq Rational where   a == b = toPrelude a == toPrelude b @@ -166,8 +170,8 @@ -- 'showsPrecTypeLit' 0 ('rationalVal' ('Proxy' \@(1'/'2))) \"z\" == \"P 1 % 2z\" -- @ showsPrecTypeLit :: Int -> Rational -> ShowS-showsPrecTypeLit p r = showParen (p > appPrec) $-  I.showsPrecTypeLit appPrec (num r) . showString " % " . shows (den r)+showsPrecTypeLit p (n :% d) = showParen (p > appPrec) $+  I.showsPrecTypeLit appPrec n . showString " % " . shows d  -- | Make a term-level "KindRational" 'Rational' number, provided that -- the numerator is not @0@, and that its numerator and denominator are@@ -176,7 +180,7 @@ rational :: (Integral num, Integral den) => num -> den -> Maybe Rational rational = \(toInteger -> n) (toInteger -> d) -> do     guard (d /= 0 && abs n <= max_ && abs d <= max_)-    pure $ let n1 P.:% d1 = n P.% d+    pure $ let n1 P.:% d1 = n P.% d -- 'P.%' normalizes            in I.fromPrelude n1 :% fromInteger d1   where     max_ :: P.Integer -- Some big enough number. TODO: Pick good number.@@ -200,9 +204,8 @@     n P.:% d      | d == 0 -> Ex.throw Ex.RatioZeroDenominator      | abs n > max_ || abs d > max_ -> Ex.throw Ex.Overflow-     | otherwise ->-       let n1 P.:% d1 = n P.% d-       in I.fromPrelude n1 :% fromInteger d1+     | otherwise -> let n1 P.:% d1 = n P.% d -- 'P.%' normalizes+                    in I.fromPrelude n1 :% fromInteger d1   where     max_ :: P.Integer -- Some big enough number. TODO: Pick good number.     max_ = 10 ^ (1000 :: Int)@@ -211,15 +214,12 @@ unsafeCheckPrelude :: P.Rational -> P.Rational unsafeCheckPrelude = toPrelude . unsafeFromPrelude --- | Convert a term-level "KindRational" 'Rational' into a term-level--- "Prelude" 'P.Rational'.+-- | Convert a term-level "KindRational" 'Rational' into a 'Normalized'+-- term-level "Prelude" 'P.Rational'. ----- @--- 'fromPrelude' . 'toPrelude'      == 'Just'--- 'fmap' 'toPrelude' . 'fromPrelude' == 'Just'--- @+-- @'fromPrelude' . 'toPrelude' == 'Just'@ toPrelude :: Rational -> P.Rational-toPrelude r = I.toPrelude (num r) P.:% toInteger (den r)+toPrelude (n :% d) = I.toPrelude n P.% toInteger d -- 'P.%' normalizes.  -------------------------------------------------------------------------------- @@ -239,7 +239,7 @@ -- which not only accepts more polymorphic inputs, but also 'Normalize's -- the type-level 'Rational'. Also note that while @n '%' 0@ is a valid -- type, all tools in the "KindRational" will reject such input.-type (n :: I.Integer) % (d :: Natural) = n ':% d :: Rational+type (n :: I.Integer) % (d :: Natural) = n :% d :: Rational  -- | Normalize a type-level 'Rational' so that a /0/ denominator fails to -- type-check, and that the 'Num'erator and denominator have no common factors.@@ -490,7 +490,7 @@ -- | Term-level version of the "Terminates" function. -- Takes a "KindRational" 'P.Rational' as input. terminates' :: Rational -> Bool-terminates' = go . den+terminates' = \(_ :% d) -> go d   where     go = \case       5 -> True@@ -519,13 +519,19 @@ class KnownRational (r :: Rational) where   rationalSing :: SRational r +-- | This instance checks that @r@ 'Normalize's, but the obtained 'SRational' is+-- not normalized. This is so that 'SDecide', 'TestEquality' and 'TestCoercion'+-- behave as expected.  If you want a 'Normalize'd 'SRational', then use+-- @'rationalSing' \@('Normalize' r)@. instance forall r n d.   ( Normalize r ~ n % d-  , I.KnownInteger n-  , L.KnownNat d+  , I.KnownInteger (Num_ r)+  , L.KnownNat (Den_ r)   ) => KnownRational r where-  rationalSing = UnsafeSRational-    (I.fromPrelude (I.integerVal (Proxy @n)) :% N.natVal (Proxy @d))+  rationalSing =+    let n = I.fromSInteger' (I.SInteger @(Num_ r))+        d = N.natVal (Proxy @(Den_ r))+    in UnsafeSRational (n :% d)  -- | Term-level "KindRational" 'Rational' representation of the type-level -- 'Rational' @r@.@@ -596,6 +602,7 @@  -- | Singleton type for a type-level 'Rational' @r@. newtype SRational (r :: Rational) = UnsafeSRational Rational+type role SRational nominal  -- | A explicitly bidirectional pattern synonym relating an 'SRational' to a -- 'KnownRational' constraint.@@ -632,19 +639,38 @@   showsPrec p (UnsafeSRational r) = showParen (p > appPrec) $     showString "SRational @" . showsPrecTypeLit appPrec1 r +-- | Note that this checks for type equality, not arithmetic equality.+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,+-- even if they are arithmetically equal. instance TestEquality SRational where-  testEquality (UnsafeSRational x) (UnsafeSRational y) = do-    guard (toPrelude x P.== toPrelude y)-    pure (unsafeCoerce Refl)+  testEquality = decideEquality+  {-# INLINE testEquality #-} +-- | Note that this checks for type equality, not arithmetic equality.+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,+-- even if they are arithmetically equal. instance TestCoercion SRational where-  testCoercion x y = fmap (\Refl -> Coercion) (testEquality x y)+  testCoercion = decideCoercion+  {-# INLINE testCoercion #-}  -- | Return the term-level "Prelude" 'P.Rational' number corresponding--- to @r@ in a @'SRational' r@ value.+-- to @r@ in a @'SRational' r@ value. This 'P.Rational' is 'Normalize'd. fromSRational :: SRational r -> P.Rational fromSRational (UnsafeSRational r) = toPrelude r +-- | Return the term-level "KindRational" 'Rational' number corresponding+-- to @r@ in a @'SRational' r@ value. This 'Rational' is not 'Normalize'd.+fromSRational' :: SRational r -> Rational+fromSRational' (UnsafeSRational r) = r++-- | Whether the internal representation of the 'Rational's are equal.+--+-- Note that this is not the same as '(==)'. Use '(==)' unless you+-- know what you are doing.+eqRationalRep :: Rational -> Rational -> Bool+eqRationalRep (ln :% ld) (rn :% rd) = I.eqIntegerRep ln rn && ld P.== rd+{-# INLINE eqRationalRep #-}+ -- | Convert an explicit @'SRational' r@ value into an implicit -- @'KnownRational' r@ constraint. withKnownRational@@ -658,6 +684,19 @@ withSomeSRational r k = k (UnsafeSRational r) -- It's very important to keep this NOINLINE! See the docs at "GHC.TypeNats" {-# NOINLINE withSomeSRational #-}++--------------------------------------------------------------------------------++type instance Sing = SRational++-- | Note that this checks for type equality, not arithmetic equality.+-- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,+-- even if they are arithmetically equal.+instance SDecide Rational where+  UnsafeSRational l %~ UnsafeSRational r =+    case eqRationalRep l r of+      True  -> Proved (unsafeCoerce Refl)+      False -> Disproved (\Refl -> error "SDecide.Rational")  -------------------------------------------------------------------------------- -- Extra stuff that doesn't belong here.

@@ -9,6 +9,7 @@ import Data.List qualified as List import Data.Maybe import Data.Proxy+import Data.Type.Equality (TestEquality(..)) import Data.Type.Ord (type (<=), type (<)) import GHC.Exts (Constraint) import System.Exit@@ -481,6 +482,59 @@       in readMaybe @P.Rational str             == fmap (\(K.SomeRational p) -> K.rationalVal p)                     (readMaybe @K.SomeRational str)++   -- TODO test TestEquality++  , assert "TestEquality +0/1 +0/1" $+     isJust (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(P 0 % 1)))+  , assert "TestEquality -0/1 -0/1" $+     isJust (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(N 0 % 1)))+  , assert "TestEquality +1/2 +1/2" $+     isJust (testEquality (K.SRational @(P 1 % 2)) (K.SRational @(P 1 % 2)))+  , assert "TestEquality -1/2 -1/2" $+     isJust (testEquality (K.SRational @(N 1 % 2)) (K.SRational @(N 1 % 2)))+  , assert "TestEquality +0/1 -0/1" $+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(N 0 % 1)))+  , assert "TestEquality -0/1 +0/1" $+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(P 0 % 1)))+  , assert "TestEquality +0/1 +1/1" $+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(P 1 % 1)))+  , assert "TestEquality +0/1 -1/1" $+     isNothing (testEquality (K.SRational @(P 0 % 1)) (K.SRational @(N 1 % 1)))+  , assert "TestEquality -0/1 +1/1" $+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(P 1 % 1)))+  , assert "TestEquality -0/1 -1/1" $+     isNothing (testEquality (K.SRational @(N 0 % 1)) (K.SRational @(N 1 % 1)))+  , assert "TestEquality +1/1 +0/1" $+     isNothing (testEquality (K.SRational @(P 1 % 1)) (K.SRational @(P 0 % 1)))+  , assert "TestEquality +1/1 -0/1" $+     isNothing (testEquality (K.SRational @(P 1 % 1)) (K.SRational @(N 0 % 1)))+  , assert "TestEquality -1/1 +0/1" $+     isNothing (testEquality (K.SRational @(N 1 % 1)) (K.SRational @(P 0 % 1)))+  , assert "TestEquality -1/1 -0/1" $+     isNothing (testEquality (K.SRational @(N 1 % 1)) (K.SRational @(N 0 % 1)))+  , assert "TestEquality +1/2 +2/4" $+     isNothing (testEquality (K.SRational @(P 1 % 2)) (K.SRational @(P 2 % 4)))+  , assert "TestEquality -1/2 -2/4" $+     isNothing (testEquality (K.SRational @(N 1 % 2)) (K.SRational @(N 2 % 4)))++  , assert "Show Rational +0" $+     "0 % 1" == show (K.fromSRational (K.SRational @(P 0 % 1)))+  , assert "Show Rational -0" $+     "0 % 1" == show (K.fromSRational (K.SRational @(N 0 % 1)))+  , assert "Show Rational +1" $+     "1 % 1" == show (K.fromSRational (K.SRational @(P 1 % 1)))+  , assert "Show Rational -1" $+     "(-1) % 1" == show (K.fromSRational (K.SRational @(N 1 % 1)))++  , assert "Show SRational +0" $+     "SRational @(P 0 % 1)" == show (K.SRational @(P 0 % 1))+  , assert "Show SRational -0" $+     "SRational @(N 0 % 1)" == show (K.SRational @(N 0 % 1))+  , assert "Show SRational +1" $+     "SRational @(P 1 % 1)" == show (K.SRational @(P 1 % 1))+  , assert "Show SRational -1" $+     "SRational @(N 1 % 1)" == show (K.SRational @(N 1 % 1))    ] <> testsDivRem <> testsTerminating