packages feed

kind-rational 0.3 → 0.4

raw patch · 4 files changed

+85/−96 lines, 4 filesdep ~kind-integer

Dependency ranges changed: kind-integer

Files

CHANGELOG.md view
@@ -1,3 +1,14 @@+# Version 0.3.1++* COMPILER ASSISTED BREAKING CHANGE: `rationalVal`, `someRationalVal`,+  `fromSRational`, `terminates`, `divRem`, `div` and `rem` now deal+  with `KindRational`'s `Rational`s, rather than `Prelude`'s `Rational`s.++* COMPILER ASSISTED BREAKING CHANGE: Removed `fromSRational'`.++* Added `SingI` and `SingKind` instances.++ # Version 0.3  * COMPILER ASSISTED BREAKING CHANGE: `TestEquality` and `TestCoercion`
kind-rational.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.4 name: kind-rational-version: 0.3+version: 0.4 license: BSD-3-Clause license-file: LICENSE extra-source-files: README.md CHANGELOG.md@@ -25,7 +25,7 @@   ghc-options: -O2 -Wall -Werror=incomplete-patterns   build-depends:     base ==4.*,-    kind-integer >=0.2,+    kind-integer >=0.5,     singletons,   default-extensions:     DataKinds
lib/KindRational.hs view
@@ -40,7 +40,6 @@   , SRational   , pattern SRational   , fromSRational-  , fromSRational'   , withSomeSRational   , withKnownRational @@ -77,7 +76,7 @@   , type (==?), type (==), type (/=?), type (/=)   ) --}   where-import Control.Exception qualified as Ex+ import Control.Monad import Data.Proxy import Data.Singletons@@ -109,21 +108,18 @@ -- pattern-match on it. -- -- 'Rational' is mostly used as a kind, with its types constructed--- using '/'.  However, it might also be used as type, with its terms+-- using '/'.  However, it is also used as type, with its terms -- constructed using 'rational' or 'fromPrelude'. One reason why you may want a -- 'Rational' at the term-level is so that you embed it in larger data-types -- (for example, this 'Rational' embeds the 'I.Integer' similarly offered by -- the "KindInteger" module). But perhaps more importantly, this 'Rational' -- offers better safety than the 'P.Rational' from "Prelude", since it's not -- possible to construct one with a zero denominator, or so large that--- operating with it would exhaust system resources. Notwithstanding this, for--- ergonomic reasons, all of the functions exported by this module take--- "Prelude" 'Rational's as input and produce "Prelude" 'Rational's as outputs.--- Internally, however, the beforementioned checks are always performed, and--- fail with 'Ex.throw' if necessary. If you want to be sure those 'error's--- never happen, just filter your "Prelude" 'Rational's with 'fromPrelude'. In--- practice, it's very unlikely that you will be affected by this unless if--- you are unsafelly constructing "Prelude" 'Rational's.+-- operating with it would exhaust system resources. Additionally,+-- a "KindRational"'s 'Rational' can fully represent the internal structure+-- of a type-level 'Rational'. For these reasons, functions like+-- 'fromSRational' and 'withSomeSRational' deal with it, rather than with+-- "Prelude"'s 'P.Rational'. data Rational   = -- | This constructor is /unsafe/ because it doesn't check for the things     -- that 'rational' checks for.@@ -192,28 +188,10 @@ -- -- @ -- 'fromPrelude' . 'toPrelude'      == 'Just'--- 'fmap' 'toPrelude' . 'fromPrelude' == 'Just' -- @ fromPrelude :: P.Rational -> Maybe Rational fromPrelude (n P.:% d) = rational n d --- | Like 'fromPrelude', but 'Ex.throw's in situations where--- 'fromPrelude' fails with 'Nothing'.-unsafeFromPrelude :: P.Rational -> Rational-unsafeFromPrelude = \case-    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 -- 'P.%' normalizes-                    in I.fromPrelude n1 :% fromInteger d1-  where-    max_ :: P.Integer -- Some big enough number. TODO: Pick good number.-    max_ = 10 ^ (1000 :: Int)---- | Like 'unsafeFromPrelude', but returns a "Prelude" 'P.Rational'.-unsafeCheckPrelude :: P.Rational -> P.Rational-unsafeCheckPrelude = toPrelude . unsafeFromPrelude- -- | Convert a term-level "KindRational" 'Rational' into a 'Normalized' -- term-level "Prelude" 'P.Rational'. --@@ -401,33 +379,32 @@  -- | Term-level version of 'Div'. ----- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Integer'.-div :: I.Round -> P.Rational -> P.Integer+-- Takes a "KindInteger" 'Rational' as input, returns a "Prelude"+-- 'P.Integer'.+div :: I.Round -> Rational -> P.Integer div r = let f = I.div r-        in \a -> let (n P.:% d) = unsafeCheckPrelude a-                 in  f n d+        in \(n :% d) -> f (I.toPrelude n) (toInteger d)  -- | Term-level version of 'Rem'. ----- Takes a "Prelude" 'P.Rational' as input, returns a "Prelude" 'P.Rational'.-rem :: I.Round -> P.Rational -> P.Rational+-- Takes a "KindInteger" 'Rational' as input, returns a "KindInteger" 'Rational'.+rem :: I.Round -> Rational -> Rational rem r = snd . divRem r  -- | Term-level version of 'DivRem'. ----- Takes a "Prelude" 'P.Rational' as input, returns a pair of "Prelude"--- 'P.Rational's /(quotient, remerence)/.+-- Takes a "KindInteger" 'Rational' as input, returns a pair of+-- /(quotient, reminder)/. -- -- @--- forall ('r' :: 'I.Round') (a :: 'P.Rational').+-- forall ('r' :: 'I.Round') (a :: 'Rational'). --   ('P.denominator' a 'P./=' 0) => --     'divRem' r a  'P.=='  ('div' r a, 'rem' r a) -- @-divRem :: I.Round -> P.Rational -> (P.Integer, P.Rational)+divRem :: I.Round -> Rational -> (P.Integer, Rational) divRem r = let f = I.divRem r-           in \a -> let (n P.:% d) = unsafeCheckPrelude a-                        (q, m) = f n d-                    in  (q, m P.% d) -- (m % d) == (a - q)+           in \(n :% d) -> let (q, m) = f (I.toPrelude n) (toInteger d)+                           in  (q, I.fromPrelude m :% d) -- (m % d) == (a - q)  -------------------------------------------------------------------------------- @@ -456,7 +433,7 @@   => (Terminating r => a)   -> Maybe a withTerminating g = do-  guard (terminates' (rationalVal' (Proxy @r)))+  guard (terminates (rationalVal (Proxy @r)))   case unsafeCoerce (Dict @(Terminating (P 1 % 1))) of     (Dict :: Dict (Terminating r)) -> pure g @@ -483,14 +460,9 @@   Terminates_2 _ _ = 'False  -- | Term-level version of the "Terminates" function.--- Takes a "Prelude" 'P.Rational' as input.-terminates :: P.Rational -> Bool-terminates = terminates' . unsafeFromPrelude---- | Term-level version of the "Terminates" function.--- Takes a "KindRational" 'P.Rational' as input.-terminates' :: Rational -> Bool-terminates' = \(_ :% d) -> go d+-- Takes a "KindRational" 'Rational' as input.+terminates :: Rational -> Bool+terminates = \(_ :% d) -> go (toInteger d)   where     go = \case       5 -> True@@ -529,31 +501,25 @@   , L.KnownNat (Den_ r)   ) => KnownRational r where   rationalSing =-    let n = I.fromSInteger' (I.SInteger @(Num_ r))+    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@.-rationalVal' :: forall r proxy. KnownRational r => proxy r -> Rational-rationalVal' _ = case rationalSing :: SRational r of-                   UnsafeSRational x -> x---- | Term-level "Prelude" 'P.Rational' representation of the type-level--- 'Rational' @r@.-rationalVal :: forall r proxy. KnownRational r => proxy r -> P.Rational-rationalVal = toPrelude . rationalVal'+rationalVal :: forall r proxy. KnownRational r => proxy r -> Rational+rationalVal _ = case rationalSing :: SRational r of UnsafeSRational x -> x  -- | This type represents unknown type-level 'Rational'. data SomeRational = forall n. KnownRational n => SomeRational (Proxy n) --- | Convert a term-level "Prelude" 'Rational' into an unknown+-- | Convert a term-level "KindRational" 'Rational' into an unknown -- type-level 'Rational'.-someRationalVal :: P.Rational -> SomeRational-someRationalVal r =-  withSomeSRational (unsafeFromPrelude r) $ \(sr :: SRational r) ->-    withKnownRational sr (SomeRational @r Proxy)+someRationalVal :: Rational -> SomeRational+someRationalVal r = withSomeSRational r $ \(sr :: SRational r) ->+                    withKnownRational sr (SomeRational @r Proxy) +-- | Arithmethic equality. That is, \(\frac{1}{2} == \frac{2}{4}\). instance Eq SomeRational where   SomeRational x == SomeRational y = rationalVal x P.== rationalVal y @@ -653,19 +619,14 @@   testCoercion = decideCoercion   {-# INLINE testCoercion #-} --- | Return the term-level "Prelude" 'P.Rational' number corresponding--- 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+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+-- Note that this is not the same as '(P.==)'. Use '(P.==)' unless you -- know what you are doing. eqRationalRep :: Rational -> Rational -> Bool eqRationalRep (ln :% ld) (rn :% rd) = I.eqIntegerRep ln rn && ld P.== rd@@ -677,7 +638,7 @@   :: forall r rep (a :: TYPE rep). SRational r -> (KnownRational r => a) -> a withKnownRational = withDict @(KnownRational r) --- | Convert a "Prelude" 'P.Rational' number into an @'SRational' n@ value,+-- | Convert a "KindRational" 'Rational' number into an @'SRational' n@ value, -- where @n@ is a fresh type-level 'Rational'. withSomeSRational   :: forall rep (a :: TYPE rep). Rational -> (forall r. SRational r -> a) -> a@@ -688,6 +649,20 @@ --------------------------------------------------------------------------------  type instance Sing = SRational++instance KnownRational r => SingI (r :: Rational) where+  sing = rationalSing+  {-# INLINE sing #-}++-- | 'Demote' refers to "KindRational"'s 'Rational' rather than "Prelude"'s+-- 'Rational' so that the 'SRational''s internal representation is preserved.+-- Use 'toPrelude' and 'fromPrelude' as necessary.+instance SingKind Rational where+  type Demote Rational = Rational+  fromSing = fromSRational+  {-# INLINE fromSing #-}+  toSing r = withSomeSRational r SomeSing+  {-# INLINE toSing #-}  -- | Note that this checks for type equality, not arithmetic equality. -- That is, @'P' 1 '%' 2@ and @'P' 2 '%' 4@ are not equal types,
test/Main.hs view
@@ -1,4 +1,4 @@-{-# OPTIONS_GHC -Wno-missing-signatures #-}+{-# OPTIONS_GHC -Wno-missing-signatures -Wno-incomplete-uni-patterns #-} module Main {--}   ( main   ) --}@@ -431,23 +431,22 @@     [] -> exitSuccess     _  -> exitFailure -rats :: P.Integer -> [P.Rational]+rats :: P.Integer -> [K.Rational] rats i = do n <- [negate i .. i]             d <- [negate i .. i]-            guard (d /= 0)-            pure (n P.% d)+            maybeToList $ K.rational n d  main :: IO () main = testsMain $   [ assert "rationalVal . someRationalVal == id" $-    flip all (rats 4) $ \r ->-      case K.someRationalVal r of+    flip all (rats 4) $ \a ->+      case K.someRationalVal a of         K.SomeRational pa ->-          r == K.rationalVal pa+          a == K.rationalVal pa    , assert "sameRationalVal a a" $-    flip all (rats 4) $ \r ->-      case K.someRationalVal r of+    flip all (rats 4) $ \a ->+      case K.someRationalVal a of         K.SomeRational pa ->           isJust (K.sameRational pa pa) @@ -470,17 +469,17 @@    , assert "Ord SomeRational" $     flip all (liftA2 (,) (rats 4) (rats 4))$ \(a, b) ->-      (a `compare` b) == (K.someRationalVal a `compare` K.someRationalVal b)+      compare a b == compare (K.someRationalVal a) (K.someRationalVal b)    , assert "Show SomeRational" $     flip all (rats 4) $ \a ->       show a == show (K.someRationalVal a)    , assert "Read SomeRational" $-    flip all (rats 4) $ \r ->-      let str = show r+    flip all (rats 4) $ \a ->+      let str = show a       in readMaybe @P.Rational str-            == fmap (\(K.SomeRational p) -> K.rationalVal p)+            == fmap (\(K.SomeRational p) -> K.toPrelude (K.rationalVal p))                     (readMaybe @K.SomeRational str)     -- TODO test TestEquality@@ -540,13 +539,15 @@  testsDivRem :: [IO Bool] testsDivRem = do-  a@(n P.:% d) <- rats 4+  a <- rats 4+  let n P.:% d = K.toPrelude a   r :: K.Round <- [minBound .. maxBound]   let tname :: String -> ShowS       tname t = showString t . showChar ' ' . shows r . showChar ' '               . shows n . showChar ' ' . shows d-  [   assert (tname "divRem" "") $ case K.divRem r a of-                                        (q, x) -> a == toRational q + x+  [   assert (tname "divRem" "") $+         case K.divRem r a of+           (q, x) -> Just a == K.fromPrelude (toRational q + K.toPrelude x)     , assert (tname "divRem/div" "") $ fst (K.divRem r a) == K.div r a     , assert (tname "divRem/rem" "") $ snd (K.divRem r a) == K.rem r a     ]@@ -566,8 +567,9 @@                isNothing (K.withTerminating @a () :: Maybe ())     ]   where-   ok :: [P.Rational]-   ok = [ 0 P.% 1+   ok :: [K.Rational]+   Just ok = traverse K.fromPrelude+        [ 0 P.% 1         , -1 P.% 1         , 2 P.% 1         , -1 P.% 2@@ -589,8 +591,9 @@         , -3 P.% 50         , 3 P.% 10000000         ]-   no :: [P.Rational]-   no = [ 1 P.% 3+   no :: [K.Rational]+   Just no = traverse K.fromPrelude+        [ 1 P.% 3         , -1 P.% 12         , 1 P.% 15         , -2 P.% 3