Copyright	(C) 2014 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (rae@cs.brynmawr.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.

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 #
PNum Nat Source #
Associated Types type (Nat :+ (arg :: Nat)) (arg :: Nat) :: a Source # type (Nat :- (arg :: Nat)) (arg :: Nat) :: a Source # type (Nat :* (arg :: Nat)) (arg :: Nat) :: a Source # type Negate Nat (arg :: Nat) :: a Source # type Abs Nat (arg :: Nat) :: a Source # type Signum Nat (arg :: Nat) :: a Source # type FromInteger Nat (arg :: Nat) :: a 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 #
PEnum Nat Source #
Associated Types type Succ Nat (arg :: Nat) :: a Source # type Pred Nat (arg :: Nat) :: a Source # type ToEnum Nat (arg :: Nat) :: a Source # type FromEnum Nat (arg :: Nat) :: Nat Source # type EnumFromTo Nat (arg :: Nat) (arg :: Nat) :: [a] Source # type EnumFromThenTo Nat (arg :: Nat) (arg :: Nat) (arg :: 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 Nat Constraint -> *) KnownNatSym0 Source #
Methods suppressUnusedWarnings :: Proxy KnownNatSym0 t -> () Source #
SuppressUnusedWarnings ((TyFun a6989586621679458102 Bool -> Type) -> TyFun [a6989586621679458102] [Nat] -> *) (FindIndicesSym1 a6989586621679458102) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym1 a6989586621679458102) t -> () Source #
SuppressUnusedWarnings ((TyFun a6989586621679458103 Bool -> Type) -> TyFun [a6989586621679458103] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679458103) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym1 a6989586621679458103) t -> () Source #
SuppressUnusedWarnings ([a6989586621679458076] -> TyFun Nat a6989586621679458076 -> *) ((:!!$$) a6989586621679458076) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679458076) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679458093] [a6989586621679458093] -> *) (DropSym1 a6989586621679458093) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679458093) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679458094] [a6989586621679458094] -> *) (TakeSym1 a6989586621679458094) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679458094) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]) -> *) (SplitAtSym1 a6989586621679458092) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679458092) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun a6989586621679458078 [a6989586621679458078] -> *) (ReplicateSym1 a6989586621679458078) Source #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym1 a6989586621679458078) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679729633) [a6989586621679729633] -> *) (TakeSym1 a6989586621679729633) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym1 a6989586621679729633) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679729632) [a6989586621679729632] -> *) (DropSym1 a6989586621679729632) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym1 a6989586621679729632) t -> () Source #
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679729631) ([a6989586621679729631], [a6989586621679729631]) -> *) (SplitAtSym1 a6989586621679729631) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym1 a6989586621679729631) t -> () Source #
SuppressUnusedWarnings (a6989586621679458104 -> TyFun [a6989586621679458104] [Nat] -> *) (ElemIndicesSym1 a6989586621679458104) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym1 a6989586621679458104) t -> () Source #
SuppressUnusedWarnings (a6989586621679458105 -> TyFun [a6989586621679458105] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679458105) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym1 a6989586621679458105) t -> () Source #
SuppressUnusedWarnings (NonEmpty a6989586621679729611 -> TyFun Nat a6989586621679729611 -> *) ((:!!$$) a6989586621679729611) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$$) a6989586621679729611) t -> () Source #
SuppressUnusedWarnings (TyFun (TyFun a6989586621679458102 Bool -> Type) (TyFun [a6989586621679458102] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679458102) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndicesSym0 a6989586621679458102) t -> () Source #
SuppressUnusedWarnings (TyFun (TyFun a6989586621679458103 Bool -> Type) (TyFun [a6989586621679458103] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679458103) Source #
Methods suppressUnusedWarnings :: Proxy (FindIndexSym0 a6989586621679458103) t -> () Source #
SuppressUnusedWarnings (TyFun [a6989586621679458076] (TyFun Nat a6989586621679458076 -> Type) -> *) ((:!!$) a6989586621679458076) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679458076) t -> () Source #
SuppressUnusedWarnings (TyFun [a6989586621679458079] Nat -> *) (LengthSym0 a6989586621679458079) Source #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679458079) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679458093] [a6989586621679458093] -> Type) -> *) (DropSym0 a6989586621679458093) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679458093) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679458094] [a6989586621679458094] -> Type) -> *) (TakeSym0 a6989586621679458094) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679458094) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]) -> Type) -> *) (SplitAtSym0 a6989586621679458092) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679458092) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679458078 [a6989586621679458078] -> Type) -> *) (ReplicateSym0 a6989586621679458078) Source #
Methods suppressUnusedWarnings :: Proxy (ReplicateSym0 a6989586621679458078) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679729633) [a6989586621679729633] -> Type) -> *) (TakeSym0 a6989586621679729633) Source #
Methods suppressUnusedWarnings :: Proxy (TakeSym0 a6989586621679729633) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679729632) [a6989586621679729632] -> Type) -> *) (DropSym0 a6989586621679729632) Source #
Methods suppressUnusedWarnings :: Proxy (DropSym0 a6989586621679729632) t -> () Source #
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679729631) ([a6989586621679729631], [a6989586621679729631]) -> Type) -> *) (SplitAtSym0 a6989586621679729631) Source #
Methods suppressUnusedWarnings :: Proxy (SplitAtSym0 a6989586621679729631) t -> () Source #
SuppressUnusedWarnings (TyFun Nat a6989586621679410509 -> *) (FromIntegerSym0 a6989586621679410509) Source #
Methods suppressUnusedWarnings :: Proxy (FromIntegerSym0 a6989586621679410509) t -> () Source #
SuppressUnusedWarnings (TyFun Nat a6989586621679809090 -> *) (ToEnumSym0 a6989586621679809090) Source #
Methods suppressUnusedWarnings :: Proxy (ToEnumSym0 a6989586621679809090) t -> () Source #
SuppressUnusedWarnings (TyFun a6989586621679458104 (TyFun [a6989586621679458104] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679458104) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndicesSym0 a6989586621679458104) t -> () Source #
SuppressUnusedWarnings (TyFun a6989586621679458105 (TyFun [a6989586621679458105] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679458105) Source #
Methods suppressUnusedWarnings :: Proxy (ElemIndexSym0 a6989586621679458105) t -> () Source #
SuppressUnusedWarnings (TyFun a6989586621679809090 Nat -> *) (FromEnumSym0 a6989586621679809090) Source #
Methods suppressUnusedWarnings :: Proxy (FromEnumSym0 a6989586621679809090) t -> () Source #
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679729611) (TyFun Nat a6989586621679729611 -> Type) -> *) ((:!!$) a6989586621679729611) Source #
Methods suppressUnusedWarnings :: Proxy ((:!!$) a6989586621679729611) t -> () Source #
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679729664) Nat -> *) (LengthSym0 a6989586621679729664) Source #
Methods suppressUnusedWarnings :: Proxy (LengthSym0 a6989586621679729664) t -> () Source #
type Demote Nat Source #
type Demote Nat = Integer
data Sing Nat Source #
data Sing Nat where SNat :: Sing Nat n
type Negate Nat a Source #
type Negate Nat a = Error Symbol Nat "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 a Source #
type Succ Nat a
type Pred Nat a Source #
type Pred Nat a
type ToEnum Nat a Source #
type ToEnum Nat a
type FromEnum Nat a Source #
type FromEnum Nat a
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 arg1 arg2 Source #
type (:<) Nat arg1 arg2
type (:<=) Nat arg1 arg2 Source #
type (:<=) Nat arg1 arg2
type (:>) Nat arg1 arg2 Source #
type (:>) Nat arg1 arg2
type (:>=) Nat arg1 arg2 Source #
type (:>=) Nat arg1 arg2
type Max Nat arg1 arg2 Source #
type Max Nat arg1 arg2
type Min Nat arg1 arg2 Source #
type Min Nat arg1 arg2
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 a1 a2 Source #
type EnumFromTo Nat a1 a2
type Apply Nat Constraint KnownNatSym0 l Source #
type Apply Nat Constraint KnownNatSym0 l = KnownNat l
type EnumFromThenTo Nat a1 a2 a3 Source #
type EnumFromThenTo Nat a1 a2 a3
type Apply Nat Nat ((:^$$) l1) l2 Source #
type Apply Nat Nat ((:^$$) l1) l2 = (:^) l1 l2
type Apply Nat k2 (FromIntegerSym0 k2) l Source #
type Apply Nat k2 (FromIntegerSym0 k2) l = FromInteger k2 l
type Apply Nat k2 (ToEnumSym0 k2) l Source #
type Apply Nat k2 (ToEnumSym0 k2) l = ToEnum k2 l
type Apply a Nat (FromEnumSym0 a) l Source #
type Apply a Nat (FromEnumSym0 a) l = FromEnum a l
type Apply Nat a ((:!!$$) a l1) l2 Source #
type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2
type Apply Nat a ((:!!$$) a l1) l2 Source #
type Apply Nat a ((:!!$$) a l1) l2 = (:!!) a l1 l2
type Apply Nat (TyFun Nat Nat -> *) (:^$) l Source #
type Apply Nat (TyFun Nat Nat -> *) (:^$) l = (:^$$) l
type Apply Nat (TyFun [a6989586621679458093] [a6989586621679458093] -> Type) (DropSym0 a6989586621679458093) l Source #
type Apply Nat (TyFun [a6989586621679458093] [a6989586621679458093] -> Type) (DropSym0 a6989586621679458093) l = DropSym1 a6989586621679458093 l
type Apply Nat (TyFun [a6989586621679458094] [a6989586621679458094] -> Type) (TakeSym0 a6989586621679458094) l Source #
type Apply Nat (TyFun [a6989586621679458094] [a6989586621679458094] -> Type) (TakeSym0 a6989586621679458094) l = TakeSym1 a6989586621679458094 l
type Apply Nat (TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]) -> Type) (SplitAtSym0 a6989586621679458092) l Source #
type Apply Nat (TyFun [a6989586621679458092] ([a6989586621679458092], [a6989586621679458092]) -> Type) (SplitAtSym0 a6989586621679458092) l = SplitAtSym1 a6989586621679458092 l
type Apply Nat (TyFun a6989586621679458078 [a6989586621679458078] -> Type) (ReplicateSym0 a6989586621679458078) l Source #
type Apply Nat (TyFun a6989586621679458078 [a6989586621679458078] -> Type) (ReplicateSym0 a6989586621679458078) l = ReplicateSym1 a6989586621679458078 l
type Apply Nat (TyFun (NonEmpty a6989586621679729633) [a6989586621679729633] -> Type) (TakeSym0 a6989586621679729633) l Source #
type Apply Nat (TyFun (NonEmpty a6989586621679729633) [a6989586621679729633] -> Type) (TakeSym0 a6989586621679729633) l = TakeSym1 a6989586621679729633 l
type Apply Nat (TyFun (NonEmpty a6989586621679729632) [a6989586621679729632] -> Type) (DropSym0 a6989586621679729632) l Source #
type Apply Nat (TyFun (NonEmpty a6989586621679729632) [a6989586621679729632] -> Type) (DropSym0 a6989586621679729632) l = DropSym1 a6989586621679729632 l
type Apply Nat (TyFun (NonEmpty a6989586621679729631) ([a6989586621679729631], [a6989586621679729631]) -> Type) (SplitAtSym0 a6989586621679729631) l Source #
type Apply Nat (TyFun (NonEmpty a6989586621679729631) ([a6989586621679729631], [a6989586621679729631]) -> Type) (SplitAtSym0 a6989586621679729631) l = SplitAtSym1 a6989586621679729631 l
type Apply a6989586621679458104 (TyFun [a6989586621679458104] [Nat] -> Type) (ElemIndicesSym0 a6989586621679458104) l Source #
type Apply a6989586621679458104 (TyFun [a6989586621679458104] [Nat] -> Type) (ElemIndicesSym0 a6989586621679458104) l = ElemIndicesSym1 a6989586621679458104 l
type Apply a6989586621679458105 (TyFun [a6989586621679458105] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679458105) l Source #
type Apply a6989586621679458105 (TyFun [a6989586621679458105] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679458105) l = ElemIndexSym1 a6989586621679458105 l
type Apply [a] Nat (LengthSym0 a) l Source #
type Apply [a] Nat (LengthSym0 a) l = Length a l
type Apply (NonEmpty a) Nat (LengthSym0 a) l Source #
type Apply (NonEmpty a) Nat (LengthSym0 a) l = Length a l
type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 Source #
type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 = FindIndices a l1 l2
type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 Source #
type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 = ElemIndices a l1 l2
type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 Source #
type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 = FindIndex a l1 l2
type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 Source #
type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 = ElemIndex a l1 l2
type Apply [a6989586621679458076] (TyFun Nat a6989586621679458076 -> Type) ((:!!$) a6989586621679458076) l Source #
type Apply [a6989586621679458076] (TyFun Nat a6989586621679458076 -> Type) ((:!!$) a6989586621679458076) l = (:!!$$) a6989586621679458076 l
type Apply (NonEmpty a6989586621679729611) (TyFun Nat a6989586621679729611 -> Type) ((:!!$) a6989586621679729611) l Source #
type Apply (NonEmpty a6989586621679729611) (TyFun Nat a6989586621679729611 -> Type) ((:!!$) a6989586621679729611) l = (:!!$$) a6989586621679729611 l
type Apply (TyFun a6989586621679458102 Bool -> Type) (TyFun [a6989586621679458102] [Nat] -> Type) (FindIndicesSym0 a6989586621679458102) l Source #
type Apply (TyFun a6989586621679458102 Bool -> Type) (TyFun [a6989586621679458102] [Nat] -> Type) (FindIndicesSym0 a6989586621679458102) l = FindIndicesSym1 a6989586621679458102 l
type Apply (TyFun a6989586621679458103 Bool -> Type) (TyFun [a6989586621679458103] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679458103) l Source #
type Apply (TyFun a6989586621679458103 Bool -> Type) (TyFun [a6989586621679458103] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679458103) l = FindIndexSym1 a6989586621679458103 l

