Data.Singletons.TypeLits

Defines and exports singletons useful for the Nat and Symbol kinds. This exports the internal, unsafe constructors. Use Data.Singletons.TypeLits for a safe interface.

Documentation

data Nat :: *

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

Instances

SNum Nat

Methods

(%:+) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t) t)

(%:-) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t) t)

(%:*) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:*$) Nat) t) t)

sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t)

sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t)

sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t)

sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t)

SEnum Nat

Methods

sSucc :: Sing Nat t -> Sing Nat (Apply Nat Nat (SuccSym0 Nat) t)

sPred :: Sing Nat t -> Sing Nat (Apply Nat Nat (PredSym0 Nat) t)

sToEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (ToEnumSym0 Nat) t)

sFromEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromEnumSym0 Nat) t)

sEnumFromTo :: Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromToSym0 Nat) t) t)

sEnumFromThenTo :: Sing Nat t -> Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (Apply Nat (TyFun Nat (TyFun Nat [Nat] -> Type) -> Type) (EnumFromThenToSym0 Nat) t) t) t)

PNum Nat (Proxy * Nat)

Associated Types

type ((Proxy * Nat) :+ (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a

type ((Proxy * Nat) :- (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a

type ((Proxy * Nat) :* (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a

type Negate (Proxy * Nat) (arg :: Proxy * Nat) :: a

type Abs (Proxy * Nat) (arg :: Proxy * Nat) :: a

type Signum (Proxy * Nat) (arg :: Proxy * Nat) :: a

type FromInteger (Proxy * Nat) (arg :: Nat) :: a

PEnum Nat (Proxy * Nat)

Associated Types

type Succ (Proxy * Nat) (arg :: Proxy * Nat) :: a

type Pred (Proxy * Nat) (arg :: Proxy * Nat) :: a

type ToEnum (Proxy * Nat) (arg :: Nat) :: a

type FromEnum (Proxy * Nat) (arg :: Proxy * Nat) :: Nat

type EnumFromTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a]

type EnumFromThenTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a]

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$)

Methods

suppressUnusedWarnings :: Proxy (:^$$) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$)

Methods

suppressUnusedWarnings :: Proxy (:^$) t -> ()

SuppressUnusedWarnings ((TyFun a1627953316 Bool -> Type) -> TyFun [a1627953316] (Maybe Nat) -> *) (FindIndexSym1 a1627953316)

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym1 a1627953316) t -> ()

SuppressUnusedWarnings ((TyFun a1627953315 Bool -> Type) -> TyFun [a1627953315] [Nat] -> *) (FindIndicesSym1 a1627953315)

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym1 a1627953315) t -> ()

SuppressUnusedWarnings ([a1627953289] -> TyFun Nat a1627953289 -> *) ((:!!$$) a1627953289)

Methods

suppressUnusedWarnings :: Proxy ((:!!$$) a1627953289) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a1627953305] ([a1627953305], [a1627953305]) -> *) (SplitAtSym1 a1627953305)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym1 a1627953305) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a1627953307] [a1627953307] -> *) (TakeSym1 a1627953307)

Methods

suppressUnusedWarnings :: Proxy (TakeSym1 a1627953307) t -> ()

SuppressUnusedWarnings (Nat -> TyFun [a1627953306] [a1627953306] -> *) (DropSym1 a1627953306)

Methods

suppressUnusedWarnings :: Proxy (DropSym1 a1627953306) t -> ()

SuppressUnusedWarnings (Nat -> TyFun a1627953291 [a1627953291] -> *) (ReplicateSym1 a1627953291)

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym1 a1627953291) t -> ()

SuppressUnusedWarnings (a1627953318 -> TyFun [a1627953318] (Maybe Nat) -> *) (ElemIndexSym1 a1627953318)

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym1 a1627953318) t -> ()

SuppressUnusedWarnings (a1627953317 -> TyFun [a1627953317] [Nat] -> *) (ElemIndicesSym1 a1627953317)

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a1627953317) t -> ()

SuppressUnusedWarnings (TyFun (TyFun a1627953316 Bool -> Type) (TyFun [a1627953316] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a1627953316)

Methods

suppressUnusedWarnings :: Proxy (FindIndexSym0 a1627953316) t -> ()

SuppressUnusedWarnings (TyFun (TyFun a1627953315 Bool -> Type) (TyFun [a1627953315] [Nat] -> Type) -> *) (FindIndicesSym0 a1627953315)

Methods

suppressUnusedWarnings :: Proxy (FindIndicesSym0 a1627953315) t -> ()

SuppressUnusedWarnings (TyFun [a1627953292] Nat -> *) (LengthSym0 a1627953292)

Methods

suppressUnusedWarnings :: Proxy (LengthSym0 a1627953292) t -> ()

SuppressUnusedWarnings (TyFun [a1627953289] (TyFun Nat a1627953289 -> Type) -> *) ((:!!$) a1627953289)

Methods

suppressUnusedWarnings :: Proxy ((:!!$) a1627953289) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) -> *) (SplitAtSym0 a1627953305)

