Data.TypeLits

This module provides the same interface as GHC.TypeLits, but with naming conflicts resolved in favour of this package. For example, '(<=)' resolves to the kind-polymorphic version from Data.TypeNums.

If you are only working with type-level numbers, import Data.TypeNums instead. This module is purely for convenience for those who want to use both functionality from GHC.TypeLits and functionality from Data.TypeNums.

Type level numbers

Naturals

data Nat :: *

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

Instances

KnownNat n => KnownInt Nat n

Methods

intSing :: SInt n n

type (==) Nat a b

type (==) Nat a b = EqNat a b

class KnownNat (n :: Nat)

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 :: KnownNat n => proxy n -> Integer

Since: 4.7.0.0

natVal' :: KnownNat n => Proxy# Nat n -> Integer

Since: 4.8.0.0

data SomeNat :: * where

This type represents unknown type-level natural numbers.

Since: 4.10.0.0

Constructors

SomeNat :: SomeNat

Instances

Eq SomeNat

Since: 4.7.0.0

Methods

(==) :: SomeNat -> SomeNat -> Bool

(/=) :: SomeNat -> SomeNat -> Bool

Ord SomeNat

Since: 4.7.0.0

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

Since: 4.7.0.0

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: 4.7.0.0

Methods

showsPrec :: Int -> SomeNat -> ShowS

show :: SomeNat -> String

showList :: [SomeNat] -> ShowS

someNatVal :: Integer -> Maybe SomeNat

Convert an integer into an unknown type-level natural.

Since: 4.7.0.0

sameNat :: (KnownNat a, KnownNat b) => Proxy Nat a -> Proxy Nat b -> Maybe ((:~:) Nat a b)

We either get evidence that this function was instantiated with the same type-level numbers, or Nothing.

Since: 4.7.0.0

Integers

data TInt

(Kind) An integer that may be negative.

Constructors

Pos Nat

Neg Nat

Instances

KnownNat n => KnownInt TInt (Pos n)

Methods

intSing :: SInt (Pos n) n

KnownNat n => KnownInt TInt (Neg n)

Methods

intSing :: SInt (Neg n) n

class KnownInt (n :: k)

This class gives the (value-level) integer associated with a type-level integer. There are instances of this class for every concrete natural: 0, 1, 2, etc. There are also instances of this class for every negated natural, such as Neg 1.

Minimal complete definition

intSing

Instances

KnownNat n => KnownInt Nat n

Methods

intSing :: SInt n n

KnownNat n => KnownInt TInt (Pos n)

Methods

intSing :: SInt (Pos n) n

KnownNat n => KnownInt TInt (Neg n)

Methods

intSing :: SInt (Neg n) n

intVal :: forall n proxy. KnownInt n => proxy n -> Integer

Get the value associated with a type-level integer

intVal' :: forall n. KnownInt n => Proxy# n -> Integer

Get the value associated with a type-level integer. The difference between this function and intVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

data SomeInt

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

KnownInt n => SomeInt (Proxy n)

Instances

Eq SomeInt

Methods

(==) :: SomeInt -> SomeInt -> Bool

(/=) :: SomeInt -> SomeInt -> Bool

Ord SomeInt

Methods

compare :: SomeInt -> SomeInt -> Ordering

(<) :: SomeInt -> SomeInt -> Bool

(<=) :: SomeInt -> SomeInt -> Bool

(>) :: SomeInt -> SomeInt -> Bool

(>=) :: SomeInt -> SomeInt -> Bool

max :: SomeInt -> SomeInt -> SomeInt

min :: SomeInt -> SomeInt -> SomeInt

Read SomeInt

Methods

readsPrec :: Int -> ReadS SomeInt

readList :: ReadS [SomeInt]

readPrec :: ReadPrec SomeInt

readListPrec :: ReadPrec [SomeInt]

Show SomeInt

Methods

showsPrec :: Int -> SomeInt -> ShowS

show :: SomeInt -> String

showList :: [SomeInt] -> ShowS

someIntVal :: Integer -> SomeInt

Convert an integer into an unknown type-level integer.

Since: 0.1.1

Rationals

data Rat

Type constructor for a rational

Constructors

k :% Nat

Instances

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d)

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0)

Methods

ratSing :: SRat ((k :% n) 0) r

class KnownRat r

This class gives the (value-level) rational associated with a type-level rational. There are instances of this class for every combination of a concrete integer and concrete natural.

Minimal complete definition

ratSing

Instances

KnownInt k n => KnownRat k n

Methods

ratSing :: SRat n r

(KnownInt k n, KnownNat d, (/=) Nat d 0) => KnownRat Rat ((:%) k n d)

Methods

ratSing :: SRat ((k :% n) d) r

TypeError Constraint (Text "Denominator must not equal 0") => KnownRat Rat ((:%) k n 0)

Methods

ratSing :: SRat ((k :% n) 0) r

ratVal :: forall proxy r. KnownRat r => proxy r -> Rational

Get the value associated with a type-level rational

ratVal' :: forall r. KnownRat r => Proxy# r -> Rational

Get the value associated with a type-level rational. The difference between this function and ratVal is that it takes a Proxy# parameter, which has zero runtime representation and so is entirely free.

data SomeRat

This type represents unknown type-level integers.

