diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs --- a/Data/Type/Natural.hs +++ b/Data/Type/Natural.hs @@ -5,47 +5,47 @@ -- | Type level peano natural number, some arithmetic functions and their singletons. module Data.Type.Natural (-- * Re-exported modules. module Data.Singletons, - -- * Natural Numbers - -- | Peano natural numbers. It will be promoted to the type-level natural number. - Nat(..), - -- | Singleton type for 'Nat'. - SNat, Sing (SZ, SS) - -- ** Smart constructors - , sZ, sS - -- ** Arithmetic functions and their singletons. - , min, Min, sMin, max, Max, sMax - , (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*) - , (:-:), (:-), (%:-), (%-) - -- ** Type-level predicate & judgements - , Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance(..), leqRefl, leqSucc - , boolToPropLeq, boolToClassLeq, propToClassLeq - , LeqTrueInstance(..), propToBoolLeq - -- * Conversion functions - , natToInt, intToNat, sNatToInt - -- * Quasi quotes for natural numbers - , nat, snat - -- * Properties of natural numbers - , succCongEq, plusCongR, plusCongL, succPlusL, succPlusR - , plusZR, plusZL, eqPreservesS, plusAssociative - , multAssociative, multComm, multZL, multZR, multOneL, multOneR - , 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 - -- * 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 - , Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten - , Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty - , sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven - , sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty - , n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20 - , N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20 - , sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14 - , sN15, sN16, sN17, sN18, sN19, sN20 - ) where + -- * Natural Numbers + -- | Peano natural numbers. It will be promoted to the type-level natural number. + Nat(..), + -- | Singleton type for 'Nat'. + SNat, Sing (SZ, SS), + -- ** Smart constructors + sZ, sS, + -- ** Arithmetic functions and their singletons. + min, Min, sMin, max, Max, sMax, + (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*), + (:-:), (:-), (%:-), (%-), + -- ** Type-level predicate & judgements + Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance(..), leqRefl, leqSucc, + boolToPropLeq, boolToClassLeq, propToClassLeq, + LeqTrueInstance(..), propToBoolLeq, + -- * Conversion functions + natToInt, intToNat, sNatToInt, + -- * Quasi quotes for natural numbers + nat, snat, + -- * Properties of natural numbers + succCongEq, plusCongR, plusCongL, succPlusL, succPlusR, + plusZR, plusZL, eqPreservesS, plusAssociative, + multAssociative, multComm, multZL, multZR, multOneL, multOneR, + 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, + -- * 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, + Zero, One, Two, Three, Four, Five, Six, Seven, Eight, Nine, Ten, + Eleven, Twelve, Thirteen, Fourteen, Fifteen, Sixteen, Seventeen, Eighteen, Nineteen, Twenty, + sZero, sOne, sTwo, sThree, sFour, sFive, sSix, sSeven, sEight, sNine, sTen, sEleven, + sTwelve, sThirteen, sFourteen, sFifteen, sSixteen, sSeventeen, sEighteen, sNineteen, sTwenty, + n0, n1, n2, n3, n4, n5, n6, n7, n8, n9, n10, n11, n12, n13, n14, n15, n16, n17, n18, n19, n20, + N0, N1, N2, N3, N4, N5, N6, N7, N8, N9, N10, N11, N12, N13, N14, N15, N16, N17, N18, N19, N20, + sN0, sN1, sN2, sN3, sN4, sN5, sN6, sN7, sN8, sN9, sN10, sN11, sN12, sN13, sN14, + sN15, sN16, sN17, sN18, sN19, sN20 + ) where import Data.Singletons import Data.Type.Monomorphic import Prelude (Int, Bool (..), Eq (..), Integral (..), Ord ((<)), @@ -275,77 +275,6 @@ instance Preorder Leq where reflexivity = leqRefl transitivity = leqTrans - -{- -singletons [d| - (<<) :: Nat -> Nat -> Bool - Zero << Succ n = True - n << Zero = False - Succ n << Succ m = n << m - (<<=) :: Nat -> Nat -> Bool - Zero <<= _ = True - Succ n <<= Zero = False - Succ n <<= Succ m = n <<= m - |] - -type a :>> b = b :<< a -type a :> b = b :<: a - -type a :<=: b = a :<: b :\/: a :=: b - -instance FromBool (n :<: m) where - type Predicate (n :<: m) = n :<< m - type Args (n :<: m) = '[Sing n, Sing m] - fromBool = boolToPropLt - -boolToPropLt :: (x :<< y) ~ True => SNat x -> SNat y -> x :<: y -boolToPropLt SZ (SS _) = ZeroLtSucc -boolToPropLt (SS n) (SS m) = SuccLtSucc $ boolToPropLt n m -boolToPropLt _ _ = bugInGHC - -instance FromBool (n :<=: m) where - type Predicate (n :<=: m) = n :<<= m - type Args (n :<=: m) = '[Sing n, Sing m] - fromBool = boolToPropLe - -boolToPropLe :: (x :<<= y) ~ True => SNat x -> SNat y -> x :<=: y -boolToPropLe SZ SZ = Right Refl -boolToPropLe SZ (SS _) = Left ZeroLtSucc -boolToPropLe (SS n) (SS m) = - case boolToPropLe n m of - Left reason -> Left $ SuccLtSucc reason - Right Refl -> Right Refl -boolToPropLe _ _ = bugInGHC - -rev :: (n :<<= m) ~ False => SNat n -> SNat m -> m :<: n -rev (SS _) SZ = ZeroLtSucc -rev (SS n) (SS m) = SuccLtSucc $ rev n m -rev _ _ = bugInGHC - -leTrans :: forall n m l. n :<=: m -> m :<=: l -> n :<=: l -leTrans (Right Refl) a = a -leTrans a (Right Refl) = a -leTrans (Left ZeroLtSucc) (Left (SuccLtSucc _)) = Left ZeroLtSucc -leTrans (Left (SuccLtSucc a)) (Left (SuccLtSucc b)) = - case leTrans (Left a) (Left b) of - Right Refl -> Right Refl - Left le -> Left $ SuccLtSucc le -leTrans _ _ = bugInGHC - -nLtSn :: SNat n -> n :<: Succ n -nLtSn SZ = ZeroLtSucc -nLtSn (SS n) = SuccLtSucc (nLtSn n) - -comparable :: SNat n -> SNat m -> n :<: m :\/: n :=: m :\/: m :<: n -comparable SZ SZ = orIntroR (orIntroL Refl) -comparable SZ (SS _) = orIntroL ZeroLtSucc -comparable (SS _) SZ = orIntroR (orIntroR ZeroLtSucc) -comparable (SS n) (SS m) = - case comparable n m of - Left nLTm -> orIntroL $ SuccLtSucc nLTm - Right (Left Refl) -> orIntroR $ orIntroL Refl - Right (Right mLTn) -> orIntroR $ orIntroR $ SuccLtSucc mLTn --} -------------------------------------------------- -- * Properties diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -7,12 +7,12 @@ ( -- * Data-types Ordinal (..), -- * Conversion from cardinals to ordinals. - sNatToOrd', sNatToOrd, ordToInt, ordToSNat, + sNatToOrd', sNatToOrd, ordToInt, ordToSNat, unsafeFromInt, -- * Ordinal arithmetics - (@+) + (@+), enumOrdinal ) where import Data.Type.Monomorphic -import Data.Type.Natural +import Data.Type.Natural hiding (promote) -- | Set-theoretic (finite) ordinals: -- @@ -27,11 +27,56 @@ instance Read (Ordinal Z) where readsPrec _ _ = [] +instance SingRep n => Num (Ordinal n) where + _ + _ = error "Finite ordinal is not closed under addition." + _ - _ = error "Ordinal subtraction is not defined" + negate OZ = OZ + negate _ = error "There are no negative oridnals!" + OZ * _ = OZ + _ * OZ = OZ + _ * _ = error "Finite ordinal is not closed under multiplication" + abs = id + signum = error "What does Ordinal sign mean?" + fromInteger = unsafeFromInt . fromInteger + deriving instance Read (Ordinal n) => Read (Ordinal (S n)) deriving instance Show (Ordinal n) deriving instance Eq (Ordinal n) deriving instance Ord (Ordinal n) +instance SingRep 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 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 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 + minBound = OZ + maxBound = + case propToBoolLeq $ leqRefl (sing :: SNat n) of + LeqTrueInstance -> sNatToOrd (sing :: SNat n) + +unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n +unsafeFromInt n = + case promote n of + Monomorphic sn -> + case sS sn %:<<= (sing :: SNat n) of + STrue -> sNatToOrd' (sing :: SNat n) sn + SFalse -> error "Bound over!" + -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. sNatToOrd' :: (S m :<<= n) ~ True => SNat n -> SNat m -> Ordinal n sNatToOrd' (SS _) SZ = OZ @@ -80,4 +125,3 @@ case sing :: SNat n of SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m _ -> bugInGHC - diff --git a/type-natural.cabal b/type-natural.cabal --- a/type-natural.cabal +++ b/type-natural.cabal @@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural -version: 0.0.4.0 +version: 0.0.5.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