natural-arithmetic 0.1.0.0 → 0.1.1.0

raw patch · 7 files changed

+212/−37 lines, 7 filesPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

API changes (from Hackage documentation)

Files

• natural-arithmetic.cabal +1/−1
• src/Arithmetic/Fin.hs +162/−31
• src/Arithmetic/Lt.hs +11/−2
• src/Arithmetic/Lte.hs +2/−2
• src/Arithmetic/Nat.hs +27/−1
• src/Arithmetic/Types.hs +4/−0
• src/Arithmetic/Unsafe.hs +5/−0

@@ -1,6 +1,6 @@ cabal-version: 2.2 name: natural-arithmetic-version: 0.1.0.0+version: 0.1.1.0 synopsis: Arithmetic of natural numbers description:   A search for terms like `arithmetic` and `natural` on hackage reveals

@@ -10,15 +10,26 @@   ( -- * Modification     incrementL   , incrementR+  , weaken   , weakenL   , weakenR     -- * Traverse+    -- | These use the terms @ascend@ and @descend@ rather than the+    -- more popular @l@ (left) and @r@ (right) that pervade the Haskell+    -- ecosystem. The general rule is that ascending functions pair+    -- the initial accumulator with zero with descending functions+    -- pair the initial accumulator with the last index.   , ascend+  , ascend'   , ascendM   , ascendM_+  , descend+  , descendM+  , descendM_   , ascending   , descending   , ascendingSlice+  , descendingSlice     -- * Absurdities   , absurd     -- * Demote@@ -33,6 +44,7 @@  import qualified Arithmetic.Lt as Lt import qualified Arithmetic.Lte as Lte+import qualified Arithmetic.Equal as Eq import qualified Arithmetic.Nat as Nat import qualified Arithmetic.Plus as Plus @@ -46,7 +58,8 @@ incrementL :: forall n m. Nat m -> Fin n -> Fin (m + n) incrementL m (Fin i pf) = Fin (Nat.plus m i) (Lt.incrementL @m pf) --- | Weaken the bound by one. This does not change the index.+-- | Weaken the bound by @m@, adding it to the left-hand side of+-- the existing bound. This does not change the index. weakenL :: forall n m. Fin n -> Fin (m + n) weakenL (Fin i pf) = Fin i   ( Lt.substituteR@@ -54,26 +67,69 @@     (Lt.plus pf (Lte.zero @m))   ) --- side of @n@. This does not change the index.+-- | Weaken the bound by @m@, adding it to the right-hand side of+-- the existing bound. This does not change the index. weakenR :: forall n m. Fin n -> Fin (n + m) weakenR (Fin i pf) = Fin i (Lt.plus pf Lte.zero) +-- | Weaken the bound, replacing it by another number greater than+-- or equal to itself. This does not change the index.+weaken :: forall n m. (n <= m) -> Fin n -> Fin m+weaken lt (Fin i pf) = Fin i (Lt.transitiveNonstrictR pf lt)+ -- | A finite set of no values is impossible. absurd :: Fin 0 -> void absurd (Fin _ pf) = Lt.absurd pf --- | Strict fold over the numbers bounded by @n@ in ascending--- order. For convenince, this differs from @foldl'@ in the--- order of the parameters differs from @foldl@. Roughly:+-- | Fold over the numbers bounded by @n@ in descending+-- order. This is lazy in the accumulator. For convenince,+-- this differs from @foldr@ in the order of the parameters. --+-- > descend 4 z f = f 0 (f 1 (f 2 (f 3 z)))+descend :: forall a n.+     Nat n -- ^ Upper bound+  -> a -- ^ Initial accumulator+  -> (Fin n -> a -> a) -- ^ Update accumulator+  -> a+{-# inline descend #-}+descend !n b0 f = go Nat.zero+  where+  go :: Nat m -> a+  go !m = case m <? n of+    Nothing -> b0+    Just lt -> f (Fin m lt) (go (Nat.succ m))++-- | Fold over the numbers bounded by @n@ in ascending order. This+-- is lazy in the accumulator.+-- -- > ascend 4 z f = f 3 (f 2 (f 1 (f 0 z))) ascend :: forall a n.+     Nat n+  -> a+  -> (Fin n -> a -> a)+  -> a+{-# inline ascend #-}+ascend !n !b0 f = go n Lte.reflexive+  where+    go :: Nat p -> (p <= n) -> a+    go !m pLteEn = case Nat.monus m Nat.one of+      Nothing -> b0+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+        let !cLtEn = descendLemma cPlusOneEqP pLteEn+        in f (Fin mpred cLtEn) (go mpred (Lte.fromStrict cLtEn))++-- | Strict fold over the numbers bounded by @n@ in ascending+-- order. For convenince, this differs from @foldl'@ in the+-- order of the parameters.+--+-- > ascend' 4 z f = f 3 (f 2 (f 1 (f 0 z)))+ascend' :: forall a n.      Nat n -- ^ Upper bound   -> a -- ^ Initial accumulator   -> (Fin n -> a -> a) -- ^ Update accumulator   -> a-{-# inline ascend #-}-ascend !n !b0 f = go Nat.zero b0+{-# inline ascend' #-}+ascend' !n !b0 f = go Nat.zero b0   where   go :: Nat m -> a -> a   go !m !b = case m <? n of@@ -83,7 +139,7 @@ -- | Strict monadic left fold over the numbers bounded by @n@ -- in ascending order. Roughly: ----- > ascendM 4 z f =+-- > ascendM 4 z0 f = -- >   f 0 z0 >>= \z1 -> -- >   f 1 z1 >>= \z2 -> -- >   f 2 z2 >>= \z3 ->@@ -117,10 +173,59 @@     Nothing -> pure ()     Just lt -> f (Fin m lt) *> go (Nat.succ m) +descendLemma :: forall a b c. a + 1 :=: b -> b <= c -> a < c+{-# inline descendLemma #-}+descendLemma !aPlusOneEqB !bLteC = id+  $ Lt.transitiveNonstrictR+      (Lt.substituteR (Plus.commutative @1 @a)+      (Lt.plus Lt.zero Lte.reflexive))+  $ Lte.substituteL (Eq.symmetric aPlusOneEqB) bLteC++-- | Strict monadic left fold over the numbers bounded by @n@+-- in descending order. Roughly:+--+-- > descendM 4 z f =+-- >   f 3 z0 >>= \z1 ->+-- >   f 2 z1 >>= \z2 ->+-- >   f 1 z2 >>= \z3 ->+-- >   f 0 z3+descendM :: forall m a n. Monad m+  => Nat n+  -> a+  -> (Fin n -> a -> m a)+  -> m a+{-# inline descendM #-}+descendM !n !b0 f = go n Lte.reflexive b0+  where+    go :: Nat p -> p <= n -> a -> m a+    go !m pLteEn !b = case Nat.monus m Nat.one of+      Nothing -> pure b+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+        let !cLtEn = descendLemma cPlusOneEqP pLteEn+        in go mpred (Lte.fromStrict cLtEn) =<< f (Fin mpred cLtEn) b++-- | Monadic traversal of the numbers bounded by @n@+-- in descending order.+--+-- > descendM_ 4 f = f 3 *> f 2 *> f 1 *> f 0+descendM_ :: forall m a n. Applicative m+  => Nat n -- ^ Upper bound+  -> (Fin n -> m a) -- ^ Effectful interpretion+  -> m ()+{-# inline descendM_ #-}+descendM_ !n f = go n Lte.reflexive+  where+  go :: Nat p -> p <= n -> m ()+  go !m !pLteEn = case Nat.monus m Nat.one of+    Nothing -> pure ()+    Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+      let !cLtEn = descendLemma cPlusOneEqP pLteEn+      in f (Fin mpred cLtEn) *> go mpred (Lte.fromStrict cLtEn)+ -- | Generate all values of a finite set in ascending order. -- -- >>> ascending (Nat.constant @3)--- [0, 1, 2]+-- [Fin 0,Fin 1,Fin 2] ascending :: forall n. Nat n -> [Fin n] ascending !n = go Nat.zero   where@@ -132,42 +237,68 @@ -- | Generate all values of a finite set in descending order. -- -- >>> descending (Nat.constant @3)--- [2, 1, 0]+-- [Fin 2,Fin 1,Fin 0] descending :: forall n. Nat n -> [Fin n]-descending n = go n Lte.reflexive+descending !n = go n Lte.reflexive   where-    go :: forall m. Nat m -> (m <= n) -> [Fin n]-    go !m !lt = case Nat.monus m Nat.one of+    go :: Nat p -> (p <= n) -> [Fin n]+    go !m !pLteEn = case Nat.monus m Nat.one of       Nothing -> []-      Just (Difference mpred eq) -> go2 lt mpred eq-    go2 :: forall m c. (m <= n) -> Nat c -> (c + 1 :=: m) -> [Fin n]-    go2 !lt !c !eq = -        let ceeLtEm :: c < m-            ceeLtEm = id-              $ Lt.substituteR eq-              $ Lt.substituteL Plus.zeroL-              $ Lt.incrementL @c Lt.zero-         in Fin c (Lt.transitiveNonstrictR ceeLtEm lt) : go c-              (Lte.transitive (Lte.substituteR eq (Lte.weakenR @1 (Lte.reflexive @c))) lt)+      Just (Difference (mpred :: Nat c) cPlusOneEqP) ->+        let !cLtEn = descendLemma cPlusOneEqP pLteEn+        in Fin mpred cLtEn : go mpred (Lte.fromStrict cLtEn) --- | Generate 'len' values starting from 'off'.+-- | Generate 'len' values starting from 'off' in ascending order. ----- >>> slice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)--- [2, 3, 4]-ascendingSlice :: forall n off len.-     Nat off+-- >>> ascendingSlice (Nat.constant @2) (Nat.constant @3) (Lte.constant @_ @6)+-- [Fin 2,Fin 3,Fin 4]+ascendingSlice+  :: forall n off len+  .  Nat off   -> Nat len-  -> (off + len < n)+  -> off + len <= n   -> [Fin n]-ascendingSlice off len !offPlusLenLtEn = go Nat.zero+{-# inline ascendingSlice #-}+ascendingSlice off len !offPlusLenLteEn = go Nat.zero   where     go :: Nat m -> [Fin n]     go !m = case m <? len of       Nothing -> []       Just emLtLen ->         let !offPlusEmLtOffPlusLen = Lt.incrementL @off emLtLen-            !offPlusEmLtEn = Lt.transitive offPlusEmLtOffPlusLen offPlusLenLtEn+            !offPlusEmLtEn = Lt.transitiveNonstrictR offPlusEmLtOffPlusLen offPlusLenLteEn          in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)++-- | Generate 'len' values starting from 'off + len - 1' in descending order.+--+-- >>> descendingSlice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)+-- [Fin 4,Fin 3,Fin 2]+descendingSlice+  :: forall n off len+  .  Nat off+  -> Nat len+  -> off + len <= n+  -> [Fin n]+{-# inline descendingSlice #-}+descendingSlice !off !len !offPlusLenLteEn =+  go len Lte.reflexive+  where+    go :: Nat m -> m <= len -> [Fin n]+    go !m !mLteEn = case Nat.monus m Nat.one of+      Nothing -> []+      Just (Difference (mpred :: Nat c) cPlusOneEqEm) ->+        let !cLtLen = Lt.transitiveNonstrictR+              (Lt.substituteR (Plus.commutative @1 @c) (Lt.plus Lt.zero Lte.reflexive))+              -- c < c + 1+              (Lte.substituteL (Eq.symmetric cPlusOneEqEm) mLteEn)+              -- c + 1 <= len+            !cPlusOffLtEn = Lt.transitiveNonstrictR+              (Lt.substituteR+                (Plus.commutative @len @off)+                (Lt.plus cLtLen (Lte.reflexive @off)))+              -- c + off < off + len+              offPlusLenLteEn+        in Fin (mpred `Nat.plus` off) cPlusOffLtEn : go mpred (Lte.fromStrict cLtLen)  -- | Extract the 'Int' from a 'Fin n'. This is intended to be used -- at a boundary where a safe interface meets the unsafe primitives

@@ -21,6 +21,9 @@   , transitive   , transitiveNonstrictL   , transitiveNonstrictR+    -- * Convert to Inequality+  , toLteL+  , toLteR     -- * Absurdities   , absurd     -- * Integration with GHC solver@@ -33,9 +36,15 @@  import qualified GHC.TypeNats as GHC --- | Replace the right-hand side of a strict inequality+toLteR :: (a < b) -> (a + 1 <= b)+toLteR Lt = Lte++toLteL :: (a < b) -> (1 + a <= b)+toLteL Lt = Lte++-- | Replace the left-hand side of a strict inequality -- with an equal number.-substituteL :: (b :=: c) -> (a < b) -> (a < c)+substituteL :: (b :=: c) -> (b < a) -> (c < a) substituteL Eq Lt = Lt  -- | Replace the right-hand side of a strict inequality

@@ -35,9 +35,9 @@  import qualified GHC.TypeNats as GHC --- | Replace the right-hand side of a strict inequality+-- | Replace the left-hand side of a strict inequality -- with an equal number.-substituteL :: (b :=: c) -> (a <= b) -> (a <= c)+substituteL :: (b :=: c) -> (b <= a) -> (c <= a) substituteL Eq Lte = Lte  -- | Replace the right-hand side of a strict inequality

@@ -2,6 +2,7 @@ {-# language ExplicitForAll #-} {-# language KindSignatures #-} {-# language MagicHash #-}+{-# language RankNTypes #-} {-# language ScopedTypeVariables #-} {-# language TypeOperators #-} @@ -16,15 +17,19 @@   , testEqual   , testLessThan   , testLessThanEqual+  , testZero   , (=?)   , (<?)   , (<=?)     -- * Constants   , zero   , one+  , two+  , three   , constant-    -- * Demote+    -- * Convert   , demote+  , with   ) where  import Prelude hiding (succ)@@ -67,6 +72,12 @@   then Just Eq   else Nothing +-- | Is zero equal to this number or less than it?+testZero :: Nat a -> Either (0 :=: a) (0 < a)+testZero (Nat x) = case x of+  0 -> Left Eq+  _ -> Right Lt+ -- | Add two numbers. plus :: Nat a -> Nat b -> Nat (a + b) plus (Nat x) (Nat y) = Nat (x + y)@@ -90,6 +101,14 @@ one :: Nat 1 one = Nat 1 +-- | The number two.+two :: Nat 2+two = Nat 2++-- | The number three.+three :: Nat 3+three = Nat 3+ -- | Use GHC's built-in type-level arithmetic to create a witness -- of a type-level number. This only reduces if the number is a -- constant.@@ -101,3 +120,10 @@ -- on top of which it is built. demote :: Nat n -> Int 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+-- segfault.+with :: Int -> (forall n. Nat n -> a) -> a+with i f = f (Nat i)

@@ -7,6 +7,7 @@  module Arithmetic.Types   ( Nat+  , WithNat(..)   , Difference(..)   , Fin(..)   , type (<)@@ -20,6 +21,9 @@ import GHC.TypeNats (type (+))  import qualified GHC.TypeNats as GHC++data WithNat :: (GHC.Nat -> Type) -> Type where+  WithNat :: Nat n -> f n -> WithNat f  -- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }' data Fin :: GHC.Nat -> Type where

@@ -1,8 +1,11 @@ {-# language DataKinds #-}+{-# language DerivingStrategies #-} {-# language ExplicitNamespaces #-} {-# language GADTSyntax #-}+{-# language GeneralizedNewtypeDeriving #-} {-# language KindSignatures #-} {-# language RoleAnnotations #-}+{-# language StandaloneDeriving #-} {-# language TypeOperators #-}  module Arithmetic.Unsafe@@ -33,6 +36,8 @@ -- | A value-level representation of a natural number @n@. newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int } type role Nat nominal++deriving newtype instance Show (Nat n)  -- | Proof that the first argument is strictly less than the -- second argument.