Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.TypeLits

Contents

Orphan instances

Description

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.

Synopsis

Documentation

data Nat :: * #

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

Instances

SNum Nat Source #
Methods (%:+) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:+$) Nat) t) t) Source # (%:-) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:-$) Nat) t) t) Source # (%:) :: Sing Nat t -> Sing Nat t -> Sing Nat (Apply Nat Nat (Apply Nat (TyFun Nat Nat -> Type) ((:$) Nat) t) t) Source # sNegate :: Sing Nat t -> Sing Nat (Apply Nat Nat (NegateSym0 Nat) t) Source # sAbs :: Sing Nat t -> Sing Nat (Apply Nat Nat (AbsSym0 Nat) t) Source # sSignum :: Sing Nat t -> Sing Nat (Apply Nat Nat (SignumSym0 Nat) t) Source # sFromInteger :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromIntegerSym0 Nat) t) Source #
SEnum Nat Source #
Methods sSucc :: Sing Nat t -> Sing Nat (Apply Nat Nat (SuccSym0 Nat) t) Source # sPred :: Sing Nat t -> Sing Nat (Apply Nat Nat (PredSym0 Nat) t) Source # sToEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (ToEnumSym0 Nat) t) Source # sFromEnum :: Sing Nat t -> Sing Nat (Apply Nat Nat (FromEnumSym0 Nat) t) Source # sEnumFromTo :: Sing Nat t -> Sing Nat t -> Sing [Nat] (Apply Nat [Nat] (Apply Nat (TyFun Nat [Nat] -> Type) (EnumFromToSym0 Nat) t) t) Source # 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) Source #
PNum Nat (Proxy * Nat) Source #
Associated Types type ((Proxy * Nat) :+ (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a Source # type ((Proxy * Nat) :- (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a Source # type ((Proxy * Nat) :* (arg :: Proxy * Nat)) (arg :: Proxy * Nat) :: a Source # type Negate (Proxy * Nat) (arg :: Proxy * Nat) :: a Source # type Abs (Proxy * Nat) (arg :: Proxy * Nat) :: a Source # type Signum (Proxy * Nat) (arg :: Proxy * Nat) :: a Source # type FromInteger (Proxy * Nat) (arg :: Nat) :: a Source #
PEnum Nat (Proxy * Nat) Source #
Associated Types type Succ (Proxy * Nat) (arg :: Proxy * Nat) :: a Source # type Pred (Proxy * Nat) (arg :: Proxy * Nat) :: a Source # type ToEnum (Proxy * Nat) (arg :: Nat) :: a Source # type FromEnum (Proxy * Nat) (arg :: Proxy * Nat) :: Nat Source # type EnumFromTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a] Source # type EnumFromThenTo (Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) (arg :: Proxy * Nat) :: [a] Source #
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) Source #
Methods suppressUnusedWarnings :: Proxy (:^$$) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:^$) Source #
Methods suppressUnusedWarnings :: Proxy (:^$) t -> () Source #
SuppressUnusedWarnings ((TyFun a1627953316 Bool -> Type) -> TyFun [a1627953316] (Maybe Nat) -> *) (FindIndexSym1 a1627953316) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym1 a1627953316) t -> () Source #
SuppressUnusedWarnings ((TyFun a1627953315 Bool -> Type) -> TyFun [a1627953315] [Nat] -> *) (FindIndicesSym1 a1627953315) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym1 a1627953315) t -> () Source #
SuppressUnusedWarnings ([a1627953289] -> TyFun Nat a1627953289 -> *) ((:!!$$) a1627953289) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a1627953289) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a1627953305] ([a1627953305], [a1627953305]) -> *) (SplitAtSym1 a1627953305) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a1627953305) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a1627953307] [a1627953307] -> *) (TakeSym1 a1627953307) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a1627953307) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a1627953306] [a1627953306] -> *) (DropSym1 a1627953306) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a1627953306) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun a1627953291 [a1627953291] -> *) (ReplicateSym1 a1627953291) Source #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym1 a1627953291) t -> () Source #
SuppressUnusedWarnings (a1627953318 -> TyFun [a1627953318] (Maybe Nat) -> *) (ElemIndexSym1 a1627953318) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym1 a1627953318) t -> () Source #
SuppressUnusedWarnings (a1627953317 -> TyFun [a1627953317] [Nat] -> *) (ElemIndicesSym1 a1627953317) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a1627953317) t -> () Source #
SuppressUnusedWarnings (TyFun (TyFun a1627953316 Bool -> Type) (TyFun [a1627953316] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a1627953316) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym0 a1627953316) t -> () Source #
SuppressUnusedWarnings (TyFun (TyFun a1627953315 Bool -> Type) (TyFun [a1627953315] [Nat] -> Type) -> *) (FindIndicesSym0 a1627953315) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym0 a1627953315) t -> () Source #
SuppressUnusedWarnings (TyFun [a1627953292] Nat -> *) (LengthSym0 a1627953292) Source #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a1627953292) t -> () Source #
SuppressUnusedWarnings (TyFun [a1627953289] (TyFun Nat a1627953289 -> Type) -> *) ((:!!$) a1627953289) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a1627953289) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) -> *) (SplitAtSym0 a1627953305) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a1627953305) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953307] [a1627953307] -> Type) -> *) (TakeSym0 a1627953307) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a1627953307) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a1627953306] [a1627953306] -> Type) -> *) (DropSym0 a1627953306) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a1627953306) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun a1627953291 [a1627953291] -> Type) -> *) (ReplicateSym0 a1627953291) Source #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym0 a1627953291) t -> () Source #
SuppressUnusedWarnings (TyFun Nat a1627817219 -> *) (FromIntegerSym0 a1627817219) Source #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a1627817219) t -> () Source #
SuppressUnusedWarnings (TyFun Nat a1627864213 -> *) (ToEnumSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a1627864213) t -> () Source #
SuppressUnusedWarnings (TyFun a1627864213 Nat -> *) (FromEnumSym0 a1627864213) Source #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a1627864213) t -> () Source #
SuppressUnusedWarnings (TyFun a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a1627953318) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym0 a1627953318) t -> () Source #
SuppressUnusedWarnings (TyFun a1627953317 (TyFun [a1627953317] [Nat] -> Type) -> *) (ElemIndicesSym0 a1627953317) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a1627953317) t -> () Source #
type DemoteRep Nat Source #
type DemoteRep Nat = Integer
data Sing Nat Source #
data Sing Nat where SNat :: Sing Nat n
type Negate Nat a Source #
type Negate Nat a = Error Nat Symbol "Cannot negate a natural number"
type Abs Nat a Source #
type Abs Nat a = a
type Signum Nat a Source #
type Signum Nat a
type FromInteger Nat a Source #
type FromInteger Nat a = a
type Succ Nat a0 Source #
type Succ Nat a0
type Pred Nat a0 Source #
type Pred Nat a0
type ToEnum Nat a0 Source #
type ToEnum Nat a0
type FromEnum Nat a0 Source #
type FromEnum Nat a0
type (==) Nat a b
type (==) Nat a b = EqNat a b
type (:==) Nat a b Source #
type (:==) Nat a b = (==) Nat a b
type (:/=) Nat x y Source #
type (:/=) Nat x y = Not ((:==) Nat x y)
type Compare Nat a b Source #
type Compare Nat a b = CmpNat a b
type (:<) Nat arg0 arg1 Source #
type (:<) Nat arg0 arg1
type (:<=) Nat arg0 arg1 Source #
type (:<=) Nat arg0 arg1
type (:>) Nat arg0 arg1 Source #
type (:>) Nat arg0 arg1
type (:>=) Nat arg0 arg1 Source #
type (:>=) Nat arg0 arg1
type Max Nat arg0 arg1 Source #
type Max Nat arg0 arg1
type Min Nat arg0 arg1 Source #
type Min Nat arg0 arg1
type (:+) Nat a b Source #
type (:+) Nat a b = (+) a b
type (:-) Nat a b Source #
type (:-) Nat a b = (-) a b
type (:*) Nat a b Source #
type (:) Nat a b = a b
type EnumFromTo Nat a0 a1 Source #
type EnumFromTo Nat a0 a1
type EnumFromThenTo Nat a0 a1 a2 Source #
type EnumFromThenTo Nat a0 a1 a2
type Apply Nat Nat ((:^$$) l1) l0 Source #
type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0
type Apply Nat k2 (FromIntegerSym0 k2) l0 Source #
type Apply Nat k2 (FromIntegerSym0 k2) l0 = FromIntegerSym1 k2 l0
type Apply Nat k2 (ToEnumSym0 k2) l0 Source #
type Apply Nat k2 (ToEnumSym0 k2) l0 = ToEnumSym1 k2 l0
type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 Source #
type Apply a1627864213 Nat (FromEnumSym0 a1627864213) l0 = FromEnumSym1 a1627864213 l0
type Apply Nat a1627953289 ((:!!$$) a1627953289 l1) l0 Source #
type Apply Nat a1627953289 ((:!!$$) a1627953289 l1) l0 = (:!!$$$) a1627953289 l1 l0
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 Source #
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0
type Apply Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) (SplitAtSym0 a1627953305) l0 Source #
type Apply Nat (TyFun [a1627953305] ([a1627953305], [a1627953305]) -> Type) (SplitAtSym0 a1627953305) l0 = SplitAtSym1 a1627953305 l0
type Apply Nat (TyFun [a1627953307] [a1627953307] -> Type) (TakeSym0 a1627953307) l0 Source #
type Apply Nat (TyFun [a1627953307] [a1627953307] -> Type) (TakeSym0 a1627953307) l0 = TakeSym1 a1627953307 l0
type Apply Nat (TyFun [a1627953306] [a1627953306] -> Type) (DropSym0 a1627953306) l0 Source #
type Apply Nat (TyFun [a1627953306] [a1627953306] -> Type) (DropSym0 a1627953306) l0 = DropSym1 a1627953306 l0
type Apply Nat (TyFun a1627953291 [a1627953291] -> Type) (ReplicateSym0 a1627953291) l0 Source #
type Apply Nat (TyFun a1627953291 [a1627953291] -> Type) (ReplicateSym0 a1627953291) l0 = ReplicateSym1 a1627953291 l0
type Apply a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) (ElemIndexSym0 a1627953318) l0 Source #
type Apply a1627953318 (TyFun [a1627953318] (Maybe Nat) -> Type) (ElemIndexSym0 a1627953318) l0 = ElemIndexSym1 a1627953318 l0
type Apply a1627953317 (TyFun [a1627953317] [Nat] -> Type) (ElemIndicesSym0 a1627953317) l0 Source #
type Apply a1627953317 (TyFun [a1627953317] [Nat] -> Type) (ElemIndicesSym0 a1627953317) l0 = ElemIndicesSym1 a1627953317 l0
type Apply [a1627953292] Nat (LengthSym0 a1627953292) l0 Source #
type Apply [a1627953292] Nat (LengthSym0 a1627953292) l0 = LengthSym1 a1627953292 l0
type Apply [a1627953318] (Maybe Nat) (ElemIndexSym1 a1627953318 l1) l0 Source #
type Apply [a1627953318] (Maybe Nat) (ElemIndexSym1 a1627953318 l1) l0 = ElemIndexSym2 a1627953318 l1 l0
type Apply [a1627953316] (Maybe Nat) (FindIndexSym1 a1627953316 l1) l0 Source #
type Apply [a1627953316] (Maybe Nat) (FindIndexSym1 a1627953316 l1) l0 = FindIndexSym2 a1627953316 l1 l0
type Apply [a1627953317] [Nat] (ElemIndicesSym1 a1627953317 l1) l0 Source #
type Apply [a1627953317] [Nat] (ElemIndicesSym1 a1627953317 l1) l0 = ElemIndicesSym2 a1627953317 l1 l0
type Apply [a1627953315] [Nat] (FindIndicesSym1 a1627953315 l1) l0 Source #
type Apply [a1627953315] [Nat] (FindIndicesSym1 a1627953315 l1) l0 = FindIndicesSym2 a1627953315 l1 l0
type Apply [a1627953289] (TyFun Nat a1627953289 -> Type) ((:!!$) a1627953289) l0 Source #
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 Source #
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 Source #
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 Source #
type DemoteRep Symbol = String
data Sing Symbol Source #
data Sing Symbol where SSym :: Sing Symbol n
type (==) Symbol a b
type (==) Symbol a b = EqSymbol a b
type (:==) Symbol a b Source #
type (:==) Symbol a b = (==) Symbol a b
type (:/=) Symbol x y Source #
type (:/=) Symbol x y = Not ((:==) Symbol x y)
type Compare Symbol a b Source #
type Compare Symbol a b = CmpSymbol a b
type (:<) Symbol arg0 arg1 Source #
type (:<) Symbol arg0 arg1
type (:<=) Symbol arg0 arg1 Source #
type (:<=) Symbol arg0 arg1
type (:>) Symbol arg0 arg1 Source #
type (:>) Symbol arg0 arg1
type (:>=) Symbol arg0 arg1 Source #
type (:>=) Symbol arg0 arg1
type Max Symbol arg0 arg1 Source #
type Max Symbol arg0 arg1
type Min Symbol arg0 arg1 Source #
type Min Symbol arg0 arg1
type DemoteRep Symbol (KProxy Symbol)
type DemoteRep Symbol (KProxy Symbol) = String

