| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
GHC.TypeLits
Description
This module is an internal GHC module. It declares the constants used in the implementation of type-level natural numbers. The programmer interface for working with type-level naturals should be defined in a separate library.
Since: 4.6.0.0
- data Nat
- data Symbol
- class KnownNat n
- natVal :: forall n proxy. KnownNat n => proxy n -> Integer
- natVal' :: forall n. KnownNat n => Proxy# n -> Integer
- class KnownSymbol n
- symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
- symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
- data SomeNat = forall n . KnownNat n => SomeNat (Proxy n)
- data SomeSymbol = forall n . KnownSymbol n => SomeSymbol (Proxy n)
- someNatVal :: Integer -> Maybe 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 (<=) x y = (x <=? y) ~ True
- type family m <=? n :: Bool
- type family m + n :: Nat
- type family m * n :: Nat
- type family m ^ n :: Nat
- type family m - n :: Nat
- type family CmpNat m n :: Ordering
- type family CmpSymbol m n :: Ordering
Kinds
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: 4.7.0.0
Minimal complete definition
natSing
class KnownSymbol n Source
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 :: forall n proxy. KnownSymbol n => proxy n -> String Source
Since: 4.7.0.0
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String Source
Since: 4.8.0.0
This type represents unknown type-level natural numbers.
data SomeSymbol Source
This type represents unknown type-level symbols.
Constructors
| forall n . KnownSymbol n => SomeSymbol (Proxy n) | Since: 4.7.0.0 |
Instances
someNatVal :: Integer -> Maybe SomeNat Source
Convert an integer into an unknown type-level natural.
Since: 4.7.0.0
someSymbolVal :: String -> SomeSymbol Source
Convert a string into an unknown type-level symbol.
Since: 4.7.0.0
sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source
We either get evidence that this function was instantiated with the
same type-level numbers, or Nothing.
Since: 4.7.0.0
sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) Source
We either get evidence that this function was instantiated with the
same type-level symbols, or Nothing.
Since: 4.7.0.0
Functions on type literals
type family m <=? n :: Bool infix 4 Source
Comparison of type-level naturals, as a function.
NOTE: The functionality for this function should be subsumed
by CmpNat, so this might go away in the future.
Please let us know, if you encounter discrepancies between the two.