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
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.
- data Nat :: *
- data Symbol :: *
- data family Sing (a :: k)
- type SNat x = Sing x
- type SSymbol x = Sing x
- withKnownNat :: Sing n -> (KnownNat n => r) -> r
- withKnownSymbol :: Sing n -> (KnownSymbol n => r) -> r
- type family Error (str :: k0) :: k
- data ErrorSym0 l
- type ErrorSym1 t = Error t
- sError :: Sing (str :: Symbol) -> a
- class KnownNat n
- natVal :: KnownNat n => proxy n -> Integer
- class KnownSymbol n
- symbolVal :: KnownSymbol n => proxy n -> String
- type (:^) a b = a ^ b
- data (:^$) l
- data l :^$$ l
- type (:^$$$) t t = (:^) t t
Documentation
(Kind) This is the kind of type-level natural numbers.
Instances
SNum Nat # | |
SEnum Nat # | |
PNum Nat (Proxy * Nat) # | |
PEnum Nat (Proxy * Nat) # | |
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$) # | |
SuppressUnusedWarnings ((TyFun a6989586621679796322 Bool -> Type) -> TyFun [a6989586621679796322] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679796322) # | |
SuppressUnusedWarnings ((TyFun a6989586621679796321 Bool -> Type) -> TyFun [a6989586621679796321] [Nat] -> *) (FindIndicesSym1 a6989586621679796321) # | |
SuppressUnusedWarnings ([a6989586621679796295] -> TyFun Nat a6989586621679796295 -> *) ((:!!$$) a6989586621679796295) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> *) (SplitAtSym1 a6989586621679796311) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796313] [a6989586621679796313] -> *) (TakeSym1 a6989586621679796313) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679796312] [a6989586621679796312] -> *) (DropSym1 a6989586621679796312) # | |
SuppressUnusedWarnings (Nat -> TyFun a6989586621679796297 [a6989586621679796297] -> *) (ReplicateSym1 a6989586621679796297) # | |
SuppressUnusedWarnings (a6989586621679796324 -> TyFun [a6989586621679796324] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679796324) # | |
SuppressUnusedWarnings (a6989586621679796323 -> TyFun [a6989586621679796323] [Nat] -> *) (ElemIndicesSym1 a6989586621679796323) # | |
SuppressUnusedWarnings (TyFun (TyFun a6989586621679796322 Bool -> Type) (TyFun [a6989586621679796322] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679796322) # | |
SuppressUnusedWarnings (TyFun (TyFun a6989586621679796321 Bool -> Type) (TyFun [a6989586621679796321] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679796321) # | |
SuppressUnusedWarnings (TyFun [a6989586621679796298] Nat -> *) (LengthSym0 a6989586621679796298) # | |
SuppressUnusedWarnings (TyFun [a6989586621679796295] (TyFun Nat a6989586621679796295 -> Type) -> *) ((:!!$) a6989586621679796295) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> Type) -> *) (SplitAtSym0 a6989586621679796311) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796313] [a6989586621679796313] -> Type) -> *) (TakeSym0 a6989586621679796313) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679796312] [a6989586621679796312] -> Type) -> *) (DropSym0 a6989586621679796312) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679796297 [a6989586621679796297] -> Type) -> *) (ReplicateSym0 a6989586621679796297) # | |
SuppressUnusedWarnings (TyFun Nat a6989586621679685236 -> *) (FromIntegerSym0 a6989586621679685236) # | |
SuppressUnusedWarnings (TyFun Nat a6989586621679697496 -> *) (ToEnumSym0 a6989586621679697496) # | |
SuppressUnusedWarnings (TyFun a6989586621679697496 Nat -> *) (FromEnumSym0 a6989586621679697496) # | |
SuppressUnusedWarnings (TyFun a6989586621679796324 (TyFun [a6989586621679796324] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679796324) # | |
SuppressUnusedWarnings (TyFun a6989586621679796323 (TyFun [a6989586621679796323] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679796323) # | |
type DemoteRep Nat # | |
data Sing Nat # | |
type Negate Nat a # | |
type Abs Nat a # | |
type Signum Nat a # | |
type FromInteger Nat a # | |
type Succ Nat a0 # | |
type Pred Nat a0 # | |
type ToEnum Nat a0 # | |
type FromEnum Nat a0 # | |
type (==) Nat a b | |
type (:==) Nat a b # | |
type (:/=) Nat x y # | |
type Compare Nat 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 # | |
type (:-) Nat a b # | |
type (:*) Nat a b # | |
type EnumFromTo Nat a1 a0 # | |
type EnumFromThenTo Nat a2 a1 a0 # | |
type Apply Nat Nat ((:^$$) l1) l0 # | |
type Apply Nat k2 (FromIntegerSym0 k2) l0 # | |
type Apply Nat k2 (ToEnumSym0 k2) l0 # | |
type Apply a6989586621679697496 Nat (FromEnumSym0 a6989586621679697496) l0 # | |
type Apply Nat a6989586621679796295 ((:!!$$) a6989586621679796295 l0) l1 # | |
type Apply Nat (TyFun Nat Nat -> *) (:^$) l0 # | |
type Apply Nat (TyFun [a6989586621679796311] ([a6989586621679796311], [a6989586621679796311]) -> Type) (SplitAtSym0 a6989586621679796311) l0 # | |
type Apply Nat (TyFun [a6989586621679796313] [a6989586621679796313] -> Type) (TakeSym0 a6989586621679796313) l0 # | |
type Apply Nat (TyFun [a6989586621679796312] [a6989586621679796312] -> Type) (DropSym0 a6989586621679796312) l0 # | |
type Apply Nat (TyFun a6989586621679796297 [a6989586621679796297] -> Type) (ReplicateSym0 a6989586621679796297) l0 # | |
type Apply a6989586621679796324 (TyFun [a6989586621679796324] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679796324) l0 # | |
type Apply a6989586621679796323 (TyFun [a6989586621679796323] [Nat] -> Type) (ElemIndicesSym0 a6989586621679796323) l0 # | |
type Apply [a6989586621679796298] Nat (LengthSym0 a6989586621679796298) l0 # | |
type Apply [a6989586621679796324] (Maybe Nat) (ElemIndexSym1 a6989586621679796324 l0) l1 # | |
type Apply [a6989586621679796322] (Maybe Nat) (FindIndexSym1 a6989586621679796322 l0) l1 # | |
type Apply [a6989586621679796323] [Nat] (ElemIndicesSym1 a6989586621679796323 l0) l1 # | |
type Apply [a6989586621679796321] [Nat] (FindIndicesSym1 a6989586621679796321 l0) l1 # | |
type Apply [a6989586621679796295] (TyFun Nat a6989586621679796295 -> Type) ((:!!$) a6989586621679796295) l0 # | |
type Apply (TyFun a6989586621679796322 Bool -> Type) (TyFun [a6989586621679796322] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679796322) l0 # | |
type Apply (TyFun a6989586621679796321 Bool -> Type) (TyFun [a6989586621679796321] [Nat] -> Type) (FindIndicesSym0 a6989586621679796321) l0 # | |
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
KnownSymbol a => SingI Symbol a | |
SingKind Symbol (KProxy Symbol) | |
data Sing Symbol | |
type DemoteRep Symbol # | |
data Sing Symbol # | |
type (==) Symbol a b | |
type (:==) Symbol a b # | |
type (:/=) Symbol x y # | |
type Compare Symbol 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) | |
The singleton kind-indexed data family.
Instances
data Sing Bool # | |
data Sing Ordering # | |
data Sing * # | |
data Sing Nat # | |
data Sing Symbol # | |
data Sing () # | |
data Sing [a0] # | |
data Sing (Maybe a0) # | |
data Sing (NonEmpty a0) # | |
data Sing (Either a0 b0) # | |
data Sing (a0, b0) # | |
data Sing ((~>) k1 k2) # | |
data Sing (a0, b0, c0) # | |
data Sing (a0, b0, c0, d0) # | |
data Sing (a0, b0, c0, d0, e0) # | |
data Sing (a0, b0, c0, d0, e0, f0) # | |
data Sing (a0, b0, c0, d0, e0, f0, g0) # | |
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.
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
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