data family Sing (a :: k) Source #

The singleton kind-indexed data family.

Instances

data Sing Bool Source #
data Sing Bool where SFalse :: Sing Bool z STrue :: Sing Bool z
data Sing Ordering Source #
data Sing Ordering where SLT :: Sing Ordering z SEQ :: Sing Ordering z SGT :: Sing Ordering z
data Sing * Source #
data Sing * where STypeRep :: Sing * a
data Sing Nat Source #
data Sing Nat where SNat :: Sing Nat n
data Sing Symbol Source #
data Sing Symbol where SSym :: Sing Symbol n
data Sing () Source #
data Sing () where STuple0 :: Sing () z
data Sing [a0] Source #
data Sing [a0] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a0) Source #
data Sing (Maybe a0) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a0) Source #
data Sing (NonEmpty a0) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a0 b0) Source #
data Sing (Either a0 b0) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a0, b0) Source #
data Sing (a0, b0) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2) Source #
data Sing ((~>) k1 k2) = SLambda { applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a0, b0, c0) Source #
data Sing (a0, b0, c0) where STuple3 :: Sing (a, b, c) z
data Sing (a0, b0, c0, d0) Source #
data Sing (a0, b0, c0, d0) where STuple4 :: Sing (a, b, c, d) z
data Sing (a0, b0, c0, d0, e0) Source #
data Sing (a0, b0, c0, d0, e0) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a0, b0, c0, d0, e0, f0) Source #
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) Source #
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 Source #

