base-4.16.0.0: Basic libraries
Safe HaskellTrustworthy
LanguageHaskell2010

GHC.TypeLits

Description

GHC's DataKinds language extension lifts data constructors, natural numbers, and strings to the type level. This module provides the primitives needed for working with type-level numbers (the Nat kind), strings (the Symbol kind), and characters (the Char kind). It also defines the TypeError type family, a feature that makes use of type-level strings to support user defined type errors.

For now, this module is the API for working with type-level literals. However, please note that it is a work in progress and is subject to change. Once the design of the DataKinds feature is more stable, this will be considered only an internal GHC module, and the programmer interface for working with type-level data will be defined in a separate library.

Since: base-4.6.0.0

Synopsis

Kinds

data Natural Source #

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

Instances

Instances details
Data Natural #

Since: base-4.8.0.0

Instance details

Defined in Data.Data

Methods

gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> Natural -> c Natural Source #

gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c Natural Source #

toConstr :: Natural -> Constr Source #

dataTypeOf :: Natural -> DataType Source #

dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c Natural) Source #

dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c Natural) Source #

gmapT :: (forall b. Data b => b -> b) -> Natural -> Natural Source #

gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r Source #

gmapQr :: forall r r'. (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> Natural -> r Source #

gmapQ :: (forall d. Data d => d -> u) -> Natural -> [u] Source #

gmapQi :: Int -> (forall d. Data d => d -> u) -> Natural -> u Source #

gmapM :: Monad m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> Natural -> m Natural Source #

Bits Natural #

Since: base-4.8.0

Instance details

Defined in GHC.Bits

Enum Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Enum

Ix Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Ix

Num Natural #

Note that Natural's Num instance isn't a ring: no element but 0 has an additive inverse. It is a semiring though.

Since: base-4.8.0.0

Instance details

Defined in GHC.Num

Read Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Read

Integral Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Real

Real Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Real

Show Natural #

Since: base-4.8.0.0

Instance details

Defined in GHC.Show

PrintfArg Natural #

Since: base-4.8.0.0

Instance details

Defined in Text.Printf

Eq Natural 
Instance details

Defined in GHC.Num.Natural

Ord Natural 
Instance details

Defined in GHC.Num.Natural

KnownNat n => HasResolution (n :: Nat) #

For example, Fixed 1000 will give you a Fixed with a resolution of 1000.

Instance details

Defined in Data.Fixed

Methods

resolution :: p n -> Integer Source #

type Compare (a :: Natural) (b :: Natural) # 
Instance details

Defined in Data.Type.Ord

type Compare (a :: Natural) (b :: Natural) = CmpNat a b

type Nat = Natural Source #

A type synonym for Natural.

Prevously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.15.0.0

data Symbol Source #

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

Instances

Instances details
type Compare (a :: Symbol) (b :: Symbol) # 
Instance details

Defined in Data.Type.Ord

type Compare (a :: Symbol) (b :: Symbol) = CmpSymbol a b

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

Minimal complete definition

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

Minimal complete definition

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

class KnownChar (n :: Char) Source #

Since: base-4.16.0.0

Minimal complete definition

charSing

charVal :: forall n proxy. KnownChar n => proxy n -> Char Source #

charVal' :: forall n. KnownChar n => Proxy# n -> Char Source #

data SomeNat Source #

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

forall n.KnownNat n => SomeNat (Proxy n) 

Instances

Instances details
Read SomeNat #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Show SomeNat #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Eq SomeNat #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

Ord SomeNat #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeNats

data SomeSymbol Source #

This type represents unknown type-level symbols.

Constructors

forall n.KnownSymbol n => SomeSymbol (Proxy n)

Since: base-4.7.0.0

Instances

Instances details
Read SomeSymbol #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Show SomeSymbol #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Eq SomeSymbol #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

Ord SomeSymbol #

Since: base-4.7.0.0

Instance details

Defined in GHC.TypeLits

data SomeChar Source #

Constructors

forall n.KnownChar n => SomeChar (Proxy n) 

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

someCharVal :: Char -> SomeChar Source #

Convert a character into an unknown type-level char.

Since: base-4.16.0.0

sameNat :: (KnownNat a, KnownNat b) => proxy1 a -> proxy2 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) => proxy1 a -> proxy2 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

sameChar :: (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) Source #

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

Since: base-4.16.0.0

data OrderingI a b where Source #

Ordering data type for type literals that provides proof of their ordering.

Since: base-4.16.0.0

Constructors

LTI :: Compare a b ~ 'LT => OrderingI a b 
EQI :: Compare a a ~ 'EQ => OrderingI a a 
GTI :: Compare a b ~ 'GT => OrderingI a b 

Instances

Instances details
Show (OrderingI a b) # 
Instance details

Defined in Data.Type.Ord

Eq (OrderingI a b) # 
Instance details

Defined in Data.Type.Ord

Methods

(==) :: OrderingI a b -> OrderingI a b -> Bool Source #

(/=) :: OrderingI a b -> OrderingI a b -> Bool Source #

cmpNat :: forall a b proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b Source #

Like sameNat, but if the numbers aren't equal, this additionally provides proof of LT or GT.

Since: base-4.16.0.0

cmpSymbol :: forall a b proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> OrderingI a b Source #

Like sameSymbol, but if the symbols aren't equal, this additionally provides proof of LT or GT.

Since: base-4.16.0.0

cmpChar :: forall a b proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> OrderingI a b Source #

Like sameChar, but if the Chars aren't equal, this additionally provides proof of LT or GT.

Since: base-4.16.0.0

Functions on type literals

type (<=) x y = Assert (x <=? y) (LeErrMsg x y) infix 4 Source #

Comparison (<=) of comparable types, as a constraint.

Since: base-4.16.0.0

type (<=?) m n = OrdCond (Compare m n) 'True 'True 'False infix 4 Source #

Comparison (<=) of comparable types, as a function.

Since: base-4.16.0.0

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 :: Natural) (n :: Natural) :: 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 CmpChar (a :: Char) (b :: Char) :: Ordering Source #

Comparison of type-level characters.

Since: base-4.16.0.0

type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol Source #

Extending a type-level symbol with a type-level character

Since: base-4.16.0.0

type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) Source #

This type family yields type-level Just storing the first character of a symbol and its tail if it is defined and Nothing otherwise.

Since: base-4.16.0.0

type family CharToNat (c :: Char) :: Nat Source #

Convert a character to its Unicode code point (cf. ord)

Since: base-4.16.0.0

type family NatToChar (n :: Nat) :: Char Source #

Convert a Unicode code point to a character (cf. chr)

Since: base-4.16.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: base-4.9.0.0

data ErrorMessage Source #

A description of a custom type error.

Constructors

Text Symbol

Show the text as is.

forall t. 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.