| Safe Haskell | Trustworthy |
|---|---|
| Language | Haskell2010 |
GHC.TypeLits
Description
This module is an internal GHC module. It declares the constants usedin the implementation of type-level natural numbers. The programmer interfacefor working with type-level naturals should be defined in a separate library.
Since: 4.6.0.0
classKnownNat (n ::Nat)Source#
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
classKnownSymbol (n ::Symbol)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 ->StringSource#
Since: 4.7.0.0
symbolVal' ::forall n.KnownSymbol n =>Proxy# n ->StringSource#
Since: 4.8.0.0
This type represents unknown type-level natural numbers.
Since: 4.10.0.0
This type represents unknown type-level symbols.
Constructors
| KnownSymbol n =>SomeSymbol (Proxy n) | Since: 4.7.0.0 |
| EqSomeSymbolSource# | Since: 4.7.0.0 |
Instance detailsDefined inGHC.TypeLits | |
| OrdSomeSymbolSource# | Since: 4.7.0.0 |
Instance detailsDefined inGHC.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# | |
| ReadSomeSymbolSource# | Since: 4.7.0.0 |
Instance detailsDefined inGHC.TypeLits | |
| ShowSomeSymbolSource# | Since: 4.7.0.0 |
Instance detailsDefined inGHC.TypeLits | |
someNatVal ::Integer ->MaybeSomeNatSource#
Convert an integer into an unknown type-level natural.
Since: 4.7.0.0
someSymbolVal ::String ->SomeSymbolSource#
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, orNothing.
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, orNothing.
Since: 4.7.0.0
type(<=) x y = (x<=? y) ~Trueinfix 4Source#
Comparison of type-level naturals, as a constraint.
Since: 4.7.0.0
type family (m ::Nat)<=? (n ::Nat) ::Boolinfix 4Source#
Comparison of type-level naturals, as a function.NOTE: The functionality for this function should be subsumedbyCmpNat, so this might go away in the future.Please let us know, if you encounter discrepancies between the two.
type family (m ::Nat)* (n ::Nat) ::Natinfixl 7Source#
Multiplication of type-level naturals.
Since: 4.7.0.0
type family (m ::Nat)^ (n ::Nat) ::Natinfixr 8Source#
Exponentiation of type-level naturals.
Since: 4.7.0.0
type family (m ::Nat)- (n ::Nat) ::Natinfixl 6Source#
Subtraction of type-level naturals.
Since: 4.7.0.0
type familyDiv (m ::Nat) (n ::Nat) ::Natinfixl 7Source#
Division (round down) of natural numbers.Div x 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type familyMod (m ::Nat) (n ::Nat) ::Natinfixl 7Source#
Modulus of natural numbers.Mod x 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type familyLog2 (m ::Nat) ::NatSource#
Log base 2 (round down) of natural numbers.Log 0 is undefined (i.e., it cannot be reduced).
Since: 4.11.0.0
type familyAppendSymbol (m ::Symbol) (n ::Symbol) ::SymbolSource#
Concatenation of type-level symbols.
Since: 4.10.0.0
type familyCmpNat (m ::Nat) (n ::Nat) ::OrderingSource#
Comparison of type-level naturals, as a function.
Since: 4.7.0.0
type familyCmpSymbol (m ::Symbol) (n ::Symbol) ::OrderingSource#
Comparison of type-level symbols, as a function.
Since: 4.7.0.0
type familyTypeError (a ::ErrorMessage) :: bwhere ...Source#
The type-level equivalent oferror.
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 contextinstance TypeError (Text "CannotShow 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: 4.9.0.0
A description of a custom type error.
Constructors
| TextSymbol | Show the text as is. |
| ShowType t | Pretty print the type. |
| ErrorMessage:<>:ErrorMessageinfixl 6 | Put two pieces of error message next to each other. |
| ErrorMessage:$$:ErrorMessageinfixl 5 | Stack two pieces of error message on top of each other. |
Produced byHaddock version 2.20.0