diff --git a/Data/Type/Natural.hs b/Data/Type/Natural.hs --- a/Data/Type/Natural.hs +++ b/Data/Type/Natural.hs @@ -1,48 +1,32 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} +{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} +{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-} +{-# LANGUAGE TypeOperators, UndecidableInstances, EmptyCase, LambdaCase #-} -- | 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(..), -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 SSym0, SSym1, ZSym0, -#endif -- | 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, -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 MinSym0, MinSym1, MinSym2, MaxSym0, MaxSym1, MaxSym2, -#endif (:+:), (:+), -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 (:+$), (:+$$), (:+$$$), -#endif (%+), (%:+), (:*), (:*:), -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 (:*$), (:*$$), (:*$$$), -#endif (%:*), (%*), (:-:), (:-), (:**:), (:**), (%:**), (%**), -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 (:-$), (:-$$), (:-$$$), -#endif (%:-), (%-), -- ** Type-level predicate & judgements Leq(..), (:<=), (:<<=), -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 (:<<=$),(:<<=$$),(:<<=$$$), -#endif (%:<<=), LeqInstance, boolToPropLeq, boolToClassLeq, propToClassLeq, LeqTrueInstance, propToBoolLeq, @@ -52,13 +36,13 @@ nat, snat, -- * Properties of natural numbers succCongEq, plusCongR, plusCongL, succPlusL, succPlusR, - plusZR, plusZL, eqPreservesS, plusAssociative, + pluSZR, pluSZL, eqPreserveSS, plusAssociative, multAssociative, multComm, multZL, multZR, multOneL, multOneR, snEqZAbsurd, succInjective, plusInjectiveL, plusInjectiveR, plusMultDistr, multPlusDistr, multCongL, multCongR, sAndPlusOne, plusCommutative, minusCongEq, minusNilpotent, eqSuccMinus, plusMinusEqL, plusMinusEqR, - zAbsorbsMinR, zAbsorbsMinL, plusSR, plusNeutralR, plusNeutralL, + zAbsorbsMinR, zAbsorbsMinL, pluSSR, plusNeutralR, plusNeutralL, leqRhs, leqLhs, minComm, maxZL, maxComm, maxZR, -- * Properties of ordering 'Leq' leqRefl, leqSucc, leqTrans, plusMonotone, plusLeqL, plusLeqR, @@ -69,49 +53,34 @@ 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, -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 ZeroSym0, OneSym0, TwoSym0, ThreeSym0, FourSym0, FiveSym0, SixSym0, SevenSym0, EightSym0, NineSym0, TenSym0, ElevenSym0, TwelveSym0, ThirteenSym0, FourteenSym0, FifteenSym0, SixteenSym0, SeventeenSym0, EighteenSym0, NineteenSym0, TwentySym0, -#endif 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, -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 N0Sym0, N1Sym0, N2Sym0, N3Sym0, N4Sym0, N5Sym0, N6Sym0, N7Sym0, N8Sym0, N9Sym0, N10Sym0, N11Sym0, N12Sym0, N13Sym0, N14Sym0, N15Sym0, N16Sym0, N17Sym0, N18Sym0, N19Sym0, N20Sym0, -#endif 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 -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 -import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2, - Min, MinSym0, MinSym1, MinSym2, SOrd (..)) -import Data.Singletons.TH (singletons) -#endif +import Data.Type.Natural.Compat +import Data.Type.Natural.Core +import Data.Type.Natural.Definitions hiding ((:<=)) + import Data.Constraint hiding ((:-)) +import Data.Singletons import Data.Type.Monomorphic import Language.Haskell.TH import Language.Haskell.TH.Quote import Prelude (Bool (..), Eq (..), Int, - Integral (..), Ord ((<)), Show (..), - error, id, otherwise, undefined, - ($), (.)) + Integral (..), Ord ((<)), error, + otherwise, ($), (.)) +import Prelude (Ord (..)) import qualified Prelude as P import Proof.Equational -import Unsafe.Coerce -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710 -import Data.Type.Natural.Definitions hiding ((:<=)) --- import Data.Type.Natural.Proofs.GHC710 -import Prelude (Num (..), Ord (..)) -#else -import Data.Type.Natural.Definitions --- import Data.Type.Natural.Proofs.GHC708 -#endif -import Data.Type.Natural.Core -------------------------------------------------- -- * Conversion functions. @@ -139,37 +108,32 @@ demote (Monomorphic sn) = sNatToInt sn promote n | n < 0 = error "negative integer!" -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 708 - | n == 0 = Monomorphic sZ - | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ sS sn -#else | n == 0 = Monomorphic SZ | otherwise = withPolymorhic (n P.- 1) $ \sn -> Monomorphic $ SS sn -#endif -------------------------------------------------- -- * Properties -------------------------------------------------- -plusZR :: SNat n -> n :+: Z :=: n -plusZR SZ = Refl -plusZR (SS n) = +pluSZR :: SNat n -> n :+: 'Z :=: n +pluSZR SZ = Refl +pluSZR (SS n) = start (SS n %+ SZ) =~= SS (n %+ SZ) - === SS n `because` cong' SS (plusZR n) + === SS n `because` cong' SS (pluSZR n) -eqPreservesS :: n :=: m -> S n :=: S m -eqPreservesS Refl = Refl +eqPreserveSS :: n :=: m -> 'S n :=: 'S m +eqPreserveSS Refl = Refl -plusZL :: SNat n -> Z :+: n :=: n -plusZL _ = Refl +pluSZL :: SNat n -> 'Z :+: n :=: n +pluSZL _ = Refl -succCongEq :: n :=: m -> S n :=: S m +succCongEq :: n :=: m -> 'S n :=: 'S m succCongEq Refl = Refl -snEqZAbsurd :: S n :=: Z -> a -snEqZAbsurd _ = bugInGHC "impossible!" +snEqZAbsurd :: 'S n :=: 'Z -> a +snEqZAbsurd _ = bugInGHC -succInjective :: S n :=: S m -> n :=: m +succInjective :: 'S n :=: 'S m -> n :=: m succInjective Refl = Refl plusInjectiveL :: SNat n -> SNat m -> SNat l -> n :+ m :=: n :+ l -> m :=: l @@ -183,7 +147,7 @@ === m %:+ l `because` eq === l %:+ m `because` plusCommutative m l -sAndPlusOne :: SNat n -> S n :=: n :+: One +sAndPlusOne :: SNat n -> 'S n :=: n :+: One sAndPlusOne SZ = Refl sAndPlusOne (SS n) = start (SS (SS n)) @@ -200,8 +164,8 @@ =~= SS (n %+ m) %+ l =~= (SS n %+ m) %+ l -plusSR :: SNat n -> SNat m -> S (n :+: m) :=: n :+: S m -plusSR n m = +pluSSR :: SNat n -> SNat m -> 'S (n :+: m) :=: n :+: 'S m +pluSSR n m = start (SS (n %+ m)) === (n %+ m) %+ sOne `because` sAndPlusOne (n %+ m) === n %+ (m %+ sOne) `because` symmetry (plusAssociative n m sOne) @@ -213,10 +177,10 @@ plusCongR :: SNat n -> m :=: m' -> m :+ n :=: m' :+ n plusCongR _ Refl = Refl -succPlusL :: SNat n -> SNat m -> S n :+ m :=: S (n :+ m) +succPlusL :: SNat n -> SNat m -> 'S n :+ m :=: 'S (n :+ m) succPlusL _ _ = Refl -succPlusR :: SNat n -> SNat m -> n :+ S m :=: S (n :+ m) +succPlusR :: SNat n -> SNat m -> n :+ 'S m :=: 'S (n :+ m) succPlusR SZ _ = Refl succPlusR (SS n) m = start (SS n %+ SS m) @@ -249,32 +213,35 @@ === m %+ (n %+ sOne) `because` symmetry (plusAssociative m n sOne) === m %+ SS n `because` plusCongL m (symmetry $ sAndPlusOne n) -eqSuccMinus :: ((m :<<= n) ~ True) - => SNat n -> SNat m -> (S n :-: m) :=: (S (n :-: m)) +eqSuccMinus :: ((m :<<= n) ~ 'True) + => SNat n -> SNat m -> ('S n :-: m) :=: ('S (n :-: m)) eqSuccMinus _ SZ = Refl eqSuccMinus (SS n) (SS m) = start (SS (SS n) %:- SS m) =~= SS n %:- m === SS (n %:- m) `because` eqSuccMinus n m =~= SS (SS n %:- SS m) +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 eqSuccMinus _ _ = bugInGHC +#endif + plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n plusMinusEqL SZ m = minusNilpotent m plusMinusEqL (SS n) m = case propToBoolLeq (plusLeqR n m) of - Dict -> 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) -zAbsorbsMinR :: SNat n -> Min n Z :=: Z +zAbsorbsMinR :: SNat n -> Min n 'Z :=: 'Z zAbsorbsMinR SZ = Refl zAbsorbsMinR (SS n) = case zAbsorbsMinR n of Refl -> Refl -zAbsorbsMinL :: SNat n -> Min Z n :=: Z +zAbsorbsMinL :: SNat n -> Min 'Z n :=: 'Z zAbsorbsMinL SZ = Refl zAbsorbsMinL (SS n) = case zAbsorbsMinL n of Refl -> Refl @@ -284,7 +251,7 @@ minComm (SS _) SZ = Refl minComm (SS n) (SS m) = case minComm n m of Refl -> Refl -maxZL :: SNat n -> Max Z n :=: n +maxZL :: SNat n -> Max 'Z n :=: n maxZL SZ = Refl maxZL (SS _) = Refl @@ -294,7 +261,7 @@ maxComm (SS _) SZ = Refl maxComm (SS n) (SS m) = case maxComm n m of Refl -> Refl -maxZR :: SNat n -> Max n Z :=: n +maxZR :: SNat n -> Max n 'Z :=: n maxZR n = transitivity (maxComm n SZ) (maxZL n) multPlusDistr :: forall n m l. SNat n -> SNat m -> SNat l -> n :* (m :+ l) :=: (n :* m) :+ (n :* l) @@ -380,14 +347,14 @@ === 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 :: 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 :: 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 @@ -401,14 +368,16 @@ leqRefl SZ = ZeroLeq SZ leqRefl (SS n) = SuccLeqSucc $ leqRefl n -leqSucc :: SNat n -> Leq n (S 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 +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 leqTrans _ _ = error "impossible!" +#endif instance Preorder Leq where reflexivity = leqRefl @@ -417,12 +386,12 @@ 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 + 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 SZ m = ZeroLeq $ coerce (symmetry $ pluSZL m) m plusLeqL (SS n) m = start (SS n) =<= SS (n %+ m) `because` SuccLeqSucc (plusLeqL n m) @@ -443,8 +412,10 @@ leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m leqAnitsymmetric (ZeroLeq _) (ZeroLeq _) = Refl -leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreservesS $ leqAnitsymmetric leq1 leq2 -leqAnitsymmetric _ _ = bugInGHC +leqAnitsymmetric (SuccLeqSucc leq1) (SuccLeqSucc leq2) = eqPreserveSS $ leqAnitsymmetric leq1 leq2 +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +leqAnitsymmetric _ _ = error "impossible!" +#endif maxLeqL :: SNat n -> SNat m -> Leq n (Max n m) maxLeqL SZ m = ZeroLeq (sMax SZ m) @@ -456,28 +427,37 @@ maxLeqR n m = case maxComm n m of Refl -> maxLeqL m n -leqSnZAbsurd :: Leq (S n) Z -> a -leqSnZAbsurd _ = error "cannot be occured" +leqSnZAbsurd :: Leq ('S n) 'Z -> a +leqSnZAbsurd = \case {} -leqnZElim :: Leq n Z -> n :=: Z +leqnZElim :: Leq n 'Z -> n :=: 'Z leqnZElim (ZeroLeq SZ) = Refl -leqSnLeq :: Leq (S n) m -> Leq n m +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 +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +leqSnLeq _ = bugInGHC +#endif -leqPred :: Leq (S n) (S m) -> Leq n m +leqPred :: Leq ('S n) ('S m) -> Leq n m leqPred (SuccLeqSucc leq) = leq +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +leqPred _ = bugInGHC +#endif -leqSnnAbsurd :: Leq (S n) n -> a +leqSnnAbsurd :: Leq ('S n) n -> a leqSnnAbsurd (SuccLeqSucc leq) = case leqLhs leq of SS _ -> leqSnnAbsurd leq +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 _ -> bugInGHC "cannot be occured" +leqSnnAbsurd _ = bugInGHC +#endif -------------------------------------------------- -- * Quasi Quoter diff --git a/Data/Type/Natural/Builtin.hs b/Data/Type/Natural/Builtin.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Builtin.hs @@ -0,0 +1,328 @@ +{-# LANGUAGE ConstraintKinds, CPP, DataKinds, GADTs, PolyKinds, RankNTypes #-} +{-# LANGUAGE TypeFamilies, TypeOperators, UndecidableInstances #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Presburger #-} +{-# OPTIONS_GHC -fplugin GHC.TypeLits.Normalise #-} +-- | Coercion between Peano Numerals @'Data.Type.Natural.Nat'@ and builtin naturals @'GHC.TypeLits.Nat'@ +module Data.Type.Natural.Builtin + ( -- * Sysnonym to avoid confusion + Peano, + -- * Coercion between builtin type-level natural and peano numerals + FromPeano, ToPeano, sFromPeano, sToPeano, + -- * Properties of @'FromPeano'@ and @'ToPeano'@. + fromPeanoInjective, toPeanoInjective, + -- ** Bijection + fromToPeano, toFromPeano, + -- ** Algebraic isomorphisms + fromPeanoZeroCong, toPeanoZeroCong, + fromPeanoOneCong, toPeanoOneCong, + fromPeanoSuccCong, toPeanoSuccCong, + fromPeanoPlusCong, toPeanoPlusCong, + fromPeanoMultCong, toPeanoMultCong, + fromPeanoMonotone, toPeanoMonotone, + -- * Peano and commutative ring axioms for built-in @'GHC.TypeLits.Nat'@ + plusZR, plusZL, plusSuccR, plusSuccL, + multZR, multZL, multSuccR, multSuccL, + inductionNat, + plusComm, multComm, plusAssoc, multAssoc, + plusMultDistr, multPlusDistr + ) + where +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +import Data.Type.Natural.Compat +#endif + +import Data.Promotion.Prelude.Enum (Succ) +import Data.Singletons (Sing, SingI, sing) +import Data.Singletons.Decide (Decision (..), (%~)) +import Data.Singletons.Decide (Void) +import Data.Singletons.Prelude.Bool (Sing (..)) +import Data.Singletons.Prelude.Enum (Pred, sPred, sSucc) +import Data.Singletons.Prelude.Num (SNum (..)) +import Data.Type.Natural (Nat (S, Z), Sing (SS, SZ)) +import Data.Type.Natural (plusCongR, succCongEq) +import qualified Data.Type.Natural as PN +import Data.Void (absurd) +import qualified GHC.TypeLits as TL +import Proof.Equational ((:=:), (:~:) (Refl), coerce) +import Proof.Equational (start, sym, (===), (=~=)) +import Proof.Equational (because) +import Unsafe.Coerce (unsafeCoerce) + +-- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@. +type Peano = PN.Nat + +type family FromPeano (n :: PN.Nat) :: TL.Nat where + FromPeano 'Z = 0 + FromPeano ('S n) = Succ (FromPeano n) + +type family ToPeano (n :: TL.Nat) :: PN.Nat where + ToPeano 0 = 'Z + ToPeano n = 'S (ToPeano (Pred n)) + +data NatView (n :: TL.Nat) where + IsZero :: NatView 0 + IsSucc :: Sing n -> NatView (Succ n) + +viewNat :: Sing n -> NatView n +viewNat n = + case n %~ (sing :: Sing 0) of + Proved Refl -> IsZero + Disproved _ -> IsSucc (sPred n) + +sFromPeano :: Sing n -> Sing (FromPeano n) +sFromPeano SZ = sing +sFromPeano (SS sn) = sSucc (sFromPeano sn) + +toPeanoInjective :: ToPeano n :=: ToPeano m -> n :=: m +toPeanoInjective Refl = Refl + +-- trustMe :: a :=: b +-- trustMe = unsafeCoerce (Refl :: () :=: ()) +-- {-# WARNING trustMe +-- "Used unproven type-equalities; This may cause disastrous result..." #-} + +toPeanoSuccCong :: Sing n -> ToPeano (Succ n) :=: 'S (ToPeano n) +toPeanoSuccCong _ = unsafeCoerce (Refl :: () :=: ()) + -- We cannot prove this lemma within Haskell, so we assume it a priori. + +sToPeano :: Sing n -> Sing (ToPeano n) +sToPeano sn = + case sn %~ (sing :: Sing 0) of + Proved Refl -> SZ + Disproved _pf -> coerce (sym (toPeanoSuccCong (sPred sn))) (SS (sToPeano (sPred sn))) + +-- litSuccInjective :: forall (n :: TL.Nat) (m :: TL.Nat). +-- Succ n :=: Succ m -> n :=: m +-- litSuccInjective Refl = Refl + +toFromPeano :: Sing n -> ToPeano (FromPeano n) :=: n +toFromPeano SZ = Refl +toFromPeano (SS sn) = + start (sToPeano (sFromPeano (SS sn))) + =~= sToPeano (sSucc (sFromPeano sn)) + === SS (sToPeano (sFromPeano sn)) `because` toPeanoSuccCong (sFromPeano sn) + === SS sn `because` succCongEq (toFromPeano sn) + +congFromPeano :: n :=: m -> FromPeano n :=: FromPeano m +congFromPeano Refl = Refl + +congToPeano :: n :=: m -> ToPeano n :=: ToPeano m +congToPeano Refl = Refl + +congSucc :: n :=: m -> Succ n :=: Succ m +congSucc Refl = Refl + +fromToPeano :: Sing n -> FromPeano (ToPeano n) :=: n +fromToPeano sn = + case viewNat sn of + IsZero -> Refl + IsSucc n1 -> + start (sFromPeano (sToPeano sn)) + =~= sFromPeano (sToPeano (sSucc n1)) + === sFromPeano (SS (sToPeano n1)) + `because` congFromPeano (toPeanoSuccCong n1) + =~= sSucc (sFromPeano (sToPeano n1)) + === sSucc n1 `because` congSucc (fromToPeano n1) + +fromPeanoInjective :: forall n m. (SingI n, SingI m) + => FromPeano n :=: FromPeano m -> n :=: m +fromPeanoInjective frEq = + let sn = sing :: Sing n + sm = sing :: Sing m + in start sn + === sToPeano (sFromPeano sn) `because` sym (toFromPeano sn) + === sToPeano (sFromPeano sm) `because` congToPeano frEq + === sm `because` toFromPeano sm + +fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :=: Succ (FromPeano n) +fromPeanoSuccCong _sn = Refl + +fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :=: FromPeano n TL.+ FromPeano m +fromPeanoPlusCong SZ _ = Refl +fromPeanoPlusCong (SS sn) sm = + start (sFromPeano (SS sn %:+ sm)) + =~= sFromPeano (SS (sn %:+ sm)) + === sSucc (sFromPeano (sn %:+ sm)) `because` fromPeanoSuccCong (sn %:+ sm) + === sSucc (sFromPeano sn %:+ sFromPeano sm) `because` congSucc (fromPeanoPlusCong sn sm) + =~= sSucc (sFromPeano sn) %:+ sFromPeano sm + =~= sFromPeano (SS sn) %:+ sFromPeano sm + +toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n TL.+ m) :=: ToPeano n PN.:+ ToPeano m +toPeanoPlusCong sn sm = + case viewNat sn of + IsZero -> Refl + IsSucc pn -> + start (sToPeano (sSucc pn %:+ sm)) + =~= sToPeano (sSucc (pn %:+ sm)) + === SS (sToPeano (pn %:+ sm)) + `because` toPeanoSuccCong (pn %:+ sm) + === SS (sToPeano pn %:+ sToPeano sm) + `because` succCongEq (toPeanoPlusCong pn sm) + =~= SS (sToPeano pn) %:+ sToPeano sm + === (sToPeano (sSucc pn) %:+ sToPeano sm) + `because` plusCongR (sToPeano sm) (sym (toPeanoSuccCong pn)) + =~= sToPeano sn %:+ sToPeano sm + +fromPeanoZeroCong :: FromPeano 'Z :=: 0 +fromPeanoZeroCong = Refl + +toPeanoZeroCong :: ToPeano 0 :=: 'Z +toPeanoZeroCong = Refl + +fromPeanoOneCong :: FromPeano PN.One :=: 1 +fromPeanoOneCong = Refl + +toPeanoOneCong :: ToPeano 1 :=: PN.One +toPeanoOneCong = Refl + +natPlusCongR :: Sing r -> n :=: m -> n TL.+ r :=: m TL.+ r +natPlusCongR _ Refl = Refl + +fromPeanoMultCong :: Sing n -> Sing m -> FromPeano (n PN.:* m) :=: FromPeano n TL.* FromPeano m +fromPeanoMultCong SZ _ = Refl +fromPeanoMultCong (SS psn) sm = + start (sFromPeano (SS psn %:* sm)) + =~= sFromPeano (psn %:* sm %:+ sm) + === sFromPeano (psn %:* sm) %:+ sFromPeano sm + `because` fromPeanoPlusCong (psn %:* sm) sm + === sFromPeano psn %:* sFromPeano sm %:+ sFromPeano sm + `because` natPlusCongR (sFromPeano sm) (fromPeanoMultCong psn sm) + =~= sSucc (sFromPeano psn) %:* sFromPeano sm + =~= sFromPeano (SS psn) %:* sFromPeano sm + + +toPeanoMultCong :: Sing n -> Sing m -> ToPeano (n PN.:* m) :=: ToPeano n PN.:* ToPeano m +toPeanoMultCong sn sm = + case viewNat sn of + IsZero -> Refl + IsSucc psn -> + start (sToPeano (sSucc psn %:* sm)) + =~= sToPeano (psn %:* sm %:+ sm) + === sToPeano (psn %:* sm) %:+ sToPeano sm + `because` toPeanoPlusCong (psn %:* sm) sm + === sToPeano psn %:* sToPeano sm %:+ sToPeano sm + `because` plusCongR (sToPeano sm) (toPeanoMultCong psn sm) + =~= SS (sToPeano psn) %:* sToPeano sm + === sToPeano (sSucc psn) %:* sToPeano sm + `because` PN.multCongR (sToPeano sm) (sym (toPeanoSuccCong psn)) + +infix 4 %:<=? +(%:<=?) :: Sing n -> Sing m -> Sing (n TL.<=? m) +sn %:<=? sm = + case viewNat sn of + IsZero -> STrue + IsSucc pn -> case viewNat sm of + IsZero -> SFalse + IsSucc pm -> + case pn %:<=? pm of + STrue -> STrue + SFalse -> SFalse + +natLeqSuccEq :: Sing n -> Sing m -> ((n TL.+ 1) TL.<=? (m TL.+ 1)) :~: (n TL.<=? m) +natLeqSuccEq _ _ = Refl + +leqqCong :: n :=: m -> l :=: z -> (n TL.<=? l) :~: (m TL.<=? z) +leqqCong Refl Refl = Refl + +leqCong :: n :=: m -> l :=: z -> (n PN.:<<= l) :~: (m PN.:<<= z) +leqCong Refl Refl = Refl + +fromPeanoMonotone :: ((n PN.:<<= m) ~ 'True) => Sing n -> Sing m -> (FromPeano n TL.<=? FromPeano m) :=: 'True +fromPeanoMonotone SZ _ = Refl +fromPeanoMonotone (SS n) (SS m) = + start (sFromPeano (SS n) %:<=? sFromPeano (SS m)) + === (sSucc (sFromPeano n) %:<=? sSucc (sFromPeano m)) + `because` leqqCong (fromPeanoSuccCong n) (fromPeanoSuccCong m) + === (sFromPeano n %:<=? sFromPeano m) + `because` natLeqSuccEq (sFromPeano n) (sFromPeano m) + === STrue + `because` fromPeanoMonotone n m +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +fromPeanoMonotone _ _ = bugInGHC +#endif + +natLeqZero :: (n TL.<= 0) => Sing n -> n :~: 0 +natLeqZero _ = Refl + +-- | Currently, ghc-typelits-natnormalise reduces @(0 - 1) + 1@ to @0@, +-- which is contradictory to current GHC's behaviour. +-- So our assumption @((n :~: 0) -> Void)@ is simply disregarded. +natSuccPred :: ((n :~: 0) -> Void) -> Succ (Pred n) :=: n +natSuccPred _ = Refl + +myLeqPred :: Sing n -> Sing m -> ('S n PN.:<<= 'S m) :=: (n PN.:<<= m) +myLeqPred SZ _ = Refl +myLeqPred (SS _) (SS _) = Refl +myLeqPred (SS _) SZ = Refl + +toPeanoCong :: a :=: b -> ToPeano a :=: ToPeano b +toPeanoCong Refl = Refl + +toPeanoMonotone :: (n TL.<= m) + => Sing n -> Sing m -> ((ToPeano n) PN.:<<= (ToPeano m)) :~: 'True +toPeanoMonotone sn sm = + case sn %~ (sing :: Sing 0) of + Proved Refl -> Refl + Disproved nPos -> case sm %~ (sing :: Sing 0) of + Proved Refl -> absurd $ nPos $ natLeqZero sm + Disproved mPos -> + let pn = sPred sn + pm = sPred sm + in start (sToPeano sn PN.%:<<= sToPeano sm) + === (sToPeano (sSucc pn) PN.%:<<= sToPeano (sSucc pm)) + `because` leqCong (toPeanoCong $ sym $ natSuccPred nPos) + (toPeanoCong $ sym $ natSuccPred mPos) + === (SS (sToPeano pn) PN.%:<<= SS (sToPeano pm)) + `because` leqCong (toPeanoSuccCong pn) (toPeanoSuccCong pm) + === (sToPeano pn PN.%:<<= sToPeano pm) + `because` myLeqPred (sToPeano pn) (sToPeano pm) + === STrue `because` toPeanoMonotone pn pm + +-- | Induction scheme for built-in @'TL.Nat'@. +inductionNat :: forall p n. p 0 -> (forall m. p m -> p (m TL.+ 1)) -> Sing n -> p n +inductionNat base step snat = + case viewNat snat of + IsZero -> base + IsSucc sl -> step (inductionNat base step sl) + +plusZR :: Sing n -> n TL.+ 0 :~: n +plusZR _ = Refl + +plusZL :: Sing n -> 0 TL.+ n :~: n +plusZL _ = Refl + +plusSuccL :: Sing n -> Sing m -> (Succ n) TL.+ m :~: Succ (n TL.+ m) +plusSuccL _ _ = Refl + +plusSuccR :: Sing n -> Sing m -> n TL.+ (Succ m) :~: Succ (n TL.+ m) +plusSuccR _ _ = Refl + +multZL :: Sing n -> 0 TL.* n :~: 0 +multZL _ = Refl + +multZR :: Sing n -> n TL.* 0 :~: 0 +multZR _ = Refl + +multSuccL :: Sing n -> Sing m -> Succ n TL.* m :~: (n TL.* m) TL.+ m +multSuccL _ _ = Refl + +multSuccR :: Sing n -> Sing m -> n TL.* Succ m :~: (n TL.* m) TL.+ n +multSuccR _ _ = Refl + +plusComm :: Sing n -> Sing m -> (n TL.+ m) :~: (m TL.+ n) +plusComm _ _ = Refl + +multComm :: Sing n -> Sing m -> (n TL.* m) :~: (m TL.* n) +multComm _ _ = Refl + +plusAssoc :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.+ l :~: n TL.+ (m TL.+ l) +plusAssoc _ _ _ = Refl + +multAssoc :: Sing n -> Sing m -> Sing l -> (n TL.* m) TL.* l :~: n TL.* (m TL.* l) +multAssoc _ _ _ = Refl + +plusMultDistr :: Sing n -> Sing m -> Sing l -> (n TL.+ m) TL.* l :~: n TL.* l TL.+ m TL.* l +plusMultDistr _ _ _ = Refl + +multPlusDistr :: Sing n -> Sing m -> Sing l -> n TL.* (m TL.+ l) :~: n TL.* m TL.+ n TL.* l +multPlusDistr _ _ _ = Refl diff --git a/Data/Type/Natural/Compat.hs b/Data/Type/Natural/Compat.hs new file mode 100644 --- /dev/null +++ b/Data/Type/Natural/Compat.hs @@ -0,0 +1,8 @@ +{-# LANGUAGE CPP #-} +module Data.Type.Natural.Compat (bugInGHC) where +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +import Data.Singletons.Prelude (bugInGHC) +#else +bugInGHC :: a +bugInGHC = error "GHC case-analysis error!" +#endif diff --git a/Data/Type/Natural/Core.hs b/Data/Type/Natural/Core.hs --- a/Data/Type/Natural/Core.hs +++ b/Data/Type/Natural/Core.hs @@ -1,75 +1,47 @@ -{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} -{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} -{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables, StandaloneDeriving #-} -{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} +{-# LANGUAGE CPP, DataKinds, FlexibleContexts, FlexibleInstances, GADTs #-} +{-# LANGUAGE KindSignatures, MultiParamTypeClasses, NoImplicitPrelude #-} +{-# LANGUAGE PolyKinds, RankNTypes, ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving, TemplateHaskell, TypeFamilies #-} +{-# LANGUAGE TypeOperators, UndecidableInstances #-} module Data.Type.Natural.Core where -import Data.Singletons -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 708 -import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2, - Min, MinSym0, MinSym1, MinSym2, SOrd (..)) -import Data.Singletons.TH (singletons) -#endif -import Data.Constraint hiding ((:-)) -import Data.Type.Monomorphic -import Language.Haskell.TH -import Language.Haskell.TH.Quote -import Prelude (Bool (..), Eq (..), Int, - Integral (..), Ord ((<)), Show (..), - error, id, otherwise, undefined, - ($), (.)) -import qualified Prelude as P -import Proof.Equational -import Unsafe.Coerce -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 710 -import Data.Type.Natural.Definitions hiding ((:<=)) -import Prelude (Num (..)) -#else -import Data.Type.Natural.Definitions +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +import Data.Type.Natural.Compat #endif - --------------------------------------------------- --- ** Convenient synonyms --------------------------------------------------- - -#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 +import Data.Constraint hiding ((:-)) +import Data.Type.Natural.Definitions hiding ((:<=)) +import Prelude (Bool (..), Eq (..), Show (..), ($)) +import Unsafe.Coerce -------------------------------------------------- -- ** Type-level predicate & judgements. -------------------------------------------------- -- | Comparison via type-class. class (n :: Nat) :<= (m :: Nat) -instance Z :<= n -instance (n :<= m) => S n :<= S m +instance 'Z :<= n +instance (n :<= m) => 'S n :<= 'S m -- | Comparison via GADTs. data Leq (n :: Nat) (m :: Nat) where ZeroLeq :: SNat m -> Leq Zero m - SuccLeqSucc :: Leq n m -> Leq (S n) (S m) + SuccLeqSucc :: Leq n m -> Leq ('S n) ('S m) -type LeqTrueInstance a b = Dict ((a :<<= b) ~ True) +type LeqTrueInstance a b = Dict ((a :<<= b) ~ 'True) -(%-) :: (m :<<= n) ~ True => SNat n -> SNat m -> SNat (n :-: m) +(%-) :: (m :<<= n) ~ 'True => SNat n -> SNat m -> SNat (n :-: m) n %- SZ = n SS n %- SS m = n %- m -_ %- _ = error "impossible!" +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +_ %- _ = bugInGHC +#endif infixl 6 %- deriving instance Show (SNat n) deriving instance Eq (SNat n) data (a :: Nat) :<: (b :: Nat) where - ZeroLtSucc :: Zero :<: S m - SuccLtSucc :: n :<: m -> S n :<: S m + ZeroLtSucc :: Zero :<: 'S m + SuccLtSucc :: n :<: m -> 'S n :<: 'S m deriving instance Show (a :<: b) @@ -80,7 +52,7 @@ propToBoolLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE propToBoolLeq #-} -boolToClassLeq :: (n :<<= m) ~ True => SNat n -> SNat m -> LeqInstance n m +boolToClassLeq :: (n :<<= m) ~ 'True => SNat n -> SNat m -> LeqInstance n m boolToClassLeq _ = unsafeCoerce (Dict :: Dict ()) {-# INLINE boolToClassLeq #-} @@ -93,40 +65,30 @@ 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 _ = 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 _) = 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 :: (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 +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +boolToPropLeq _ _ = bugInGHC +#endif leqRhs :: Leq n m -> SNat m leqRhs (ZeroLeq m) = m -leqRhs (SuccLeqSucc leq) = sS $ leqRhs leq +leqRhs (SuccLeqSucc leq) = SS $ leqRhs leq leqLhs :: Leq n m -> SNat n -leqLhs (ZeroLeq _) = sZ -leqLhs (SuccLeqSucc leq) = sS $ leqLhs leq +leqLhs (ZeroLeq _) = SZ +leqLhs (SuccLeqSucc leq) = SS $ leqLhs leq diff --git a/Data/Type/Natural/Definitions.hs b/Data/Type/Natural/Definitions.hs --- a/Data/Type/Natural/Definitions.hs +++ b/Data/Type/Natural/Definitions.hs @@ -22,21 +22,13 @@ import Data.Singletons.Prelude hiding ((:<=), Max, MaxSym0, MaxSym1, MaxSym2, Min, MinSym0, MinSym1, MinSym2, SOrd (..)) #endif -import Data.Singletons.TH (singletons) #endif -import Data.Constraint hiding ((:-)) -import Data.Type.Monomorphic -import Data.Typeable (Typeable) -import Language.Haskell.TH -import Language.Haskell.TH.Quote -import Prelude (Bool (..), Eq (..), Int, - Integral (..), Ord ((<)), Show (..), - error, id, otherwise, undefined, - ($), (.)) -import qualified Prelude as P -import Proof.Equational -import Unsafe.Coerce +import Data.Typeable (Typeable) +import Prelude (Bool (..), Eq (..), Show (..)) +import qualified Prelude as P + + -------------------------------------------------- -- * Natural numbers and its singleton type -------------------------------------------------- @@ -113,7 +105,7 @@ abs n = n signum Z = Z - signum (S n) = S Z + signum (S _) = S Z fromInteger n = if n == 0 then Z else S (fromInteger (n-1)) |] @@ -159,7 +151,7 @@ singletons [d| (**) :: Nat -> Nat -> Nat - n ** Z = S Z + _ ** Z = S Z n ** S m = (n ** m) * n |] diff --git a/Data/Type/Ordinal.hs b/Data/Type/Ordinal.hs --- a/Data/Type/Ordinal.hs +++ b/Data/Type/Ordinal.hs @@ -1,11 +1,7 @@ -{-# LANGUAGE DeriveDataTypeable #-} -{-# LANGUAGE CPP, DataKinds, EmptyDataDecls, FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures, PolyKinds #-} -{-# LANGUAGE ScopedTypeVariables, StandaloneDeriving, TemplateHaskell #-} -{-# LANGUAGE TypeFamilies, TypeOperators #-} -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -{-# LANGUAGE EmptyCase, LambdaCase #-} -#endif +{-# LANGUAGE CPP, DataKinds, DeriveDataTypeable, EmptyCase, EmptyDataDecls #-} +{-# LANGUAGE FlexibleContexts, FlexibleInstances, GADTs, KindSignatures #-} +{-# LANGUAGE LambdaCase, PolyKinds, ScopedTypeVariables, StandaloneDeriving #-} +{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-} -- | Set-theoretic ordinal arithmetic module Data.Type.Ordinal ( -- * Data-types @@ -21,34 +17,33 @@ -- * Quasi Quoter od ) where +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 +import Data.Type.Natural.Compat +#endif + +import Control.Monad (liftM) import Data.Constraint +import Data.Singletons.Prelude import Data.Type.Monomorphic -import Data.Type.Natural hiding (promote) +import Data.Type.Natural +import Data.Typeable (Typeable) import Language.Haskell.TH import Language.Haskell.TH.Quote -import Proof.Equational (coerce) import Unsafe.Coerce -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 -import Data.Singletons.Prelude -import Data.Typeable (Typeable) -#endif -import Control.Monad (liftM) -- | Set-theoretic (finite) ordinals: -- -- > n = {0, 1, ..., n-1} -- --- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal Z@ is isomorphic to @Void@. +-- So, @Ordinal n@ has exactly n inhabitants. So especially @Ordinal 'Z@ is isomorphic to @Void@. data Ordinal n where - OZ :: Ordinal (S n) - OS :: Ordinal n -> Ordinal (S n) + OZ :: Ordinal ('S n) + OS :: Ordinal n -> Ordinal ('S n) -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 --- | Since 0.2.3.0 +-- | Since 0.2.3.0 deriving instance Typeable Ordinal -#endif -- | Parsing always fails, because there are no inhabitant. -instance Read (Ordinal Z) where +instance Read (Ordinal 'Z) where readsPrec _ _ = [] instance SingI n => Num (Ordinal n) where @@ -63,7 +58,7 @@ signum = error "What does Ordinal sign mean?" fromInteger = unsafeFromInt . fromInteger -deriving instance Read (Ordinal n) => Read (Ordinal (S n)) +deriving instance Read (Ordinal n) => Read (Ordinal ('S n)) deriving instance Show (Ordinal n) deriving instance Eq (Ordinal n) deriving instance Ord (Ordinal n) @@ -87,7 +82,7 @@ enumOrdinal SZ = [] enumOrdinal (SS n) = OZ : map OS (enumOrdinal n) -instance SingI n => Bounded (Ordinal (S n)) where +instance SingI n => Bounded (Ordinal ('S n)) where minBound = OZ maxBound = case propToBoolLeq $ leqRefl (sing :: SNat n) of @@ -97,38 +92,32 @@ unsafeFromInt n = case (promote n :: Monomorphic (Sing :: Nat -> *)) of Monomorphic sn -> -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707 - case singInstance sn of - SingInstance -> -#endif 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' :: ('S m :<<= n) ~ 'True => SNat n -> SNat m -> Ordinal n sNatToOrd' (SS _) SZ = OZ sNatToOrd' (SS n) (SS m) = OS $ sNatToOrd' n m +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 sNatToOrd' _ _ = bugInGHC +#endif -- | 'sNatToOrd'' with @n@ inferred. -sNatToOrd :: (SingI 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 - CastedOrdinal :: (S m :<<= n) ~ True => SNat m -> CastedOrdinal n + CastedOrdinal :: ('S m :<<= n) ~ 'True => SNat m -> CastedOrdinal n --- | Convert @Ordinal n@ into @SNat m@ with the proof of @S m :<<= n@. +-- | Convert @Ordinal n@ into @SNat m@ with the proof of @'S m :<<= n@. ordToSNat' :: Ordinal n -> CastedOrdinal n ordToSNat' OZ = CastedOrdinal SZ ordToSNat' (OS on) = case ordToSNat' on of CastedOrdinal m -> -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 707 - case singInstance m of - SingInstance -> -#endif - CastedOrdinal (SS m) + CastedOrdinal (SS m) -- | Convert @Ordinal n@ into monomorphic @SNat@ ordToSNat :: Ordinal n -> Monomorphic (Sing :: Nat -> *) @@ -145,12 +134,12 @@ ordToInt (OS n) = 1 + ordToInt n -- | Inclusion function for ordinals. -inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m +inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-} {- -- The "proof" of the correctness of the above -inclusion' :: (n :<<= m) ~ True => SNat m -> Ordinal n -> Ordinal m +inclusion' :: (n :<<= m) ~ 'True => SNat m -> Ordinal n -> Ordinal m inclusion' (SS SZ) OZ = OZ inclusion' (SS (SS _)) OZ = OZ inclusion' (SS (SS n)) (OS m) = OS $ inclusion' (SS n) m @@ -158,7 +147,7 @@ -} -- | Inclusion function for ordinals with codomain inferred. -inclusion :: ((n :<<= m) ~ True) => Ordinal n -> Ordinal m +inclusion :: ((n :<<= m) ~ 'True) => Ordinal n -> Ordinal m inclusion on = unsafeCoerce on {-# INLINE inclusion #-} @@ -172,30 +161,28 @@ OS n @+ m = case sing :: SNat n of SS sn -> case singInstance sn of SingInstance -> OS $ n @+ m +#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 800 _ -> bugInGHC +#endif --- | Since @Ordinal Z@ is logically not inhabited, we can coerce it to any value. +-- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. -- -- Since 0.2.3.0 -absurdOrd :: Ordinal Z -> a -#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 707 +absurdOrd :: Ordinal 'Z -> a absurdOrd cs = case cs of {} -#else -absurdOrd _ = error "Impossible!" -#endif -- | 'absurdOrd' for the value in 'Functor'. --- +-- -- Since 0.2.3.0 -vacuousOrd :: Functor f => f (Ordinal Z) -> f a +vacuousOrd :: Functor f => f (Ordinal 'Z) -> f a vacuousOrd = fmap absurdOrd -- | 'absurdOrd' for the value in 'Monad'. -- This function will become uneccesary once 'Applicative' (and hence 'Functor') -- become the superclass of 'Monad'. --- +-- -- Since 0.2.3.0 -vacuousOrdM :: Monad m => m (Ordinal Z) -> m a +vacuousOrdM :: Monad m => m (Ordinal 'Z) -> m a vacuousOrdM = liftM absurdOrd -- | Quasiquoter for ordinals 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.3.0.0 +version: 0.4.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 @@ -13,9 +13,8 @@ copyright: (C) Hiromi ISHII 2013-2014 category: Math build-type: Simple -cabal-version: >=1.8 -tested-with: GHC == 7.8.3, GHC == 7.8.4, - GHC == 7.10.2 +cabal-version: >= 1.10 +tested-with: GHC == 7.10.3, GHC == 8.0.1 source-repository head Type: git @@ -23,18 +22,34 @@ library - exposed-modules: Data.Type.Natural, Data.Type.Ordinal - other-modules: Data.Type.Natural.Definitions, - Data.Type.Natural.Core - build-depends: base >= 4 && < 5 - , equational-reasoning == 0.2.* - , monomorphic >= 0.0.3 - , template-haskell >= 2.8 && < 2.11 - , constraints >= 0.3 && < 0.5 - if impl(ghc < 7.8) - build-depends: singletons == 0.8.* - else - if impl(ghc < 7.10) - build-depends: singletons == 1.* - else - build-depends: singletons == 2.0.* + ghc-options: -Wall -O2 -fno-warn-orphans + if impl(ghc >= 8.0.0) + ghc-options: -Wno-redundant-constraints + exposed-modules: Data.Type.Natural + , Data.Type.Ordinal + , Data.Type.Natural.Builtin + other-modules: Data.Type.Natural.Definitions + , Data.Type.Natural.Core + , Data.Type.Natural.Compat + build-depends: base >= 4 && < 5 + , equational-reasoning == 0.4.* + , monomorphic >= 0.0.3 + , template-haskell >= 2.8 && < 3 + , constraints >= 0.3 && < 0.9 + , ghc-typelits-natnormalise == 0.4.* + , ghc-typelits-presburger == 0.1.* + , singletons >= 2.0 && < 2.3 + + default-language: Haskell2010 + default-extensions: DataKinds + PolyKinds + ConstraintKinds + GADTs + ScopedTypeVariables + TemplateHaskell + TypeFamilies + TypeOperators + MultiParamTypeClasses + UndecidableInstances + FlexibleContexts + FlexibleInstances