| Copyright | (c) Artem Chirkin |
|---|---|
| License | BSD3 |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Type.Lits
Description
Synopsis
- data Nat
- data Symbol
- type KindOf (t :: k) = k
- type KindOfEl (ts :: [k]) = k
- class KnownNat (n :: Nat)
- natVal :: KnownNat n => proxy n -> Natural
- natVal' :: KnownNat n => Proxy# n -> Natural
- class KnownSymbol (n :: Symbol)
- symbolVal :: KnownSymbol n => proxy n -> String
- symbolVal' :: KnownSymbol n => Proxy# n -> String
- data SomeNat where
- data SomeSymbol where
- SomeSymbol :: forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol
- someNatVal :: Natural -> SomeNat
- someSymbolVal :: String -> SomeSymbol
- sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b)
- type family (a :: Nat) + (b :: Nat) :: Nat where ...
- type family (a :: Nat) * (b :: Nat) :: Nat where ...
- type family (a :: Nat) ^ (b :: Nat) :: Nat where ...
- type family (a :: Nat) - (b :: Nat) :: Nat where ...
- type family Div (a :: Nat) (b :: Nat) :: Nat where ...
- type family Mod (a :: Nat) (b :: Nat) :: Nat where ...
- type family Log2 (a :: Nat) :: Nat where ...
- type Min (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
- type Max (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b)
- type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ...
- type family ShowNat (n :: Nat) :: Symbol where ...
- type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ...
- type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ...
- type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b)
- data SOrdering :: Ordering -> Type where
- cmpNat :: forall (a :: Nat) (b :: Nat) (proxy :: Nat -> Type). (KnownNat a, KnownNat b) => proxy a -> proxy b -> SOrdering (CmpNat a b)
- cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy :: Symbol -> Type). (KnownSymbol a, KnownSymbol b) => proxy a -> proxy b -> SOrdering (CmpSymbol a b)
- type family TypeError (a :: ErrorMessage) :: b where ...
- data ErrorMessage where
- Text :: forall. Symbol -> ErrorMessage
- ShowType :: forall t. t -> ErrorMessage
- (:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage
- (:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage
Kinds
(Kind) This is the kind of type-level natural numbers.
Instances
(Kind) This is the kind of type-level symbols. Declared here because class IP needs it
Instances
| SingKind Symbol | Since: base-4.9.0.0 |
Defined in GHC.Generics | |
| KnownSymbol a => SingI (a :: Symbol) | Since: base-4.9.0.0 |
Defined in GHC.Generics Methods sing :: Sing a | |
| data Sing (s :: Symbol) | |
Defined in GHC.Generics | |
| type DemoteRep Symbol | |
Defined in GHC.Generics | |
type KindOf (t :: k) = k Source #
Get the kind of a given type. Useful when we don't want to introduce another type parameter into a type signature (because the kind is determined by the type), but need to have some constraints on the type's kind.
type KindOfEl (ts :: [k]) = k Source #
Get the kind of a given list type. Useful when we don't want to introduce another type parameter into a type signature (because the kind is determined by the type), but need to have some constraints on the type's kind.
Linking type and value level
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: base-4.7.0.0
Minimal complete definition
natSing
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: base-4.7.0.0
Minimal complete definition
symbolSing
symbolVal :: KnownSymbol n => proxy n -> String #
Since: base-4.7.0.0
symbolVal' :: KnownSymbol n => Proxy# n -> String #
Since: base-4.8.0.0
This type represents unknown type-level natural numbers.
Since: base-4.10.0.0
data SomeSymbol where #
This type represents unknown type-level symbols.
Constructors
| SomeSymbol :: forall (n :: Symbol). KnownSymbol n => Proxy n -> SomeSymbol | Since: base-4.7.0.0 |
Instances
| Eq SomeSymbol | Since: base-4.7.0.0 |
Defined in GHC.TypeLits | |
| Ord SomeSymbol | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods compare :: SomeSymbol -> SomeSymbol -> Ordering # (<) :: SomeSymbol -> SomeSymbol -> Bool # (<=) :: SomeSymbol -> SomeSymbol -> Bool # (>) :: SomeSymbol -> SomeSymbol -> Bool # (>=) :: SomeSymbol -> SomeSymbol -> Bool # max :: SomeSymbol -> SomeSymbol -> SomeSymbol # min :: SomeSymbol -> SomeSymbol -> SomeSymbol # | |
| Read SomeSymbol | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods readsPrec :: Int -> ReadS SomeSymbol # readList :: ReadS [SomeSymbol] # readPrec :: ReadPrec SomeSymbol # readListPrec :: ReadPrec [SomeSymbol] # | |
| Show SomeSymbol | Since: base-4.7.0.0 |
Defined in GHC.TypeLits Methods showsPrec :: Int -> SomeSymbol -> ShowS # show :: SomeSymbol -> String # showList :: [SomeSymbol] -> ShowS # | |
someNatVal :: Natural -> SomeNat #
Convert an integer into an unknown type-level natural.
Since: base-4.10.0.0
someSymbolVal :: String -> SomeSymbol #
Convert a string into an unknown type-level symbol.
Since: base-4.7.0.0
sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) #
We either get evidence that this function was instantiated with the
same type-level numbers, or Nothing.
Since: base-4.7.0.0
sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) #
We either get evidence that this function was instantiated with the
same type-level symbols, or Nothing.
Since: base-4.7.0.0
Functions on type literals
type family (a :: Nat) + (b :: Nat) :: Nat where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) * (b :: Nat) :: Nat where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Nat) - (b :: Nat) :: Nat where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family Div (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0 is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Mod (a :: Nat) (b :: Nat) :: Nat where ... infixl 7 #
Modulus of natural numbers.
Mod x 0 is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Log2 (a :: Nat) :: Nat where ... #
Log base 2 (round down) of natural numbers.
Log 0 is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type Min (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b) Source #
Miminum among two type-level naturals.
type Max (a :: Nat) (b :: Nat) = Min' a b (CmpNat a b) Source #
Maximum among two type-level naturals.
type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... #
Concatenation of type-level symbols.
Since: base-4.10.0.0
type family ShowNat (n :: Nat) :: Symbol where ... Source #
Convert a type-level Nat into a type-level Symbol.
type family CmpNat (a :: Nat) (b :: Nat) :: Ordering where ... #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... #
Comparison of type-level symbols, as a function.
Since: base-4.7.0.0
type (<=) (a :: Nat) (b :: Nat) = LE a b (CmpNat a b) Source #
Comparison of type-level naturals, as a constraint.
data SOrdering :: Ordering -> Type where Source #
Singleton-style version of Ordering.
Pattern-match againts its constructor to witness the result of
type-level comparison.
cmpNat :: forall (a :: Nat) (b :: Nat) (proxy :: Nat -> Type). (KnownNat a, KnownNat b) => proxy a -> proxy b -> SOrdering (CmpNat a b) Source #
Pattern-match against the result of this function to get the evidence of comparing type-level Nats.
cmpSymbol :: forall (a :: Symbol) (b :: Symbol) (proxy :: Symbol -> Type). (KnownSymbol a, KnownSymbol b) => proxy a -> proxy b -> SOrdering (CmpSymbol a b) Source #
Pattern-match against the result of this function to get the evidence of comparing type-level Symbols.
User-defined type errors
type family TypeError (a :: ErrorMessage) :: b where ... #
The type-level equivalent of error.
The polymorphic kind of this type allows it to be used in several settings. For instance, it can be used as a constraint, e.g. to provide a better error message for a non-existent instance,
-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
Text "Perhaps there is a missing argument?")
=> Show (a -> b) where
showsPrec = error "unreachable"
It can also be placed on the right-hand side of a type-level function to provide an error for an invalid case,
type family ByteSize x where
ByteSize Word16 = 2
ByteSize Word8 = 1
ByteSize a = TypeError (Text "The type " :<>: ShowType a :<>:
Text " is not exportable.")
Since: base-4.9.0.0
data ErrorMessage where #
A description of a custom type error.
Constructors
| Text :: forall. Symbol -> ErrorMessage | Show the text as is. |
| ShowType :: forall t. t -> ErrorMessage | Pretty print the type.
|
| (:<>:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 6 | Put two pieces of error message next to each other. |
| (:$$:) :: forall. ErrorMessage -> ErrorMessage -> ErrorMessage infixl 5 | Stack two pieces of error message on top of each other. |