Safe Haskell | None |
---|---|
Language | Haskell2010 |
Synopsis
- data Nat
- class KnownNat (n :: Nat)
- data SNat (n :: Nat) where
- sNat :: forall n. KnownNat n => SNat n
- sNatP :: KnownNat n => pxy n -> SNat n
- toNatural :: SNat n -> Natural
- data SomeSNat where
- toSomeSNat :: Natural -> SomeSNat
- withSNat :: Natural -> (forall n. KnownNat n => SNat n -> r) -> r
- withKnownNat :: forall n r. SNat n -> (KnownNat n => r) -> r
- natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural
- natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural
- someNatVal :: Natural -> SomeNat
- data SomeNat = KnownNat n => SomeNat (Proxy n)
- (%~) :: SNat l -> SNat r -> Equality l r
- data Equality n m where
- type family a === b where ...
- viewNat :: forall n. SNat n -> ZeroOrSucc n
- zeroOrSucc :: SNat n -> ZeroOrSucc n
- data ZeroOrSucc n where
- IsZero :: ZeroOrSucc 0
- IsSucc :: SNat n -> ZeroOrSucc (n + 1)
- type Succ n = n + 1
- sSucc :: SNat n -> SNat (Succ n)
- type S n = Succ n
- type Pred n = n - 1
- sPred :: SNat n -> SNat (Pred n)
- sS :: SNat n -> SNat (Succ n)
- type Zero = 0
- sZero :: SNat 0
- type One = 1
- sOne :: SNat 1
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- (%+) :: SNat n -> SNat m -> SNat (n + m)
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- (%-) :: SNat n -> SNat m -> SNat (n - m)
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- (%*) :: SNat n -> SNat m -> SNat (n * m)
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- sDiv :: SNat n -> SNat m -> SNat (Div n m)
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- sMod :: SNat n -> SNat m -> SNat (Mod n m)
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- (%^) :: SNat n -> SNat m -> SNat (n ^ m)
- type (-.) n m = Subt n m (m <=? n)
- (%-.) :: SNat n -> SNat m -> SNat (n -. m)
- type family Log2 (a :: Nat) :: Nat where ...
- sLog2 :: SNat n -> SNat (Log2 n)
- type family (a :: Nat) <=? (b :: Nat) :: Bool where ...
- type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True
- (%<=?) :: SNat n -> SNat m -> SBool (n <=? m)
- type (<?) n m = (n + 1) <=? m
- type (<) n m = (n <? m) ~ 'True
- (%<?) :: SNat n -> SNat m -> SBool (n <? m)
- type (>=?) n m = m <=? n
- type (>=) n m = (n >=? m) ~ 'True
- (%>=?) :: SNat n -> SNat m -> SBool (n >=? m)
- type (>?) n m = m <? n
- type (>) n m = (n >? m) ~ 'True
- (%>?) :: SNat n -> SNat m -> SBool (n >? m)
- type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
- sCmpNat :: SNat n -> SNat m -> SOrdering (CmpNat n m)
- sCompare :: SNat n -> SNat m -> SOrdering (CmpNat n m)
- type Min n m = MinAux (n <=? m) n m
- sMin :: SNat n -> SNat m -> SNat (Min n m)
- type Max n m = MaxAux (n >=? m) n m
- sMax :: SNat n -> SNat m -> SNat (Max n m)
- induction :: forall p k. p 0 -> (forall n. SNat n -> p n -> p (S n)) -> SNat k -> p k
- snat :: QuasiQuoter
- data SBool (b :: Bool) where
- data SOrdering (ord :: Ordering) where
- type family FlipOrdering ord where ...
- sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)
Type-level naturals
Nat
, singletons and KnownNat manipulation,
(Kind) This is the kind of type-level natural numbers.
Instances
TestEquality SNat Source # | |
Defined in Data.Type.Natural.Core | |
KnownNat n => Reifies (n :: Nat) Integer | |
Defined in Data.Reflection | |
(KnownNat a, KnownNat b) => KnownBoolNat2 "GHC.TypeNats.<=?" (a :: Nat) (b :: Nat) | |
Defined in GHC.TypeLits.KnownNat boolNatSing2 :: SBoolKb "GHC.TypeNats.<=?" # | |
(KnownBool a, KnownNat b, KnownNat c) => KnownNat2Bool "Data.Type.Bool.If" a (b :: Nat) (c :: Nat) | |
Defined in GHC.TypeLits.KnownNat natBoolSing3 :: SNatKn "Data.Type.Bool.If" # |
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
natSing
data SNat (n :: Nat) where Source #
A singleton for type-level naturals
pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n | |
pattern Zero :: forall n. () => n ~ 0 => SNat n |
toSomeSNat :: Natural -> SomeSNat Source #
withKnownNat :: forall n r. SNat n -> (KnownNat n => r) -> r Source #
someNatVal :: Natural -> SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.10.0.0
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
Pattens and Views
viewNat :: forall n. SNat n -> ZeroOrSucc n Source #
zeroOrSucc :: SNat n -> ZeroOrSucc n Source #
data ZeroOrSucc n where Source #
IsZero :: ZeroOrSucc 0 | |
IsSucc :: SNat n -> ZeroOrSucc (n + 1) |
Promtoed and singletonised operations
Arithmetic
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type (-.) n m = Subt n m (m <=? n) infixl 6 Source #
Natural subtraction, truncated to zero if m > n.
type family Log2 (a :: Nat) :: Nat where ... #
Log base 2 (round down) of natural numbers.
Log 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
Ordering
type family (a :: Nat) <=? (b :: Nat) :: Bool where ... infix 4 #
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat
, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.
type (<=) (x :: Nat) (y :: Nat) = (x <=? y) ~ 'True infix 4 #
Comparison of type-level naturals, as a constraint.
Since: base-4.7.0.0
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
QuasiQuotes
snat :: QuasiQuoter Source #
Singletons for auxiliary types
type family FlipOrdering ord where ... Source #
FlipOrdering 'LT = 'GT | |
FlipOrdering 'GT = 'LT | |
FlipOrdering 'EQ = 'EQ |
sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord) Source #