diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -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` diff --git a/kind-rational.cabal b/kind-rational.cabal --- a/kind-rational.cabal +++ b/kind-rational.cabal @@ -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 diff --git a/lib/KindRational.hs b/lib/KindRational.hs --- a/lib/KindRational.hs +++ b/lib/KindRational.hs @@ -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, diff --git a/test/Main.hs b/test/Main.hs --- a/test/Main.hs +++ b/test/Main.hs @@ -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