Kind-restricted synonym for Sing for Nats

type SSymbol x = Sing x Source #

Kind-restricted synonym for Sing for Symbols

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

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

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

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

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

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

data ErrorSym0 l Source #

Instances

SuppressUnusedWarnings (TyFun k01627810588 k1627810590 -> *) (ErrorSym0 k01627810588 k1627810590) Source #
Methods suppressUnusedWarnings :: Proxy (ErrorSym0 k01627810588 k1627810590) t -> () Source #
type Apply k01627810588 k2 (ErrorSym0 k01627810588 k2) l0 Source #
type Apply k01627810588 k2 (ErrorSym0 k01627810588 k2) l0 = ErrorSym1 k01627810588 k2 l0

type ErrorSym1 t = Error t Source #

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

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

data (:^$) l Source #

Instances

SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> ) -> ) (:^$) Source #
Methods suppressUnusedWarnings :: Proxy (:^$) t -> () Source #
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 Source #
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 = (:^$$) l0

data l :^$$ l Source #

Instances

SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) Source #
Methods suppressUnusedWarnings :: Proxy (:^$$) t -> () Source #
type Apply Nat Nat ((:^$$) l1) l0 Source #
type Apply Nat Nat ((:^$$) l1) l0 = (:^$$$) l1 l0

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

Orphan instances

Num Nat Source #
Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #