snumber 0.2.0 → 0.3.0
raw patch · 4 files changed
+30/−23 lines, 4 filesdep +type-comparedep ~numeric-kinds
Dependencies added: type-compare
Dependency ranges changed: numeric-kinds
Files
- CHANGELOG.md +7/−0
- snumber.cabal +4/−3
- src/Data/SNumber.hs +15/−17
- src/Data/SNumber/Internal.hs +4/−3
CHANGELOG.md view
@@ -1,3 +1,10 @@+# 0.3.0 (2021-11-05)++* Get type-level `Ord` from the new `type-compare` compatibility library.+* Get `SOrdering` from `type-compare` under the new name `OrderingI`.+ * It's no longer exported from `Data.SNumber`; depend on `type-compare` or a+ new-enough version of `base`.+ # 0.2.0 (2021-10-24) * Downgrade the `unSNumber` field selector to be unidirectional.
snumber.cabal view
@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack name: snumber-version: 0.2.0+version: 0.3.0 synopsis: Integer singletons with flexible representation description: This provides singletons-style witnesses for type-level integers, and some limited arithmetic operations on them. Instead of working with (invisible,@@ -40,6 +40,7 @@ hs-source-dirs: src build-depends:- base >=4.12 && <4.16- , numeric-kinds ==0.1.*+ base >=4.12 && <4.17+ , numeric-kinds >=0.1 && <0.3+ , type-compare >=0.1.1 && <0.2 default-language: Haskell2010
src/Data/SNumber.hs view
@@ -12,8 +12,6 @@ -- See the License for the specific language governing permissions and -- limitations under the License. --- | Runtime witnesses of type-level integers.- {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE CPP #-}@@ -38,6 +36,8 @@ {-# LANGUAGE UndecidableInstances #-} {-# LANGUAGE ViewPatterns #-} +-- | Runtime witnesses of type-level integers.+ module Data.SNumber ( -- * SNumber SNumber(SNumber, N#, SN, unSNumber), SNumberRepr(..)@@ -53,7 +53,7 @@ , SomeSNumber(..), someSNumberVal, withSNumber -- ** Comparison- , SOrdering(..), compareSNumber, sameSNumber+ , compareSNumber, sameSNumber -- ** Arithmetic , OverflowArith(..)@@ -97,6 +97,7 @@ ) import Kinds.Integer (CmpInteger, KnownInteger(..), pattern Pos, pattern Neg) import qualified Kinds.Integer as K (Integer)+import Kinds.Ord (OrderingI(..)) import Kinds.Num (type (+), type (-), type (*)) #include "MachDeps.h"@@ -109,7 +110,8 @@ -- * @CmpInteger m n ~ 'LT@ iff @compare m n == LT@ (according to 'Ord'). -- * @CmpInteger m n ~ 'EQ@ iff @compare m n == EQ@. -- * @CmpInteger m n ~ 'GT@ iff @compare m n == GT@.--- * @toInteger n == integerVal \@n@+-- * @toInteger n == integerVal \@n@.+-- * @a@ upholds the 'Ord' laws. -- -- These are exactly the set of things we're willing to 'unsafeCoerce' proofs -- for. It is /unsafe/ to construct an 'SNumber' that violates these by any@@ -374,7 +376,7 @@ -- | Implementation of 'snumberVal'. -- -- This has an inconvenient type variable order because it derives from the- -- order they appear in the class head.+ -- order they appear in the class head; see 'snumberVal'. snumberVal_ :: SNumber a n default snumberVal_ :: (SNumberRepr a, KnownInteger n) => SNumber a n snumberVal_ = fromMaybe (error "KnownSNumber: unrepresentable") trySNumber@@ -396,21 +398,16 @@ -- TODO(awpr): Expose these functions as GEq/GOrd instances. --- | Ordering results carrying evidence of type-level ordering relations.-data SOrdering m n where- SLT :: CmpInteger m n ~ 'LT => SOrdering m n- -- | This doesn't currently prove m ~ n, but since we've forbidden SNumbers- -- of @'Neg 0@, it probably could.- SEQ :: CmpInteger m n ~ 'EQ => SOrdering m n- SGT :: CmpInteger m n ~ 'GT => SOrdering m n- -- | Compare two type-level 'Integer's using their runtime witnesses. compareSNumber- :: forall m n a. Ord a => SNumber a m -> SNumber a n -> SOrdering m n+ :: forall m n a. Ord a => SNumber a m -> SNumber a n -> OrderingI m n compareSNumber (N# x) (N# y) = case compare x y of- LT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'LT of Refl -> SLT- EQ -> case unsafeCoerce Refl :: CmpInteger m n :~: 'EQ of Refl -> SEQ- GT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'GT of Refl -> SGT+ LT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'LT of Refl -> LTI+ EQ ->+ case unsafeCoerce Refl :: CmpInteger m n :~: 'EQ of+ Refl -> case unsafeCoerce Refl :: m :~: n of+ Refl -> EQI+ GT -> case unsafeCoerce Refl :: CmpInteger m n :~: 'GT of Refl -> GTI -- | Test equality of two type-level 'Integer's using their runtime witnesses. sameSNumber :: Eq a => SNumber a m -> SNumber a n -> Maybe (m :~: n)@@ -525,6 +522,7 @@ => SNumber a m -> SNumber a n -> Maybe (SNumber a (m * n)) tryMul = unsafeMkTry overflowMul +-- | An exception for overflows in checked 'SNumber' arithmetic. data UnrepresentableSNumber = UnrepresentableSNumber String Integer Integer deriving Show
src/Data/SNumber/Internal.hs view
@@ -33,7 +33,8 @@ import Prelude hiding (Integer) -- No term-level stuff in this module anyway. import Kinds.Integer (Integer(..))-import Kinds.Num (type (-), type (<?), type (>=?), Cmp)+import Kinds.Num (type (-))+import Kinds.Ord (type (<?), type (>=?), Compare) type family ShowNum (n :: Integer) where ShowNum ('Pos n) = 'ShowType n@@ -89,7 +90,7 @@ (maxp1 :: Integer) (err :: Integer -> Constraint) (n :: Integer)-instance AssertLessThanMaxBound (Reduce (Cmp n maxp1)) n maxp1 (err n)+instance AssertLessThanMaxBound (Reduce (Compare n maxp1)) n maxp1 (err n) => IsLessThanMaxBound maxp1 err n -- | Assert that a numeric literal is greater than the (negative) min bound.@@ -103,7 +104,7 @@ (min :: Integer) (err :: Integer -> Constraint) (n :: Integer)-instance AssertAtLeastMinBound (Reduce (Cmp n min)) n min (err n)+instance AssertAtLeastMinBound (Reduce (Compare n min)) n min (err n) => IsAtLeastMinBound min err n type family ErrorIfNegZero n :: Constraint where