Kinds

data Natural Source

Natural number

Invariant: numbers <= 0xffffffffffffffff use the NS constructor

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.16.0.0

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

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

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

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

data SomeSymbol Source

This type represents unknown type-level symbols.

data SomeChar 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

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

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.