data Symbol :: * #

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

Instances

SingKind Symbol	Since: 4.9.0.0
Associated Types type DemoteRep Symbol :: * Methods fromSing :: Sing Symbol a -> DemoteRep Symbol
KnownSymbol a => SingI Symbol a	Since: 4.9.0.0
Methods sing :: Sing a a
SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0 Source #
Methods suppressUnusedWarnings :: Proxy KnownSymbolSym0 t -> () Source #
data Sing Symbol
data Sing Symbol where SSym :: Sing Symbol s
type DemoteRep Symbol
type DemoteRep Symbol = String
type Demote Symbol Source #
type Demote Symbol = Text
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 arg1 arg2 Source #
type (:<) Symbol arg1 arg2
type (:<=) Symbol arg1 arg2 Source #
type (:<=) Symbol arg1 arg2
type (:>) Symbol arg1 arg2 Source #
type (:>) Symbol arg1 arg2
type (:>=) Symbol arg1 arg2 Source #
type (:>=) Symbol arg1 arg2
type Max Symbol arg1 arg2 Source #
type Max Symbol arg1 arg2
type Min Symbol arg1 arg2 Source #
type Min Symbol arg1 arg2
type Apply Symbol Constraint KnownSymbolSym0 l Source #
type Apply Symbol Constraint KnownSymbolSym0 l = KnownSymbol l

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 [a] Source #
data Sing [a] where SNil :: Sing [a] z SCons :: Sing [a] z
data Sing (Maybe a) Source #
data Sing (Maybe a) where SNothing :: Sing (Maybe a) z SJust :: Sing (Maybe a) z
data Sing (NonEmpty a) Source #
data Sing (NonEmpty a) where (:%\|) :: Sing (NonEmpty a) z
data Sing (Either a b) Source #
data Sing (Either a b) where SLeft :: Sing (Either a b) z SRight :: Sing (Either a b) z
data Sing (a, b) Source #
data Sing (a, b) where STuple2 :: Sing (a, b) z
data Sing ((~>) k1 k2) Source #
data Sing ((~>) k1 k2) = SLambda { applySing :: forall (t :: k1). Sing k1 t -> Sing k2 ((@@) k1 k2 f t) }
data Sing (a, b, c) Source #
data Sing (a, b, c) where STuple3 :: Sing (a, b, c) z
data Sing (a, b, c, d) Source #
data Sing (a, b, c, d) where STuple4 :: Sing (a, b, c, d) z
data Sing (a, b, c, d, e) Source #
data Sing (a, b, c, d, e) where STuple5 :: Sing (a, b, c, d, e) z
data Sing (a, b, c, d, e, f) Source #
data Sing (a, b, c, d, e, f) where STuple6 :: Sing (a, b, c, d, e, f) z
data Sing (a, b, c, d, e, f, g) Source #
data Sing (a, b, c, d, e, f, g) where STuple7 :: Sing (a, b, c, d, e, f, g) z

