numeric-kinds 0.1.0.0 → 0.2.0

raw patch · 4 files changed

+28/−109 lines, 4 filesdep +type-comparePVP ok

version bump matches the API change (PVP)

Dependencies added: type-compare

API changes (from Hackage documentation)

Files

• CHANGELOG.md +5/−1
• numeric-kinds.cabal +5/−8
• src/Kinds/Integer.hs +7/−19
• src/Kinds/Num.hs +11/−81

@@ -1,3 +1,7 @@-# 0.1.0.0+# 0.2.0 (2021-11-05)++* Remove `Cmp` in favor of the new `type-compare` compatibility layer.++# 0.1.0.0 (2021-09-08)  Initial version.

@@ -1,14 +1,12 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.33.0.+-- This file has been generated from package.yaml by hpack version 0.34.4. -- -- see: https://github.com/sol/hpack------ hash: 05ac8c3fea5a45f8da84a8ec3977066bf0902c70969070e7baab2643ef9c665b  name:           numeric-kinds-version:        0.1.0.0-synopsis:       Type-level numeric types, classes, and instances.+version:        0.2.0+synopsis:       Type-level numeric types and classes description:    This provides numeric types meant for use at the type level with -XDataKinds,                 along with type families that act like type-level typeclasses providing                 various operations.@@ -38,10 +36,9 @@   exposed-modules:     Kinds.Integer     Kinds.Num-  other-modules:-    Paths_numeric_kinds   hs-source-dirs:     src   build-depends:-    base >=4.12 && <4.16+    base >=4.12 && <4.17,+    type-compare ==0.1.*   default-language: Haskell2010

