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
Description
Defines and exports singletons useful for the Nat and Symbol kinds.
- data Nat :: *
- data Symbol :: *
- data family Sing (a :: k)
- type SNat (x :: Nat) = Sing x
- type SSymbol (x :: Symbol) = 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 :: TyFun k06989586621679342626 k6989586621679342628)
- type ErrorSym1 (t :: k06989586621679342626) = Error t
- sError :: Sing (str :: Symbol) -> a
- class KnownNat (n :: Nat)
- data KnownNatSym0 (l :: TyFun Nat Constraint)
- type KnownNatSym1 (t :: Nat) = KnownNat t
- natVal :: KnownNat n => proxy n -> Integer
- class KnownSymbol (n :: Symbol)
- data KnownSymbolSym0 (l :: TyFun Symbol Constraint)
- type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t
- symbolVal :: KnownSymbol n => proxy n -> String
- type (:^) a b = a ^ b
- data (:^$) l
- data (l :: Nat) :^$$ l
- type (:^$$$) (t :: Nat) (t :: Nat) = (:^) t t
Documentation
(Kind) This is the kind of type-level natural numbers.
Instances
SNum Nat # | |
PNum Nat # | |
SEnum Nat # | |
PEnum Nat # | |
SuppressUnusedWarnings (Nat -> TyFun Nat Nat -> *) (:^$$) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun Nat Nat -> *) -> *) (:^$) # | |
SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0 # | |
SuppressUnusedWarnings ((TyFun a6989586621679389254 Bool -> Type) -> TyFun [a6989586621679389254] [Nat] -> *) (FindIndicesSym1 a6989586621679389254) # | |
SuppressUnusedWarnings ((TyFun a6989586621679389255 Bool -> Type) -> TyFun [a6989586621679389255] (Maybe Nat) -> *) (FindIndexSym1 a6989586621679389255) # | |
SuppressUnusedWarnings ([a6989586621679389228] -> TyFun Nat a6989586621679389228 -> *) ((:!!$$) a6989586621679389228) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679389245] [a6989586621679389245] -> *) (DropSym1 a6989586621679389245) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679389246] [a6989586621679389246] -> *) (TakeSym1 a6989586621679389246) # | |
SuppressUnusedWarnings (Nat -> TyFun [a6989586621679389244] ([a6989586621679389244], [a6989586621679389244]) -> *) (SplitAtSym1 a6989586621679389244) # | |
SuppressUnusedWarnings (Nat -> TyFun a6989586621679389230 [a6989586621679389230] -> *) (ReplicateSym1 a6989586621679389230) # | |
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679609015) [a6989586621679609015] -> *) (TakeSym1 a6989586621679609015) # | |
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679609014) [a6989586621679609014] -> *) (DropSym1 a6989586621679609014) # | |
SuppressUnusedWarnings (Nat -> TyFun (NonEmpty a6989586621679609013) ([a6989586621679609013], [a6989586621679609013]) -> *) (SplitAtSym1 a6989586621679609013) # | |
SuppressUnusedWarnings (a6989586621679389256 -> TyFun [a6989586621679389256] [Nat] -> *) (ElemIndicesSym1 a6989586621679389256) # | |
SuppressUnusedWarnings (a6989586621679389257 -> TyFun [a6989586621679389257] (Maybe Nat) -> *) (ElemIndexSym1 a6989586621679389257) # | |
SuppressUnusedWarnings (NonEmpty a6989586621679608993 -> TyFun Nat a6989586621679608993 -> *) ((:!!$$) a6989586621679608993) # | |
SuppressUnusedWarnings (TyFun (TyFun a6989586621679389254 Bool -> Type) (TyFun [a6989586621679389254] [Nat] -> Type) -> *) (FindIndicesSym0 a6989586621679389254) # | |
SuppressUnusedWarnings (TyFun (TyFun a6989586621679389255 Bool -> Type) (TyFun [a6989586621679389255] (Maybe Nat) -> Type) -> *) (FindIndexSym0 a6989586621679389255) # | |
SuppressUnusedWarnings (TyFun [a6989586621679389228] (TyFun Nat a6989586621679389228 -> Type) -> *) ((:!!$) a6989586621679389228) # | |
SuppressUnusedWarnings (TyFun [a6989586621679389231] Nat -> *) (LengthSym0 a6989586621679389231) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679389245] [a6989586621679389245] -> Type) -> *) (DropSym0 a6989586621679389245) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679389246] [a6989586621679389246] -> Type) -> *) (TakeSym0 a6989586621679389246) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun [a6989586621679389244] ([a6989586621679389244], [a6989586621679389244]) -> Type) -> *) (SplitAtSym0 a6989586621679389244) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun a6989586621679389230 [a6989586621679389230] -> Type) -> *) (ReplicateSym0 a6989586621679389230) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679609015) [a6989586621679609015] -> Type) -> *) (TakeSym0 a6989586621679609015) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679609014) [a6989586621679609014] -> Type) -> *) (DropSym0 a6989586621679609014) # | |
SuppressUnusedWarnings (TyFun Nat (TyFun (NonEmpty a6989586621679609013) ([a6989586621679609013], [a6989586621679609013]) -> Type) -> *) (SplitAtSym0 a6989586621679609013) # | |
SuppressUnusedWarnings (TyFun Nat a6989586621679348813 -> *) (FromIntegerSym0 a6989586621679348813) # | |
SuppressUnusedWarnings (TyFun Nat a6989586621679673920 -> *) (ToEnumSym0 a6989586621679673920) # | |
SuppressUnusedWarnings (TyFun a6989586621679389256 (TyFun [a6989586621679389256] [Nat] -> Type) -> *) (ElemIndicesSym0 a6989586621679389256) # | |
SuppressUnusedWarnings (TyFun a6989586621679389257 (TyFun [a6989586621679389257] (Maybe Nat) -> Type) -> *) (ElemIndexSym0 a6989586621679389257) # | |
SuppressUnusedWarnings (TyFun a6989586621679673920 Nat -> *) (FromEnumSym0 a6989586621679673920) # | |
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679608993) (TyFun Nat a6989586621679608993 -> Type) -> *) ((:!!$) a6989586621679608993) # | |
SuppressUnusedWarnings (TyFun (NonEmpty a6989586621679609046) Nat -> *) (LengthSym0 a6989586621679609046) # | |
type Demote Nat # | |
data Sing Nat # | |
type Negate Nat a # | |
type Abs Nat a # | |
type Signum Nat a # | |
type FromInteger Nat a # | |
type Succ Nat a # | |
type Pred Nat a # | |
type ToEnum Nat a # | |
type FromEnum Nat a # | |
type (==) Nat a b | |
type (:==) Nat a b # | |
type (:/=) Nat x y # | |
type Compare Nat a b # | |
type (:<) Nat arg1 arg2 # | |
type (:<=) Nat arg1 arg2 # | |
type (:>) Nat arg1 arg2 # | |
type (:>=) Nat arg1 arg2 # | |
type Max Nat arg1 arg2 # | |
type Min Nat arg1 arg2 # | |
type (:+) Nat a b # | |
type (:-) Nat a b # | |
type (:*) Nat a b # | |
type EnumFromTo Nat a1 a2 # | |
type Apply Nat Constraint KnownNatSym0 l # | |
type EnumFromThenTo Nat a1 a2 a3 # | |
type Apply Nat Nat ((:^$$) l1) l2 # | |
type Apply Nat k2 (FromIntegerSym0 k2) l # | |
type Apply Nat k2 (ToEnumSym0 k2) l # | |
type Apply a Nat (FromEnumSym0 a) l # | |
type Apply Nat a ((:!!$$) a l1) l2 # | |
type Apply Nat a ((:!!$$) a l1) l2 # | |
type Apply Nat (TyFun Nat Nat -> *) (:^$) l # | |
type Apply Nat (TyFun [a6989586621679389245] [a6989586621679389245] -> Type) (DropSym0 a6989586621679389245) l # | |
type Apply Nat (TyFun [a6989586621679389246] [a6989586621679389246] -> Type) (TakeSym0 a6989586621679389246) l # | |
type Apply Nat (TyFun [a6989586621679389244] ([a6989586621679389244], [a6989586621679389244]) -> Type) (SplitAtSym0 a6989586621679389244) l # | |
type Apply Nat (TyFun a6989586621679389230 [a6989586621679389230] -> Type) (ReplicateSym0 a6989586621679389230) l # | |
type Apply Nat (TyFun (NonEmpty a6989586621679609015) [a6989586621679609015] -> Type) (TakeSym0 a6989586621679609015) l # | |
type Apply Nat (TyFun (NonEmpty a6989586621679609014) [a6989586621679609014] -> Type) (DropSym0 a6989586621679609014) l # | |
type Apply Nat (TyFun (NonEmpty a6989586621679609013) ([a6989586621679609013], [a6989586621679609013]) -> Type) (SplitAtSym0 a6989586621679609013) l # | |
type Apply a6989586621679389256 (TyFun [a6989586621679389256] [Nat] -> Type) (ElemIndicesSym0 a6989586621679389256) l # | |
type Apply a6989586621679389257 (TyFun [a6989586621679389257] (Maybe Nat) -> Type) (ElemIndexSym0 a6989586621679389257) l # | |
type Apply [a] Nat (LengthSym0 a) l # | |
type Apply (NonEmpty a) Nat (LengthSym0 a) l # | |
type Apply [a] [Nat] (FindIndicesSym1 a l1) l2 # | |
type Apply [a] [Nat] (ElemIndicesSym1 a l1) l2 # | |
type Apply [a] (Maybe Nat) (FindIndexSym1 a l1) l2 # | |
type Apply [a] (Maybe Nat) (ElemIndexSym1 a l1) l2 # | |
type Apply [a6989586621679389228] (TyFun Nat a6989586621679389228 -> Type) ((:!!$) a6989586621679389228) l # | |
type Apply (NonEmpty a6989586621679608993) (TyFun Nat a6989586621679608993 -> Type) ((:!!$) a6989586621679608993) l # | |
type Apply (TyFun a6989586621679389254 Bool -> Type) (TyFun [a6989586621679389254] [Nat] -> Type) (FindIndicesSym0 a6989586621679389254) l # | |
type Apply (TyFun a6989586621679389255 Bool -> Type) (TyFun [a6989586621679389255] (Maybe Nat) -> Type) (FindIndexSym0 a6989586621679389255) l # | |
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
SingKind Symbol | Since: 4.9.0.0 |
KnownSymbol a => SingI Symbol a | Since: 4.9.0.0 |
SuppressUnusedWarnings (TyFun Symbol Constraint -> *) KnownSymbolSym0 # | |
data Sing Symbol | |
type DemoteRep Symbol | |
type Demote Symbol # | |
data Sing Symbol # | |
type (==) Symbol a b | |
type (:==) Symbol a b # | |
type (:/=) Symbol x y # | |
type Compare Symbol a b # | |
type (:<) Symbol arg1 arg2 # | |
type (:<=) Symbol arg1 arg2 # | |
type (:>) Symbol arg1 arg2 # | |
type (:>=) Symbol arg1 arg2 # | |
type Max Symbol arg1 arg2 # | |
type Min Symbol arg1 arg2 # | |
type Apply Symbol Constraint KnownSymbolSym0 l # | |
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 [a] # | |
data Sing (Maybe a) # | |
data Sing (NonEmpty a) # | |
data Sing (Either a b) # | |
data Sing (a, b) # | |
data Sing ((~>) k1 k2) # | |
data Sing (a, b, c) # | |
data Sing (a, b, c, d) # | |
data Sing (a, b, c, d, e) # | |
data Sing (a, b, c, d, e, f) # | |
data Sing (a, b, c, d, e, f, g) # | |
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
data KnownNatSym0 (l :: TyFun Nat Constraint) #
Instances
SuppressUnusedWarnings (TyFun Nat Constraint -> *) KnownNatSym0 # | |
type Apply Nat Constraint KnownNatSym0 l # | |
type KnownNatSym1 (t :: Nat) = KnownNat t #
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) #
Instances
type KnownSymbolSym1 (t :: Symbol) = KnownSymbol t #
symbolVal :: KnownSymbol n => proxy n -> String #
Since: 4.7.0.0
Orphan instances
Eq Nat # | |
Eq Symbol # | 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. |
Num Nat # | This bogus |
Ord Nat # | |
Ord Symbol # | |