Safe Haskell	None
Language	Haskell2010

Data.Type.Natural

Contents

Type-level naturals
- Nat, singletons and KnownNat manipulation,
  - Pattens and Views
- Promtoed and singletonised operations
  - Arithmetic
  - Ordering
QuasiQuotes
Singletons for auxiliary types

Description

Coercion between Peano Numerals Nat and builtin naturals Nat

Synopsis

type Nat = Natural
class KnownNat (n :: Nat)
data SNat (n :: Nat) where
- pattern Succ :: forall n n1. () => n ~ Succ n1 => SNat n1 -> SNat n
- pattern Zero :: () => n ~ 0 => SNat n
sNat :: forall (n :: Nat). KnownNat n => SNat n
sNatP :: forall (n :: Nat) pxy. KnownNat n => pxy n -> SNat n
toNatural :: forall (n :: Nat). SNat n -> Natural
data SomeSNat where
- SomeSNat :: forall (n :: Nat). KnownNat n => SNat n -> SomeSNat
toSomeSNat :: Natural -> SomeSNat
withSNat :: Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r
withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r
fromSNat :: forall (n :: Nat). SNat n -> Natural
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)
(%~) :: forall (l :: Nat) (r :: Nat). SNat l -> SNat r -> Equality l r
data Equality (n :: k) (m :: k) where
- Equal :: forall {k} (n :: k). (n == n) ~ 'True => Equality n n
- NonEqual :: forall {k} (n :: k) (m :: k). ((n === m) ~ 'False, (n == m) ~ 'False) => Equality n m
type family (a :: k) === (b :: k) :: Bool where ...
viewNat :: forall (n :: Nat). SNat n -> ZeroOrSucc n
zeroOrSucc :: forall (n :: Nat). SNat n -> ZeroOrSucc n
data ZeroOrSucc (n :: Natural) where
- IsZero :: ZeroOrSucc 0
- IsSucc :: forall (n1 :: Natural). SNat n1 -> ZeroOrSucc (n1 + 1)
type Succ (n :: Natural) = n + 1
sSucc :: forall (n :: Nat). SNat n -> SNat (Succ n)
type S (n :: Natural) = Succ n
type Pred (n :: Natural) = n - 1
sPred :: forall (n :: Nat). SNat n -> SNat (Pred n)
sS :: forall (n :: Nat). SNat n -> SNat (Succ n)
type Zero = 0
sZero :: SNat 0
type One = 1
sOne :: SNat 1
type family (a :: Natural) + (b :: Natural) :: Natural where ...
(%+) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m)
type family (a :: Natural) - (b :: Natural) :: Natural where ...
(%-) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m)
type family (a :: Natural) * (b :: Natural) :: Natural where ...
(%*) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m)
type family Div (a :: Natural) (b :: Natural) :: Natural where ...
sDiv :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Div n m)
type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
sMod :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Mod n m)
type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
(%^) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m)
type (-.) (n :: Natural) (m :: Natural) = Subt n m (m <=? n)
(%-.) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m)
type family Log2 (a :: Natural) :: Natural where ...
sLog2 :: forall (n :: Nat). SNat n -> SNat (Log2 n)
type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False
type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint)
(%<=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m)
type (<?) (n :: Nat) (m :: Nat) = n <? m
type (<) (n :: Nat) (m :: Nat) = n < m
(%<?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m)
type (>=?) (n :: Nat) (m :: Nat) = n >=? m
type (>=) (n :: Nat) (m :: Nat) = n >= m
(%>=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m)
type (>?) (n :: Nat) (m :: Nat) = n >? m
type (>) (n :: Nat) (m :: Nat) = n > m
(%>?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >? m)
type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ...
sCmpNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m)
sCompare :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m)
type Min (m :: Nat) (n :: Nat) = Min m n
sMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m)
type Max (m :: Nat) (n :: Nat) = Max m n
sMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m)
induction :: forall p (k :: Nat). p 0 -> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k
snat :: QuasiQuoter
data SBool (b :: Bool) where
- SFalse :: SBool 'False
- STrue :: SBool 'True
data SOrdering (ord :: Ordering) where
- SLT :: SOrdering 'LT
- SEQ :: SOrdering 'EQ
- SGT :: SOrdering 'GT
data OrderingI (a :: k) (b :: k) where
- LTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'LT => OrderingI a b
- EQI :: forall {k} (a :: k). Compare a a ~ 'EQ => OrderingI a a
- GTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'GT => OrderingI a b
fromOrderingI :: forall (n :: Natural) (m :: Natural). OrderingI n m -> SOrdering (CmpNat n m)
toOrderingI :: forall (n :: Natural) (m :: Natural). SOrdering (CmpNat n m) -> OrderingI n m
type family FlipOrdering (ord :: Ordering) :: Ordering where ...
sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord)

