diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,15 @@ # Revision history for natural-arithmetic +## 0.2.0.0 -- 2024-01-09 + +* Change the types of `with#` and `construct#` (both in `Arithmetic.Fin`) + to use an unboxed "less than" instead of a boxed one. This is a breaking + change. +* Add patterns for the natural numbers 5, 6, 7. +* Add a lot of primitives for working with unboxed natural and inequalities. + GHC is unable to eliminate the boxed `Fin` type in a suprisingly large + number of cases, and `Fin#` helps a lot with this. + ## 0.1.4.0 -- 2023-05-31 * Add unboxed Nat type diff --git a/natural-arithmetic.cabal b/natural-arithmetic.cabal --- a/natural-arithmetic.cabal +++ b/natural-arithmetic.cabal @@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic -version: 0.1.4.0 +version: 0.2.0.0 synopsis: Arithmetic of natural numbers description: A search for terms like `arithmetic` and `natural` on hackage reveals @@ -74,7 +74,9 @@ Arithmetic.Types Arithmetic.Unsafe Arithmetic.Plus - build-depends: base>=4.14 && <5 + build-depends: + , base>=4.14 && <5 + , unlifted >=0.2.1 hs-source-dirs: src default-language: Haskell2010 ghc-options: -Wall -O2 diff --git a/src/Arithmetic/Equal.hs b/src/Arithmetic/Equal.hs --- a/src/Arithmetic/Equal.hs +++ b/src/Arithmetic/Equal.hs @@ -1,15 +1,20 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-} +{-# language MagicHash #-} {-# language TypeOperators #-} +{-# language UnboxedTuples #-} module Arithmetic.Equal ( symmetric , plusR , plusL + , plusR# + , plusL# + , lift ) where -import Arithmetic.Unsafe (type (:=:)(Eq)) +import Arithmetic.Unsafe (type (:=:)(Eq), type (:=:#)(Eq#)) import GHC.TypeNats (type (+)) symmetric :: (m :=: n) -> (n :=: m) @@ -23,3 +28,15 @@ plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c) {-# inline plusR #-} plusR Eq = Eq + +plusL# :: forall c m n. (m :=:# n) -> (c + m :=:# c + n) +{-# inline plusL# #-} +plusL# _ = Eq# (# #) + +plusR# :: forall c m n. (m :=:# n) -> (m + c :=:# n + c) +{-# inline plusR# #-} +plusR# _ = Eq# (# #) + +lift :: (m :=:# n) -> (m :=: n) +{-# inline lift #-} +lift _ = Eq diff --git a/src/Arithmetic/Fin.hs b/src/Arithmetic/Fin.hs --- a/src/Arithmetic/Fin.hs +++ b/src/Arithmetic/Fin.hs @@ -4,17 +4,22 @@ {-# language GADTs #-} {-# language KindSignatures #-} {-# language MagicHash #-} +{-# language PatternSynonyms #-} {-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeApplications #-} {-# language TypeOperators #-} +{-# language UnboxedTuples #-} module Arithmetic.Fin ( -- * Modification incrementL , incrementR + , incrementR# , weaken , weakenL , weakenR + , succ + , succ# -- * Traverse -- | These use the terms @ascend@ and @descend@ rather than the -- more popular @l@ (left) and @r@ (right) that pervade the Haskell @@ -30,6 +35,7 @@ , ascendM_ , ascendM_# , descend + , descend# , descend' , descendM , descendM_ @@ -41,21 +47,26 @@ , absurd -- * Demote , demote + , demote# -- * Deconstruct , with , with# -- * Construct , construct# + , remInt# + , remWord# -- * Lift and Unlift , lift , unlift ) where -import Prelude hiding (last) +import Prelude hiding (last,succ) import Arithmetic.Nat (( Fin# n -> Fin# (n + m) +{-# inline incrementR# #-} +incrementR# (Nat# n) (Fin# i) = Fin# (n +# i) + -- | Raise the index by @m@ and weaken the bound by @m@, adding -- @m@ to the left-hand side of @n@. incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n) @@ -122,6 +138,14 @@ Nothing -> b0 Just lt -> f (Fin m lt) (go (Nat.succ m)) +descend# :: forall a n. + Nat# n -- ^ Upper bound + -> a -- ^ Initial accumulator + -> (Fin# n -> a -> a) -- ^ Update accumulator + -> a +{-# inline descend# #-} +descend# !n b0 f = descend (Nat.lift n) b0 (\ix a -> f (unlift ix) a) + -- | Fold over the numbers bounded by @n@ in descending -- order. This is strict in the accumulator. For convenince, -- this differs from @foldr'@ in the order of the parameters. @@ -397,6 +421,10 @@ {-# inline demote #-} demote (Fin i _) = Nat.demote i +demote# :: Fin# n -> Int# +{-# inline demote# #-} +demote# (Fin# i) = i + lift :: Unsafe.Fin# n -> Fin n {-# inline lift #-} lift (Unsafe.Fin# i) = Fin (Unsafe.Nat (I# i)) Unsafe.Lt @@ -411,10 +439,43 @@ with (Fin i lt) f = f lt i -- | Variant of 'with' for unboxed argument and result types. -with# :: Fin# n -> (forall i. (i < n) -> Nat# i -> a) -> a +with# :: Fin# n -> (forall i. (i <# n) -> Nat# i -> a) -> a {-# inline with# #-} -with# (Unsafe.Fin# i) f = f Unsafe.Lt (Unsafe.Nat# i) +with# (Unsafe.Fin# i) f = f (Unsafe.Lt# (# #)) (Unsafe.Nat# i) -construct# :: (i < n) -> Nat# i -> Fin# n +construct# :: (i <# n) -> Nat# i -> Fin# n {-# inline construct# #-} construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x + +-- | Return the successor of the Fin or return nothing if the +-- argument is the greatest inhabitant. +succ :: Nat n -> Fin n -> Maybe (Fin n) +{-# inline succ #-} +succ n (Fin ix _) = case ix' Nothing + Just lt -> Just (Fin ix' lt) + where + ix' = Nat.succ ix + +-- | Variant of 'succ' for unlifted finite numbers. +succ# :: Nat# n -> Fin# n -> MaybeFin# n +{-# inline succ# #-} +succ# (Nat# n) (Fin# ix) = case ix' Exts.<# n of + 0# -> MaybeFinNothing# + _ -> MaybeFinJust# (Fin# ix') + where + !ix' = ix +# 1# + +-- | This crashes if @n = 0@. Divides @i@ by @n@ and takes +-- the remainder. +remInt# :: Int# -> Nat# n -> Fin# n +remInt# i (Nat# n) = case n of + 0# -> errorWithoutStackTrace "Arithmetic.Fin.remInt#: cannot divide by zero" + _ -> Fin# (Exts.remInt# i n) + +-- | This crashes if @n = 0@. Divides @i@ by @n@ and takes +-- the remainder. +remWord# :: Word# -> Nat# n -> Fin# n +remWord# w (Nat# n) = case n of + 0# -> errorWithoutStackTrace "Arithmetic.Fin.remWord#: cannot divide by zero" + _ -> Fin# (Exts.word2Int# (Exts.remWord# w (Exts.int2Word# n))) diff --git a/src/Arithmetic/Lt.hs b/src/Arithmetic/Lt.hs --- a/src/Arithmetic/Lt.hs +++ b/src/Arithmetic/Lt.hs @@ -2,29 +2,44 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-} +{-# language MagicHash #-} +{-# language UnboxedTuples #-} {-# language TypeFamilies #-} {-# language TypeOperators #-} module Arithmetic.Lt ( -- * Special Inequalities zero + , zero# -- * Substitution , substituteL , substituteR -- * Increment , incrementL + , incrementL# , incrementR + , incrementR# -- * Decrement , decrementL + , decrementL# , decrementR + , decrementR# -- * Weaken , weakenL + , weakenL# , weakenR + , weakenR# + , weakenLhsL# + , weakenLhsR# -- * Composition , plus + , plus# , transitive + , transitive# , transitiveNonstrictL + , transitiveNonstrictL# , transitiveNonstrictR + , transitiveNonstrictR# -- * Multiplication and Division , reciprocalA , reciprocalB @@ -35,10 +50,15 @@ , absurd -- * Integration with GHC solver , constant + , constant# + -- * Lift and Unlift + , lift + , unlift ) where import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) import Arithmetic.Unsafe (type (<=)(Lte)) +import Arithmetic.Unsafe (type (<#)(Lt#),type (<=#)) import GHC.TypeNats (CmpNat,type (+)) import qualified GHC.TypeNats as GHC @@ -68,6 +88,10 @@ {-# inline plus #-} plus Lt Lte = Lt +plus# :: (a <# b) -> (c <=# d) -> (a + c <# b + d) +{-# inline plus# #-} +plus# _ _ = Lt# (# #) + -- | Add a constant to the left-hand side of both sides of -- the strict inequality. incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -75,6 +99,11 @@ {-# inline incrementL #-} incrementL Lt = Lt +incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> (c + a <# c + b) +{-# inline incrementL# #-} +incrementL# _ = Lt# (# #) + -- | Add a constant to the right-hand side of both sides of -- the strict inequality. incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -82,6 +111,11 @@ {-# inline incrementR #-} incrementR Lt = Lt +incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> (a + c <# b + c) +{-# inline incrementR# #-} +incrementR# _ = Lt# (# #) + -- | Subtract a constant from the left-hand side of both sides of -- the inequality. This is the opposite of 'incrementL'. decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -89,6 +123,11 @@ {-# inline decrementL #-} decrementL Lt = Lt +decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + ((c + a) <# (c + b)) -> (a <# b) +{-# inline decrementL# #-} +decrementL# _ = Lt# (# #) + -- | Subtract a constant from the right-hand side of both sides of -- the inequality. This is the opposite of 'incrementR'. decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -96,6 +135,11 @@ {-# inline decrementR #-} decrementR Lt = Lt +decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <# b + c) -> (a <# b) +{-# inline decrementR# #-} +decrementR# _ = Lt# (# #) + -- | Add a constant to the left-hand side of the right-hand side of -- the strict inequality. weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -103,6 +147,21 @@ {-# inline weakenL #-} weakenL Lt = Lt +weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> (a <# c + b) +{-# inline weakenL# #-} +weakenL# _ = Lt# (# #) + +weakenLhsL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a <# b) -> (a <# b) +{-# inline weakenLhsL# #-} +weakenLhsL# _ = Lt# (# #) + +weakenLhsR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <# b) -> (a <# b) +{-# inline weakenLhsR# #-} +weakenLhsR# _ = Lt# (# #) + -- | Add a constant to the right-hand side of the right-hand side of -- the strict inequality. weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -110,26 +169,47 @@ {-# inline weakenR #-} weakenR Lt = Lt +weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <# b) -> (a <# b + c) +{-# inline weakenR# #-} +weakenR# _ = Lt# (# #) + -- | Compose two strict inequalities using transitivity. transitive :: (a < b) -> (b < c) -> (a < c) {-# inline transitive #-} transitive Lt Lt = Lt +transitive# :: (a <# b) -> (b <# c) -> (a <# c) +{-# inline transitive# #-} +transitive# _ _ = Lt# (# #) + -- | Compose a strict inequality (the first argument) with a nonstrict -- inequality (the second argument). transitiveNonstrictR :: (a < b) -> (b <= c) -> (a < c) {-# inline transitiveNonstrictR #-} transitiveNonstrictR Lt Lte = Lt +transitiveNonstrictR# :: (a <# b) -> (b <=# c) -> (a <# c) +{-# inline transitiveNonstrictR# #-} +transitiveNonstrictR# _ _ = Lt# (# #) + transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c) {-# inline transitiveNonstrictL #-} transitiveNonstrictL Lte Lt = Lt +transitiveNonstrictL# :: (a <=# b) -> (b <# c) -> (a <# c) +{-# inline transitiveNonstrictL# #-} +transitiveNonstrictL# _ _ = Lt# (# #) + -- | Zero is less than one. zero :: 0 < 1 {-# inline zero #-} zero = Lt +zero# :: (# #) -> 0 <# 1 +{-# inline zero# #-} +zero# _ = Lt# (# #) + -- | Nothing is less than zero. absurd :: n < 0 -> void {-# inline absurd #-} @@ -142,6 +222,10 @@ {-# inline constant #-} constant = Lt +constant# :: forall a b. (CmpNat a b ~ 'LT) => (# #) -> (a <# b) +{-# inline constant# #-} +constant# _ = Lt# (# #) + -- | Given that @m < n/p@, we know that @p*m < n@. reciprocalA :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat). (m < GHC.Div n p) -> (p GHC.* m) < n @@ -153,3 +237,9 @@ (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n {-# inline reciprocalB #-} reciprocalB _ = Lt + +unlift :: (a < b) -> (a <# b) +unlift _ = Lt# (# #) + +lift :: (a <# b) -> (a < b) +lift _ = Lt diff --git a/src/Arithmetic/Lte.hs b/src/Arithmetic/Lte.hs --- a/src/Arithmetic/Lte.hs +++ b/src/Arithmetic/Lte.hs @@ -1,36 +1,54 @@ {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-} +{-# language MagicHash #-} {-# language TypeFamilies #-} {-# language TypeOperators #-} +{-# language UnboxedTuples #-} module Arithmetic.Lte ( -- * Special Inequalities zero , reflexive + , reflexive# -- * Substitution , substituteL , substituteR -- * Increment , incrementL + , incrementL# , incrementR + , incrementR# -- * Decrement , decrementL + , decrementL# , decrementR + , decrementR# -- * Weaken , weakenL + , weakenL# , weakenR + , weakenR# -- * Composition , transitive + , transitive# , plus + , plus# -- * Convert Strict Inequality , fromStrict + , fromStrict# + , fromStrictSucc + , fromStrictSucc# -- * Integration with GHC solver , constant + -- * Lift and Unlift + , lift + , unlift ) where import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq)) import Arithmetic.Unsafe (type (<=)(Lte)) +import Arithmetic.Unsafe (type (<=#)(Lte#),type (<#)) import GHC.TypeNats (CmpNat,type (+)) import qualified GHC.TypeNats as GHC @@ -52,16 +70,28 @@ {-# inline plus #-} plus Lte Lte = Lte +plus# :: (a <=# b) -> (c <=# d) -> (a + c <=# b + d) +{-# inline plus# #-} +plus# _ _ = Lte# (# #) + -- | Compose two inequalities using transitivity. transitive :: (a <= b) -> (b <= c) -> (a <= c) {-# inline transitive #-} transitive Lte Lte = Lte +transitive# :: (a <=# b) -> (b <=# c) -> (a <=# c) +{-# inline transitive# #-} +transitive# _ _ = Lte# (# #) + -- | Any number is less-than-or-equal-to itself. reflexive :: a <= a {-# inline reflexive #-} reflexive = Lte +reflexive# :: (# #) -> a <=# a +{-# inline reflexive# #-} +reflexive# _ = Lte# (# #) + -- | Add a constant to the left-hand side of both sides of -- the inequality. incrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -69,6 +99,11 @@ {-# inline incrementL #-} incrementL Lte = Lte +incrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> (c + a <=# c + b) +{-# inline incrementL# #-} +incrementL# _ = Lte# (# #) + -- | Add a constant to the right-hand side of both sides of -- the inequality. incrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -76,6 +111,11 @@ {-# inline incrementR #-} incrementR Lte = Lte +incrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> (a + c <=# b + c) +{-# inline incrementR# #-} +incrementR# _ = Lte# (# #) + -- | Add a constant to the left-hand side of the right-hand side of -- the inequality. weakenL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -83,6 +123,11 @@ {-# inline weakenL #-} weakenL Lte = Lte +weakenL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> (a <=# c + b) +{-# inline weakenL# #-} +weakenL# _ = Lte# (# #) + -- | Add a constant to the right-hand side of the right-hand side of -- the inequality. weakenR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -90,6 +135,11 @@ {-# inline weakenR #-} weakenR Lte = Lte +weakenR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a <=# b) -> (a <=# b + c) +{-# inline weakenR# #-} +weakenR# _ = Lte# (# #) + -- | Subtract a constant from the left-hand side of both sides of -- the inequality. This is the opposite of 'incrementL'. decrementL :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -97,6 +147,11 @@ {-# inline decrementL #-} decrementL Lte = Lte +decrementL# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (c + a <=# c + b) -> (a <=# b) +{-# inline decrementL# #-} +decrementL# _ = Lte# (# #) + -- | Subtract a constant from the right-hand side of both sides of -- the inequality. This is the opposite of 'incrementR'. decrementR :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). @@ -104,11 +159,30 @@ {-# inline decrementR #-} decrementR Lte = Lte +decrementR# :: forall (c :: GHC.Nat) (a :: GHC.Nat) (b :: GHC.Nat). + (a + c <=# b + c) -> (a <=# b) +{-# inline decrementR# #-} +decrementR# _ = Lte# (# #) + -- | Weaken a strict inequality to a non-strict inequality. fromStrict :: (a < b) -> (a <= b) {-# inline fromStrict #-} fromStrict Lt = Lte +fromStrict# :: (a <# b) -> (a <=# b) +{-# inline fromStrict# #-} +fromStrict# _ = Lte# (# #) + +-- | Weaken a strict inequality to a non-strict inequality, incrementing +-- the right-hand argument by one. +fromStrictSucc :: (a < b) -> (a + 1 <= b) +{-# inline fromStrictSucc #-} +fromStrictSucc Lt = Lte + +fromStrictSucc# :: (a <# b) -> (a + 1 <=# b) +{-# inline fromStrictSucc# #-} +fromStrictSucc# _ = Lte# (# #) + -- | Zero is less-than-or-equal-to any number. zero :: 0 <= a {-# inline zero #-} @@ -125,3 +199,9 @@ IsLte 'GT = 'False IsLte 'LT = 'True IsLte 'EQ = 'True + +unlift :: (a <= b) -> (a <=# b) +unlift _ = Lte# (# #) + +lift :: (a <=# b) -> (a <= b) +lift _ = Lte diff --git a/src/Arithmetic/Nat.hs b/src/Arithmetic/Nat.hs --- a/src/Arithmetic/Nat.hs +++ b/src/Arithmetic/Nat.hs @@ -2,10 +2,12 @@ {-# language ExplicitForAll #-} {-# language KindSignatures #-} {-# language MagicHash #-} +{-# language PatternSynonyms #-} {-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeOperators #-} {-# language UnboxedTuples #-} +{-# language UnboxedSums #-} module Arithmetic.Nat ( -- * Addition @@ -20,13 +22,18 @@ , times -- * Successor , succ + , succ# -- * Compare , testEqual + , testEqual# , testLessThan + , testLessThan# , testLessThanEqual , testZero + , testZero# , (=?) , ( Nat# b -> MaybeVoid# (a <# b) +{-# inline ( Nat b -> Maybe (a < b) @@ -77,6 +113,12 @@ then Just Lt else Nothing +testLessThan# :: Nat# a -> Nat# b -> MaybeVoid# (a <# b) +{-# inline testLessThan# #-} +testLessThan# (Nat# x) (Nat# y) = case x <# y of + 0# -> NothingVoid# + _ -> JustVoid# (Lt# (# #)) + -- | Is the first argument less-than-or-equal-to the second -- argument? testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b) @@ -92,6 +134,12 @@ then Just Eq else Nothing +testEqual# :: Nat# a -> Nat# b -> MaybeVoid# (a :=:# b) +{-# inline testEqual# #-} +testEqual# (Nat# x) (Nat# y) = case x ==# y of + 0# -> NothingVoid# + _ -> JustVoid# (Eq# (# #)) + -- | Is zero equal to this number or less than it? testZero :: Nat a -> Either (0 :=: a) (0 < a) {-# inline testZero #-} @@ -99,6 +147,11 @@ 0 -> Left Eq _ -> Right Lt +testZero# :: Nat# a -> EitherVoid# (0 :=:# a) (0 <# a) +testZero# (Nat# x) = case x of + 0# -> LeftVoid# (Eq# (# #)) + _ -> RightVoid# (Lt# (# #)) + -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b) {-# inline plus #-} @@ -132,6 +185,11 @@ {-# inline succ #-} succ n = plus n one +-- | Unlifted variant of 'succ'. +succ# :: Nat# a -> Nat# (a + 1) +{-# inline succ# #-} +succ# n = plus# n (one# (# #)) + -- | Subtract the second argument from the first argument. monus :: Nat a -> Nat b -> Maybe (Difference a b) {-# inline monus #-} @@ -166,10 +224,19 @@ {-# inline constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n))) +constant# :: forall n. KnownNat n => (# #) -> Nat# n +{-# inline constant# #-} +constant# _ = case fromIntegral (natVal' (proxy# :: Proxy# n)) of + I# i -> Nat# i + -- | The number zero. Unboxed. zero# :: (# #) -> Nat# 0 zero# _ = Nat# 0# +-- | The number one. Unboxed. +one# :: (# #) -> Nat# 1 +one# _ = Nat# 1# + -- | Extract the 'Int' from a 'Nat'. This is intended to be used -- at a boundary where a safe interface meets the unsafe primitives -- on top of which it is built. @@ -177,6 +244,10 @@ {-# inline demote #-} demote (Nat n) = n +demote# :: Nat# n -> Int# +{-# inline demote# #-} +demote# (Nat# n) = n + -- | Run a computation on a witness of a type-level number. The -- argument 'Int' must be greater than or equal to zero. This is -- not checked. Failure to upload this invariant will lead to a @@ -185,6 +256,10 @@ {-# inline with #-} with i f = f (Nat i) +with# :: Int# -> (forall n. Nat# n -> a) -> a +{-# inline with# #-} +with# i f = f (Nat# i) + unlift :: Nat n -> Nat# n {-# inline unlift #-} unlift (Nat (I# i)) = Nat# i @@ -192,3 +267,57 @@ lift :: Nat# n -> Nat n {-# inline lift #-} lift (Nat# i) = Nat (I# i) + +pattern N0# :: Nat# 0 +pattern N0# = Nat# 0# + +pattern N1# :: Nat# 1 +pattern N1# = Nat# 1# + +pattern N2# :: Nat# 2 +pattern N2# = Nat# 2# + +pattern N3# :: Nat# 3 +pattern N3# = Nat# 3# + +pattern N4# :: Nat# 4 +pattern N4# = Nat# 4# + +pattern N5# :: Nat# 5 +pattern N5# = Nat# 5# + +pattern N6# :: Nat# 6 +pattern N6# = Nat# 6# + +pattern N7# :: Nat# 7 +pattern N7# = Nat# 7# + +pattern N8# :: Nat# 8 +pattern N8# = Nat# 8# + +pattern N16# :: Nat# 16 +pattern N16# = Nat# 16# + +pattern N32# :: Nat# 32 +pattern N32# = Nat# 32# + +pattern N64# :: Nat# 64 +pattern N64# = Nat# 64# + +pattern N128# :: Nat# 128 +pattern N128# = Nat# 128# + +pattern N256# :: Nat# 256 +pattern N256# = Nat# 256# + +pattern N512# :: Nat# 512 +pattern N512# = Nat# 512# + +pattern N1024# :: Nat# 1024 +pattern N1024# = Nat# 1024# + +pattern N2048# :: Nat# 2048 +pattern N2048# = Nat# 2048# + +pattern N4096# :: Nat# 4096 +pattern N4096# = Nat# 4096# diff --git a/src/Arithmetic/Types.hs b/src/Arithmetic/Types.hs --- a/src/Arithmetic/Types.hs +++ b/src/Arithmetic/Types.hs @@ -1,10 +1,14 @@ {-# language DataKinds #-} {-# language MagicHash #-} {-# language ExplicitNamespaces #-} +{-# language PatternSynonyms #-} +{-# language ViewPatterns #-} {-# language GADTs #-} {-# language KindSignatures #-} {-# language RankNTypes #-} {-# language TypeOperators #-} +{-# language UnboxedTuples #-} +{-# language UnboxedSums #-} module Arithmetic.Types ( Nat @@ -13,13 +17,25 @@ , Difference(..) , Fin(..) , Fin# + , Fin32# + -- * Maybe Fin + , MaybeFin# + , pattern MaybeFinJust# + , pattern MaybeFinNothing# + -- * Infix Operators , type (<) , type (<=) + , type (<#) + , type (<=#) , type (:=:) + , type (:=:#) ) where -import Arithmetic.Unsafe (Fin#,Nat#,Nat(getNat), type (<=)) +import Arithmetic.Unsafe (Fin#(Fin#),Nat#,Nat(getNat), type (<=)) +import Arithmetic.Unsafe (Fin32#) +import Arithmetic.Unsafe (MaybeFin#(..)) import Arithmetic.Unsafe (type (<), type (:=:)) +import Arithmetic.Unsafe (type (<#), type (<=#), (:=:#)) import Data.Kind (type Type) import GHC.TypeNats (type (+)) @@ -54,3 +70,16 @@ instance Ord (Fin n) where Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y) + +pattern MaybeFinJust# :: Fin# n -> MaybeFin# n +pattern MaybeFinJust# f <- (maybeFinToFin# -> (# | f #)) where + MaybeFinJust# (Fin# i) = MaybeFin# i + +pattern MaybeFinNothing# :: MaybeFin# n +pattern MaybeFinNothing# = MaybeFin# (-1#) + +maybeFinToFin# :: MaybeFin# n -> (# (# #) | Fin# n #) +{-# inline maybeFinToFin# #-} +maybeFinToFin# (MaybeFin# i) = case i of + -1# -> (# (# #) | #) + _ -> (# | Fin# i #) diff --git a/src/Arithmetic/Unsafe.hs b/src/Arithmetic/Unsafe.hs --- a/src/Arithmetic/Unsafe.hs +++ b/src/Arithmetic/Unsafe.hs @@ -8,22 +8,28 @@ {-# language RoleAnnotations #-} {-# language StandaloneDeriving #-} {-# language TypeOperators #-} +{-# language UnboxedTuples #-} {-# language UnliftedNewtypes #-} module Arithmetic.Unsafe ( Nat(..) , Nat#(..) , Fin#(..) + , MaybeFin#(..) + , Fin32#(..) + , type (<#)(Lt#) + , type (<=#)(Lte#) , type (<)(Lt) , type (<=)(Lte) , type (:=:)(Eq) + , type (:=:#)(Eq#) ) where import Prelude hiding ((>=),(<=)) import Control.Category (Category) import Data.Kind (Type) -import GHC.Exts (Int#,TYPE,RuntimeRep(IntRep)) +import GHC.Exts (Int#,Int32#,TYPE,RuntimeRep(IntRep,Int32Rep,TupleRep)) import qualified Control.Category import qualified GHC.TypeNats as GHC @@ -36,7 +42,10 @@ infix 4 < infix 4 <= +infix 4 <# +infix 4 <=# infix 4 :=: +infix 4 :=:# -- | A value-level representation of a natural number @n@. newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int } @@ -54,19 +63,39 @@ Fin# :: Int# -> Fin# n type role Fin# nominal +-- | Either a @Fin#@ or Nothing. Internally, this uses negative +-- one to mean Nothing. +newtype MaybeFin# :: GHC.Nat -> TYPE 'IntRep where + MaybeFin# :: Int# -> MaybeFin# n +type role MaybeFin# nominal + +-- | Variant of 'Fin#' that only allows 32-bit integers. +newtype Fin32# :: GHC.Nat -> TYPE 'Int32Rep where + Fin32# :: Int32# -> Fin32# n +type role Fin32# nominal + -- | Proof that the first argument is strictly less than the -- second argument. data (<) :: GHC.Nat -> GHC.Nat -> Type where Lt :: a < b +newtype (<#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where + Lt# :: (# #) -> a <# b + -- | Proof that the first argument is less than or equal to the -- second argument. data (<=) :: GHC.Nat -> GHC.Nat -> Type where Lte :: a <= b +newtype (<=#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where + Lte# :: (# #) -> a <=# b + -- | Proof that the first argument is equal to the second argument. data (:=:) :: GHC.Nat -> GHC.Nat -> Type where Eq :: a :=: b + +newtype (:=:#) :: GHC.Nat -> GHC.Nat -> TYPE ('TupleRep '[]) where + Eq# :: (# #) -> a :=:# b instance Category (<=) where id = Lte