packages feed

natural-arithmetic 0.1.3.0 → 0.1.4.0

raw patch · 9 files changed

+208/−7 lines, 9 files

Files

CHANGELOG.md view
@@ -1,5 +1,12 @@ # Revision history for natural-arithmetic +## 0.1.4.0 -- 2023-05-31++* Add unboxed Nat type+* Add nominal role for Fin# type constructor. Technically, this is a breaking+  change, but if anyone was using coerce on a Fin#, they were already in a+  bunch of trouble. So, there is not going to be a major version bump for this.+ ## 0.1.3.0 -- 2022-05-23  * Add strict variant of descend.
natural-arithmetic.cabal view
@@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic-version: 0.1.3.0+version: 0.1.4.0 synopsis: Arithmetic of natural numbers description:   A search for terms like `arithmetic` and `natural` on hackage reveals
src/Arithmetic/Equal.hs view
@@ -13,10 +13,13 @@ import GHC.TypeNats (type (+))  symmetric :: (m :=: n) -> (n :=: m)+{-# inline symmetric #-} symmetric Eq = Eq  plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)+{-# inline plusL #-} plusL Eq = Eq  plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)+{-# inline plusR #-} plusR Eq = Eq
src/Arithmetic/Fin.hs view
@@ -4,6 +4,7 @@ {-# language GADTs #-} {-# language KindSignatures #-} {-# language MagicHash #-}+{-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeApplications #-} {-# language TypeOperators #-}@@ -22,8 +23,12 @@     -- pair the initial accumulator with the last index.   , ascend   , ascend'+  , ascendFrom'+  , ascendFrom'#   , ascendM+  , ascendM#   , ascendM_+  , ascendM_#   , descend   , descend'   , descendM@@ -36,6 +41,11 @@   , absurd     -- * Demote   , demote+    -- * Deconstruct+  , with+  , with#+    -- * Construct+  , construct#     -- * Lift and Unlift   , lift   , unlift@@ -44,7 +54,7 @@ import Prelude hiding (last)  import Arithmetic.Nat ((<?))-import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))+import Arithmetic.Types (Fin(..),Fin#,Difference(..),Nat,Nat#,type (<), type (<=), type (:=:)) import GHC.Exts (Int(I#)) import GHC.TypeNats (type (+)) @@ -169,6 +179,34 @@     Nothing -> b     Just lt -> go (Nat.succ m) (f (Fin m lt) b) +-- | Generalization of @ascend'@ that lets the caller pick the starting index:+--+-- > ascend' === ascendFrom' 0+ascendFrom' :: forall a m n.+     Nat m -- ^ Index to start at+  -> Nat n -- ^ Number of steps to take+  -> a -- ^ Initial accumulator+  -> (Fin (m + n) -> a -> a) -- ^ Update accumulator+  -> a+{-# inline ascendFrom' #-}+ascendFrom' !m0 !n !b0 f = go m0 b0+  where+  end = Nat.plus m0 n+  go :: Nat k -> a -> a+  go !m !b = case m <? end of+    Nothing -> b+    Just lt -> go (Nat.succ m) (f (Fin m lt) b)++-- | Variant of @ascendFrom'@ with unboxed arguments.+ascendFrom'# :: forall a m n.+     Nat# m -- ^ Index to start at+  -> Nat# n -- ^ Number of steps to take+  -> a -- ^ Initial accumulator+  -> (Fin# (m + n) -> a -> a) -- ^ Update accumulator+  -> a+{-# inline ascendFrom'# #-}+ascendFrom'# !m0 !n !b0 f = ascendFrom' (Nat.lift m0) (Nat.lift n) b0 (\ix -> f (unlift ix))+ -- | Strict monadic left fold over the numbers bounded by @n@ -- in ascending order. Roughly: --@@ -190,6 +228,16 @@     Nothing -> pure b     Just lt -> go (Nat.succ m) =<< f (Fin m lt) b +-- | Variant of @ascendM@ that takes an unboxed Nat and provides+-- an unboxed Fin to the callback.+ascendM# :: forall m a n. Monad m+  => Nat# n -- ^ Upper bound+  -> a -- ^ Initial accumulator+  -> (Fin# n -> a -> m a) -- ^ Update accumulator+  -> m a+{-# inline ascendM# #-}+ascendM# n !a0 f = ascendM (Nat.lift n) a0 (\ix a -> f (unlift ix) a)+ -- | Monadic traversal of the numbers bounded by @n@ -- in ascending order. --@@ -206,6 +254,15 @@     Nothing -> pure ()     Just lt -> f (Fin m lt) *> go (Nat.succ m) +-- | Variant of @ascendM_@ that takes an unboxed Nat and provides+-- an unboxed Fin to the callback.+ascendM_# :: forall m a n. Monad m+  => Nat# n -- ^ Upper bound+  -> (Fin# n -> m a) -- ^ Update accumulator+  -> m ()+{-# inline ascendM_# #-}+ascendM_# n f = ascendM_ (Nat.lift n) (\ix -> f (unlift ix))+ descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c {-# inline descendLemma #-} descendLemma !aPlusOneEqB !bLteC = id@@ -347,3 +404,17 @@ unlift :: Fin n -> Unsafe.Fin# n {-# inline unlift #-} unlift (Fin (Unsafe.Nat (I# i)) _) = Unsafe.Fin# i++-- | Consume the natural number and the proof in the Fin.+with :: Fin n -> (forall i. (i < n) -> Nat i -> a) -> a+{-# inline with #-}+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+{-# inline with# #-}+with# (Unsafe.Fin# i) f = f Unsafe.Lt (Unsafe.Nat# i)++construct# :: (i < n) -> Nat# i -> Fin# n+{-# inline construct# #-}+construct# _ (Unsafe.Nat# x) = Unsafe.Fin# x
src/Arithmetic/Lt.hs view
@@ -1,3 +1,4 @@+{-# language AllowAmbiguousTypes #-} {-# language DataKinds #-} {-# language ExplicitForAll #-} {-# language KindSignatures #-}@@ -13,6 +14,9 @@     -- * Increment   , incrementL   , incrementR+    -- * Decrement+  , decrementL+  , decrementR     -- * Weaken   , weakenL   , weakenR@@ -21,6 +25,9 @@   , transitive   , transitiveNonstrictL   , transitiveNonstrictR+    -- * Multiplication and Division+  , reciprocalA+  , reciprocalB     -- * Convert to Inequality   , toLteL   , toLteR@@ -37,72 +44,112 @@ import qualified GHC.TypeNats as GHC  toLteR :: (a < b) -> (a + 1 <= b)+{-# inline toLteR #-} toLteR Lt = Lte  toLteL :: (a < b) -> (1 + a <= b)+{-# inline toLteL #-} toLteL Lt = Lte  -- | Replace the left-hand side of a strict inequality -- with an equal number. substituteL :: (b :=: c) -> (b < a) -> (c < a)+{-# inline substituteL #-} substituteL Eq Lt = Lt  -- | Replace the right-hand side of a strict inequality -- with an equal number. substituteR :: (b :=: c) -> (a < b) -> (a < c)+{-# inline substituteR #-} substituteR Eq Lt = Lt  -- | Add a strict inequality to a nonstrict inequality. plus :: (a < b) -> (c <= d) -> (a + c < b + d)+{-# inline plus #-} plus Lt Lte = 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).   (a < b) -> (c + a < c + b)+{-# inline incrementL #-} incrementL Lt = 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).   (a < b) -> (a + c < b + c)+{-# inline incrementR #-} incrementR Lt = 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).+  (c + a < c + b) -> (a < b)+{-# inline decrementL #-}+decrementL Lt = 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).+  (a + c < b + c) -> (a < b)+{-# inline decrementR #-}+decrementR Lt = 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).   (a < b) -> (a < c + b)+{-# inline weakenL #-} weakenL Lt = 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).   (a < b) -> (a < b + c)+{-# inline weakenR #-} weakenR Lt = Lt  -- | Compose two strict inequalities using transitivity. transitive :: (a < b) -> (b < c) -> (a < c)+{-# inline transitive #-} transitive Lt Lt = 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  transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)+{-# inline transitiveNonstrictL #-} transitiveNonstrictL Lte Lt = Lt  -- | Zero is less than one. zero :: 0 < 1+{-# inline zero #-} zero = Lt  -- | Nothing is less than zero. absurd :: n < 0 -> void-absurd Lt = error "Arithmetic.Nat.absurd: n < 0"+{-# inline absurd #-}+absurd Lt = errorWithoutStackTrace "Arithmetic.Nat.absurd: n < 0"  -- | Use GHC's built-in type-level arithmetic to prove -- that one number is less than another. The type-checker -- only reduces 'CmpNat' if both arguments are constants. 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+{-# inline reciprocalA #-}+reciprocalA _ = Lt++-- | Given that @m < roundUp(n/p)@, we know that @p*m < n@.+reciprocalB :: forall (m :: GHC.Nat) (n :: GHC.Nat) (p :: GHC.Nat).+  (m < GHC.Div (n GHC.- 1) p + 1) -> (p GHC.* m) < n+{-# inline reciprocalB #-}+reciprocalB _ = Lt
src/Arithmetic/Lte.hs view
@@ -38,73 +38,87 @@ -- | Replace the left-hand side of a strict inequality -- with an equal number. substituteL :: (b :=: c) -> (b <= a) -> (c <= a)+{-# inline substituteL #-} substituteL Eq Lte = Lte  -- | Replace the right-hand side of a strict inequality -- with an equal number. substituteR :: (b :=: c) -> (a <= b) -> (a <= c)+{-# inline substituteR #-} substituteR Eq Lte = Lte  -- | Add two inequalities. plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)+{-# inline plus #-} plus Lte Lte = Lte  -- | Compose two inequalities using transitivity. transitive :: (a <= b) -> (b <= c) -> (a <= c)+{-# inline transitive #-} transitive Lte Lte = Lte  -- | Any number is less-than-or-equal-to itself. 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).   (a <= b) -> (c + a <= c + b)+{-# inline incrementL #-} incrementL Lte = 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).   (a <= b) -> (a + c <= b + c)+{-# inline incrementR #-} incrementR Lte = 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).   (a <= b) -> (a <= c + b)+{-# inline weakenL #-} weakenL Lte = 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).   (a <= b) -> (a <= b + c)+{-# inline weakenR #-} weakenR Lte = 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).   (c + a <= c + b) -> (a <= b)+{-# inline decrementL #-} decrementL Lte = 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).   (a + c <= b + c) -> (a <= b)+{-# inline decrementR #-} decrementR Lte = Lte  -- | Weaken a strict inequality to a non-strict inequality. fromStrict :: (a < b) -> (a <= b)+{-# inline fromStrict #-} fromStrict Lt = Lte  -- | Zero is less-than-or-equal-to any number. zero :: 0 <= a+{-# inline zero #-} zero = Lte  -- | Use GHC's built-in type-level arithmetic to prove -- that one number is less-than-or-equal-to another. The type-checker -- only reduces 'CmpNat' if both arguments are constants. constant :: forall a b. (IsLte (CmpNat a b) ~ 'True) => (a <= b)+{-# inline constant #-} constant = Lte  type family IsLte (o :: Ordering) :: Bool where
src/Arithmetic/Nat.hs view
@@ -5,12 +5,19 @@ {-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeOperators #-}+{-# language UnboxedTuples #-}  module Arithmetic.Nat   ( -- * Addition     plus+  , plus#     -- * Subtraction   , monus+    -- * Division+  , divide+  , divideRoundingUp+    -- * Multiplication+  , times     -- * Successor   , succ     -- * Compare@@ -27,8 +34,12 @@   , two   , three   , constant+    -- * Unboxed Constants+  , zero#     -- * Convert   , demote+  , unlift+  , lift   , with   ) where @@ -36,10 +47,13 @@  import Arithmetic.Types import Arithmetic.Unsafe ((:=:)(Eq), type (<=)(Lte))-import Arithmetic.Unsafe (Nat(Nat),type (<)(Lt))-import GHC.Exts (Proxy#,proxy#)-import GHC.TypeNats (type (+),KnownNat,natVal')+import Arithmetic.Unsafe (Nat(Nat),Nat#(Nat#),type (<)(Lt))+import GHC.Exts (Proxy#,proxy#,(+#))+import GHC.TypeNats (type (+),type (-),Div,KnownNat,natVal')+import GHC.Int (Int(I#)) +import qualified GHC.TypeNats as GHC+ -- | Infix synonym of 'testLessThan'. (<?) :: Nat a -> Nat b -> Maybe (a < b) {-# inline (<?) #-}@@ -90,6 +104,29 @@ {-# inline plus #-} plus (Nat x) (Nat y) = Nat (x + y) +-- | Variant of 'plus' for unboxed nats.+plus# :: Nat# a -> Nat# b -> Nat# (a + b)+{-# inline plus# #-}+plus# (Nat# x) (Nat# y) = Nat# (x +# y)++-- | Divide two numbers. Rounds down (towards zero)+divide :: Nat a -> Nat b -> Nat (Div a b)+{-# inline divide #-}+divide (Nat x) (Nat y) = Nat (div x y)++-- | Divide two numbers. Rounds up (away from zero)+divideRoundingUp :: Nat a -> Nat b -> Nat (Div (a - 1) b + 1)+{-# inline divideRoundingUp #-}+divideRoundingUp (Nat x) (Nat y) =+  -- Implementation note. We must use div so that when x=0,+  -- the result is (-1) and not 0. Then when we add 1, we get 0.+  Nat (1 + (div (x - 1) y))++-- | Multiply two numbers.+times :: Nat a -> Nat b -> Nat (a GHC.* b)+{-# inline times #-}+times (Nat x) (Nat y) = Nat (x * y)+ -- | The successor of a number. succ :: Nat a -> Nat (a + 1) {-# inline succ #-}@@ -129,6 +166,10 @@ {-# inline constant #-} constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n))) +-- | The number zero. Unboxed.+zero# :: (# #) -> Nat# 0+zero# _ = Nat# 0#+ -- | 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.@@ -143,3 +184,11 @@ 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++lift :: Nat# n -> Nat n+{-# inline lift #-}+lift (Nat# i) = Nat (I# i)
src/Arithmetic/Types.hs view
@@ -1,4 +1,5 @@ {-# language DataKinds #-}+{-# language MagicHash #-} {-# language ExplicitNamespaces #-} {-# language GADTs #-} {-# language KindSignatures #-}@@ -7,15 +8,17 @@  module Arithmetic.Types   ( Nat+  , Nat#   , WithNat(..)   , Difference(..)   , Fin(..)+  , Fin#   , type (<)   , type (<=)   , type (:=:)   ) where -import Arithmetic.Unsafe (Nat(getNat), type (<=))+import Arithmetic.Unsafe (Fin#,Nat#,Nat(getNat), type (<=)) import Arithmetic.Unsafe (type (<), type (:=:)) import Data.Kind (type Type) import GHC.TypeNats (type (+))
src/Arithmetic/Unsafe.hs view
@@ -12,6 +12,7 @@  module Arithmetic.Unsafe   ( Nat(..)+  , Nat#(..)   , Fin#(..)   , type (<)(Lt)   , type (<=)(Lte)@@ -43,9 +44,15 @@  deriving newtype instance Show (Nat n) +-- | Unboxed variant of Nat.+newtype Nat# :: GHC.Nat -> TYPE 'IntRep where+  Nat# :: Int# -> Nat# n+type role Nat# nominal+ -- | Finite numbers without the overhead of carrying around a proof. newtype Fin# :: GHC.Nat -> TYPE 'IntRep where   Fin# :: Int# -> Fin# n+type role Fin# nominal  -- | Proof that the first argument is strictly less than the -- second argument.