type-natural 0.5.0.0 → 0.6.0.0
raw patch · 6 files changed
+182/−225 lines, 6 filesdep ~singletons
Dependency ranges changed: singletons
Files
- Data/Type/Natural.hs +9/−28
- Data/Type/Natural/Builtin.hs +7/−10
- Data/Type/Natural/Class/Arithmetic.hs +54/−52
- Data/Type/Natural/Class/Order.hs +43/−27
- Data/Type/Ordinal.hs +65/−104
- type-natural.cabal +4/−4
Data/Type/Natural.hs view
@@ -25,8 +25,7 @@ (:-$), (:-$$), (:-$$$), (%:-), (%-), -- ** Type-level predicate & judgements- Leq(..), (:<=),- LeqInstance,+ Leq(..), (:<=), LeqInstance, boolToPropLeq, boolToClassLeq, propToClassLeq, propToBoolLeq, -- * Conversion functions@@ -35,10 +34,10 @@ nat, snat, -- * Properties of natural numbers IsPeano(..),- plusCongR, plusCongL, snEqZAbsurd,- plusInjectiveL, plusInjectiveR,- multCongL, multCongR,- plusMinusEqL, leqRhs, leqLhs,+ plusCong, plusCongR, plusCongL,+ snEqZAbsurd, plusInjectiveL, plusInjectiveR,+ multCongL, multCongR, multCong,+ plusMinusEqL, plusNeutralR, plusNeutralL, -- * Properties of ordering 'Leq' PeanoOrder(..),@@ -65,11 +64,6 @@ import Data.Type.Natural.Class hiding (One, Zero, sOne, sZero) import Data.Type.Natural.Core import Data.Type.Natural.Definitions hiding ((:<=))--#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800-import Data.Kind-#endif- import Data.Singletons import Data.Singletons.Prelude.Ord import Data.Singletons.Decide@@ -114,7 +108,8 @@ -------------------------------------------------- -- | Since 0.5.0.0-instance IsPeano ('KProxy :: KProxy Nat) where+instance IsPeano Nat where+ {-# SPECIALISE instance IsPeano Nat #-} induction base _step SZ = base induction base step (SS n) = step n (induction base step n) @@ -154,18 +149,6 @@ === m %:+ l `because` eq === l %:+ m `because` plusComm m l --- 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- reflToSEqual :: SNat n -> SNat m -> n :~: m -> IsTrue (n :== m) reflToSEqual SZ _ Refl = Witness reflToSEqual (SS n) (SS m) Refl =@@ -217,7 +200,8 @@ STrue -> Refl SFalse -> case sleqFlip n m $ snequalToNoRefl n m Witness of {} -instance PeanoOrder ('KProxy :: KProxy Nat) where+instance PeanoOrder Nat where+ {-# SPECIALISE instance PeanoOrder Nat #-} leqZero _ = Witness leqSucc _ _ Witness = Witness viewLeq SZ n Witness = LeqZero n@@ -228,9 +212,6 @@ case n %:== m of SFalse -> case n %:<= m of STrue -> Witness- _ -> bugInGHC- _ -> bugInGHC- eqlCmpEQ n m Refl = case n %:== m of STrue -> Refl
Data/Type/Natural/Builtin.hs view
@@ -27,13 +27,11 @@ ) where import Data.Type.Natural.Class-import Data.Type.Natural.Compat import Data.Singletons.Decide (SDecide (..)) import Data.Singletons.Decide (Decision (..))-import Data.Singletons.Prelude (PNum (..), SNum (..), Sing (..))+import Data.Singletons.Prelude (SNum (..), PNum(..), Sing (..)) import Data.Singletons.Prelude (SingI (..))-import Data.Singletons.Prelude (KProxy (..)) import Data.Singletons.Prelude (SingKind (..), SomeSing (..)) import Data.Singletons.Prelude.Enum (PEnum (..), SEnum (..)) import Data.Singletons.Prelude.Ord (POrd (..), SOrd (..))@@ -53,9 +51,6 @@ import Proof.Equational (because) import Proof.Propositional (Empty (..), IsTrue (..)) import Unsafe.Coerce (unsafeCoerce)-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800-import Data.Kind-#endif -- | Type synonym for @'PN.Nat'@ to avoid confusion with built-in @'TL.Nat'@. type Peano = PN.Nat@@ -142,7 +137,7 @@ fromPeanoSuccCong :: Sing n -> FromPeano ('S n) :~: Succ (FromPeano n) fromPeanoSuccCong _sn = Refl -fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n PN.:+ m) :~: FromPeano n :+ FromPeano m+fromPeanoPlusCong :: Sing n -> Sing m -> FromPeano (n :+ m) :~: FromPeano n :+ FromPeano m fromPeanoPlusCong SZ _ = Refl fromPeanoPlusCong (SS sn) sm = start (sFromPeano (SS sn %:+ sm))@@ -152,7 +147,7 @@ =~= sSucc (sFromPeano sn) %:+ sFromPeano sm =~= sFromPeano (SS sn) %:+ sFromPeano sm -toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n :+ m) :~: ToPeano n :+ ToPeano m+toPeanoPlusCong :: Sing n -> Sing m -> ToPeano (n + m) :~: ToPeano n :+ ToPeano m toPeanoPlusCong sn sm = case viewNat sn of IsZero -> Refl@@ -287,7 +282,8 @@ IsSucc sl -> step (inductionNat base step sl) -instance IsPeano ('KProxy :: KProxy TL.Nat) where+instance IsPeano TL.Nat where+ {-# SPECIALISE instance IsPeano TL.Nat #-} predSucc _ = Refl plusMinus _ _ = Refl succInj Refl = Refl@@ -344,7 +340,8 @@ MyLeqHelper n m 'EQ = 'True MyLeqHelper n m 'GT = 'False -instance PeanoOrder ('KProxy :: KProxy TL.Nat) where+instance PeanoOrder TL.Nat where+ {-# SPECIALISE instance PeanoOrder TL.Nat #-} eqlCmpEQ _ _ Refl = Refl ltToLeq _ _ Refl = Witness succLeqToLT m n Witness =
Data/Type/Natural/Class/Arithmetic.hs view
@@ -2,7 +2,7 @@ {-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-} {-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-} {-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}-{-# LANGUAGE ViewPatterns #-}+{-# LANGUAGE TypeInType, ViewPatterns #-} module Data.Type.Natural.Class.Arithmetic (Zero, One, S, sZero, sOne, ZeroOrSucc(..), plusCong, plusCongR, plusCongL, succCong,@@ -18,21 +18,21 @@ import Proof.Equational import Proof.Propositional -type family Zero (kproxy :: KProxy nat) :: nat where- Zero 'KProxy = FromInteger 0+type family Zero nat :: nat where+ Zero nat = FromInteger 0 -sZero :: (SNum kproxy) => Sing (Zero kproxy)+sZero :: (SNum nat) => Sing (Zero nat) sZero = sFromInteger (sing :: Sing 0) -type family One (kproxy :: KProxy nat) :: nat where- One 'KProxy = FromInteger 1+type family One nat :: nat where+ One nat = FromInteger 1 -sOne :: SNum kproxy => Sing (One kproxy)+sOne :: SNum nat => Sing (One nat) sOne = sFromInteger (sing :: Sing 1) type S n = Succ n -sS :: SEnum ('KProxy :: KProxy nat) => Sing (n :: nat) -> Sing (S n)+sS :: SEnum nat => Sing (n :: nat) -> Sing (S n) sS = sSucc predCong :: n :~: m -> Pred n :~: Pred m@@ -69,7 +69,7 @@ minusCongR _ Refl = Refl data ZeroOrSucc (n :: nat) where- IsZero :: ZeroOrSucc (Zero 'KProxy)+ IsZero :: ZeroOrSucc (Zero nat) IsSucc :: Sing n -> ZeroOrSucc (Succ n) newtype Assoc op n = Assoc { assocProof :: forall k l. Sing k -> Sing l ->@@ -81,11 +81,11 @@ newtype IdentityR op e (n :: nat) = IdentityR { idRProof :: Apply (op n) e :~: n } newtype IdentityL op e (n :: nat) = IdentityL { idLProof :: Apply (op e) n :~: n } -type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero 'KProxy) n+type PlusZeroR (n :: nat) = IdentityR (:+$$) (Zero nat) n newtype PlusSuccR (n :: nat) = PlusSuccR { plusSuccRProof :: forall m. Sing m -> n :+ S m :~: S (n :+ m) } -type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero 'KProxy) n+type PlusZeroL (n :: nat) = IdentityL (:+$$) (Zero nat) n newtype PlusSuccL (m :: nat) = PlusSuccL { plusSuccLProof :: forall n. Sing n -> S n :+ m :~: S (n :+ m) } @@ -93,48 +93,48 @@ type PlusComm = Comm (:+$$) -data MultZeroL n =- MultZeroL { multZeroLProof :: !(Zero ('KProxy :: KProxy nat) :* n :~: Zero 'KProxy) }-data MultZeroR (n :: nat) =- MultZeroR { multZeroRProof :: !(n :* Zero ('KProxy :: KProxy nat) :~: Zero 'KProxy) }+newtype MultZeroL (n :: nat) = MultZeroL { multZeroLProof :: Zero nat :* n :~: Zero nat }+newtype MultZeroR (n :: nat) =+ MultZeroR { multZeroRProof :: n :* Zero nat :~: Zero nat } newtype MultSuccL (m :: nat) = MultSuccL { multSuccLProof :: forall n. Sing n -> S n :* m :~: n :* m :+ m }-data MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n }+newtype MultSuccR (n :: nat) = MultSuccR { multSuccRProof :: forall m. Sing m -> n :* S m :~: n :* m :+ n } -data PlusMultDistrib n =+newtype PlusMultDistrib (n :: nat) = PlusMultDistrib { plusMultDistribProof :: forall m l. Sing m -> Sing l -> (n :+ m) :* l :~: n :* l :+ m :* l } -newtype PlusEqCancelL n = PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l+newtype PlusEqCancelL (n :: nat) =+ PlusEqCancelL { plusEqCancelLProof :: forall m l . Sing m -> Sing l -> n :+ m :~: n :+ l -> m :~: l } -data SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: !(Succ n :~: One 'KProxy :+ n) }+newtype SuccPlusL (n :: nat) = SuccPlusL { proofSuccPlusL :: Succ n :~: One nat :+ n } newtype MultEqCancelR n = MultEqCancelR { proofMultEqCancelR :: forall m l. Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m } -class (SDecide kproxy, SNum kproxy, SEnum kproxy, kproxy ~ 'KProxy)- => IsPeano (kproxy :: KProxy nat) where+class (SDecide nat, SNum nat, SEnum nat, nat ~ nat)+ => IsPeano nat where {-# MINIMAL succOneCong, succNonCyclic, predSucc, plusMinus, succInj, ( (plusZeroL, plusSuccL) | (plusZeroR, plusZeroL)) , ( (multZeroL, multSuccL) | (multZeroR, multSuccR)), induction #-} - succOneCong :: Succ (Zero kproxy) :~: One kproxy+ succOneCong :: Succ (Zero nat) :~: One nat succInj :: Succ n :~: Succ (m :: nat) -> n :~: m succInj' :: proxy n -> proxy' m -> Succ n :~: Succ (m :: nat) -> n :~: m succInj' _ _ = succInj- succNonCyclic :: Sing n -> Succ n :~: Zero kproxy -> Void- induction :: p (Zero kproxy) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k+ succNonCyclic :: Sing n -> Succ n :~: Zero nat -> Void+ induction :: p (Zero nat) -> (forall n. Sing n -> p n -> p (S n)) -> Sing k -> p k plusMinus :: Sing (n :: nat) -> Sing m -> n :+ m :- m :~: n - plusZeroL :: Sing n -> (Zero kproxy :+ n) :~: n+ plusZeroL :: Sing n -> (Zero nat :+ n) :~: n plusZeroL sn = idLProof (induction base step sn) where- base :: PlusZeroL (Zero kproxy)+ base :: PlusZeroL (Zero nat) base = IdentityL (plusZeroR sZero) step :: Sing (n :: nat) -> PlusZeroL n -> PlusZeroL (S n)@@ -146,7 +146,7 @@ plusSuccL :: Sing n -> Sing m -> S n :+ m :~: S (n :+ m :: nat) plusSuccL sn0 sm0 = plusSuccLProof (induction base step sm0) sn0 where- base :: PlusSuccL (Zero kproxy)+ base :: PlusSuccL (Zero nat) base = PlusSuccL $ \sn -> start (sS sn %:+ sZero) === sS sn `because` plusZeroR (sS sn)@@ -159,10 +159,10 @@ === sS (sS (sn %:+ sm)) `because` succCong (ih sn) === sS (sn %:+ sS sm) `because` succCong (sym $ plusSuccR sn sm) - plusZeroR :: Sing n -> (n :+ Zero kproxy) :~: n+ plusZeroR :: Sing n -> (n :+ Zero nat) :~: n plusZeroR sn = idRProof (induction base step sn) where- base :: PlusZeroR (Zero kproxy)+ base :: PlusZeroR (Zero nat) base = IdentityR (plusZeroL sZero) step :: Sing (n :: nat) -> PlusZeroR n -> PlusZeroR (S n)@@ -174,7 +174,7 @@ plusSuccR :: Sing n -> Sing m -> n :+ S m :~: S (n :+ m :: nat) plusSuccR sn0 = plusSuccRProof (induction base step sn0) where- base :: PlusSuccR (Zero kproxy)+ base :: PlusSuccR (Zero nat) base = PlusSuccR $ \sk -> start (sZero %:+ sS sk) === sS sk `because` plusZeroL (sS sk)@@ -190,7 +190,7 @@ plusComm :: Sing n -> Sing m -> n :+ m :~: (m :: nat) :+ n plusComm sn0 = commProof (induction base step sn0) where- base :: PlusComm (Zero kproxy)+ base :: PlusComm (Zero nat) base = Comm $ \sk -> start (sZero %:+ sk) === sk `because` plusZeroL sk@@ -207,7 +207,7 @@ -> (n :+ m) :+ l :~: n :+ (m :+ l) plusAssoc sn m l = assocProof (induction base step sn) m l where- base :: Assoc (:+$$) (Zero kproxy)+ base :: Assoc (:+$$) (Zero nat) base = Assoc $ \ sk sl -> start ((sZero %:+ sk) %:+ sl) === sk %:+ sl@@ -224,10 +224,10 @@ === sS sk %:+ (sl %:+ su) `because` sym (plusSuccL sk (sl %:+ su)) - multZeroL :: Sing n -> Zero kproxy :* n :~: Zero kproxy+ multZeroL :: Sing n -> Zero nat :* n :~: Zero nat multZeroL sn0 = multZeroLProof $ induction base step sn0 where- base :: MultZeroL (Zero kproxy)+ base :: MultZeroL (Zero nat) base = MultZeroL (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroL k -> MultZeroL (S k)@@ -240,7 +240,7 @@ multSuccL :: Sing (n :: nat) -> Sing m -> S n :* m :~: n :* m :+ m multSuccL sn0 sm0 = multSuccLProof (induction base step sm0) sn0 where- base :: MultSuccL (Zero kproxy)+ base :: MultSuccL (Zero nat) base = MultSuccL $ \sk -> start (sS sk %:* sZero) === sZero `because` multZeroR (sS sk)@@ -266,10 +266,10 @@ `because` succCong (plusCongL (sym $ multSuccR sk sm) sm) === sk %:* sS sm %:+ sS sm `because` sym (plusSuccR (sk %:* sS sm) sm) - multZeroR :: Sing n -> n :* Zero kproxy :~: Zero kproxy+ multZeroR :: Sing n -> n :* Zero nat :~: Zero nat multZeroR sn0 = multZeroRProof $ induction base step sn0 where- base :: MultZeroR (Zero kproxy)+ base :: MultZeroR (Zero nat) base = MultZeroR (multZeroR sZero) step :: Sing (k :: nat) -> MultZeroR k -> MultZeroR (S k)@@ -282,7 +282,7 @@ multSuccR :: Sing n -> Sing m -> n :* S m :~: n :* m :+ (n :: nat) multSuccR sn0 = multSuccRProof $ induction base step sn0 where- base :: MultSuccR (Zero kproxy)+ base :: MultSuccR (Zero nat) base = MultSuccR $ \sk -> start (sZero %:* sS sk) === sZero@@ -317,7 +317,7 @@ multComm :: Sing (n :: nat) -> Sing m -> n :* m :~: m :* n multComm sn0 = commProof (induction base step sn0) where- base :: Comm (:*$$) (Zero kproxy)+ base :: Comm (:*$$) (Zero nat) base = Comm $ \sk -> start (sZero %:* sk) === sZero `because` multZeroL sk@@ -330,7 +330,7 @@ === sk %:* sn %:+ sk `because` plusCongL (ih sk) sk === sk %:* sS sn `because` sym (multSuccR sk sn) - multOneR :: Sing n -> n :* One kproxy :~: n+ multOneR :: Sing n -> n :* One nat :~: n multOneR sn = start (sn %:* sOne) === sn %:* sS sZero `because` multCongR sn (sym $ succOneCong)@@ -338,7 +338,7 @@ === sZero %:+ sn `because` plusCongL (multZeroR sn) sn === sn `because` plusZeroL sn - multOneL :: Sing n -> One kproxy :* n :~: n+ multOneL :: Sing n -> One nat :* n :~: n multOneL sn = start (sOne %:* sn) === sn %:* sOne `because` multComm sOne sn@@ -348,7 +348,7 @@ -> (n :+ m) :* l :~: n :* l :+ m :* l plusMultDistrib sn0 = plusMultDistribProof $ induction base step sn0 where- base :: PlusMultDistrib (Zero kproxy)+ base :: PlusMultDistrib (Zero nat) base = PlusMultDistrib $ \sk sl -> start ((sZero %:+ sk) %:* sl) === (sk %:* sl)@@ -377,7 +377,7 @@ === m %:* n %:+ l %:* n `because` plusMultDistrib m l n === n %:* m %:+ n %:* l `because` plusCong (multComm m n) (multComm l n) - minusNilpotent :: Sing n -> n :- n :~: Zero kproxy+ minusNilpotent :: Sing n -> n :- n :~: Zero nat minusNilpotent n = start (n %:- n) === (sZero %:+ n) %:- n `because` minusCongL (sym $ plusZeroL n) n@@ -388,7 +388,7 @@ -> (n :* m) :* l :~: n :* (m :* l) multAssoc sn0 = assocProof $ induction base step sn0 where- base :: Assoc (:*$$) (Zero kproxy)+ base :: Assoc (:*$$) (Zero nat) base = Assoc $ \ m l -> start (sZero %:* m %:* l) === sZero %:* l `because` multCongL (multZeroL m) l@@ -406,7 +406,7 @@ plusEqCancelL :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ m :~: n :+ l -> m :~: l plusEqCancelL = plusEqCancelLProof . induction base step where- base :: PlusEqCancelL (Zero kproxy)+ base :: PlusEqCancelL (Zero nat) base = PlusEqCancelL $ \l m nlnm -> start l === sZero %:+ l `because` sym (plusZeroL l) === sZero %:+ m `because` nlnm@@ -429,10 +429,10 @@ === (m %:+ l) `because` nlml === (l %:+ m) `because` plusComm m l - succAndPlusOneL :: Sing n -> Succ n :~: One kproxy :+ n+ succAndPlusOneL :: Sing n -> Succ n :~: One nat :+ n succAndPlusOneL = proofSuccPlusL . induction base step where- base :: SuccPlusL (Zero kproxy)+ base :: SuccPlusL (Zero nat) base = SuccPlusL $ start (sSucc sZero) === sOne `because` succOneCong@@ -444,7 +444,7 @@ === sSucc (sOne %:+ sn) `because` succCong ih === sOne %:+ sSucc sn `because` sym (plusSuccR sOne sn) - succAndPlusOneR :: Sing n -> Succ n :~: n :+ One kproxy+ succAndPlusOneR :: Sing n -> Succ n :~: n :+ One nat succAndPlusOneR n = start (sSucc n) === sOne %:+ n `because` succAndPlusOneL n@@ -458,13 +458,13 @@ base = IsZero step sn _ = IsSucc sn - plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> n :~: Zero kproxy+ plusEqZeroL :: Sing n -> Sing m -> n :+ m :~: Zero nat -> n :~: Zero nat plusEqZeroL n m Refl = case zeroOrSucc n of IsZero -> Refl IsSucc pn -> absurd $ succNonCyclic (pn %:+ m) (sym $ plusSuccL pn m) - plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero kproxy -> m :~: Zero kproxy+ plusEqZeroR :: Sing n -> Sing m -> n :+ m :~: Zero nat -> m :~: Zero nat plusEqZeroR n m = plusEqZeroL m n . trans (plusComm m n) predUnique :: Sing (n :: nat) -> Sing m -> Succ n :~: m -> n :~: Pred m@@ -487,7 +487,7 @@ multEqCancelR :: Sing (n :: nat) -> Sing m -> Sing l -> n :* Succ l :~: m :* Succ l -> n :~: m multEqCancelR = proofMultEqCancelR . induction base step where- base :: MultEqCancelR (Zero kproxy)+ base :: MultEqCancelR (Zero nat) base = MultEqCancelR $ \m l zslmsl -> sym $ plusEqZeroR (m %:* l) m $ sym $ start sZero === sZero %:* l `because` sym (multZeroL l)@@ -512,7 +512,7 @@ === (m' %:* sSucc l %:+ sSucc l) `because` multSuccL m' (sSucc l) in succCong pf' `trans` sym sm'Em - succPred :: Sing n -> (n :~: Zero kproxy -> Void) -> Succ (Pred n) :~: n+ succPred :: Sing n -> (n :~: Zero nat -> Void) -> Succ (Pred n) :~: n succPred n nonZero = case zeroOrSucc n of IsZero -> absurd $ nonZero Refl@@ -534,8 +534,10 @@ refute [t| 'GT :~: 'EQ |] refute [t| 'True :~: 'False |] +pattern Zero :: forall nat (n :: nat). IsPeano nat => n ~ Zero nat => Sing n pattern Zero <- (zeroOrSucc -> IsZero) where Zero = sZero +pattern Succ :: forall nat (n :: nat). IsPeano nat => forall (n1 :: nat). n ~ Succ n1 => Sing n1 -> Sing n pattern Succ n <- (zeroOrSucc -> IsSucc n) where Succ n = sSucc n
Data/Type/Natural/Class/Order.hs view
@@ -1,7 +1,7 @@-{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}-{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies #-}+{-# LANGUAGE DataKinds, EmptyCase, ExplicitForAll, FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances, GADTs, KindSignatures #-}+{-# LANGUAGE MultiParamTypeClasses, PatternSynonyms, PolyKinds, RankNTypes #-}+{-# LANGUAGE ScopedTypeVariables, TemplateHaskell, TypeFamilies, TypeInType #-} module Data.Type.Natural.Class.Order (PeanoOrder(..), DiffNat(..), LeqView(..), FlipOrdering, sFlipOrdering, coerceLeqL, coerceLeqR,@@ -19,7 +19,7 @@ import Proof.Propositional data LeqView (n :: nat) (m :: nat) where- LeqZero :: Sing n -> LeqView (Zero 'KProxy) n+ LeqZero :: Sing n -> LeqView (Zero nat) n LeqSucc :: Sing n -> Sing m -> IsTrue (n :<= m) -> LeqView (Succ n) (Succ m) data DiffNat n m where@@ -28,15 +28,15 @@ newtype LeqWitPf n = LeqWitPf { leqWitPf :: forall m. Sing m -> IsTrue (n :<= m) -> DiffNat n m } newtype LeqStepPf n = LeqStepPf { leqStepPf :: forall m l. Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m) } -succDiffNat :: IsPeano ('KProxy :: KProxy nat)+succDiffNat :: IsPeano nat => Sing n -> Sing m -> DiffNat (n :: nat) m -> DiffNat (Succ n) (Succ m) succDiffNat _ _ (DiffNat n m) = coerce (plusSuccL n m) $ DiffNat (sSucc n) m -coerceLeqL :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) => n :~: m -> Sing l+coerceLeqL :: forall (n :: nat) m l . IsPeano nat => n :~: m -> Sing l -> IsTrue (n :<= l) -> IsTrue (m :<= l) coerceLeqL Refl _ Witness = Witness -coerceLeqR :: forall (n :: nat) m l . IsPeano ('KProxy :: KProxy nat) => Sing l -> n :~: m+coerceLeqR :: forall (n :: nat) m l . IsPeano nat => Sing l -> n :~: m -> IsTrue (l :<= n) -> IsTrue (l :<= m) coerceLeqR _ Refl Witness = Witness @@ -71,7 +71,7 @@ newtype LeqViewRefl n = LeqViewRefl { proofLeqViewRefl :: LeqView n n } -class (SOrd kproxy, IsPeano kproxy) => PeanoOrder (kproxy :: KProxy nat) where+class (SOrd nat, IsPeano nat) => PeanoOrder nat where {-# MINIMAL ( succLeqToLT, cmpZero, leqRefl | leqZero, leqSucc , viewLeq | leqWitness, leqStep@@ -133,7 +133,7 @@ ltToSuccLeq n m nLTm = leqNeqToSuccLeq n m (ltToLeq n m nLTm) (ltToNeq n m nLTm) - cmpZero :: Sing a -> Compare (Zero kproxy) (Succ a) :~: 'LT+ cmpZero :: Sing a -> Compare (Zero nat) (Succ a) :~: 'LT cmpZero sn = leqToLT sZero (sSucc sn) $ leqStep (sSucc sZero) (sSucc sn) sn $ start (sSucc sZero %:+ sn) === sSucc (sZero %:+ sn) `because` plusSuccL sZero sn@@ -147,13 +147,13 @@ === sFlipOrdering SLT `because` congFlipOrdering (leqToLT b a sbLEQa) =~= SGT - cmpZero' :: Sing a -> Either (Compare (Zero kproxy) a :~: 'EQ) (Compare (Zero kproxy) a :~: 'LT)+ cmpZero' :: Sing a -> Either (Compare (Zero nat) a :~: 'EQ) (Compare (Zero nat) a :~: 'LT) cmpZero' n = case zeroOrSucc n of IsZero -> Left $ eqlCmpEQ sZero n Refl IsSucc n' -> Right $ cmpZero n' - zeroNoLT :: Sing a -> Compare a (Zero kproxy) :~: 'LT -> Void+ zeroNoLT :: Sing a -> Compare a (Zero nat) :~: 'LT -> Void zeroNoLT n eql = case cmpZero' n of Left cmp0nEQ -> eliminate $@@ -207,8 +207,8 @@ ltSucc :: Sing (a :: nat) -> Compare a (Succ a) :~: 'LT ltSucc = proofLTSucc . induction base step where- base :: LTSucc (Zero kproxy)- base = LTSucc $ cmpZero (sZero :: Sing (Zero kproxy))+ base :: LTSucc (Zero nat)+ base = LTSucc $ cmpZero (sZero :: Sing (Zero nat)) step :: Sing (n :: nat) -> LTSucc n -> LTSucc (Succ n) step n (LTSucc ih) = LTSucc $@@ -220,7 +220,7 @@ -> Compare n (Succ m) :~: 'LT cmpSuccStepR = proofCmpSuccStepR . induction base step where- base :: CmpSuccStepR (Zero kproxy)+ base :: CmpSuccStepR (Zero nat) base = CmpSuccStepR $ \m _ -> cmpZero m step :: Sing (n :: nat) -> CmpSuccStepR n -> CmpSuccStepR (Succ n)@@ -254,7 +254,7 @@ === SLT `because` ltSucc n Right nLTm -> ltSuccLToLT n m nLTm - leqZero :: Sing n -> IsTrue (Zero kproxy :<= n)+ leqZero :: Sing n -> IsTrue (Zero nat :<= n) leqZero sn = case zeroOrSucc sn of IsZero -> leqRefl sn@@ -273,7 +273,7 @@ leqViewRefl :: Sing (n :: nat) -> LeqView n n leqViewRefl = proofLeqViewRefl . induction base step where- base :: LeqViewRefl (Zero kproxy)+ base :: LeqViewRefl (Zero nat) base = LeqViewRefl $ LeqZero sZero step :: Sing (n :: nat) -> LeqViewRefl n -> LeqViewRefl (Succ n) step n (LeqViewRefl nLEQn) =@@ -293,7 +293,7 @@ leqWitness :: Sing (n :: nat) -> Sing m -> IsTrue (n :<= m) -> DiffNat n m leqWitness = leqWitPf . induction base step where- base :: LeqWitPf (Zero kproxy)+ base :: LeqWitPf (Zero nat) base = LeqWitPf $ \sm _ -> coerce (plusZeroL sm) $ DiffNat sZero sm step :: Sing (n :: nat) -> LeqWitPf n -> LeqWitPf (Succ n)@@ -306,7 +306,7 @@ leqStep :: Sing (n :: nat) -> Sing m -> Sing l -> n :+ l :~: m -> IsTrue (n :<= m) leqStep = leqStepPf . induction base step where- base :: LeqStepPf (Zero kproxy)+ base :: LeqStepPf (Zero nat) base = LeqStepPf $ \k _ _ -> leqZero k step :: Sing (n :: nat) -> LeqStepPf n -> LeqStepPf (Succ n)@@ -394,7 +394,7 @@ `because` sym (plusAssoc n mMINn k) =~= m %:+ k - leqZeroElim :: Sing n -> IsTrue (n :<= Zero kproxy) -> n :~: Zero kproxy+ leqZeroElim :: Sing n -> IsTrue (n :<= Zero nat) -> n :~: Zero nat leqZeroElim n nLE0 = case viewLeq n sZero nLE0 of LeqZero _ -> Refl@@ -436,11 +436,11 @@ coerceLeqL (plusComm n m) (l %:+ n) $ coerceLeqR (n %:+ m) (plusComm n l) nmLEQnl - succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero kproxy) -> Void+ succLeqZeroAbsurd :: Sing n -> IsTrue (S n :<= Zero nat) -> Void succLeqZeroAbsurd n leq = succNonCyclic n (leqZeroElim (sSucc n) leq) - succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero kproxy) :~: 'False+ succLeqZeroAbsurd' :: Sing n -> (S n :<= Zero nat) :~: 'False succLeqZeroAbsurd' n = case sSucc n %:<= sZero of STrue -> absurd $ succLeqZeroAbsurd n Witness@@ -588,7 +588,7 @@ ltToLneq n m nLTm = coerce (sym $ lneqSuccLeq n m) $ ltToSuccLeq n m nLTm - lneqZero :: Sing (a :: nat) -> IsTrue (Zero kproxy :< Succ a)+ lneqZero :: Sing (a :: nat) -> IsTrue (Zero nat :< Succ a) lneqZero n = ltToLneq sZero (sSucc n) $ cmpZero n lneqSucc :: Sing (n :: nat) -> IsTrue (n :< Succ n)@@ -606,6 +606,18 @@ -> m :~: Succ (Pred m) lneqRightPredSucc n m nLNEQm = ltRightPredSucc n m $ lneqToLT n m nLNEQm + lneqSuccStepL :: Sing (n :: nat) -> Sing m -> IsTrue (Succ n :< m) -> IsTrue (n :< m)+ lneqSuccStepL n m snLNEQm =+ coerce (sym $ lneqSuccLeq n m) $+ leqSuccStepL (sSucc n) m $+ coerce (lneqSuccLeq (sSucc n) m) snLNEQm++ lneqSuccStepR :: Sing (n :: nat) -> Sing m -> IsTrue (n :< m) -> IsTrue (n :< Succ m)+ lneqSuccStepR n m nLNEQm =+ coerce (sym $ lneqSuccLeq n (sSucc m)) $+ leqSuccStepR (sSucc n) m $+ coerce (lneqSuccLeq n m) nLNEQm+ plusStrictMonotone :: Sing (n :: nat) -> Sing m -> Sing l -> Sing k -> IsTrue (n :< m) -> IsTrue (l :< k) -> IsTrue (n :+ l :< m :+ k)@@ -617,16 +629,16 @@ (leqTrans l (sSucc l) k (leqSuccStepR l l (leqRefl l)) $ coerce (lneqSuccLeq l k) lLNk) - maxZeroL :: Sing n -> Max (Zero kproxy) n :~: n+ maxZeroL :: Sing n -> Max (Zero nat) n :~: n maxZeroL n = leqToMax sZero n (leqZero n) - maxZeroR :: Sing n -> Max n (Zero kproxy) :~: n+ maxZeroR :: Sing n -> Max n (Zero nat) :~: n maxZeroR n = geqToMax n sZero (leqZero n) - minZeroL :: Sing n -> Min (Zero kproxy) n :~: Zero kproxy+ minZeroL :: Sing n -> Min (Zero nat) n :~: Zero nat minZeroL n = leqToMin sZero n (leqZero n) - minZeroR :: Sing n -> Min n (Zero kproxy) :~: Zero kproxy+ minZeroR :: Sing n -> Min n (Zero nat) :~: Zero nat minZeroR n = geqToMin n sZero (leqZero n) minusSucc :: Sing (n :: nat) -> Sing m -> IsTrue (m :<= n) -> Succ n :- m :~: Succ (n :- m)@@ -641,3 +653,7 @@ === sSucc (k %:+ m %:- m) `because` succCong (sym $ plusMinus k m) === sSucc (m %:+ k %:- m) `because` succCong (minusCongL (plusComm k m) m) =~= sSucc (n %:- m)++ lneqZeroAbsurd :: Sing n -> IsTrue (n :< Zero nat) -> Void+ lneqZeroAbsurd n leq =+ succLeqZeroAbsurd n (coerce (lneqSuccLeq n sZero) leq)
Data/Type/Ordinal.hs view
@@ -2,11 +2,12 @@ {-# LANGUAGE ExplicitNamespaces, FlexibleContexts, FlexibleInstances #-} {-# LANGUAGE GADTs, KindSignatures, LambdaCase, PatternSynonyms, PolyKinds #-} {-# LANGUAGE RankNTypes, ScopedTypeVariables, StandaloneDeriving #-}-{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeOperators #-}+{-# LANGUAGE TemplateHaskell, TypeFamilies, TypeInType, TypeOperators #-}+{-# LANGUAGE ViewPatterns #-} -- | Set-theoretic ordinals for general peano arithmetic models module Data.Type.Ordinal ( -- * Data-types- Ordinal (..), HasOrdinal,+ Ordinal (..), pattern OZ, pattern OS, HasOrdinal, -- * Conversion from cardinals to ordinals. sNatToOrd', sNatToOrd, ordToInt, ordToSing, ordToSing', CastedOrdinal(..),@@ -19,6 +20,7 @@ od ) where import Control.Monad (liftM)+import Data.Kind import Data.List (genericDrop, genericTake) import Data.Ord (comparing) import Data.Singletons.Prelude@@ -29,6 +31,7 @@ import Data.Type.Natural.Builtin () import Data.Type.Natural.Class import Data.Typeable (Typeable)+import Data.Void (absurd) import GHC.TypeLits (type (+)) import qualified GHC.TypeLits as TL import Language.Haskell.TH hiding (Type)@@ -36,11 +39,7 @@ import Proof.Equational import Proof.Propositional import Unsafe.Coerce-#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ >= 800-import Data.Kind-#endif - -- | Set-theoretic (finite) ordinals: -- -- > n = {0, 1, ..., n-1}@@ -49,65 +48,80 @@ -- -- Since 0.5.0.0 data Ordinal (n :: nat) where- OZ :: Sing n -> Ordinal (Succ n)- OS :: Ordinal n -> Ordinal (Succ n)- OLt :: (n :< m) ~ 'True => Sing n -> Ordinal m+ OLt :: (IsPeano nat, (n :< m) ~ 'True) => Sing (n :: nat) -> Ordinal m +fromOLt :: forall nat n m. (PeanoOrder nat, (Succ n :< Succ m) ~ 'True, SingI m)+ => Sing (n :: nat) -> Ordinal m+fromOLt n =+ case coerce (sym $ succLneqSucc n (sing :: Sing m)) Witness of+ Witness -> OLt n++-- | Pattern synonym representing the 0-th ordinal.+pattern OZ :: forall nat (n :: nat). IsPeano nat+ => (Zero nat :< n) ~ 'True => Ordinal n+pattern OZ <- OLt Zero where+ OZ = OLt sZero++-- | Pattern synonym @'OS' n@ represents (n+1)-th ordinal.+pattern OS :: forall nat (t :: nat). (PeanoOrder nat, SingI t)+ => (IsPeano nat)+ => Ordinal t -> Ordinal (Succ t)+pattern OS n <- OLt (Succ (fromOLt -> n)) where+ OS o = succOrd o+ -- | Since 0.2.3.0 deriving instance Typeable Ordinal -- | Class synonym for Peano numerals with ordinals. -- -- Since 0.5.0.0-class (PeanoOrder kproxy, Monomorphicable (Sing :: nat -> *),+class (PeanoOrder nat, Monomorphicable (Sing :: nat -> *), Integral (MonomorphicRep (Sing :: nat -> *)),- SingKind kproxy, kproxy ~ 'KProxy,- Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal (kproxy :: KProxy nat)-instance (PeanoOrder ('KProxy :: KProxy nat), Monomorphicable (Sing :: nat -> *),+ Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat+instance (PeanoOrder nat, Monomorphicable (Sing :: nat -> *), Integral (MonomorphicRep (Sing :: nat -> *)),- SingKind ('KProxy :: KProxy nat),- Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal ('KProxy :: KProxy nat)+ Show (MonomorphicRep (Sing :: nat -> *))) => HasOrdinal nat -instance (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))+instance (HasOrdinal nat, SingI (n :: nat)) => Num (Ordinal n) where {-# SPECIALISE instance SingI n => Num (Ordinal (n :: PN.Nat)) #-} {-# SPECIALISE instance SingI n => Num (Ordinal (n :: TL.Nat)) #-} _ + _ = error "Finite ordinal is not closed under addition." _ - _ = error "Ordinal subtraction is not defined"- negate (OZ pxy) = OZ pxy+ negate OZ = OZ negate _ = error "There are no negative oridnals!"- OZ pxy * _ = OZ pxy- _ * OZ pxy = OZ pxy+ OZ * _ = OZ+ _ * OZ = OZ _ * _ = error "Finite ordinal is not closed under multiplication" abs = id signum = error "What does Ordinal sign mean?"- fromInteger = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromInteger+ fromInteger = unsafeFromInt' (Proxy :: Proxy nat) . fromInteger -- deriving instance Read (Ordinal n) => Read (Ordinal (Succ n))-instance (SingI n, HasOrdinal ('KProxy :: KProxy nat))+instance (SingI n, HasOrdinal nat) => Show (Ordinal (n :: nat)) where {-# SPECIALISE instance SingI n => Show (Ordinal (n :: PN.Nat)) #-} {-# SPECIALISE instance SingI n => Show (Ordinal (n :: TL.Nat)) #-} showsPrec d o = showChar '#' . showParen True (showsPrec d (ordToInt o) . showString " / " . showsPrec d (demote $ Monomorphic (sing :: Sing n))) -instance (HasOrdinal ('KProxy :: KProxy nat))+instance (HasOrdinal nat) => Eq (Ordinal (n :: nat)) where {-# SPECIALISE instance Eq (Ordinal (n :: PN.Nat)) #-} {-# SPECIALISE instance Eq (Ordinal (n :: TL.Nat)) #-} o == o' = ordToInt o == ordToInt o' -instance (HasOrdinal ('KProxy :: KProxy nat)) => Ord (Ordinal (n :: nat)) where+instance (HasOrdinal nat) => Ord (Ordinal (n :: nat)) where compare = comparing ordToInt -instance (HasOrdinal ('KProxy :: KProxy nat), SingI n)+instance (HasOrdinal nat, SingI n) => Enum (Ordinal (n :: nat)) where fromEnum = fromIntegral . ordToInt- toEnum = unsafeFromInt' (Proxy :: Proxy ('KProxy :: KProxy nat)) . fromIntegral+ toEnum = unsafeFromInt' (Proxy :: Proxy nat) . fromIntegral enumFrom = enumFromOrd enumFromTo = enumFromToOrd enumFromToOrd :: forall (n :: nat).- (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ (HasOrdinal nat, SingI n) => Ordinal n -> Ordinal n -> [Ordinal n] enumFromToOrd ok ol = let k = ordToInt ok@@ -115,27 +129,22 @@ in genericTake (l - k + 1) $ enumFromOrd ok enumFromOrd :: forall (n :: nat).- (HasOrdinal ('KProxy :: KProxy nat), SingI n)+ (HasOrdinal nat, SingI n) => Ordinal n -> [Ordinal n] enumFromOrd ord = genericDrop (ordToInt ord) $ enumOrdinal (sing :: Sing n) -enumOrdinal :: (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Sing (n :: nat) -> [Ordinal n]+enumOrdinal :: (PeanoOrder nat, SingI n) => Sing (n :: nat) -> [Ordinal n] enumOrdinal (Succ n) = withSingI n $ case lneqZero n of Witness -> OLt sZero : map succOrd (enumOrdinal n) enumOrdinal _ = [] -succOrd :: forall (n :: nat). (SingKind ('KProxy :: KProxy nat), PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> Ordinal (Succ n)+succOrd :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> Ordinal (Succ n) succOrd (OLt n) = case succLneqSucc n (sing :: Sing n) of Refl -> OLt (sSucc n)-succOrd (OZ n) =- case (succLneqSucc sZero (sSucc n), lneqZero n) of- (Refl, Witness) -> OLt $ coerce (sym succOneCong) sOne-succOrd (OS o) =- case (succLneqSucc sZero (sSucc (sing :: Sing n)), lneqZero (sing :: Sing n)) of- (Refl, Witness) -> OS (OS o)+{-# INLINE succOrd #-} instance SingI n => Bounded (Ordinal ('PN.S n)) where minBound = OLt PN.SZ@@ -155,7 +164,7 @@ {-# INLINE maxBound #-} -unsafeFromInt :: forall (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI (n :: nat))+unsafeFromInt :: forall (n :: nat). (HasOrdinal nat, SingI (n :: nat)) => MonomorphicRep (Sing :: nat -> *) -> Ordinal n unsafeFromInt n = case promote (n :: MonomorphicRep (Sing :: nat -> *)) of@@ -164,8 +173,8 @@ STrue -> sNatToOrd' (sing :: Sing n) sn SFalse -> error "Bound over!" -unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal ('KProxy :: KProxy nat), SingI n)- => proxy ('KProxy :: KProxy nat) -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n+unsafeFromInt' :: forall proxy (n :: nat). (HasOrdinal nat, SingI n)+ => proxy nat -> MonomorphicRep (Sing :: nat -> *) -> Ordinal n unsafeFromInt' _ n = case promote (n :: MonomorphicRep (Sing :: nat -> *)) of Monomorphic sn ->@@ -176,53 +185,33 @@ -- | 'sNatToOrd'' @n m@ injects @m@ as @Ordinal n@. -- -- Since 0.5.0.0-sNatToOrd' :: (PeanoOrder ('KProxy :: KProxy nat), (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n+sNatToOrd' :: (PeanoOrder nat, (m :< n) ~ 'True) => Sing (n :: nat) -> Sing m -> Ordinal n sNatToOrd' _ m = OLt m+{-# INLINE sNatToOrd' #-} -- | 'sNatToOrd'' with @n@ inferred.-sNatToOrd :: (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n+sNatToOrd :: (PeanoOrder nat, SingI (n :: nat), (m :< n) ~ 'True) => Sing m -> Ordinal n sNatToOrd = sNatToOrd' sing data CastedOrdinal n where CastedOrdinal :: (m :< n) ~ 'True => Sing m -> CastedOrdinal n -- | Convert @Ordinal n@ into @Sing m@ with the proof of @'S m :<= n@.-ordToSing' :: forall (n :: nat). (PeanoOrder ('KProxy :: KProxy nat), SingI n) => Ordinal n -> CastedOrdinal n-ordToSing' (OZ sk) =- case lneqZero sk of- (Witness) -> CastedOrdinal sZero-ordToSing' (OS (on :: Ordinal k)) =- withSingI (sing :: Sing n) $- withPredSingI (Proxy :: Proxy k) (sing :: Sing n) $- case ordToSing' on of- CastedOrdinal m ->- case succLneqSucc m (sing :: Sing k) of- Refl -> CastedOrdinal (Succ m)+ordToSing' :: forall (n :: nat). (PeanoOrder nat, SingI n) => Ordinal n -> CastedOrdinal n ordToSing' (OLt s) = CastedOrdinal s--withPredSingI :: forall proxy (n :: nat) r. PeanoOrder ('KProxy :: KProxy nat)- => proxy (n :: nat) -> Sing (Succ n) -> (SingI n => r) -> r-withPredSingI pxy sn r = withSingI (sPred' pxy sn) r-+{-# INLINE ordToSing' #-} -- | Convert @Ordinal n@ into monomorphic @Sing@ -- -- Since 0.5.0.0-ordToSing :: (PeanoOrder ('KProxy :: KProxy nat)) => Ordinal (n :: nat) -> SomeSing ('KProxy :: KProxy nat)+ordToSing :: (PeanoOrder nat) => Ordinal (n :: nat) -> SomeSing nat ordToSing (OLt n) = SomeSing n-ordToSing OZ{} = SomeSing sZero-ordToSing (OS n) =- case ordToSing n of- SomeSing sn ->- case singInstance sn of- SingInstance -> SomeSing (Succ sn)+{-# INLINE ordToSing #-} -- | Convert ordinal into @Int@.-ordToInt :: (HasOrdinal ('KProxy :: KProxy nat), int ~ MonomorphicRep (Sing :: nat -> *))+ordToInt :: (HasOrdinal nat, int ~ MonomorphicRep (Sing :: nat -> *)) => Ordinal (n :: nat) -> int-ordToInt OZ{} = 0-ordToInt (OS n) = 1 + ordToInt n ordToInt (OLt n) = demote $ Monomorphic n {-# SPECIALISE ordToInt :: Ordinal (n :: PN.Nat) -> Integer #-} {-# SPECIALISE ordToInt :: Ordinal (n :: TL.Nat) -> Integer #-}@@ -231,14 +220,6 @@ inclusion' :: (n :< m) ~ 'True => Sing m -> Ordinal n -> Ordinal m inclusion' _ = unsafeCoerce {-# INLINE inclusion' #-}-{---- The "proof" of the correctness of the above-inclusion' :: (n :<= m) ~ 'True => Sing 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-inclusion' _ _ = bugInGHC--} -- | Inclusion function for ordinals with codomain inferred. inclusion :: ((n :<= m) ~ 'True) => Ordinal n -> Ordinal m@@ -247,43 +228,23 @@ -- | Ordinal addition.-(@+) :: forall n m. (PeanoOrder ('KProxy :: KProxy nat), SingI (n :: nat), SingI m) => Ordinal n -> Ordinal m -> Ordinal (n :+ m)-OLt s @+ n =- case ordToSing' n of- CastedOrdinal n' ->- case plusStrictMonotone s (sing :: Sing n) n' (sing :: Sing m) Witness Witness of- Witness -> OLt $ s %:+ n'-OZ {} @+ n =- let sn = sing :: Sing n- sm = sing :: Sing m- in case plusLeqR sn sm of- Witness -> inclusion n-OS (n :: Ordinal k) @+ m =- withPredSingI n (sing :: Sing n) $- case sing :: Sing n of- Zero -> absurdOrd (OS n)- Succ sn ->- case singInstance sn of- SingInstance ->- let sm = sing :: Sing m- sn' = sing :: Sing n- sk = sing :: Sing k- pf = start (sSucc (sk %:+ sm))- === sSucc sk %:+ sm `because` sym (plusSuccL sk sm)- =~= sn' %:+ sm- in coerce pf $ OS $ n @+ m- _ -> error "inaccessible pattern"+(@+) :: forall n m. (PeanoOrder nat, SingI (n :: nat), SingI m)+ => Ordinal n -> Ordinal m -> Ordinal (n :+ m)+OLt k @+ OLt l =+ let (n, m) = (n :: Sing n, m :: Sing m)+ in case plusStrictMonotone k n l m Witness Witness of+ Witness -> OLt $ k %:+ l -- | Since @Ordinal 'Z@ is logically not inhabited, we can coerce it to any value. -- -- Since 0.2.3.0-absurdOrd :: PeanoOrder ('KProxy :: KProxy nat) => Ordinal (Zero ('KProxy :: KProxy nat)) -> a-absurdOrd _cs = undefined -- case cs of {}+absurdOrd :: PeanoOrder nat => Ordinal (Zero nat) -> a+absurdOrd (OLt n) = absurd $ lneqZeroAbsurd n Witness -- | 'absurdOrd' for the value in 'Functor'. -- -- Since 0.2.3.0-vacuousOrd :: (PeanoOrder ('KProxy :: KProxy nat), Functor f) => f (Ordinal (Zero ('KProxy :: KProxy nat))) -> f a+vacuousOrd :: (PeanoOrder nat, Functor f) => f (Ordinal (Zero nat)) -> f a vacuousOrd = fmap absurdOrd -- | 'absurdOrd' for the value in 'Monad'.@@ -291,7 +252,7 @@ -- become the superclass of 'Monad'. -- -- Since 0.2.3.0-vacuousOrdM :: (PeanoOrder ('KProxy :: KProxy nat), Monad m) => m (Ordinal (Zero ('KProxy :: KProxy nat))) -> m a+vacuousOrdM :: (PeanoOrder nat, Monad m) => m (Ordinal (Zero nat)) -> m a vacuousOrdM = liftM absurdOrd -- | Quasiquoter for ordinals
type-natural.cabal view
@@ -2,13 +2,13 @@ -- documentation, see http://haskell.org/cabal/users-guide/ name: type-natural-version: 0.5.0.0+version: 0.6.0.0 synopsis: Type-level natural and proofs of their properties. description: Type-level natural numbers and proofs of their properties. .- This version 0.5.0.0 supports __GHC 7.10.* only__.+ Version 0.6+ supports __GHC 8+ only__. .- __Use >= 0.6.0.0 with GHC 8.0.0+__.+ __Use 0.5.* with ~ GHC 7.10.3__. homepage: https://github.com/konn/type-natural license: BSD3 license-file: LICENSE@@ -45,7 +45,7 @@ , constraints >= 0.3 && < 0.9 , ghc-typelits-natnormalise == 0.4.* , ghc-typelits-presburger >= 0.1.1 && < 1- , singletons == 2.1+ , singletons == 2.2.* default-language: Haskell2010 default-extensions: DataKinds