Safe Haskell	Trustworthy
Language	Haskell2010

GHC.TypeLits

Contents

Kinds
Linking type and value level
Functions on type literals
User-defined type errors

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

Synopsis

data Nat :: *
data Symbol :: *
class KnownNat (n :: Nat)
natVal :: forall n proxy. KnownNat n => proxy n -> Integer
natVal' :: forall n. KnownNat n => Proxy# n -> Integer
class KnownSymbol (n :: Symbol)
symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String
symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String
data SomeNat = KnownNat n => SomeNat (Proxy n)
data SomeSymbol = 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 :: Nat) <=? (n :: Nat) :: Bool
type family (m :: Nat) + (n :: Nat) :: Nat
type family (m :: Nat) * (n :: Nat) :: Nat
type family (m :: Nat) ^ (n :: Nat) :: Nat
type family (m :: Nat) - (n :: Nat) :: Nat
type family Div (m :: Nat) (n :: Nat) :: Nat
type family Mod (m :: Nat) (n :: Nat) :: Nat
type family Log2 (m :: Nat) :: Nat
type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol
type family CmpNat (m :: Nat) (n :: Nat) :: Ordering
type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering
type family TypeError (a :: ErrorMessage) :: b where ...
data ErrorMessage
- = Text Symbol
- | ShowType t
- | ErrorMessage :<>: ErrorMessage
- | ErrorMessage :$$: ErrorMessage

Kinds

data Nat :: * Source #

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

data Symbol :: * Source #

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

Linking type and value level

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: 4.7.0.0

Minimal complete definition

natSing

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

Since: 4.7.0.0

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

Since: 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: 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

data SomeNat Source #

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n)

Instances

Eq SomeNat #	Since: 4.7.0.0
Instance details Methods (==) :: SomeNat -> SomeNat -> Bool Source # (/=) :: SomeNat -> SomeNat -> Bool Source #
Ord SomeNat #	Since: 4.7.0.0
Instance details Methods compare :: SomeNat -> SomeNat -> Ordering Source # (<) :: SomeNat -> SomeNat -> Bool Source # (<=) :: SomeNat -> SomeNat -> Bool Source # (>) :: SomeNat -> SomeNat -> Bool Source # (>=) :: SomeNat -> SomeNat -> Bool Source # max :: SomeNat -> SomeNat -> SomeNat Source # min :: SomeNat -> SomeNat -> SomeNat Source #
Read SomeNat #	Since: 4.7.0.0
Instance details Methods readsPrec :: Int -> ReadS SomeNat Source # readList :: ReadS [SomeNat] Source # readPrec :: ReadPrec SomeNat Source # readListPrec :: ReadPrec [SomeNat] Source #
Show SomeNat #	Since: 4.7.0.0
Instance details Methods showsPrec :: Int -> SomeNat -> ShowS Source # show :: SomeNat -> String Source # showList :: [SomeNat] -> ShowS Source #

data SomeSymbol Source #

This type represents unknown type-level symbols.

Constructors

KnownSymbol n => SomeSymbol (Proxy n)

Since: 4.7.0.0

Instances

Eq SomeSymbol #	Since: 4.7.0.0
Instance details Methods (==) :: SomeSymbol -> SomeSymbol -> Bool Source # (/=) :: SomeSymbol -> SomeSymbol -> Bool Source #
Ord SomeSymbol #	Since: 4.7.0.0
Instance details Methods compare :: 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: 4.7.0.0
Instance details Methods readsPrec :: Int -> ReadS SomeSymbol Source # readList :: ReadS [SomeSymbol] Source # readPrec :: ReadPrec SomeSymbol Source # readListPrec :: ReadPrec [SomeSymbol] Source #
Show SomeSymbol #	Since: 4.7.0.0
Instance details Methods showsPrec :: 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: 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 (<=) x y = (x <=? y) ~ True infix 4 Source #

Comparison of type-level naturals, as a constraint.

Since: 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: 4.7.0.0

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

Multiplication of type-level naturals.

Since: 4.7.0.0

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

Exponentiation of type-level naturals.

Since: 4.7.0.0

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

Subtraction of type-level naturals.

Since: 4.7.0.0

type family Div (m :: Nat) (n :: Nat) :: Nat Source #

Division (round down) of natural numbers. Div x 0 is undefined (i.e., it cannot be reduced).

Since: 4.11.0.0

type family Mod (m :: Nat) (n :: Nat) :: Nat Source #

Modulus of natural numbers. Mod x 0 is undefined (i.e., it cannot be reduced).

Since: 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: 4.11.0.0

type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source #

Concatenation of type-level symbols.

Since: 4.10.0.0

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

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

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

Comparison of type-level symbols, as a function.

Since: 4.7.0.0

User-defined type errors

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: 4.9.0.0

data ErrorMessage Source #

A description of a custom type error.

Constructors

Text Symbol	Show the text as is.
ShowType t	Pretty print the type. `ShowType :: k -> ErrorMessage`
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.