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 (KProxy Nat)

PNum Nat (KProxy Nat)

SEnum Nat (KProxy Nat)

PEnum Nat (KProxy Nat)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> *) -> *) (TakeSym0 k)

SuppressUnusedWarnings (TyFun Nat (TyFun [k] [k] -> *) -> *) (DropSym0 k)

SuppressUnusedWarnings (TyFun Nat (TyFun k [k] -> *) -> *) (ReplicateSym0 k)

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

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

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

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

SuppressUnusedWarnings (TyFun k (TyFun [k] [Nat] -> *) -> *) (ElemIndicesSym0 k)

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

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

type Abs Nat a = a

type Signum Nat a

type FromInteger Nat a = a

type Succ Nat a0

type Pred Nat a0

type ToEnum Nat a0

type FromEnum Nat a0

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

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

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

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 Max Nat arg0 arg1

type Min Nat arg0 arg1

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

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

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

type EnumFromTo Nat a0 a1

type EnumFromThenTo Nat a0 a1 a2

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

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

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

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

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

type DemoteRep Nat (KProxy Nat) = Integer

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

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

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

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

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

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

type Apply (TyFun [k] (Maybe Nat) -> *) k (ElemIndexSym0 k) l0 = ElemIndexSym1 k l0

type Apply (TyFun [k] [Nat] -> *) k (ElemIndicesSym0 k) l0 = ElemIndicesSym1 k l0

type Apply (TyFun [k] ((,) [k] [k]) -> *) Nat (SplitAtSym0 k) l0 = SplitAtSym1 k l0

type Apply (TyFun [k] [k] -> *) Nat (TakeSym0 k) l0 = TakeSym1 k l0

type Apply (TyFun [k] [k] -> *) Nat (DropSym0 k) l0 = DropSym1 k l0

type Apply (TyFun k [k] -> *) Nat (ReplicateSym0 k) l0 = ReplicateSym1 k l0

type Apply (TyFun Nat k -> *) [k] ((:!!$) k) l0 = (:!!$$) k l0

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

type Apply (TyFun [k] [Nat] -> *) (TyFun k Bool -> *) (FindIndicesSym0 k) l0 = FindIndicesSym1 k l0

data Symbol :: *

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

Instances

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

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

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

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

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 Max Symbol arg0 arg1

type Min Symbol arg0 arg1

type DemoteRep Symbol (KProxy Symbol) = String

data family Sing a

The singleton kind-indexed data family.

Instances

data Sing Bool where

• SFalse :: (~) Bool z False => Sing Bool z
• STrue :: (~) Bool z True => Sing Bool z

data Sing Ordering where

• SLT :: (~) Ordering z LT => Sing Ordering z
• SEQ :: (~) Ordering z EQ => Sing Ordering z
• SGT :: (~) Ordering z GT => Sing Ordering z

data Sing * where

• STypeRep :: Typeable * a => Sing * a

data Sing Nat where

• SNat :: KnownNat n => Sing Nat n

data Sing Symbol where

• SSym :: KnownSymbol n => Sing Symbol n

data Sing () where

• STuple0 :: (~) () z () => Sing () z

data Sing [a0] where

• SNil :: (~) [a] z ([] a) => Sing [a] z
• SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z

data Sing (Maybe a0) where

• SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z
• SJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z

data Sing (TyFun k1 k2 -> *) = SLambda {

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

}

data Sing (Either a0 b0) where

• SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z
• SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z

data Sing ((,) a0 b0) where

• STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z

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

• STuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z

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

• STuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z

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

• STuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z

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

• STuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z

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

• STuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> 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 :: k

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

data ErrorSym0 l

Instances

SuppressUnusedWarnings (TyFun k k -> *) (ErrorSym0 k k)

type Apply k k1 (ErrorSym0 k1 k) l0 = ErrorSym1 k1 k 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 -> *) -> *) (:^$)

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

data l :^$$ l

Instances

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

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

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