@@ -52,9 +52,6 @@            -- * Axioms          , plusMinusInverseL, plusMinusInverseR          , mulCommutes--           -- * Utility-         , CaseOrdering          ) where  import Prelude hiding (Integer)@@ -65,7 +62,8 @@ import GHC.TypeNats (KnownNat, Nat, natVal') import Unsafe.Coerce (unsafeCoerce) -import Kinds.Num (type (+), type (-), type (*), Cmp, FromNat, ToInteger)+import Kinds.Num (type (+), type (-), type (*), FromNat, ToInteger)+import Kinds.Ord (Compare, OrdCond)  -- | Type-level signed numbers data Integer = Pos Nat | Neg Nat@@ -84,7 +82,7 @@           then error "illegal KnownInteger (-0)"           else negate $ toInteger x -type instance Cmp {- k=Integer -} x y = CmpInteger x y+type instance Compare {- k=Integer -} x y = CmpInteger x y type instance FromNat {- k=Integer -} n = 'Pos n  type instance ToInteger {- k=Integer -} n = n@@ -97,27 +95,17 @@  -- | Comparison of type-level integers. type family CmpInteger m n where-  CmpInteger ('Pos m) ('Pos n) = Cmp m n+  CmpInteger ('Pos m) ('Pos n) = Compare m n   CmpInteger ('Pos 0) ('Neg 0) = 'EQ   CmpInteger ('Pos m) ('Neg n) = 'GT   CmpInteger ('Neg 0) ('Pos 0) = 'EQ   CmpInteger ('Neg m) ('Pos n) = 'LT-  CmpInteger ('Neg m) ('Neg n) = Cmp n m -- Note: reversed---- | Type-level eliminator for 'Ordering'.------ @CaseOrdering o lt eq gt@ selects from among @lt@, @eq@, and @gt@ according--- to @o@.  This is primarily exported so Haddock doesn't complain about being--- unable to link it when it's mentioned in type instance clauses.-type family CaseOrdering (o :: Ordering) (lt :: k) (eq :: k) (gt :: k) :: k where-  CaseOrdering 'LT lt eq gt = lt-  CaseOrdering 'EQ lt eq gt = eq-  CaseOrdering 'GT lt eq gt = gt+  CmpInteger ('Neg m) ('Neg n) = Compare n m -- Note: reversed  -- | Given two 'Nat's @m@ and @n@, computes @m - n@ as an 'Integer'. type family (m :: Nat) -# (n :: Nat) where   -- Redundant cases solely to make sure we get stuck reducing '-#' rather-  -- than reducing @CaseOrdering (Cmp m n) tons of junk@ when the magnitude is+  -- than reducing @OrdCond (Compare m n) tons of junk@ when the magnitude is   -- a type variable.  This is similar to adding a bang pattern or case   -- statement to a term-level function to make it strict in its arguments; but   -- we don't have case statements or bang patterns in type families, so we add@@ -125,7 +113,7 @@   n -# 0 = 'Pos n  -- Order matters: 0 -# 0 should be 'Pos 0   0 -# n = 'Neg n -  m -# n = CaseOrdering (Cmp m n)+  m -# n = OrdCond (Compare m n)     ('Neg (n - m))     ('Pos 0)     ('Pos (m - n))

@@ -12,16 +12,17 @@ -- See the License for the specific language governing permissions and -- limitations under the License. --- | Type-level 'Ord' and 'Num'.+-- | Type-level equivalent of a subset of 'Num'. -- -- This provides "kindclasses" (actually open type families) with functionality--- analogous to that provided by the typeclasses 'Ord' and 'Num'.  Since--- type-level typeclasses don't exist, instead we translate each would-be--- method to its own open type family; then "instances" are implemented by--- providing clauses for each type family "method".  Unfortunately this means--- we can't group methods into classes that must be implemented all-or-none,--- but in practice this seems to be okay.+-- analogous to that provided by the 'Num' typeclass.  Since type-level+-- typeclasses don't exist, instead we translate each would-be method to its+-- own open type family; then "instances" are implemented by providing clauses+-- for each type family "method".  Unfortunately this means we can't group+-- methods into classes that must be implemented all-or-none, but in practice+-- this seems to be okay. +{-# LANGUAGE CPP #-} {-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-} {-# LANGUAGE NoStarIsType #-}@@ -30,40 +31,20 @@ {-# LANGUAGE TypeOperators #-}  module Kinds.Num-         ( -- * Comparisons-           Cmp-         , type (<?), type (<=?), type (==?), type (/=?), type (>=?), type (>?)--           -- ** Inequality Constraints-         , type (<), type (<=), type (==), type (/=), type (>=), type (>)--           -- * Conversions-         , FromNat, ToInteger+         ( -- * Conversions+           FromNat, ToInteger             -- * Arithmetic          , type (+), type (-), type (*)--           -- * Utility-         , Proven, IsLT, IsLE, IsGT, IsGE, IsEQ, IsNE          ) where  import Prelude hiding (Integer) -import GHC.TypeNats (CmpNat, Nat)+import GHC.TypeNats (Nat) import qualified GHC.TypeNats as N (type (+), type (-), type (*))  import {-# source #-}  Kinds.Integer (Integer(..)) --- | Type-level Ord "kindclass".------ Note this has an invisible dependent @k@ parameter that makes the--- textually-identical instances for different kinds actually different.  Neat!-type family Cmp (x :: k) (y :: k) :: Ordering---- That is, this is @Cmp {k=Nat} x y@, which is distinct from--- @Cmp {k=Integer} x y@, even though both of them are written as @Cmp x y@.-type instance Cmp {- k=Nat -} x y = CmpNat x y- -- | Type-level numeric conversion from 'Nat'.  Like 'fromInteger' in 'Num'. type family FromNat (n :: Nat) :: k @@ -88,54 +69,3 @@ type family (x :: k) * (y :: k) :: k  type instance x * y = (N.*) x y--infix 4 <?, >?, <=?, >=?, ==?, /=?--type x <?  y = IsLT (Cmp x y)-type x >?  y = IsGT (Cmp x y)-type x <=? y = IsLE (Cmp x y)-type x >=? y = IsGE (Cmp x y)-type x ==? y = IsEQ (Cmp x y)-type x /=? y = IsNE (Cmp x y)---- | Turns a type-level 'Bool' into a 'Data.Kind.Constraint' that it's 'True'.-type Proven b = b ~ 'True--infix 4 <, >, <=, >=, ==, /=--type x <  y = Cmp x y ~ 'LT-type x >  y = Cmp x y ~ 'GT-type x == y = Cmp x y ~ 'EQ-type x <= y = Proven (x <=? y)-type x >= y = Proven (x >=? y)-type x /= y = Proven (x /=? y)---- | Test whether an 'Ordering' is 'LT'.-type family IsLT o where-  IsLT 'LT = 'True-  IsLT o   = 'False---- | Test whether an 'Ordering' is 'LT' or 'EQ'.-type family IsLE o where-  IsLE 'GT = 'False-  IsLE o   = 'True---- | Test whether an 'Ordering' is 'GT'.-type family IsGT o where-  IsGT 'GT = 'True-  IsGT o   = 'False---- | Test whether an 'Ordering' is 'GT' or 'EQ'.-type family IsGE o where-  IsGE 'LT = 'False-  IsGE o   = 'True---- | Test whether an 'Ordering' is 'EQ'.-type family IsEQ o where-  IsEQ 'EQ = 'True-  IsEQ o   = 'False---- | Test whether an 'Ordering' is 'LT' or 'GT'.-type family IsNE o where-  IsNE 'EQ = 'False-  IsNE o   = 'True