Safe Haskell	None
Language	Haskell2010

GHC.TypeLits

Contents

Kinds
Linking type and value level
Functions on type nats

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

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.

Linking type and value level

class KnownNat nSource

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

class KnownSymbol nSource

This class gives the integer 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

data SomeNat Source

This type represents unknown type-level natural numbers.

Constructors

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

Since: 4.7.0.0

Instances

Eq SomeNat
Ord SomeNat
Read SomeNat
Show SomeNat

data SomeSymbol Source

This type represents unknown type-level symbols.

Constructors

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

Since: 4.7.0.0

Instances

Eq SomeSymbol
Ord SomeSymbol
Read SomeSymbol
Show SomeSymbol

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 nats

type (<=) x y = (x <=? y) ~ True Source

Comparison of type-level naturals, as a constraint.

type family m <=? n :: Bool Source

Comparison of type-level naturals, as a function.

type family m + n :: Nat Source

Addition of type-level naturals.

type family m * n :: Nat Source

Multiplication of type-level naturals.

type family m ^ n :: Nat Source

Exponentiation of type-level naturals.

type family m - n :: Nat Source

Subtraction of type-level naturals.

Since: 4.7.0.0