Type-level naturals

`Nat`, singletons and KnownNat manipulation,

type Nat = Natural #

A type synonym for Natural.

Previously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

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 value-level witness for a type-level natural number. This is commonly referred to as a singleton type, as for each n, there is a single value that inhabits the type SNat n (aside from bottom).

The definition of SNat is intentionally left abstract. To obtain an SNat value, use one of the following:

The natSing method of KnownNat.
The SNat pattern synonym.
The withSomeSNat function, which creates an SNat from a Natural number.

Since: base-4.18.0.0

Bundled Patterns

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

Instances

Instances details

TestCoercion SNat #	Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods testCoercion :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (Coercion a b) #
TestEquality SNat #	Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods testEquality :: forall (a :: Nat) (b :: Nat). SNat a -> SNat b -> Maybe (a :~: b) #
Show (SNat n) #	Since: base-4.18.0.0
Instance details Defined in GHC.Internal.TypeNats Methods showsPrec :: Int -> SNat n -> ShowS # show :: SNat n -> String # showList :: [SNat n] -> ShowS #
Eq (SNat n) #	Since: base-4.19.0.0
Instance details Defined in GHC.Internal.TypeNats Methods (==) :: SNat n -> SNat n -> Bool # (/=) :: SNat n -> SNat n -> Bool #
Ord (SNat n) #	Since: base-4.19.0.0
Instance details Defined in GHC.Internal.TypeNats 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 #

sNat :: forall (n :: Nat). KnownNat n => SNat n Source #

sNatP :: forall (n :: Nat) pxy. KnownNat n => pxy n -> SNat n Source #

toNatural :: forall (n :: Nat). SNat n -> Natural Source #

Deprecated: Use fromSNat instead

data SomeSNat where Source #

Constructors

SomeSNat :: forall (n :: Nat). KnownNat n => SNat n -> SomeSNat

Instances

Instances details

Show SomeSNat Source #
Instance details Defined in Data.Type.Natural Methods showsPrec :: Int -> SomeSNat -> ShowS # show :: SomeSNat -> String # showList :: [SomeSNat] -> ShowS #
Eq SomeSNat Source #
Instance details Defined in Data.Type.Natural Methods (==) :: SomeSNat -> SomeSNat -> Bool # (/=) :: SomeSNat -> SomeSNat -> Bool #
Ord SomeSNat Source #
Instance details Defined in Data.Type.Natural Methods compare :: SomeSNat -> SomeSNat -> Ordering # (<) :: SomeSNat -> SomeSNat -> Bool # (<=) :: SomeSNat -> SomeSNat -> Bool # (>) :: SomeSNat -> SomeSNat -> Bool # (>=) :: SomeSNat -> SomeSNat -> Bool # max :: SomeSNat -> SomeSNat -> SomeSNat # min :: SomeSNat -> SomeSNat -> SomeSNat #

toSomeSNat :: Natural -> SomeSNat Source #

withSNat :: Natural -> (forall (n :: Nat). KnownNat n => SNat n -> r) -> r Source #

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r #

Convert an explicit SNat n value into an implicit KnownNat n constraint.

Since: base-4.18.0.0

fromSNat :: forall (n :: Nat). SNat n -> Natural #

Return the Natural number corresponding to n in an SNat n value.

Since: base-4.18.0.0

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

Instances details

Read SomeNat #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.TypeNats Methods readsPrec :: Int -> ReadS SomeNat # readList :: ReadS [SomeNat] # readPrec :: ReadPrec SomeNat # readListPrec :: ReadPrec [SomeNat] #
Show SomeNat #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.TypeNats Methods showsPrec :: Int -> SomeNat -> ShowS # show :: SomeNat -> String # showList :: [SomeNat] -> ShowS #
Eq SomeNat #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.TypeNats Methods (==) :: SomeNat -> SomeNat -> Bool # (/=) :: SomeNat -> SomeNat -> Bool #
Ord SomeNat #	Since: base-4.7.0.0
Instance details Defined in GHC.Internal.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 #

(%~) :: forall (l :: Nat) (r :: Nat). SNat l -> SNat r -> Equality l r infix 4 Source #

data Equality (n :: k) (m :: k) where Source #

Since 1.1.0.0 (Type changed)

Constructors

Equal :: forall {k} (n :: k). (n == n) ~ 'True => Equality n n
NonEqual :: forall {k} (n :: k) (m :: k). ((n === m) ~ 'False, (n == m) ~ 'False) => Equality n m

type family (a :: k) === (b :: k) :: Bool where ... infix 4 Source #

Equations

(a :: k) === (a :: k) = 'True
(_1 :: k) === (_2 :: k) = 'False

Pattens and Views

viewNat :: forall (n :: Nat). SNat n -> ZeroOrSucc n Source #

zeroOrSucc :: forall (n :: Nat). SNat n -> ZeroOrSucc n Source #

data ZeroOrSucc (n :: Natural) where Source #

Constructors

IsZero :: ZeroOrSucc 0
IsSucc :: forall (n1 :: Natural). SNat n1 -> ZeroOrSucc (n1 + 1)

Promtoed and singletonised operations

Arithmetic

type Succ (n :: Natural) = n + 1 Source #

sSucc :: forall (n :: Nat). SNat n -> SNat (Succ n) Source #

type S (n :: Natural) = Succ n Source #

type Pred (n :: Natural) = n - 1 Source #

sPred :: forall (n :: Nat). SNat n -> SNat (Pred n) Source #

sS :: forall (n :: Nat). SNat n -> SNat (Succ n) Source #

type Zero = 0 Source #

sZero :: SNat 0 Source #

type One = 1 Source #

sOne :: SNat 1 Source #

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 #

Addition of type-level naturals.

Since: base-4.7.0.0

(%+) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n + m) infixl 6 Source #

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

Subtraction of type-level naturals.

Since: base-4.7.0.0

(%-) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n - m) infixl 6 Source #

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

Multiplication of type-level naturals.

Since: base-4.7.0.0

(%*) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n * m) infixl 7 Source #

type family Div (a :: Natural) (b :: Natural) :: Natural 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 :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Div n m) infixl 7 Source #

type family Mod (a :: Natural) (b :: Natural) :: Natural 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 :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Mod n m) infixl 7 Source #

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

Exponentiation of type-level naturals.

Since: base-4.7.0.0

(%^) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n ^ m) infixr 8 Source #

type (-.) (n :: Natural) (m :: Natural) = Subt n m (m <=? n) infixl 6 Source #

Natural subtraction, truncated to zero if m > n.

(%-.) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (n -. m) Source #

type family Log2 (a :: Natural) :: Natural 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 :: forall (n :: Nat). SNat n -> SNat (Log2 n) Source #

Ordering

type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 #

Comparison (<=) of comparable types, as a function.

Since: base-4.16.0.0

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 #

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

(%<=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <=? m) infix 4 Source #

type (<?) (n :: Nat) (m :: Nat) = n <? m infix 4 Source #

type (<) (n :: Nat) (m :: Nat) = n < m infix 4 Source #

(%<?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n <? m) infix 4 Source #

type (>=?) (n :: Nat) (m :: Nat) = n >=? m infix 4 Source #

type (>=) (n :: Nat) (m :: Nat) = n >= m infix 4 Source #

(%>=?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >=? m) infix 4 Source #

type (>?) (n :: Nat) (m :: Nat) = n >? m infix 4 Source #

type (>) (n :: Nat) (m :: Nat) = n > m infix 4 Source #

(%>?) :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SBool (n >? m) infix 4 Source #

type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... #

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

sCmpNat :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m) Source #

sCompare :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SOrdering (CmpNat n m) Source #

type Min (m :: Nat) (n :: Nat) = Min m n Source #

sMin :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Min n m) Source #

type Max (m :: Nat) (n :: Nat) = Max m n Source #

sMax :: forall (n :: Nat) (m :: Nat). SNat n -> SNat m -> SNat (Max n m) Source #

induction :: forall p (k :: Nat). p 0 -> (forall (n :: Nat). SNat n -> p n -> p (S n)) -> SNat k -> p k Source #

QuasiQuotes

snat :: QuasiQuoter Source #

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 Source #

Constructors

SFalse :: SBool 'False
STrue :: SBool 'True

Instances

Instances details

Show (SBool ord) Source #
Instance details Defined in Data.Type.Natural.Core Methods showsPrec :: Int -> SBool ord -> ShowS # show :: SBool ord -> String # showList :: [SBool ord] -> ShowS #
Eq (SBool ord) Source #
Instance details Defined in Data.Type.Natural.Core Methods (==) :: SBool ord -> SBool ord -> Bool # (/=) :: SBool ord -> SBool ord -> Bool #

data SOrdering (ord :: Ordering) where Source #

Constructors

SLT :: SOrdering 'LT
SEQ :: SOrdering 'EQ
SGT :: SOrdering 'GT

Instances

Instances details

Show (SOrdering ord) Source #
Instance details Defined in Data.Type.Natural.Core Methods showsPrec :: Int -> SOrdering ord -> ShowS # show :: SOrdering ord -> String # showList :: [SOrdering ord] -> ShowS #
Eq (SOrdering ord) Source #
Instance details Defined in Data.Type.Natural.Core Methods (==) :: SOrdering ord -> SOrdering ord -> Bool # (/=) :: SOrdering ord -> SOrdering ord -> Bool #

data OrderingI (a :: k) (b :: k) where #

Ordering data type for type literals that provides proof of their ordering.

Since: base-4.16.0.0

Constructors

LTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'LT => OrderingI a b
EQI :: forall {k} (a :: k). Compare a a ~ 'EQ => OrderingI a a
GTI :: forall {k} (a :: k) (b :: k). Compare a b ~ 'GT => OrderingI a b

Instances

Instances details

Show (OrderingI a b) #
Instance details Defined in GHC.Internal.Data.Type.Ord Methods showsPrec :: Int -> OrderingI a b -> ShowS # show :: OrderingI a b -> String # showList :: [OrderingI a b] -> ShowS #
Eq (OrderingI a b) #
Instance details Defined in GHC.Internal.Data.Type.Ord Methods (==) :: OrderingI a b -> OrderingI a b -> Bool # (/=) :: OrderingI a b -> OrderingI a b -> Bool #

fromOrderingI :: forall (n :: Natural) (m :: Natural). OrderingI n m -> SOrdering (CmpNat n m) Source #

toOrderingI :: forall (n :: Natural) (m :: Natural). SOrdering (CmpNat n m) -> OrderingI n m Source #

type family FlipOrdering (ord :: Ordering) :: Ordering where ... Source #

Equations

FlipOrdering 'LT = 'GT
FlipOrdering 'GT = 'LT
FlipOrdering 'EQ = 'EQ

sFlipOrdering :: forall (ord :: Ordering). SOrdering ord -> SOrdering (FlipOrdering ord) Source #

Type-level naturals

Nat, singletons and KnownNat manipulation,

Instances

Instances

Instances

Pattens and Views

Promtoed and singletonised operations

Arithmetic

Ordering

QuasiQuotes

Singletons for auxiliary types

Instances

Instances

Instances

`Nat`, singletons and KnownNat manipulation,