Methods

suppressUnusedWarnings :: Proxy (SplitAtSym0 a1627953305) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953307] [a1627953307] -> Type) -> *) (TakeSym0 a1627953307)

Methods

suppressUnusedWarnings :: Proxy (TakeSym0 a1627953307) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953306] [a1627953306] -> Type) -> *) (DropSym0 a1627953306)

Methods

suppressUnusedWarnings :: Proxy (DropSym0 a1627953306) t -> ()

SuppressUnusedWarnings (TyFun Nat (TyFun a1627953291 [a1627953291] -> Type) -> *) (ReplicateSym0 a1627953291)

Methods

suppressUnusedWarnings :: Proxy (ReplicateSym0 a1627953291) t -> ()

SuppressUnusedWarnings (TyFun Nat a1627817219 -> *) (FromIntegerSym0 a1627817219)

Methods

suppressUnusedWarnings :: Proxy (FromIntegerSym0 a1627817219) t -> ()

SuppressUnusedWarnings (TyFun Nat a1627864213 -> *) (ToEnumSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (ToEnumSym0 a1627864213) t -> ()

SuppressUnusedWarnings (TyFun a1627864213 Nat -> *) (FromEnumSym0 a1627864213)

Methods

suppressUnusedWarnings :: Proxy (FromEnumSym0 a1627864213) t -> ()

SuppressUnusedWarnings (TyFun a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a1627953318)

Methods

suppressUnusedWarnings :: Proxy (ElemIndexSym0 a1627953318) t -> ()

SuppressUnusedWarnings (TyFun a1627953317 (TyFun [a1627953317] [Nat] -> Type) -> *) (ElemIndicesSym0 a1627953317)

Methods

suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a1627953317) t -> ()

type DemoteRep Nat

type DemoteRep Nat = Integer

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

type Negate Nat a

type Negate Nat a = Error Nat Symbol "Cannot negate a natural number"

type Abs Nat a

type Abs Nat a = a

type Signum Nat a

type Signum Nat a

type FromInteger Nat a

type FromInteger Nat a = a

type Succ Nat a0

type Succ Nat a0

type Pred Nat a0

type Pred Nat a0

type ToEnum Nat a0

type ToEnum Nat a0

type FromEnum Nat a0

type FromEnum Nat a0

type (==) Nat a b

type (==) Nat a b = EqNat a b

type (:==) Nat a b

type (:==) Nat a b = (==) Nat a b

type (:/=) Nat x y

type (:/=) Nat x y = Not ((:==) Nat x y)

type Compare Nat a b

type Compare Nat a b = CmpNat a b

type (:<) Nat arg0 arg1

type (:<) Nat arg0 arg1

type (:<=) Nat arg0 arg1

type (:<=) Nat arg0 arg1

type (:>) Nat arg0 arg1

type (:>) Nat arg0 arg1

type (:>=) Nat arg0 arg1

type (:>=) Nat arg0 arg1

type Max Nat arg0 arg1

type Max Nat arg0 arg1

type Min Nat arg0 arg1

type Min Nat arg0 arg1

type (:+) Nat a b

type (:+) Nat a b = (+) a b

type (:-) Nat a b

type (:-) Nat a b = (-) a b

type (:*) Nat a b

type (:*) Nat a b = * a b

type EnumFromTo Nat a0 a1

type EnumFromTo Nat a0 a1

type EnumFromThenTo Nat a0 a1 a2

type EnumFromThenTo Nat a0 a1 a2

type Apply Nat Nat ((:^$$) l1) l0

type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0

type Apply Nat k2 (FromIntegerSym0 k2) l0

type Apply Nat k2 (FromIntegerSym0 k2) l0 = FromIntegerSym1 k2 l0

type Apply Nat k2 (ToEnumSym0 k2) l0

type Apply Nat k2 (ToEnumSym0 k2) l0 = ToEnumSym1 k2 l0

type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0

type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 = FromEnumSym1 a1627864213 l0

type Apply Nat a1627953289 ((:!!$$) a1627953289 l1) l0

type Apply Nat a1627953289 ((:!!$$) a1627953289 l1) l0 = (:!!$$$) a1627953289 l1 l0

type Apply Nat (TyFun Nat Nat -> *) (:^$) l0

type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0

type Apply Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) (SplitAtSym0 a1627953305) l0

type Apply Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) (SplitAtSym0 a1627953305) l0 = SplitAtSym1 a1627953305 l0

type Apply Nat (TyFun [a1627953307] [a1627953307] -> Type) (TakeSym0 a1627953307) l0

