Safe Haskell	Trustworthy
Language	Haskell2010

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

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

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.

data SomeSymbol Source

This type represents unknown type-level symbols.

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.

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.

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

Multiplication of type-level naturals.

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

Exponentiation of type-level naturals.

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

Subtraction of type-level naturals.

Since: 4.7.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-existant 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.