type SNat (x :: Nat) = Sing x Source #

Kind-restricted synonym for Sing for Nats

type SSymbol (x :: Symbol) = 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 :: TyFun k06989586621679402464 k6989586621679402466) Source #

Instances

SuppressUnusedWarnings (TyFun k06989586621679402464 k6989586621679402466 -> *) (ErrorSym0 k06989586621679402464 k6989586621679402466) Source #
Methods suppressUnusedWarnings :: Proxy (ErrorSym0 k06989586621679402464 k6989586621679402466) t -> () Source #
type Apply k0 k2 (ErrorSym0 k0 k2) l Source #
type Apply k0 k2 (ErrorSym0 k0 k2) l = Error k0 k2 l

type ErrorSym1 (t :: k06989586621679402464) = Error t Source #

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

The singleton for error

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

Minimal complete definition

natSing

data KnownNatSym0 (l :: TyFun Nat Constraint) Source #

Instances

SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0 Source #
Methods suppressUnusedWarnings :: Proxy KnownNatSym0 t -> () Source #
type Apply Nat Constraint KnownNatSym0 l Source #
type Apply Nat Constraint KnownNatSym0 l = KnownNat l

type KnownNatSym1 (t :: Nat) = KnownNat t Source #

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

Since: 4.7.0.0