type Apply Nat (TyFun [a1627953307] [a1627953307] -> Type) (TakeSym0 a1627953307) l0 = TakeSym1 a1627953307 l0

type Apply Nat (TyFun [a1627953306] [a1627953306] -> Type) (DropSym0 a1627953306) l0

type Apply Nat (TyFun [a1627953306] [a1627953306] -> Type) (DropSym0 a1627953306) l0 = DropSym1 a1627953306 l0

type Apply Nat (TyFun a1627953291 [a1627953291] -> Type) (ReplicateSym0 a1627953291) l0

type Apply Nat (TyFun a1627953291 [a1627953291] -> Type) (ReplicateSym0 a1627953291) l0 = ReplicateSym1 a1627953291 l0

type Apply a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) (ElemIndexSym0 a1627953318) l0

type Apply a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) (ElemIndexSym0 a1627953318) l0 = ElemIndexSym1 a1627953318 l0

type Apply a1627953317 (TyFun [a1627953317] [Nat] -> Type) (ElemIndicesSym0 a1627953317) l0

type Apply a1627953317 (TyFun [a1627953317] [Nat] -> Type) (ElemIndicesSym0 a1627953317) l0 = ElemIndicesSym1 a1627953317 l0

type Apply [a1627953292] Nat (LengthSym0 a1627953292) l0

type Apply [a1627953292] Nat (LengthSym0 a1627953292) l0 = LengthSym1 a1627953292 l0

type Apply [a1627953318] (Maybe Nat) (ElemIndexSym1 a1627953318 l1) l0

type Apply [a1627953318] (Maybe Nat) (ElemIndexSym1 a1627953318 l1) l0 = ElemIndexSym2 a1627953318 l1 l0

type Apply [a1627953316] (Maybe Nat) (FindIndexSym1 a1627953316 l1) l0

type Apply [a1627953316] (Maybe Nat) (FindIndexSym1 a1627953316 l1) l0 = FindIndexSym2 a1627953316 l1 l0

type Apply [a1627953317] [Nat] (ElemIndicesSym1 a1627953317 l1) l0

type Apply [a1627953317] [Nat] (ElemIndicesSym1 a1627953317 l1) l0 = ElemIndicesSym2 a1627953317 l1 l0

type Apply [a1627953315] [Nat] (FindIndicesSym1 a1627953315 l1) l0

type Apply [a1627953315] [Nat] (FindIndicesSym1 a1627953315 l1) l0 = FindIndicesSym2 a1627953315 l1 l0

type Apply [a1627953289] (TyFun Nat a1627953289 -> Type) ((:!!$) a1627953289) l0

type Apply [a1627953289] (TyFun Nat a1627953289 -> Type) ((:!!$) a1627953289) l0 = (:!!$$) a1627953289 l0

type Apply (TyFun a1627953316 Bool -> Type) (TyFun [a1627953316] (Maybe Nat) -> Type) (FindIndexSym0 a1627953316) l0

type Apply (TyFun a1627953316 Bool -> Type) (TyFun [a1627953316] (Maybe Nat) -> Type) (FindIndexSym0 a1627953316) l0 = FindIndexSym1 a1627953316 l0

type Apply (TyFun a1627953315 Bool -> Type) (TyFun [a1627953315] [Nat] -> Type) (FindIndicesSym0 a1627953315) l0

type Apply (TyFun a1627953315 Bool -> Type) (TyFun [a1627953315] [Nat] -> Type) (FindIndicesSym0 a1627953315) l0 = FindIndicesSym1 a1627953315 l0

data Symbol :: *

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

KnownSymbol a => SingI Symbol a

Methods

sing :: Sing a a

SingKind Symbol (KProxy Symbol)

Associated Types

type DemoteRep (KProxy Symbol) (kparam :: KProxy (KProxy Symbol)) :: *

Methods

fromSing :: Sing (KProxy Symbol) a -> DemoteRep (KProxy Symbol) kparam

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol s

type DemoteRep Symbol

type DemoteRep Symbol = String

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

type (==) Symbol a b

type (==) Symbol a b = EqSymbol a b

type (:==) Symbol a b

type (:==) Symbol a b = (==) Symbol a b

type (:/=) Symbol x y

type (:/=) Symbol x y = Not ((:==) Symbol x y)

type Compare Symbol a b

type Compare Symbol a b = CmpSymbol a b

type (:<) Symbol arg0 arg1

type (:<) Symbol arg0 arg1

type (:<=) Symbol arg0 arg1

type (:<=) Symbol arg0 arg1

type (:>) Symbol arg0 arg1

type (:>) Symbol arg0 arg1

type (:>=) Symbol arg0 arg1

type (:>=) Symbol arg0 arg1

type Max Symbol arg0 arg1

