type-natural 0.2.0.0 → 0.2.1.0
raw patch · 3 files changed
+175/−97 lines, 3 filesdep ~basedep ~equational-reasoningdep ~singletons
Dependency ranges changed: base, equational-reasoning, singletons, template-haskell
Files
- Data/Type/Natural.hs +146/−74
- Data/Type/Ordinal.hs +21/−18
- type-natural.cabal +8/−5
Data/Type/Natural.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}-{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}-{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving #-}+{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-}+{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds, RankNTypes, TemplateHaskell, TypeFamilies #-}+{-# LANGUAGE TypeOperators, UndecidableInstances, StandaloneDeriving #-} -- | Type level peano natural number, some arithmetic functions and their singletons. module Data.Type.Natural (-- * Re-exported modules. module Data.Singletons,@@ -11,13 +11,15 @@ -- | Singleton type for 'Nat'. SNat, Sing (SZ, SS), -- ** Smart constructors+ -- | WARNING: Smart constructors are deprecated as of singletons 0.10,+ -- so these are provided only for backward compatibility. sZ, sS, -- ** Arithmetic functions and their singletons. min, Min, sMin, max, Max, sMax, (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*), (:-:), (:-), (%:-), (%-), -- ** Type-level predicate & judgements- Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc,+ Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, boolToPropLeq, boolToClassLeq, propToClassLeq, LeqTrueInstance, propToBoolLeq, -- * Conversion functions@@ -27,13 +29,17 @@ -- * Properties of natural numbers succCongEq, plusCongR, plusCongL, succPlusL, succPlusR, plusZR, plusZL, eqPreservesS, plusAssociative,- multAssociative, multComm, multZL, multZR, multOneL, multOneR,+ multAssociative, multComm, multZL, multZR, multOneL,+ multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR, plusMultDistr, multPlusDistr, multCongL, multCongR, sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent,- eqSuccMinus, plusMinusEqL, plusMinusEqR, plusLeqL, plusLeqR,- zAbsorbsMinR, zAbsorbsMinL, minLeqL, minLeqR, plusSR,- leqRhs, leqLhs, leqTrans, minComm, leqAnitsymmetric,- maxZL, maxComm, maxZR, maxLeqL, maxLeqR, plusMonotone,+ eqSuccMinus, plusMinusEqL, plusMinusEqR,+ zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL,+ leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR,+ -- * Properties of ordering 'Leq'+ leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR,+ minLeqL, minLeqR, leqAnitsymmetric, maxLeqL, maxLeqR,+ leqSnZAbsurd, leqnZElim, leqSnLeq, leqPred, leqSnnAbsurd, -- * Useful type synonyms and constructors zero, one, two, three, four, five, six, seven, eight, nine, ten, eleven, twelve, thirteen, fourteen, fifteen, sixteen, seventeen, eighteen, nineteen, twenty,@@ -47,6 +53,9 @@ sN15, sN16, sN17, sN18, sN19, sN20 ) where import Data.Singletons+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+import Data.Singletons.TH+#endif import Data.Type.Monomorphic import Prelude (Int, Bool (..), Eq (..), Integral (..), Ord ((<)), Show (..), error, id, otherwise, ($), (.), undefined)@@ -184,6 +193,17 @@ n20 = twenty |] +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708+sZ :: SNat Z+sZ = SZ++sS :: SNat n -> SNat (S n)+sS = SS++{-# DEPRECATED sZ, sS "Smart constructors are no longer needed in singletons; Use `SS` or `SZ` instead." #-}+#endif++ -------------------------------------------------- -- ** Type-level predicate & judgements. --------------------------------------------------@@ -272,14 +292,6 @@ boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m boolToPropLeq _ _ = bugInGHC -leqRefl :: SNat n -> Leq n n-leqRefl SZ = ZeroLeq sZ-leqRefl (SS n) = SuccLeqSucc $ leqRefl n--leqSucc :: SNat n -> Leq n (S n)-leqSucc SZ = ZeroLeq sOne-leqSucc (SS n) = SuccLeqSucc $ leqSucc n- leqRhs :: Leq n m -> SNat m leqRhs (ZeroLeq m) = m leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq@@ -288,15 +300,6 @@ leqLhs (ZeroLeq _) = sZ leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq -leqTrans :: Leq n m -> Leq m l -> Leq n l-leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq-leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql-leqTrans _ _ = error "impossible!"--instance Preorder Leq where- reflexivity = leqRefl- transitivity = leqTrans- -------------------------------------------------- -- * Properties --------------------------------------------------@@ -316,6 +319,23 @@ succCongEq :: n :=: m -> S n :=: S m succCongEq Refl = Refl +snEqZAbsurd :: S n :=: Z -> a+snEqZAbsurd _ = bugInGHC "impossible!"++succInjective :: S n :=: S m -> n :=: m+succInjective Refl = Refl++plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l+plusInjectiveL SZ _ _ Refl = Refl+plusInjectiveL (SS n) m l eq = plusInjectiveL n m l $ succInjective eq++plusInjectiveR :: SNat n -> SNat m -> SNat l -> n :+ l :=: m :+ l -> n :=: m+plusInjectiveR n m l eq = plusInjectiveL l n m $+ start (l %:+ n)+ === n %:+ l `because` plusCommutative l n+ === m %:+ l `because` eq+ === l %:+ m `because` plusCommutative m l + sAndPlusOne :: SNat n -> S n :=: n :+: One sAndPlusOne SZ = Refl sAndPlusOne (SS n) =@@ -340,13 +360,6 @@ === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne) === n %+ sS m `because` plusCongL n (symmetry $ sAndPlusOne m) -plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)-plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)-plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =- case plusSR m (leqRhs leq) of- Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq-plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'- plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m' plusCongL _ Refl = Refl @@ -399,15 +412,6 @@ =~= sS (sS n %:- sS m) eqSuccMinus _ _ = bugInGHC -plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)-plusLeqL SZ m = case plusZR m of Refl -> ZeroLeq m-plusLeqL (SS n) m = SuccLeqSucc $ plusLeqL n m--plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)-plusLeqR n m =- case plusCommutative n m of- Refl -> plusLeqL m n- plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n plusMinusEqL SZ m = minusNilpotent m plusMinusEqL (SS n) m =@@ -427,25 +431,12 @@ zAbsorbsMinL SZ = Refl zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl -minLeqL :: SNat n -> SNat m -> Leq (Min n m) n-minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ-minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n-minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)--minLeqR :: SNat n -> SNat m -> Leq (Min n m) m-minLeqR n m = case minComm n m of Refl -> minLeqL m n- minComm :: SNat n -> SNat m -> Min n m :=: Min m n minComm SZ SZ = Refl minComm SZ (SS _) = Refl minComm (SS _) SZ = Refl minComm (SS n) (SS m) = case minComm n m of Refl -> Refl -leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m-leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl-leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2-leqAnitsymmetric _ _ = bugInGHC- maxZL :: SNat n -> Max Z n :=: n maxZL SZ = Refl maxZL (SS _) = Refl@@ -459,24 +450,6 @@ maxZR :: SNat n -> Max n Z :=: n maxZR n = transitivity (maxComm n sZ) (maxZL n) -maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)-maxLeqL SZ m = ZeroLeq (sMax sZ m)-maxLeqL n SZ = case maxZR n of- Refl -> leqRefl n-maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m--maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)-maxLeqR n m = case maxComm n m of- Refl -> maxLeqL m n--newtype MultPlusDistr l m n =- MultPlusDistr { unMultPlusDistr :: l :* (m :+ n) :=: l :* m :+ l :* n}--instance Proposition (MultPlusDistr l m) where- type OriginalProp (MultPlusDistr l m) n = l :* (m :+ n) :=: l :* m :+ l :* n- wrap = MultPlusDistr- unWrap = unMultPlusDistr- multPlusDistr :: SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: n :* m :+ n :* l multPlusDistr SZ _ _ = Refl multPlusDistr (SS n) m l = @@ -559,6 +532,105 @@ === m %* (n %+ sOne) `because` symmetry (multPlusDistr m n sOne) === m %* sS n `because` multCongL m (symmetry $ sAndPlusOne n) +plusNeutralR :: SNat n -> SNat m -> n :+ m :=: n -> m :=: Z+plusNeutralR SZ m eq =+ start m+ =~= sZ %:+ m+ === sZ `because` eq+plusNeutralR (SS n) m eq = plusNeutralR n m $ succInjective eq++plusNeutralL :: SNat n -> SNat m -> n :+ m :=: m -> n :=: Z+plusNeutralL n m eq = plusNeutralR m n $+ start (m %:+ n)+ === n %:+ m `because` plusCommutative m n+ === m `because` eq++--------------------------------------------------+-- * Properties of 'Leq'+--------------------------------------------------++leqRefl :: SNat n -> Leq n n+leqRefl SZ = ZeroLeq sZ+leqRefl (SS n) = SuccLeqSucc $ leqRefl n++leqSucc :: SNat n -> Leq n (S n)+leqSucc SZ = ZeroLeq sOne+leqSucc (SS n) = SuccLeqSucc $ leqSucc n++leqTrans :: Leq n m -> Leq m l -> Leq n l+leqTrans (ZeroLeq _) leq = ZeroLeq $ leqRhs leq+leqTrans (SuccLeqSucc nLeqm) (SuccLeqSucc mLeql) = SuccLeqSucc $ leqTrans nLeqm mLeql+leqTrans _ _ = error "impossible!"++instance Preorder Leq where+ reflexivity = leqRefl+ transitivity = leqTrans++plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)+plusMonotone (ZeroLeq m) (ZeroLeq k) = ZeroLeq (m %+ k)+plusMonotone (ZeroLeq m) (SuccLeqSucc leq) =+ case plusSR m (leqRhs leq) of+ Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq+plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq'++plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)+plusLeqL SZ m = ZeroLeq $ coerce (symmetry $ plusZL m) m+plusLeqL (SS n) m =+ start (sS n)+ =<= sS (n %+ m) `because` SuccLeqSucc (plusLeqL n m)+ =~= sS n %+ m++plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)+plusLeqR n m =+ case plusCommutative n m of+ Refl -> plusLeqL m n++minLeqL :: SNat n -> SNat m -> Leq (Min n m) n+minLeqL SZ m = case zAbsorbsMinL m of Refl -> ZeroLeq sZ+minLeqL n SZ = case zAbsorbsMinR n of Refl -> ZeroLeq n+minLeqL (SS n) (SS m) = SuccLeqSucc (minLeqL n m)++minLeqR :: SNat n -> SNat m -> Leq (Min n m) m+minLeqR n m = case minComm n m of Refl -> minLeqL m n++leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m+leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl+leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2+leqAnitsymmetric _ _ = bugInGHC++maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)+maxLeqL SZ m = ZeroLeq (sMax sZ m)+maxLeqL n SZ = case maxZR n of+ Refl -> leqRefl n+maxLeqL (SS n) (SS m) = SuccLeqSucc $ maxLeqL n m++maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)+maxLeqR n m = case maxComm n m of+ Refl -> maxLeqL m n++leqSnZAbsurd :: Leq (S n) Z -> a+leqSnZAbsurd _ = error "cannot be occured"++leqnZElim :: Leq n Z -> n :=: Z+leqnZElim (ZeroLeq SZ) = Refl++leqSnLeq :: Leq (S n) m -> Leq n m+leqSnLeq (SuccLeqSucc leq) =+ let n = leqLhs leq+ m = sS $ leqRhs leq+ in start n+ =<= sS n `because` leqSucc n+ =<= m `because` SuccLeqSucc leq++leqPred :: Leq (S n) (S m) -> Leq n m+leqPred (SuccLeqSucc leq) = leq++leqSnnAbsurd :: Leq (S n) n -> a+leqSnnAbsurd (SuccLeqSucc leq) =+ case leqLhs leq of+ SS _ -> leqSnnAbsurd leq+ _ -> bugInGHC "cannot be occured"+ -------------------------------------------------- -- * Conversion functions. --------------------------------------------------
Data/Type/Ordinal.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE DataKinds, EmptyDataDecls, FlexibleContexts, FlexibleInstances #-}-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell #-}-{-# LANGUAGE GADTs, KindSignatures, PolyKinds, StandaloneDeriving #-}-{-# LANGUAGE TypeFamilies, TypeOperators #-}+{-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds #-}+{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-}+{-# LANGUAGE TypeFamilies, TypeOperators #-} -- | Set-theoretic ordinal arithmetic module Data.Type.Ordinal ( -- * Data-types@@ -15,13 +15,16 @@ -- * Quasi Quote od ) where+import Data.Constraint import Data.Type.Monomorphic-import Unsafe.Coerce-import Language.Haskell.TH.Quote+import Data.Type.Natural hiding (promote) import Language.Haskell.TH-import Data.Type.Natural hiding (promote)-import Proof.Equational (coerce)-import Data.Constraint+import Language.Haskell.TH.Quote+import Proof.Equational (coerce)+import Unsafe.Coerce+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707+import Data.Singletons.Prelude+#endif -- | Set-theoretic (finite) ordinals: --@@ -36,7 +39,7 @@ instance Read (Ordinal Z) where readsPrec _ _ = [] -instance SingRep n => Num (Ordinal n) where+instance SingI n => Num (Ordinal n) where _ + _ = error "Finite ordinal is not closed under addition." _ - _ = error "Ordinal subtraction is not defined" negate OZ = OZ@@ -53,33 +56,33 @@ deriving instance Eq (Ordinal n) deriving instance Ord (Ordinal n) -instance SingRep n => Enum (Ordinal n) where+instance SingI n => Enum (Ordinal n) where fromEnum = ordToInt toEnum = unsafeFromInt enumFrom = enumFromOrd enumFromTo = enumFromToOrd -enumFromToOrd :: forall n. SingRep n => Ordinal n -> Ordinal n -> [Ordinal n]+enumFromToOrd :: forall n. SingI n => Ordinal n -> Ordinal n -> [Ordinal n] enumFromToOrd ok ol = let k = ordToInt ok l = ordToInt ol in take (l - k + 1) $ enumFromOrd ok -enumFromOrd :: forall n. SingRep n => Ordinal n -> [Ordinal n]+enumFromOrd :: forall n. SingI n => Ordinal n -> [Ordinal n] enumFromOrd ord = drop (ordToInt ord) $ enumOrdinal (sing :: SNat n) enumOrdinal :: SNat n -> [Ordinal n] enumOrdinal SZ = [] enumOrdinal (SS n) = OZ : map OS (enumOrdinal n) -instance SingRep n => Bounded (Ordinal (S n)) where+instance SingI n => Bounded (Ordinal (S n)) where minBound = OZ maxBound = case propToBoolLeq $ leqRefl (sing :: SNat n) of Dict -> sNatToOrd (sing :: SNat n) -unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n-unsafeFromInt n = +unsafeFromInt :: forall n. SingI n => Int -> Ordinal n+unsafeFromInt n = case promote n of Monomorphic sn -> case sS sn %:<<= (sing :: SNat n) of@@ -93,7 +96,7 @@ sNatToOrd' _ _ = bugInGHC -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (SingRep n, (S m :<<= n) ~ True) => SNat m -> Ordinal n+sNatToOrd :: (SingI n, (S m :<<= n) ~ True) => SNat m -> Ordinal n sNatToOrd = sNatToOrd' sing data CastedOrdinal n where@@ -139,7 +142,7 @@ {-# INLINE inclusion #-} -- | Ordinal addition.-(@+) :: forall n m. (SingRep n, SingRep m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+(@+) :: forall n m. (SingI n, SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m) OZ @+ n = let sn = sing :: SNat n sm = sing :: SNat m
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.2.0.0+version: 0.2.1.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. homepage: https://github.com/konn/type-natural@@ -22,9 +22,12 @@ library exposed-modules: Data.Type.Natural, Data.Type.Ordinal -- other-modules: - build-depends: base == 4.6.*- , singletons == 0.8.*- , equational-reasoning == 0.0.*+ build-depends: base >= 4 && < 5+ , equational-reasoning == 0.2.* , monomorphic >= 0.0.3- , template-haskell == 2.8.*+ , template-haskell >= 2.8 && < 2.11 , constraints == 0.3.*+ if impl(ghc < 7.8)+ build-depends: singletons == 0.8.*+ else+ build-depends: singletons >= 0.10 && < 0.11