base-4.7.0.0: Basic libraries

Safe HaskellNone
LanguageHaskell2010

GHC.TypeLits

Contents

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 = EqNat a b 

data Symbol Source

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

Instances

type (==) Symbol a b = EqSymbol a b 

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

class KnownSymbol n Source

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

data SomeSymbol Source

This type represents unknown type-level symbols.

Constructors

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

Since: 4.7.0.0

Instances

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