Safe Haskell | None |
---|---|
Language | Haskell98 |
Type level peano natural number, some arithmetic functions and their singletons.
- module Data.Singletons
- data Nat
- data SSym0 l
- type SSym1 t = S t
- type ZSym0 = Z
- type SNat z = Sing z
- data family Sing a
- sZ :: SNat Z
- sS :: SNat n -> SNat (S n)
- min :: Nat -> Nat -> Nat
- type family Min a a :: Nat
- sMin :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MinSym0 t) t)
- max :: Nat -> Nat -> Nat
- type family Max a a :: Nat
- sMax :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply MaxSym0 t) t)
- data MinSym0 l
- data MinSym1 l l
- type MinSym2 t t = Min t t
- data MaxSym0 l
- data MaxSym1 l l
- type MaxSym2 t t = Max t t
- type (:+:) n m = n :+ m
- type family a :+ a :: Nat
- data (:+$) l
- data l :+$$ l
- type (:+$$$) t t = (:+) t t
- (%+) :: SNat n -> SNat m -> SNat (n :+: m)
- (%:+) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:+$) t) t)
- type family a :* a :: Nat
- type (:*:) n m = n :* m
- data (:*$) l
- data l :*$$ l
- type (:*$$$) t t = (:*) t t
- (%:*) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:*$) t) t)
- (%*) :: SNat n -> SNat m -> SNat (n :*: m)
- type (:-:) n m = n :- m
- type family a :- a :: Nat
- data (:-$) l
- data l :-$$ l
- type (:-$$$) t t = (:-) t t
- (%:-) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:-$) t) t)
- (%-) :: ((m :<<= n) ~ True) => SNat n -> SNat m -> SNat (n :-: m)
- data Leq n m where
- class n :<= m
- type family a :<<= a :: Bool
- data (:<<=$) l
- data l :<<=$$ l
- type (:<<=$$$) t t = (:<<=) t t
- (%:<<=) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:<<=$) t) t)
- type LeqInstance n m = Dict (n :<= m)
- boolToPropLeq :: ((n :<<= m) ~ True) => SNat n -> SNat m -> Leq n m
- boolToClassLeq :: ((n :<<= m) ~ True) => SNat n -> SNat m -> LeqInstance n m
- propToClassLeq :: Leq n m -> LeqInstance n m
- type LeqTrueInstance a b = Dict ((a :<<= b) ~ True)
- propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m
- natToInt :: Integral n => Nat -> n
- intToNat :: (Integral a, Ord a) => a -> Nat
- sNatToInt :: Num n => SNat x -> n
- nat :: QuasiQuoter
- snat :: QuasiQuoter
- succCongEq :: (n :=: m) -> S n :=: S m
- plusCongR :: SNat n -> (m :=: m') -> (m :+ n) :=: (m' :+ n)
- plusCongL :: SNat n -> (m :=: m') -> (n :+ m) :=: (n :+ m')
- succPlusL :: SNat n -> SNat m -> (S n :+ m) :=: S (n :+ m)
- succPlusR :: SNat n -> SNat m -> (n :+ S m) :=: S (n :+ m)
- plusZR :: SNat n -> (n :+: Z) :=: n
- plusZL :: SNat n -> (Z :+: n) :=: n
- eqPreservesS :: (n :=: m) -> S n :=: S m
- plusAssociative :: SNat n -> SNat m -> SNat l -> (n :+: (m :+: l)) :=: ((n :+: m) :+: l)
- multAssociative :: SNat n -> SNat m -> SNat l -> (n :* (m :* l)) :=: ((n :* m) :* l)
- multComm :: SNat n -> SNat m -> (n :* m) :=: (m :* n)
- multZL :: SNat m -> (Zero :* m) :=: Zero
- multZR :: SNat m -> (m :* Zero) :=: Zero
- multOneL :: SNat n -> (One :* n) :=: n
- multOneR :: SNat n -> (n :* One) :=: n
- snEqZAbsurd :: (S n :=: Z) -> a
- succInjective :: (S n :=: S m) -> n :=: m
- plusInjectiveL :: SNat n -> SNat m -> SNat l -> ((n :+ m) :=: (n :+ l)) -> m :=: l
- plusInjectiveR :: SNat n -> SNat m -> SNat l -> ((n :+ l) :=: (m :+ l)) -> n :=: m
- plusMultDistr :: SNat n -> SNat m -> SNat l -> ((n :+ m) :* l) :=: ((n :* l) :+ (m :* l))
- multPlusDistr :: SNat n -> SNat m -> SNat l -> (n :* (m :+ l)) :=: ((n :* m) :+ (n :* l))
- multCongL :: SNat n -> (m :=: l) -> (n :* m) :=: (n :* l)
- multCongR :: SNat n -> (m :=: l) -> (m :* n) :=: (l :* n)
- sAndPlusOne :: SNat n -> S n :=: (n :+: One)
- plusCommutative :: SNat n -> SNat m -> (n :+: m) :=: (m :+: n)
- minusCongEq :: (n :=: m) -> SNat l -> (n :-: l) :=: (m :-: l)
- minusNilpotent :: SNat n -> (n :-: n) :=: Zero
- eqSuccMinus :: ((m :<<= n) ~ True) => SNat n -> SNat m -> (S n :-: m) :=: S (n :-: m)
- plusMinusEqL :: SNat n -> SNat m -> ((n :+: m) :-: m) :=: n
- plusMinusEqR :: SNat n -> SNat m -> ((m :+: n) :-: m) :=: n
- zAbsorbsMinR :: SNat n -> Min n Z :=: Z
- zAbsorbsMinL :: SNat n -> Min Z n :=: Z
- plusSR :: SNat n -> SNat m -> S (n :+: m) :=: (n :+: S m)
- plusNeutralR :: SNat n -> SNat m -> ((n :+ m) :=: n) -> m :=: Z
- plusNeutralL :: SNat n -> SNat m -> ((n :+ m) :=: m) -> n :=: Z
- leqRhs :: Leq n m -> SNat m
- leqLhs :: Leq n m -> SNat n
- minComm :: SNat n -> SNat m -> Min n m :=: Min m n
- maxZL :: SNat n -> Max Z n :=: n
- maxComm :: SNat n -> SNat m -> Max n m :=: Max m n
- maxZR :: SNat n -> Max n Z :=: n
- leqRefl :: SNat n -> Leq n n
- leqSucc :: SNat n -> Leq n (S n)
- leqTrans :: Leq n m -> Leq m l -> Leq n l
- plusMonotone :: Leq n m -> Leq l k -> Leq (n :+: l) (m :+: k)
- plusLeqL :: SNat n -> SNat m -> Leq n (n :+: m)
- plusLeqR :: SNat n -> SNat m -> Leq m (n :+: m)
- minLeqL :: SNat n -> SNat m -> Leq (Min n m) n
- minLeqR :: SNat n -> SNat m -> Leq (Min n m) m
- leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m
- maxLeqL :: SNat n -> SNat m -> Leq n (Max n m)
- maxLeqR :: SNat n -> SNat m -> Leq m (Max n m)
- leqSnZAbsurd :: Leq (S n) Z -> a
- leqnZElim :: Leq n Z -> n :=: Z
- leqSnLeq :: Leq (S n) m -> Leq n m
- leqPred :: Leq (S n) (S m) -> Leq n m
- leqSnnAbsurd :: Leq (S n) n -> a
- zero :: Nat
- one :: Nat
- two :: Nat
- three :: Nat
- four :: Nat
- five :: Nat
- six :: Nat
- seven :: Nat
- eight :: Nat
- nine :: Nat
- ten :: Nat
- eleven :: Nat
- twelve :: Nat
- thirteen :: Nat
- fourteen :: Nat
- fifteen :: Nat
- sixteen :: Nat
- seventeen :: Nat
- eighteen :: Nat
- nineteen :: Nat
- twenty :: Nat
- type Zero = (ZSym0 :: Nat)
- type One = (Apply SSym0 ZeroSym0 :: Nat)
- type Two = (Apply SSym0 OneSym0 :: Nat)
- type Three = (Apply SSym0 TwoSym0 :: Nat)
- type Four = (Apply SSym0 ThreeSym0 :: Nat)
- type Five = (Apply SSym0 FourSym0 :: Nat)
- type Six = (Apply SSym0 FiveSym0 :: Nat)
- type Seven = (Apply SSym0 SixSym0 :: Nat)
- type Eight = (Apply SSym0 SevenSym0 :: Nat)
- type Nine = (Apply SSym0 EightSym0 :: Nat)
- type Ten = (Apply SSym0 NineSym0 :: Nat)
- type Eleven = (Apply SSym0 TenSym0 :: Nat)
- type Twelve = (Apply SSym0 ElevenSym0 :: Nat)
- type Thirteen = (Apply SSym0 TwelveSym0 :: Nat)
- type Fourteen = (Apply SSym0 ThirteenSym0 :: Nat)
- type Fifteen = (Apply SSym0 FourteenSym0 :: Nat)
- type Sixteen = (Apply SSym0 FifteenSym0 :: Nat)
- type Seventeen = (Apply SSym0 SixteenSym0 :: Nat)
- type Eighteen = (Apply SSym0 SeventeenSym0 :: Nat)
- type Nineteen = (Apply SSym0 EighteenSym0 :: Nat)
- type Twenty = (Apply SSym0 NineteenSym0 :: Nat)
- type ZeroSym0 = Zero
- type OneSym0 = One
- type TwoSym0 = Two
- type ThreeSym0 = Three
- type FourSym0 = Four
- type FiveSym0 = Five
- type SixSym0 = Six
- type SevenSym0 = Seven
- type EightSym0 = Eight
- type NineSym0 = Nine
- type TenSym0 = Ten
- type ElevenSym0 = Eleven
- type TwelveSym0 = Twelve
- type ThirteenSym0 = Thirteen
- type FourteenSym0 = Fourteen
- type FifteenSym0 = Fifteen
- type SixteenSym0 = Sixteen
- type SeventeenSym0 = Seventeen
- type EighteenSym0 = Eighteen
- type NineteenSym0 = Nineteen
- type TwentySym0 = Twenty
- sZero :: Sing ZeroSym0
- sOne :: Sing OneSym0
- sTwo :: Sing TwoSym0
- sThree :: Sing ThreeSym0
- sFour :: Sing FourSym0
- sFive :: Sing FiveSym0
- sSix :: Sing SixSym0
- sSeven :: Sing SevenSym0
- sEight :: Sing EightSym0
- sNine :: Sing NineSym0
- sTen :: Sing TenSym0
- sEleven :: Sing ElevenSym0
- sTwelve :: Sing TwelveSym0
- sThirteen :: Sing ThirteenSym0
- sFourteen :: Sing FourteenSym0
- sFifteen :: Sing FifteenSym0
- sSixteen :: Sing SixteenSym0
- sSeventeen :: Sing SeventeenSym0
- sEighteen :: Sing EighteenSym0
- sNineteen :: Sing NineteenSym0
- sTwenty :: Sing TwentySym0
- n0 :: Nat
- n1 :: Nat
- n2 :: Nat
- n3 :: Nat
- n4 :: Nat
- n5 :: Nat
- n6 :: Nat
- n7 :: Nat
- n8 :: Nat
- n9 :: Nat
- n10 :: Nat
- n11 :: Nat
- n12 :: Nat
- n13 :: Nat
- n14 :: Nat
- n15 :: Nat
- n16 :: Nat
- n17 :: Nat
- n18 :: Nat
- n19 :: Nat
- n20 :: Nat
- type N0 = (ZeroSym0 :: Nat)
- type N1 = (OneSym0 :: Nat)
- type N2 = (TwoSym0 :: Nat)
- type N3 = (ThreeSym0 :: Nat)
- type N4 = (FourSym0 :: Nat)
- type N5 = (FiveSym0 :: Nat)
- type N6 = (SixSym0 :: Nat)
- type N7 = (SevenSym0 :: Nat)
- type N8 = (EightSym0 :: Nat)
- type N9 = (NineSym0 :: Nat)
- type N10 = (TenSym0 :: Nat)
- type N11 = (ElevenSym0 :: Nat)
- type N12 = (TwelveSym0 :: Nat)
- type N13 = (ThirteenSym0 :: Nat)
- type N14 = (FourteenSym0 :: Nat)
- type N15 = (FifteenSym0 :: Nat)
- type N16 = (SixteenSym0 :: Nat)
- type N17 = (SeventeenSym0 :: Nat)
- type N18 = (EighteenSym0 :: Nat)
- type N19 = (NineteenSym0 :: Nat)
- type N20 = (TwentySym0 :: Nat)
- type N0Sym0 = N0
- type N1Sym0 = N1
- type N2Sym0 = N2
- type N3Sym0 = N3
- type N4Sym0 = N4
- type N5Sym0 = N5
- type N6Sym0 = N6
- type N7Sym0 = N7
- type N8Sym0 = N8
- type N9Sym0 = N9
- type N10Sym0 = N10
- type N11Sym0 = N11
- type N12Sym0 = N12
- type N13Sym0 = N13
- type N14Sym0 = N14
- type N15Sym0 = N15
- type N16Sym0 = N16
- type N17Sym0 = N17
- type N18Sym0 = N18
- type N19Sym0 = N19
- type N20Sym0 = N20
- sN0 :: Sing N0Sym0
- sN1 :: Sing N1Sym0
- sN2 :: Sing N2Sym0
- sN3 :: Sing N3Sym0
- sN4 :: Sing N4Sym0
- sN5 :: Sing N5Sym0
- sN6 :: Sing N6Sym0
- sN7 :: Sing N7Sym0
- sN8 :: Sing N8Sym0
- sN9 :: Sing N9Sym0
- sN10 :: Sing N10Sym0
- sN11 :: Sing N11Sym0
- sN12 :: Sing N12Sym0
- sN13 :: Sing N13Sym0
- sN14 :: Sing N14Sym0
- sN15 :: Sing N15Sym0
- sN16 :: Sing N16Sym0
- sN17 :: Sing N17Sym0
- sN18 :: Sing N18Sym0
- sN19 :: Sing N19Sym0
- sN20 :: Sing N20Sym0
Re-exported modules.
module Data.Singletons
Natural Numbers
Peano natural numbers. It will be promoted to the type-level natural number.
Singleton type for Nat
.
data family Sing a
The singleton kind-indexed data family.
SDecide k (KProxy k) => TestEquality k (Sing k) | |
Monomorphicable Nat (Sing Nat) | |
Eq (Sing Nat n) | |
Show (Sing Nat n) | |
data Sing Bool where | |
data Sing Ordering where | |
data Sing Nat where | |
data Sing Symbol where
| |
data Sing () where | |
data Sing Nat where | |
type MonomorphicRep Nat (Sing Nat) = Int | |
data Sing [a0] where | |
data Sing (Maybe a0) where | |
data Sing (TyFun k1 k2 -> *) = SLambda {} | |
data Sing (Either a0 b0) where | |
data Sing ((,) a0 b0) where | |
data Sing ((,,) a0 b0 c0) where | |
data Sing ((,,,) a0 b0 c0 d0) where | |
data Sing ((,,,,) a0 b0 c0 d0 e0) where | |
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where | |
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where |
Smart constructors
WARNING: Smart constructors are deprecated as of singletons 0.10, so these are provided only for backward compatibility.
Deprecated: Smart constructors are no longer needed in singletons; Use SS
or SZ
instead.
sS :: SNat n -> SNat (S n) Source
Deprecated: Smart constructors are no longer needed in singletons; Use SS
or SZ
instead.
Arithmetic functions and their singletons.
Type-level predicate & judgements
Comparison via GADTs.
type LeqInstance n m = Dict (n :<= m) Source
boolToClassLeq :: ((n :<<= m) ~ True) => SNat n -> SNat m -> LeqInstance n m Source
propToClassLeq :: Leq n m -> LeqInstance n m Source
type LeqTrueInstance a b = Dict ((a :<<= b) ~ True) Source
propToBoolLeq :: forall n m. Leq n m -> LeqTrueInstance n m Source
Conversion functions
Quasi quotes for natural numbers
nat :: QuasiQuoter Source
Quotesi-quoter for Nat
. This can be used for an expression, pattern and type.
for example: sing :: SNat ([nat| 2 |] :+ [nat| 5 |])
Properties of natural numbers
snEqZAbsurd :: (S n :=: Z) -> a Source
Properties of ordering Leq
leqAnitsymmetric :: Leq n m -> Leq m n -> n :=: m Source
leqSnZAbsurd :: Leq (S n) Z -> a Source
leqSnnAbsurd :: Leq (S n) n -> a Source
Useful type synonyms and constructors
type ElevenSym0 = Eleven Source
type TwelveSym0 = Twelve Source
type ThirteenSym0 = Thirteen Source
type FourteenSym0 = Fourteen Source
type FifteenSym0 = Fifteen Source
type SixteenSym0 = Sixteen Source
type SeventeenSym0 = Seventeen Source
type EighteenSym0 = Eighteen Source
type NineteenSym0 = Nineteen Source
type TwentySym0 = Twenty Source
type N11 = (ElevenSym0 :: Nat) Source
type N12 = (TwelveSym0 :: Nat) Source
type N13 = (ThirteenSym0 :: Nat) Source
type N14 = (FourteenSym0 :: Nat) Source
type N15 = (FifteenSym0 :: Nat) Source
type N16 = (SixteenSym0 :: Nat) Source
type N17 = (SeventeenSym0 :: Nat) Source
type N18 = (EighteenSym0 :: Nat) Source
type N19 = (NineteenSym0 :: Nat) Source
type N20 = (TwentySym0 :: Nat) Source