type-natural 0.0.6.0 → 0.1.0.0
raw patch · 3 files changed
+51/−30 lines, 3 filesdep +constraints
Dependencies added: constraints
Files
- Data/Type/Natural.hs +45/−27
- Data/Type/Ordinal.hs +4/−2
- type-natural.cabal +2/−1
Data/Type/Natural.hs view
@@ -17,9 +17,9 @@ (:+:), (:+), (%+), (%:+), (:*:), (:*), (%:*), (%*), (:-:), (:-), (%:-), (%-), -- ** Type-level predicate & judgements- Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance(..), leqRefl, leqSucc,+ Leq(..), (:<=), (:<<=), (%:<<=), LeqInstance, leqRefl, leqSucc, boolToPropLeq, boolToClassLeq, propToClassLeq,- LeqTrueInstance(..), propToBoolLeq,+ LeqTrueInstance, propToBoolLeq, -- * Conversion functions natToInt, intToNat, sNatToInt, -- * Quasi quotes for natural numbers@@ -52,7 +52,9 @@ Show (..), error, id, otherwise, ($), (.), undefined) import qualified Prelude as P import Proof.Equational+import Data.Constraint hiding ((:-)) import Language.Haskell.TH.Quote+import Unsafe.Coerce import Language.Haskell.TH --------------------------------------------------@@ -203,8 +205,7 @@ ZeroLeq :: SNat m -> Leq Zero m SuccLeqSucc :: Leq n m -> Leq (S n) (S m) -data LeqTrueInstance a b where- LeqTrueInstance :: (a :<<= b) ~ True => LeqTrueInstance a b+type LeqTrueInstance a b = Dict ((a :<<= b) ~ True) (%-) :: (n :<<= m) ~ True => SNat n -> SNat m -> SNat (n :-: m) n %- SZ = n@@ -224,33 +225,53 @@ -------------------------------------------------- -- * Total orderings on natural numbers. ---------------------------------------------------propToBoolLeq :: Leq n m -> LeqTrueInstance n m-propToBoolLeq (ZeroLeq _) = LeqTrueInstance-propToBoolLeq (SuccLeqSucc leq) =- case propToBoolLeq leq of- LeqTrueInstance -> LeqTrueInstance+propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m+propToBoolLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE propToBoolLeq #-} -data LeqInstance n m where- LeqInstance :: (n :<= m) => LeqInstance n m+boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m+boolToClassLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE boolToClassLeq #-} -boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m-boolToPropLeq SZ m = ZeroLeq m-boolToPropLeq (SS n) (SS m) = SuccLeqSucc $ boolToPropLeq n m-boolToPropLeq _ _ = bugInGHC+propToClassLeq :: Leq n m -> LeqInstance n m+propToClassLeq _ = unsafeCoerce (Dict :: Dict ())+{-# INLINE propToClassLeq #-} +{-+-- | Below is the "proof" of the correctness of above:+propToBoolLeq :: Leq n m -> LeqTrueInstance n m+propToBoolLeq (ZeroLeq _) = Dict+propToBoolLeq (SuccLeqSucc leq) = case propToBoolLeq leq of Dict -> Dict+{-# RULES+ "propToBoolLeq/unsafeCoerce" forall (x :: Leq n m) .+ propToBoolLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict ((n :<<= m) ~ True)+ #-}+ boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m-boolToClassLeq SZ _ = LeqInstance-boolToClassLeq (SS n) (SS m) =- case boolToClassLeq n m of- LeqInstance -> LeqInstance+boolToClassLeq SZ _ = Dict+boolToClassLeq (SS n) (SS m) = case boolToClassLeq n m of Dict -> Dict boolToClassLeq _ _ = bugInGHC+{-# RULES+ "boolToClassLeq/unsafeCoerce" forall (n :: SNat n) (m :: SNat m).+ boolToClassLeq n m = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)+ #-} propToClassLeq :: Leq n m -> LeqInstance n m-propToClassLeq (ZeroLeq _) = LeqInstance-propToClassLeq (SuccLeqSucc leq) =- case propToClassLeq leq of- LeqInstance -> LeqInstance+propToClassLeq (ZeroLeq _) = Dict+propToClassLeq (SuccLeqSucc leq) = case propToClassLeq leq of Dict -> Dict+{-# RULES+ "propToClassLeq/unsafeCoerce" forall (x :: Leq n m) .+ propToClassLeq x = unsafeCoerce (Dict :: Dict ()) :: Dict (n :<= m)+ #-}+-} +type LeqInstance n m = Dict (n :<= m)++boolToPropLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> Leq n m+boolToPropLeq SZ m = ZeroLeq m+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@@ -326,9 +347,6 @@ Refl -> SuccLeqSucc $ plusMonotone (ZeroLeq m) leq plusMonotone (SuccLeqSucc leq) leq' = SuccLeqSucc $ plusMonotone leq leq' -infer :: Proxy a-infer = Proxy- plusCongL :: SNat n -> m :=: m' -> n :+ m :=: n :+ m' plusCongL _ Refl = Refl @@ -394,7 +412,7 @@ plusMinusEqL SZ m = minusNilpotent m plusMinusEqL (SS n) m = case propToBoolLeq (plusLeqR n m) of- LeqTrueInstance -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m)+ Dict -> transitivity (eqSuccMinus (n %+ m) m) (eqPreservesS $ plusMinusEqL n m) plusMinusEqR :: SNat n -> SNat m -> (m :+: n) :-: m :=: n plusMinusEqR n m = transitivity (minusCongEq (plusCommutative m n) m) (plusMinusEqL n m)
Data/Type/Ordinal.hs view
@@ -15,6 +15,7 @@ ) where import Data.Type.Monomorphic import Data.Type.Natural hiding (promote)+import Data.Constraint -- | Set-theoretic (finite) ordinals: --@@ -69,7 +70,7 @@ minBound = OZ maxBound = case propToBoolLeq $ leqRefl (sing :: SNat n) of- LeqTrueInstance -> sNatToOrd (sing :: SNat n)+ Dict -> sNatToOrd (sing :: SNat n) unsafeFromInt :: forall n. SingRep n => Int -> Ordinal n unsafeFromInt n = @@ -132,8 +133,9 @@ in case singInstance (sn %+ sm) of SingInstance -> case propToBoolLeq (plusLeqR sn sm) of- LeqTrueInstance -> inclusion n+ Dict -> inclusion n OS n @+ m = case sing :: SNat n of SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m _ -> bugInGHC+
type-natural.cabal view
@@ -2,7 +2,7 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.0.6.0+version: 0.1.0.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@@ -27,3 +27,4 @@ , equational-reasoning == 0.0.* , monomorphic >= 0.0.3 , template-haskell == 2.8.*+ , constraints == 0.3.*