Safe Haskell	Trustworthy
Language	Haskell2010

GHC.TypeLits

Contents

Kinds
Linking type and value level
Functions on type literals

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.

Instances

type (==) Nat a b Source

data Symbol Source

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

Instances

type (==) Symbol a b Source

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

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

Constructors

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

Since: 4.7.0.0

Instances

Eq SomeNat Source
Methods (==) :: SomeNat -> SomeNat -> Bool (/=) :: SomeNat -> SomeNat -> Bool
Ord SomeNat Source
Methods compare :: SomeNat -> SomeNat -> Ordering (<) :: SomeNat -> SomeNat -> Bool (<=) :: SomeNat -> SomeNat -> Bool (>) :: SomeNat -> SomeNat -> Bool (>=) :: SomeNat -> SomeNat -> Bool max :: SomeNat -> SomeNat -> SomeNat min :: SomeNat -> SomeNat -> SomeNat
Read SomeNat Source
Methods readsPrec :: Int -> ReadS SomeNat Source readList :: ReadS [SomeNat] Source readPrec :: ReadPrec SomeNat Source readListPrec :: ReadPrec [SomeNat] Source
Show SomeNat Source
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

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

Since: 4.7.0.0

Instances

Eq SomeSymbol Source
Methods (==) :: SomeSymbol -> SomeSymbol -> Bool (/=) :: SomeSymbol -> SomeSymbol -> Bool
Ord SomeSymbol Source
Methods compare :: SomeSymbol -> SomeSymbol -> Ordering (<) :: SomeSymbol -> SomeSymbol -> Bool (<=) :: SomeSymbol -> SomeSymbol -> Bool (>) :: SomeSymbol -> SomeSymbol -> Bool (>=) :: SomeSymbol -> SomeSymbol -> Bool max :: SomeSymbol -> SomeSymbol -> SomeSymbol min :: SomeSymbol -> SomeSymbol -> SomeSymbol
Read SomeSymbol Source
Methods readsPrec :: Int -> ReadS SomeSymbol Source readList :: ReadS [SomeSymbol] Source readPrec :: ReadPrec SomeSymbol Source readListPrec :: ReadPrec [SomeSymbol] Source
Show SomeSymbol Source
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.

type family m <=? n :: 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 + n :: Nat infixl 6 Source

Addition of type-level naturals.

type family m * n :: Nat infixl 7 Source

Multiplication of type-level naturals.

type family m ^ n :: Nat infixr 8 Source

Exponentiation of type-level naturals.

type family m - n :: Nat infixl 6 Source

Subtraction of type-level naturals.

Since: 4.7.0.0

type family CmpNat m n :: Ordering Source

Comparison of type-level naturals, as a function.

Since: 4.7.0.0

type family CmpSymbol m n :: Ordering Source

Comparison of type-level symbols, as a function.

Since: 4.7.0.0