type Max Symbol arg0 arg1

type Min Symbol arg0 arg1

type Min Symbol arg0 arg1

type DemoteRep Symbol (KProxy Symbol)

type DemoteRep Symbol (KProxy Symbol) = String

data family Sing (a :: k)

The singleton kind-indexed data family.

Instances

data Sing Bool

data Sing Bool where

• SFalse :: Sing Bool z
• STrue :: Sing Bool z

data Sing Ordering

data Sing Ordering where

• SLT :: Sing Ordering z
• SEQ :: Sing Ordering z
• SGT :: Sing Ordering z

data Sing *

data Sing * where

• STypeRep :: Sing * a

data Sing Nat

data Sing Nat where

• SNat :: Sing Nat n

data Sing Symbol

data Sing Symbol where

• SSym :: Sing Symbol n

data Sing ()

data Sing () where

• STuple0 :: Sing () z

data Sing [a0]

data Sing [a0] where

• SNil :: Sing [a] z
• SCons :: Sing [a] z

data Sing (Maybe a0)

data Sing (Maybe a0) where

• SNothing :: Sing (Maybe a) z
• SJust :: Sing (Maybe a) z

data Sing (NonEmpty a0)

data Sing (NonEmpty a0) where

• (:%|) :: Sing (NonEmpty a) z

data Sing (Either a0 b0)

data Sing (Either a0 b0) where

• SLeft :: Sing (Either a b) z
• SRight :: Sing (Either a b) z

data Sing (a0, b0)

data Sing (a0, b0) where

• STuple2 :: Sing (a, b) z

data Sing ((~>) k1 k2)

data Sing ((~>) k1 k2) = SLambda {

• applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t)

}

data Sing (a0, b0, c0)

data Sing (a0, b0, c0) where

• STuple3 :: Sing (a, b, c) z

data Sing (a0, b0, c0, d0)

data Sing (a0, b0, c0, d0) where

• STuple4 :: Sing (a, b, c, d) z

data Sing (a0, b0, c0, d0, e0)

data Sing (a0, b0, c0, d0, e0) where

• STuple5 :: Sing (a, b, c, d, e) z

data Sing (a0, b0, c0, d0, e0, f0)

data Sing (a0, b0, c0, d0, e0, f0) where

• STuple6 :: Sing (a, b, c, d, e, f) z

data Sing (a0, b0, c0, d0, e0, f0, g0)

data Sing (a0, b0, c0, d0, e0, f0, g0) where

• STuple7 :: Sing (a, b, c, d, e, f, g) z

type SNat x = Sing x

Kind-restricted synonym for Sing for Nats

type SSymbol x = Sing x

Kind-restricted synonym for Sing for Symbols

withKnownNat :: Sing n -> (KnownNat n => r) -> r

Given a singleton for Nat, call something requiring a KnownNat instance.

withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r

Given a singleton for Symbol, call something requiring a KnownSymbol instance.

type family Error (str :: k0) :: k

The promotion of error. This version is more poly-kinded for easier use.

data ErrorSym0 l

Instances

SuppressUnusedWarnings (TyFun k01627810588 k1627810590 -> *) (ErrorSym0 k01627810588 k1627810590)

Methods

suppressUnusedWarnings :: Proxy (ErrorSym0 k01627810588 k1627810590) t -> ()

type Apply k01627810588 k2 (ErrorSym0 k01627810588 k2) l0

type Apply k01627810588 k2 (ErrorSym0 k01627810588 k2) l0 = ErrorSym1 k01627810588 k2 l0

type ErrorSym1 t = Error t

sError :: Sing (str :: Symbol) -> a

The singleton for error

class KnownNat n

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: 4.7.0.0

Minimal complete definition

natSing

natVal :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0

class KnownSymbol n

This class gives the string associated with a type-level symbol. There are instances of the class for every concrete literal: "hello", etc.

Since: 4.7.0.0

Minimal complete definition

symbolSing

symbolVal :: KnownSymbol n => proxy n -> String

Since: 4.7.0.0

type (:^) a b = a ^ b infixr 8

data (:^$) l

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$)

Methods

suppressUnusedWarnings :: Proxy (:^$) t -> ()

type Apply Nat (TyFun Nat Nat -> *) (:^$) l0

type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0

data l :^$$ l

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$)

Methods

suppressUnusedWarnings :: Proxy (:^$$) t -> ()

type Apply Nat Nat ((:^$$) l1) l0

type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0

type (:^$$$) t t = (:^) t t

Orphan instances

Num Nat

Methods

(+) :: Nat -> Nat -> Nat

(-) :: Nat -> Nat -> Nat

(*) :: Nat -> Nat -> Nat

negate :: Nat -> Nat

abs :: Nat -> Nat

signum :: Nat -> Nat

fromInteger :: Integer -> Nat