Safe Haskell | Trustworthy |
---|---|

Language | Haskell2010 |

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: base-4.6.0.0

(Kind) This is the kind of type-level natural numbers.

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

class KnownNat (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: base-4.7.0.0

natSing

natVal :: forall n proxy. KnownNat n => proxy n -> Integer Source

Since: base-4.7.0.0

natVal' :: forall n. KnownNat n => Proxy# n -> Integer Source

Since: base-4.8.0.0

class KnownSymbol (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: base-4.7.0.0

symbolSing

symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String Source

Since: base-4.7.0.0

symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String Source

Since: base-4.8.0.0

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Eq SomeNat | Since: base-4.7.0.0 |

Ord SomeNat | Since: base-4.7.0.0 |

Read SomeNat | Since: base-4.7.0.0 |

Show SomeNat | Since: base-4.7.0.0 |

data SomeSymbol Source

This type represents unknown type-level symbols.

forall n.KnownSymbol n => SomeSymbol (Proxy n) | Since: base-4.7.0.0 |

Eq SomeSymbol | Since: base-4.7.0.0 |

Defined in GHC.TypeLits ## Methods(==) :: SomeSymbol -> SomeSymbol -> Bool Source (/=) :: SomeSymbol -> SomeSymbol -> Bool Source | |

Ord SomeSymbol | Since: base-4.7.0.0 |

Defined in GHC.TypeLits ## Methodscompare :: SomeSymbol -> SomeSymbol -> Ordering Source (<) :: SomeSymbol -> SomeSymbol -> Bool Source (<=) :: SomeSymbol -> SomeSymbol -> Bool Source (>) :: SomeSymbol -> SomeSymbol -> Bool Source (>=) :: SomeSymbol -> SomeSymbol -> Bool Source max :: SomeSymbol -> SomeSymbol -> SomeSymbol Source min :: SomeSymbol -> SomeSymbol -> SomeSymbol Source | |

Read SomeSymbol | Since: base-4.7.0.0 |

Defined in GHC.TypeLits ## MethodsreadsPrec :: Int -> ReadS SomeSymbol Source readList :: ReadS [SomeSymbol] Source | |

Show SomeSymbol | Since: base-4.7.0.0 |

Defined in GHC.TypeLits ## MethodsshowsPrec :: Int -> SomeSymbol -> ShowS Source show :: SomeSymbol -> String Source showList :: [SomeSymbol] -> ShowS Source |

someNatVal :: Integer -> Maybe SomeNat Source

Convert an integer into an unknown type-level natural.

Since: base-4.7.0.0

someSymbolVal :: String -> SomeSymbol Source

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) Source

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) Source

We either get evidence that this function was instantiated with the same type-level symbols, or `Nothing`

.

Since: base-4.7.0.0

type (<=) x y = (x <=? y) ~ 'True infix 4 Source

Comparison of type-level naturals, as a constraint.

Since: base-4.7.0.0

type family (m :: Nat) <=? (n :: Nat) :: 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.

type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source

Addition of type-level naturals.

Since: base-4.7.0.0

type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source

Multiplication of type-level naturals.

Since: base-4.7.0.0

type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source

Exponentiation of type-level naturals.

Since: base-4.7.0.0

type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 Source

Subtraction of type-level naturals.

Since: base-4.7.0.0

type family Div (m :: Nat) (n :: Nat) :: Nat infixl 7 Source

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 (m :: Nat) (n :: Nat) :: Nat infixl 7 Source

Modulus of natural numbers. `Mod x 0`

is undefined (i.e., it cannot be reduced).

Since: base-4.11.0.0

type family Log2 (m :: Nat) :: Nat Source

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 family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source

Concatenation of type-level symbols.

Since: base-4.10.0.0

type family CmpNat (m :: Nat) (n :: Nat) :: Ordering Source

Comparison of type-level naturals, as a function.

Since: base-4.7.0.0

type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering Source

Comparison of type-level symbols, as a function.

Since: base-4.7.0.0

type family TypeError (a :: ErrorMessage) :: b where ... Source

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 Source

A description of a custom type error.

Text Symbol | Show the text as is. |

forall t. ShowType t | Pretty print the type. |

ErrorMessage :<>: ErrorMessage infixl 6 | Put two pieces of error message next to each other. |

ErrorMessage :$$: ErrorMessage infixl 5 | Stack two pieces of error message on top of each other. |

© The University of Glasgow and others

Licensed under a BSD-style license (see top of the page).

https://downloads.haskell.org/~ghc/8.8.3/docs/html/libraries/base-4.13.0.0/GHC-TypeLits.html