Since: 0.1.1

Constructors

KnownRat r => SomeRat (Proxy r)

Instances

Eq SomeRat

Methods

(==) :: SomeRat -> SomeRat -> Bool

(/=) :: SomeRat -> SomeRat -> Bool

Ord SomeRat

Methods

compare :: SomeRat -> SomeRat -> Ordering

(<) :: SomeRat -> SomeRat -> Bool

(<=) :: SomeRat -> SomeRat -> Bool

(>) :: SomeRat -> SomeRat -> Bool

(>=) :: SomeRat -> SomeRat -> Bool

max :: SomeRat -> SomeRat -> SomeRat

min :: SomeRat -> SomeRat -> SomeRat

Read SomeRat

Methods

readsPrec :: Int -> ReadS SomeRat

readList :: ReadS [SomeRat]

readPrec :: ReadPrec SomeRat

readListPrec :: ReadPrec [SomeRat]

Show SomeRat

Methods

showsPrec :: Int -> SomeRat -> ShowS

show :: SomeRat -> String

showList :: [SomeRat] -> ShowS

someRatVal :: Rational -> SomeRat

Convert a rational into an unknown type-level rational.

Since: 0.1.1

Type level numerical operations

Comparison

type (==?) (a :: k) (b :: k) = (==) a b infix 4

Boolean type-level equals. Useful for e.g. If (x ==? 0)

type (/=?) (a :: k) (b :: k) = Not ((==) a b) infix 4

Boolean type-level not-equals.

type family (a :: k1) <=? (b :: k2) :: Bool where ... infix 4

Boolean comparison of two type-level numbers

Equations

(a :: Nat) <=? (b :: Nat) = (<=?) a b

0 <=? (Neg 0) = True

(Neg a) <=? (b :: Nat) = True

(Neg a) <=? (Neg b) = (<=?) b a

(n1 :% d1) <=? (n2 :% d2) = (n1 * d1) <=? (n2 * d2)

a <=? (n :% d) = (a * d) <=? n

(n :% d) <=? b = n <=? (b * d)

type (==) (a :: k) (b :: k) = (==) a b ~ True infix 4

Equality constraint, used as e.g. (x == 3) => _

type (/=) (a :: k) (b :: k) = (==) a b ~ False infix 4

Not-equal constraint

type (<=) (a :: k1) (b :: k2) = (a <=? b) ~ True infix 4

type (<) (a :: k1) (b :: k2) = (b <=? a) ~ False infix 4

type (>=) (a :: k1) (b :: k2) = (b <=? a) ~ True infix 4

type (>) (a :: k1) (b :: k2) = (a <=? b) ~ False infix 4

Arithmetic

type (+) a b = Add a b infixl 6

The sum of two type-level numbers

type (-) a b = Sub a b infixl 6

The difference of two type-level numbers

type * a b = Mul a b infixl 7

The product of two type-level numbers

type family (a :: Nat) ^ (b :: Nat) :: Nat where ... infixr 8

Exponentiation of type-level naturals.

Symbols

data Symbol :: *

(Kind) This is the kind of type-level symbols. Declared here because class IP needs it

Instances

type (==) Symbol a b

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

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ...

Concatenation of type-level symbols.

Since: 4.10.0.0

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ...

Comparison of type-level symbols, as a function.

Since: 4.7.0.0

class KnownSymbol (n :: Symbol)

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 :: KnownSymbol n => proxy n -> String

Since: 4.7.0.0

symbolVal' :: KnownSymbol n => Proxy# Symbol n -> String

Since: 4.8.0.0

data SomeSymbol :: * where

This type represents unknown type-level symbols.

Constructors

SomeSymbol :: SomeSymbol

Since: 4.7.0.0

Instances

Eq SomeSymbol

Since: 4.7.0.0

Methods

(==) :: SomeSymbol -> SomeSymbol -> Bool

(/=) :: SomeSymbol -> SomeSymbol -> Bool

Ord SomeSymbol

Since: 4.7.0.0

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

Since: 4.7.0.0

Methods

readsPrec :: Int -> ReadS SomeSymbol

readList :: ReadS [SomeSymbol]

readPrec :: ReadPrec SomeSymbol

readListPrec :: ReadPrec [SomeSymbol]

Show SomeSymbol

Since: 4.7.0.0

Methods

showsPrec :: Int -> SomeSymbol -> ShowS

show :: SomeSymbol -> String

showList :: [SomeSymbol] -> ShowS

someSymbolVal :: String -> SomeSymbol

Convert a string into an unknown type-level symbol.

Since: 4.7.0.0

sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy Symbol a -> Proxy Symbol b -> Maybe ((:~:) Symbol a b)

We either get evidence that this function was instantiated with the same type-level symbols, or Nothing.

Since: 4.7.0.0

User-defined type errors

type family TypeError b (a :: ErrorMessage) :: b where ...

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

data ErrorMessage :: * where

A description of a custom type error.

Constructors

Text :: ErrorMessage

Show the text as is.

ShowType :: ErrorMessage

Pretty print the type. ShowType :: k -> ErrorMessage

(:<>:) :: ErrorMessage infixl 6

Put two pieces of error message next to each other.

(:$$:) :: ErrorMessage infixl 5

Stack two pieces of error message on top of each other.