class KnownSymbol (n :: Symbol) #

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

data KnownSymbolSym0 (l :: TyFun Symbol Constraint) Source #

Instances

SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0 Source #
Methods suppressUnusedWarnings :: Proxy KnownSymbolSym0 t -> () Source #
type Apply Symbol Constraint KnownSymbolSym0 l Source #
type Apply Symbol Constraint KnownSymbolSym0 l = KnownSymbol l

type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t Source #

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 -> *) (:^$) l Source #
type Apply Nat (TyFun Nat Nat -> *) (:^$) l = (:^$$) l

data (l :: Nat) :^$$ l Source #

Instances

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

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

Orphan instances

Eq Nat Source #
Methods (==) :: Nat -> Nat -> Bool # (/=) :: Nat -> Nat -> Bool #
Eq Symbol Source #	This bogus instance is helpful for people who want to define functions over Symbols that will only be used at the type level or as singletons.
Methods (==) :: Symbol -> Symbol -> Bool # (/=) :: Symbol -> Symbol -> Bool #
Num Nat Source #	This bogus `Num` instance is helpful for people who want to define functions over Nats that will only be used at the type level or as singletons. A correct SNum instance for Nat singletons exists.
Methods (+) :: Nat -> Nat -> Nat # (-) :: Nat -> Nat -> Nat # (*) :: Nat -> Nat -> Nat # negate :: Nat -> Nat # abs :: Nat -> Nat # signum :: Nat -> Nat # fromInteger :: Integer -> Nat #
Ord Nat Source #
Methods compare :: Nat -> Nat -> Ordering # (<) :: Nat -> Nat -> Bool # (<=) :: Nat -> Nat -> Bool # (>) :: Nat -> Nat -> Bool # (>=) :: Nat -> Nat -> Bool # max :: Nat -> Nat -> Nat # min :: Nat -> Nat -> Nat #
Ord Symbol Source #
Methods compare :: Symbol -> Symbol -> Ordering # (<) :: Symbol -> Symbol -> Bool # (<=) :: Symbol -> Symbol -> Bool # (>) :: Symbol -> Symbol -> Bool # (>=) :: Symbol -> Symbol -> Bool # max :: Symbol -> Symbol -> Symbol # min :: Symbol -> Symbol -> Symbol #