Data.Type.Natural

Coercion between Peano Numerals Nat and builtin naturals Nat

Type-level naturals

Nat, singletons and KnownNat manipulation,

data Nat

(Kind) This is the kind of type-level natural numbers.

Instances

TestEquality SNat

Defined in Data.Type.Natural.Core

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

KnownNat n => Reifies (n :: Nat) Integer

Defined in Data.Reflection

Methods

reflect :: proxy n -> Integer

(KnownNat a, KnownNat b) => KnownBoolNat2 "GHC.TypeNats.<=?" (a :: Nat) (b :: Nat)

Defined in GHC.TypeLits.KnownNat

Methods

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

Methods

natBoolSing3 :: SNatKn "Data.Type.Bool.If"

class KnownNat (n :: Nat)

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

Minimal complete definition

natSing

data SNat (n :: Nat) where

A singleton for type-level naturals

Bundled Patterns

pattern Succ :: forall n. () => forall n1. n ~ Succ n1 => SNat n1 -> SNat n

pattern Zero :: forall n. () => n ~ 0 => SNat n

Instances

TestEquality SNat

Defined in Data.Type.Natural.Core

Methods

testEquality :: forall (a :: k) (b :: k). SNat a -> SNat b -> Maybe (a :~: b)

Eq (SNat n)

Defined in Data.Type.Natural.Core

Methods

(==) :: SNat n -> SNat n -> Bool

(/=) :: SNat n -> SNat n -> Bool

Ord (SNat n)

Defined in Data.Type.Natural.Core

Methods

compare :: SNat n -> SNat n -> Ordering

(<) :: SNat n -> SNat n -> Bool

(<=) :: SNat n -> SNat n -> Bool

(>) :: SNat n -> SNat n -> Bool

(>=) :: SNat n -> SNat n -> Bool

max :: SNat n -> SNat n -> SNat n

min :: SNat n -> SNat n -> SNat n

Show (SNat n)

Defined in Data.Type.Natural.Core

Methods

showsPrec :: Int -> SNat n -> ShowS

show :: SNat n -> String

showList :: [SNat n] -> ShowS

sNat :: forall n. KnownNat n => SNat n

sNatP :: KnownNat n => pxy n -> SNat n

toNatural :: SNat n -> Natural

data SomeSNat where

Constructors

SomeSNat :: KnownNat n => SNat n -> SomeSNat

Instances

Eq SomeSNat

Defined in Data.Type.Natural

Methods

(==) :: SomeSNat -> SomeSNat -> Bool

(/=) :: SomeSNat -> SomeSNat -> Bool

Show SomeSNat

Defined in Data.Type.Natural

Methods

showsPrec :: Int -> SomeSNat -> ShowS

show :: SomeSNat -> String

showList :: [SomeSNat] -> ShowS

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

Since: base-4.10.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Natural

Since: base-4.10.0.0

someNatVal :: Natural -> SomeNat

Convert an integer into an unknown type-level natural.

Since: base-4.10.0.0

data SomeNat

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n)

Instances

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

compare :: SomeNat -> SomeNat -> Ordering

(<) :: SomeNat -> SomeNat -> Bool

(<=) :: SomeNat -> SomeNat -> Bool

(>) :: SomeNat -> SomeNat -> Bool

(>=) :: SomeNat -> SomeNat -> Bool

max :: SomeNat -> SomeNat -> SomeNat

min :: SomeNat -> SomeNat -> SomeNat

Read SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

(%~) :: SNat l -> SNat r -> Equality l r infix 4

data Equality n m where

Since 1.1.0.0 (Type changed)

Constructors

Equal :: (n == n) ~ 'True => Equality n n

NonEqual :: ((n === m) ~ 'False, (n == m) ~ 'False) => Equality n m

type family a === b where ... infix 4

Equations

a === a = 'True

_ === _ = 'False

Pattens and Views

viewNat :: forall n. SNat n -> ZeroOrSucc n

zeroOrSucc :: SNat n -> ZeroOrSucc n

data ZeroOrSucc n where

Constructors

IsZero :: ZeroOrSucc 0

IsSucc :: SNat n -> ZeroOrSucc (n + 1)

Promtoed and singletonised operations

Arithmetic

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 ... infixl 6

Addition of type-level naturals.

Since: base-4.7.0.0

(%+) :: SNat n -> SNat m -> SNat (n + m) infixl 6

type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6

Subtraction of type-level naturals.

Since: base-4.7.0.0

(%-) :: SNat n -> SNat m -> SNat (n - m) infixl 6

type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7

Multiplication of type-level naturals.

Since: base-4.7.0.0

(%*) :: SNat n -> SNat m -> SNat (n * m) infixl 7

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

sDiv :: SNat n -> SNat m -> SNat (Div n m) infixl 7

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

sMod :: SNat n -> SNat m -> SNat (Mod n m) infixl 7

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8

Exponentiation of type-level naturals.

Since: base-4.7.0.0

(%^) :: SNat n -> SNat m -> SNat (n ^ m) infixr 8

type (-.) n m = Subt n m (m <=? n) infixl 6

Natural subtraction, truncated to zero if m > n.

(%-.) :: SNat n -> SNat m -> SNat (n -. m)

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

sLog2 :: SNat n -> SNat (Log2 n)

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

(%<=?) :: SNat n -> SNat m -> SBool (n <=? m) infix 4

type (<?) n m = (n + 1) <=? m infix 4

type (<) n m = (n <? m) ~ 'True infix 4

(%<?) :: SNat n -> SNat m -> SBool (n <? m) infix 4

type (>=?) n m = m <=? n infix 4

type (>=) n m = (n >=? m) ~ 'True infix 4

(%>=?) :: SNat n -> SNat m -> SBool (n >=? m) infix 4

type (>?) n m = m <? n infix 4

type (>) n m = (n >? m) ~ 'True infix 4

(%>?) :: SNat n -> SNat m -> SBool (n >? m) infix 4

type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

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

QuasiQuotes

snat :: QuasiQuoter

Quotesi-quoter for SNatleton types for Nat. This can be used for an expression.

For example: [snat|12|] %+ [snat| 5 |].

Singletons for auxiliary types

data SBool (b :: Bool) where

Constructors

SFalse :: SBool 'False

STrue :: SBool 'True

Instances

Eq (SBool ord)

Defined in Data.Type.Natural.Core

Methods

(==) :: SBool ord -> SBool ord -> Bool

(/=) :: SBool ord -> SBool ord -> Bool

Show (SBool ord)

Defined in Data.Type.Natural.Core

Methods

showsPrec :: Int -> SBool ord -> ShowS

show :: SBool ord -> String

showList :: [SBool ord] -> ShowS

data SOrdering (ord :: Ordering) where

Constructors

SLT :: SOrdering 'LT

SEQ :: SOrdering 'EQ

SGT :: SOrdering 'GT

Instances

Eq (SOrdering ord)

Defined in Data.Type.Natural.Core

Methods

(==) :: SOrdering ord -> SOrdering ord -> Bool

(/=) :: SOrdering ord -> SOrdering ord -> Bool

Show (SOrdering ord)

Defined in Data.Type.Natural.Core

Methods

showsPrec :: Int -> SOrdering ord -> ShowS

show :: SOrdering ord -> String

showList :: [SOrdering ord] -> ShowS

type family FlipOrdering ord where ...

Equations

FlipOrdering 'LT = 'GT

FlipOrdering 'GT = 'LT

FlipOrdering 'EQ = 'EQ

sFlipOrdering :: SOrdering ord -> SOrdering (FlipOrdering ord)