packages feed

natural-arithmetic (empty) → 0.1.0.0

raw patch · 12 files changed

+764/−0 lines, 12 filesdep +basesetup-changed

Dependencies added: base

Files

+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for natural-arithmetic++## 0.1.0.0 -- 2019-09-04++* Initial release.
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2019, Andrew Martin++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++    * Redistributions of source code must retain the above copyright+      notice, this list of conditions and the following disclaimer.++    * Redistributions in binary form must reproduce the above+      copyright notice, this list of conditions and the following+      disclaimer in the documentation and/or other materials provided+      with the distribution.++    * Neither the name of Andrew Martin nor the names of other+      contributors may be used to endorse or promote products derived+      from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ natural-arithmetic.cabal view
@@ -0,0 +1,80 @@+cabal-version: 2.2+name: natural-arithmetic+version: 0.1.0.0+synopsis: Arithmetic of natural numbers+description:+  A search for terms like `arithmetic` and `natural` on hackage reveals+  no shortage of libraries for handling the arithmetic of natural+  numbers. How is this library any different some of the others? It has+  a particular purpose: providing a foundation on top on which other+  libraries may define types indexed by sizes. This uses GHC's+  non-inductively-defined `GHC.TypeNats.Nat`. As a rule, this does not+  use `unsafeCoerce` internally anywhere.+  .+  Perhaps the most direct competitor to `natural-arithmetic` is a+  typechecker plugin like+  <https://github.com/yav/type-nat-solver type-nat-solver>. The big+  difference is that `type-nat-solver` can really only be used in+  application code, not in library code. This is because libraries+  should not require the presence of typechecker plugins. Technically,+  they can (you could document it), but many developers will not+  use libraries that have unusual install procedures like this. +  .+  This library, in places, requires users to use the 'TypeApplications`+  language extension. This is done when a number is only need at+  the type level (without a runtime witness).+  .+  This library uses a non-minimal core, providing redundant primitives+  in `Arithmetic.Lt` and `Arithmetic.Lte`. This is done in the interest+  of making it easy for user to assemble proofs. Recall that proof+  assembly is done by hand rather than by an SMT solver, so removing+  some tediousness from this is helpful to users. +  .+  This library provides left and variants variants of several functions.+  For example, `Arithmetic.Lte` provides both `substituteL` and+  `substituteR`. This is only done when there are two variants of+  a function. For substitution, this is the case because we have+  `b = c, a ≤ b ==> a ≤ c` and `a = c, a ≤ b ==> c ≤ b`. So, we+  provide both `substituteL` and `substituteR`. However,+  for addition of inequalities, we have four possible variants:+  `a ≤ b, c ≤ d ==> a + c ≤ b + d`, `a ≤ b, c ≤ d ==> c + a ≤ b + d`,+  `a ≤ b, c ≤ d ==> a + c ≤ d + b`, `a ≤ b, c ≤ d ==> c + a ≤ d + b`.+  Consequently, we only provide a single `plus` function, and users+  must use `Arithmetic.Plus.commutative` to further manipulate the+  inequality.+  .+  Here are the proof-manipulation vocabulary used by this library.+  Many of these terms are not standard, but we try to be consistent+  in this library:+  .+  * Weaken: Increase an upper bound without changing the bounded value+  .+  * Increment: Increase an upper bound along with the bounded value+  .+  * Decrement: Decrease an upper bound along with the bounded value+  .+  * Substitute: Replace a number with an equal number+homepage: https://github.com/andrewthad/natural-arithmetic+bug-reports: https://github.com/andrewthad/natural-arithmetic/issues+license: BSD-3-Clause+license-file: LICENSE+author: Andrew Martin+maintainer: andrew.thaddeus@gmail.com+copyright: 2019 Andrew Martin+category: Math+extra-source-files: CHANGELOG.md++library+  exposed-modules:+    Arithmetic.Fin+    Arithmetic.Equal+    Arithmetic.Lt+    Arithmetic.Lte+    Arithmetic.Nat+    Arithmetic.Types+    Arithmetic.Unsafe+    Arithmetic.Plus+  build-depends: base>=4.11 && <5+  hs-source-dirs: src+  default-language: Haskell2010+  ghc-options: -Wall -O2
+ src/Arithmetic/Equal.hs view
@@ -0,0 +1,22 @@+{-# language DataKinds #-}+{-# language ExplicitForAll #-}+{-# language KindSignatures #-}+{-# language TypeOperators #-}++module Arithmetic.Equal+  ( symmetric+  , plusR+  , plusL+  ) where++import Arithmetic.Unsafe (type (:=:)(Eq))+import GHC.TypeNats (type (+))++symmetric :: (m :=: n) -> (n :=: m)+symmetric Eq = Eq++plusL :: forall c m n. (m :=: n) -> (c + m :=: c + n)+plusL Eq = Eq++plusR :: forall c m n. (m :=: n) -> (m + c :=: n + c)+plusR Eq = Eq
+ src/Arithmetic/Fin.hs view
@@ -0,0 +1,176 @@+{-# language BangPatterns #-}+{-# language DataKinds #-}+{-# language ExplicitNamespaces #-}+{-# language GADTs #-}+{-# language KindSignatures #-}+{-# language ScopedTypeVariables #-}+{-# language TypeApplications #-}+{-# language TypeOperators #-}+module Arithmetic.Fin+  ( -- * Modification+    incrementL+  , incrementR+  , weakenL+  , weakenR+    -- * Traverse+  , ascend+  , ascendM+  , ascendM_+  , ascending+  , descending+  , ascendingSlice+    -- * Absurdities+  , absurd+    -- * Demote+  , demote+  ) where++import Prelude hiding (last)++import Arithmetic.Nat ((<?))+import Arithmetic.Types (Fin(..),Difference(..),Nat,type (<), type (<=), type (:=:))+import GHC.TypeNats (type (+))++import qualified Arithmetic.Lt as Lt+import qualified Arithmetic.Lte as Lte+import qualified Arithmetic.Nat as Nat+import qualified Arithmetic.Plus as Plus++-- | Raise the index by @m@ and weaken the bound by @m@, adding+-- @m@ to the right-hand side of @n@.+incrementR :: forall n m. Nat m -> Fin n -> Fin (n + m)+incrementR m (Fin i pf) = Fin (Nat.plus i m) (Lt.incrementR @m pf)++-- | 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)+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.+weakenL :: forall n m. Fin n -> Fin (m + n)+weakenL (Fin i pf) = Fin i+  ( Lt.substituteR+    (Plus.commutative @n @m)+    (Lt.plus pf (Lte.zero @m))+  )++-- side of @n@. 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)++-- | 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:+--+-- > 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+  where+  go :: Nat m -> a -> a+  go !m !b = case m <? n of+    Nothing -> b+    Just lt -> go (Nat.succ m) (f (Fin m lt) b)++-- | Strict monadic left fold over the numbers bounded by @n@+-- in ascending order. Roughly:+--+-- > ascendM 4 z f =+-- >   f 0 z0 >>= \z1 ->+-- >   f 1 z1 >>= \z2 ->+-- >   f 2 z2 >>= \z3 ->+-- >   f 3 z3+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 !b0 f = go Nat.zero b0+  where+  go :: Nat p -> a -> m a+  go !m !b = case m <? n of+    Nothing -> pure b+    Just lt -> go (Nat.succ m) =<< f (Fin m lt) b++-- | Monadic traversal of the numbers bounded by @n@+-- in ascending order.+--+-- > ascendM_ 4 f = f 0 *> f 1 *> f 2 *> f 3+ascendM_ :: forall m a n. Applicative m+  => Nat n -- ^ Upper bound+  -> (Fin n -> m a) -- ^ Effectful interpretion+  -> m ()+{-# inline ascendM_ #-}+ascendM_ !n f = go Nat.zero+  where+  go :: Nat p -> m ()+  go !m = case m <? n of+    Nothing -> pure ()+    Just lt -> f (Fin m lt) *> go (Nat.succ m)++-- | Generate all values of a finite set in ascending order.+--+-- >>> ascending (Nat.constant @3)+-- [0, 1, 2]+ascending :: forall n. Nat n -> [Fin n]+ascending !n = go Nat.zero+  where+  go :: Nat m -> [Fin n]+  go !m = case m <? n of+    Nothing -> []+    Just lt -> Fin m lt : go (Nat.succ m)++-- | Generate all values of a finite set in descending order.+--+-- >>> descending (Nat.constant @3)+-- [2, 1, 0]+descending :: forall n. Nat n -> [Fin n]+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+      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)++-- | Generate 'len' values starting from 'off'.+--+-- >>> slice (Nat.constant @2) (Nat.constant @3) (Lt.constant @6)+-- [2, 3, 4]+ascendingSlice :: forall n off len.+     Nat off+  -> Nat len+  -> (off + len < n)+  -> [Fin n]+ascendingSlice off len !offPlusLenLtEn = 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+         in Fin (Nat.plus off m) offPlusEmLtEn : go (Nat.succ m)++-- | Extract the 'Int' from a 'Fin n'. This is intended to be used+-- at a boundary where a safe interface meets the unsafe primitives+-- on top of which it is built.+demote :: Fin n -> Int+demote (Fin i _) = Nat.demote i
+ src/Arithmetic/Lt.hs view
@@ -0,0 +1,99 @@+{-# language DataKinds #-}+{-# language ExplicitForAll #-}+{-# language KindSignatures #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}++module Arithmetic.Lt+  ( -- * Special Inequalities+    zero+    -- * Substitution+  , substituteL+  , substituteR+    -- * Increment+  , incrementL+  , incrementR+    -- * Weaken+  , weakenL+  , weakenR+    -- * Composition+  , plus+  , transitive+  , transitiveNonstrictL+  , transitiveNonstrictR+    -- * Absurdities+  , absurd+    -- * Integration with GHC solver+  , constant+  ) where++import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))+import Arithmetic.Unsafe (type (<=)(Lte))+import GHC.TypeNats (CmpNat,type (+))++import qualified GHC.TypeNats as GHC++-- | Replace the right-hand side of a strict inequality+-- with an equal number.+substituteL :: (b :=: c) -> (a < b) -> (a < c)+substituteL Eq Lt = Lt++-- | Replace the right-hand side of a strict inequality+-- with an equal number.+substituteR :: (b :=: c) -> (a < b) -> (a < c)+substituteR Eq Lt = Lt++-- | Add a strict inequality to a nonstrict inequality.+plus :: (a < b) -> (c <= d) -> (a + c < b + d)+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)+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)+incrementR 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)+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)+weakenR Lt = Lt++-- | Compose two strict inequalities using transitivity.+transitive :: (a < b) -> (b < c) -> (a < c)+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)+transitiveNonstrictR Lt Lte = Lt++transitiveNonstrictL :: (a <= b) -> (b < c) -> (a < c)+transitiveNonstrictL Lte Lt = Lt++-- | Zero is less than one.+zero :: 0 < 1+zero = Lt++-- | Nothing is less than zero.+absurd :: n < 0 -> void+absurd Lt = error "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)+constant = Lt+
+ src/Arithmetic/Lte.hs view
@@ -0,0 +1,113 @@+{-# language DataKinds #-}+{-# language ExplicitForAll #-}+{-# language KindSignatures #-}+{-# language TypeFamilies #-}+{-# language TypeOperators #-}++module Arithmetic.Lte+  ( -- * Special Inequalities+    zero+  , reflexive+    -- * Substitution+  , substituteL+  , substituteR+    -- * Increment+  , incrementL+  , incrementR+    -- * Decrement+  , decrementL+  , decrementR+    -- * Weaken+  , weakenL+  , weakenR+    -- * Composition+  , transitive+  , plus+    -- * Convert Strict Inequality+  , fromStrict+    -- * Integration with GHC solver+  , constant+  ) where++import Arithmetic.Unsafe (type (<)(Lt),type (:=:)(Eq))+import Arithmetic.Unsafe (type (<=)(Lte))+import GHC.TypeNats (CmpNat,type (+))++import qualified GHC.TypeNats as GHC++-- | Replace the right-hand side of a strict inequality+-- with an equal number.+substituteL :: (b :=: c) -> (a <= b) -> (a <= c)+substituteL Eq Lte = Lte++-- | Replace the right-hand side of a strict inequality+-- with an equal number.+substituteR :: (b :=: c) -> (a <= b) -> (a <= c)+substituteR Eq Lte = Lte++-- | Add two inequalities.+plus :: (a <= b) -> (c <= d) -> (a + c <= b + d)+plus Lte Lte = Lte++-- | Compose two inequalities using transitivity.+transitive :: (a <= b) -> (b <= c) -> (a <= c)+transitive Lte Lte = Lte++-- | Any number is less-than-or-equal-to itself.+reflexive :: a <= a+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)+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)+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)+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)+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)+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)+decrementR Lte = Lte++-- | Weaken a strict inequality to a non-strict inequality.+fromStrict :: (a < b) -> (a <= b)+fromStrict Lt = Lte++-- | Zero is less-than-or-equal-to any number.+zero :: 0 <= a+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)+constant = Lte++type family IsLte (o :: Ordering) :: Bool where+  IsLte 'GT = 'False+  IsLte 'LT = 'True+  IsLte 'EQ = 'True
+ src/Arithmetic/Nat.hs view
@@ -0,0 +1,103 @@+{-# language DataKinds #-}+{-# language ExplicitForAll #-}+{-# language KindSignatures #-}+{-# language MagicHash #-}+{-# language ScopedTypeVariables #-}+{-# language TypeOperators #-}++module Arithmetic.Nat+  ( -- * Addition+    plus+    -- * Subtraction+  , monus+    -- * Successor+  , succ+    -- * Compare+  , testEqual+  , testLessThan+  , testLessThanEqual+  , (=?)+  , (<?)+  , (<=?)+    -- * Constants+  , zero+  , one+  , constant+    -- * Demote+  , demote+  ) where++import Prelude hiding (succ)++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')++-- | Infix synonym of 'testLessThan'.+(<?) :: Nat a -> Nat b -> Maybe (a < b)+(<?) = testLessThan++-- | Infix synonym of 'testLessThanEqual'.+(<=?) :: Nat a -> Nat b -> Maybe (a <= b)+(<=?) = testLessThanEqual++-- | Infix synonym of 'testEqual'.+(=?) :: Nat a -> Nat b -> Maybe (a :=: b)+(=?) = testEqual++-- | Is the first argument strictly less than the second+-- argument?+testLessThan :: Nat a -> Nat b -> Maybe (a < b)+testLessThan (Nat x) (Nat y) = if x < y+  then Just Lt+  else Nothing++-- | Is the first argument less-than-or-equal-to the second+-- argument?+testLessThanEqual :: Nat a -> Nat b -> Maybe (a <= b)+testLessThanEqual (Nat x) (Nat y) = if x <= y+  then Just Lte+  else Nothing++-- | Are the two arguments equal to one another?+testEqual :: Nat a -> Nat b -> Maybe (a :=: b)+testEqual (Nat x) (Nat y) = if x == y+  then Just Eq+  else Nothing++-- | Add two numbers.+plus :: Nat a -> Nat b -> Nat (a + b)+plus (Nat x) (Nat y) = Nat (x + y)++-- | The successor of a number.+succ :: Nat a -> Nat (a + 1)+succ n = plus n one++-- | Subtract the second argument from the first argument.+monus :: Nat a -> Nat b -> Maybe (Difference a b)+{-# inline monus #-}+monus (Nat a) (Nat b) = let c = a - b in if c >= 0+  then Just (Difference (Nat c) Eq)+  else Nothing++-- | The number zero.+zero :: Nat 0+zero = Nat 0++-- | The number one.+one :: Nat 1+one = Nat 1++-- | 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.+constant :: forall n. KnownNat n => Nat n+constant = Nat (fromIntegral (natVal' (proxy# :: Proxy# n)))++-- | 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.+demote :: Nat n -> Int+demote (Nat n) = n
+ src/Arithmetic/Plus.hs view
@@ -0,0 +1,31 @@+{-# language DataKinds #-}+{-# language TypeOperators #-}+{-# language KindSignatures #-}+{-# language ExplicitForAll #-}+{-# language AllowAmbiguousTypes #-}++module Arithmetic.Plus+  ( zeroL+  , zeroR+  , commutative+  , associative+  ) where++import Arithmetic.Unsafe (type (:=:)(Eq))+import GHC.TypeNats (type (+))++-- | Any number plus zero is equal to the original number.+zeroR :: m :=: (m + 0)+zeroR = Eq++-- | Zero plus any number is equal to the original number.+zeroL :: m :=: (0 + m)+zeroL = Eq++-- | Addition is commutative.+commutative :: forall a b. a + b :=: b + a+commutative = Eq++-- | Addition is associative.+associative :: forall a b c. (a + b) + c :=: a + (b + c)+associative = Eq
+ src/Arithmetic/Types.hs view
@@ -0,0 +1,46 @@+{-# language DataKinds #-}+{-# language ExplicitNamespaces #-}+{-# language GADTs #-}+{-# language KindSignatures #-}+{-# language RankNTypes #-}+{-# language TypeOperators #-}++module Arithmetic.Types+  ( Nat+  , Difference(..)+  , Fin(..)+  , type (<)+  , type (<=)+  , type (:=:)+  ) where++import Arithmetic.Unsafe (Nat(getNat), type (<=))+import Arithmetic.Unsafe (type (<), type (:=:))+import Data.Kind (type Type)+import GHC.TypeNats (type (+))++import qualified GHC.TypeNats as GHC++-- | A finite set of 'n' elements. 'Fin n = { 0 .. n - 1 }'+data Fin :: GHC.Nat -> Type where+  Fin :: forall m n.+    { index :: !(Nat m)+    , proof :: !(m < n)+    } -> Fin n++-- | Proof that the first argument can be expressed as the+-- sum of the second argument and some other natural number.+data Difference :: GHC.Nat -> GHC.Nat -> Type where+  -- It is safe for users of this library to use this data constructor+  -- freely. However, note that the interesting Difference values come+  -- from Arithmetic.Nat.monus, which is a primitive.+  Difference :: forall a b c. Nat c -> (c + b :=: a) -> Difference a b++instance Show (Fin n) where+  showsPrec p (Fin i _) = showString "Fin " . showsPrec p (getNat i)++instance Eq (Fin n) where+  Fin x _ == Fin y _ = getNat x == getNat y++instance Ord (Fin n) where+  Fin x _ `compare` Fin y _ = compare (getNat x) (getNat y)
+ src/Arithmetic/Unsafe.hs view
@@ -0,0 +1,57 @@+{-# language DataKinds #-}+{-# language ExplicitNamespaces #-}+{-# language GADTSyntax #-}+{-# language KindSignatures #-}+{-# language RoleAnnotations #-}+{-# language TypeOperators #-}++module Arithmetic.Unsafe+  ( Nat(..)+  , type (<)(Lt)+  , type (<=)(Lte)+  , type (:=:)(Eq)+  ) where++import Prelude hiding ((>=),(<=))++import Control.Category (Category)+import Data.Kind (Type)++import qualified Control.Category+import qualified GHC.TypeNats as GHC++-- Do not import this module unless you enjoy pain.+-- Using this library to implement length-indexed arrays+-- or sized builders does not require importing this+-- module to get the value out of the Nat data constructor.+-- Use Arithmetic.Nat.demote for this purpose.++infix 4 <+infix 4 <=+infix 4 :=:++-- | A value-level representation of a natural number @n@.+newtype Nat (n :: GHC.Nat) = Nat { getNat :: Int }+type role Nat nominal++-- | Proof that the first argument is strictly less than the+-- second argument.+data (<) :: GHC.Nat -> GHC.Nat -> Type 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++-- | Proof that the first argument is equal to the second argument.+data (:=:) :: GHC.Nat -> GHC.Nat -> Type where+  Eq :: a :=: b++instance Category (<=) where+  id = Lte+  Lte . Lte = Lte++instance Category (:=:) where+  id = Eq+  Eq . Eq = Eq