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 (n :: Nat)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt n

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: base-4.7.0.0

Minimal complete definition

natSing

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer

Since: base-4.7.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer

Since: base-4.8.0.0

data SomeNat

This type represents unknown type-level natural numbers.

Since: base-4.10.0.0

Constructors

KnownNat n => SomeNat (Proxy n)

Instances

Eq SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

Methods

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

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

Ord SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

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: base-4.7.0.0

Defined in GHC.TypeNats

Methods

readsPrec :: Int -> ReadS SomeNat

readList :: ReadS [SomeNat]

readPrec :: ReadPrec SomeNat

readListPrec :: ReadPrec [SomeNat]

Show SomeNat

Since: base-4.7.0.0

Defined in GHC.TypeNats

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: base-4.7.0.0

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

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

Since: base-4.7.0.0

Integers

data TInt

(Kind) An integer that may be negative.

Constructors

Pos Nat

Neg Nat

Instances

KnownNat n => KnownInt ('Pos n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg 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 (n :: Nat)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt n

KnownNat n => KnownInt ('Pos n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Pos n)

KnownNat n => KnownInt ('Neg n :: TInt)

Defined in Data.TypeNums.Ints

Methods

intSing :: SInt ('Neg 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

forall n.KnownInt n => SomeInt (Proxy n)

Instances

Eq SomeInt

Defined in Data.TypeNums.Ints

Methods

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

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

Ord SomeInt

Defined in Data.TypeNums.Ints

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

Defined in Data.TypeNums.Ints

Methods

readsPrec :: Int -> ReadS SomeInt

readList :: ReadS [SomeInt]

readPrec :: ReadPrec SomeInt

readListPrec :: ReadPrec [SomeInt]

Show SomeInt

Defined in Data.TypeNums.Ints

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

forall k. k :% Nat

Instances

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

Defined in Data.TypeNums.Rats

Methods

ratSing :: SRat (n :% d)

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

Defined in Data.TypeNums.Rats

Methods

ratSing :: SRat (n :% 0)

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 n => KnownRat (n :: k)

Defined in Data.TypeNums.Rats

Methods

ratSing :: SRat n

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

Defined in Data.TypeNums.Rats

Methods

ratSing :: SRat (n :% d)

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

Defined in Data.TypeNums.Rats

Methods

ratSing :: SRat (n :% 0)

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

forall r.KnownRat r => SomeRat (Proxy r)

Instances

Eq SomeRat

Defined in Data.TypeNums.Rats

Methods

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

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

Ord SomeRat

Defined in Data.TypeNums.Rats

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

Defined in Data.TypeNums.Rats

Methods

readsPrec :: Int -> ReadS SomeRat

readList :: ReadS [SomeRat]

readPrec :: ReadPrec SomeRat

readListPrec :: ReadPrec [SomeRat]

Show SomeRat

Defined in Data.TypeNums.Rats

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 family Simplify (x :: Rat) :: Rat where ...

Reduce a type-level rational into its canonical form

Since: 0.1.4

Equations

Simplify ((x :: Nat) :% y) = Quot ('Pos x) (GCD x y) :% Quot y (GCD x y)

Simplify ((x :: TInt) :% y) = Quot x (GCD x y) :% Quot y (GCD x y)

Type level numerical operations

Comparison

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

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

Equations

(a :: Rat) ==? (b :: Rat) = (==) (Simplify a) (Simplify b)

(a :: Nat) ==? ('Pos a) = 'True

('Pos a) ==? (a :: Nat) = 'True

(a :: Nat) ==? (r :: Rat) = (a :% 1) ==? r

(r :: Rat) ==? (a :: Nat) = r ==? (a :% 1)

(a :: TInt) ==? (r :: Rat) = (a :% 1) ==? r

(r :: Rat) ==? (a :: TInt) = r ==? (a :% 1)

(a :: k) ==? (b :: k) = (==) a b

_ ==? _ = 'False

type (/=?) (a :: k1) (b :: k2) = 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

('Pos a) <=? ('Pos b) = (<=?) a b

('Neg _) <=? ('Pos _) = 'True

('Pos 0) <=? ('Neg 0) = 'True

('Pos _) <=? ('Neg _) = 'False

('Pos a) <=? b = a <=? b

a <=? ('Pos b) = a <=? b

0 <=? ('Neg 0) = 'True

(a :: Nat) <=? ('Neg _) = 'False

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

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

(n :% 0) <=? _ = TypeError ('Text "Denominator must not equal 0")

_ <=? (n :% 0) = TypeError ('Text "Denominator must not equal 0")

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

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

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

_ <=? _ = TypeError ('Text "Incomparable")

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

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

type (/=) (a :: k1) (b :: k2) = (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

Unary operations

type family Abs (x :: k) :: k where ...

The absolute value of a type-level number

Since: 0.1.4

Equations

Abs (x :: Nat) = x

Abs ('Pos x) = 'Pos x

Abs ('Neg x) = 'Pos x

Abs (x :% y) = Simplify (Abs x :% y)

type family Negate (x :: k) :: NegK k where ...

The result of negating a TInt

Since: 0.1.4

Equations

Negate (x :: Nat) = Negate ('Pos x)

Negate ('Pos 0) = 'Pos 0

Negate ('Neg 0) = 'Pos 0

Negate ('Pos x) = 'Neg x

Negate ('Neg x) = 'Pos x

Negate (x :% y) = Negate x :% y

type family Recip (x :: k) :: Rat where ...

The reciprocal of a type-level number

Since: 0.1.4

Equations

Recip (x :: Nat) = 'Pos 1 :% x

Recip ('Pos x) = 'Pos 1 :% x

Recip ('Neg x) = 'Neg 1 :% x

Recip ('Pos x :% y) = 'Pos y :% x

Recip ('Neg x :% y) = 'Neg y :% x

Recip ((x :: Nat) :% y) = 'Pos y :% x

type family Floor (x :: k) :: TInt where ...

Round a type-level number towards negative infinity

Since: 0.1.4

Equations

Floor (x :: Nat) = 'Pos x

Floor (x :: TInt) = x

Floor (x :% 0) = TypeError ('Text "The denominator must not be 0")

Floor ((x :: Nat) :% y) = 'Pos (Div x y)

Floor ((x :: TInt) :% y) = Div x y

type family Ceiling (x :: k) :: TInt where ...

Round a type-level number towards positive infinity

Since: 0.1.4

Equations

Ceiling (x :: Nat) = 'Pos x

Ceiling (x :: TInt) = x

Ceiling (x :% 0) = TypeError ('Text "The denominator must not be 0")

Ceiling (x :% y) = Add 1 (Floor (Sub x 1 :% y))

type family Truncate (x :: k) :: TInt where ...

Round a type-level number towards zero

Since: 0.1.4

Equations

Truncate (x :: Nat) = 'Pos x

Truncate (x :: TInt) = x

Truncate (x :% 0) = TypeError ('Text "The denominator must not be 0")

Truncate ((x :: Nat) :% y) = 'Pos (Quot x y)

Truncate ((x :: TInt) :% y) = Quot x y

Binary operations

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

For the difference of two naturals a and b, a-b is also a natural, so only exists for a >= b.

type * a b = Mul a b infixl 7

The product of two type-level numbers.

Due to changes in GHC 8.6, using this operator infix and unqualified requires the NoStarIsType language extension to be active. See the GHC 8.6.x migration guide for details: https://ghc.haskell.org/trac/ghc/wiki/Migration/8.6

type (/) a b = RatDiv a b infixl 7

The ratio of two type-level numbers

type (^) a b = Exp a b infixr 8

A type-level number raised to an integer power. For Nat powers, the result kind is the same as the base. For TInt powers, the result kind is Rat.

Since: 0.1.4

type family DivMod (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ...

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is positive such that x = q*y + r @since 0.1.4

Equations

DivMod _ 0 = TypeError ('Text "Divisor must not be 0")

DivMod (x :: Nat) y = UnPos (DivModAux ('Pos x) y ('Pos 0))

DivMod ('Pos x) y = DivModAux ('Pos x) y ('Pos 0)

DivMod ('Neg x) y = DivModNegFixup (DivModAux ('Pos x) y ('Pos 0)) y

type family QuotRem (x :: k) (y :: Nat) :: (IntDivK k, IntDivK k) where ...

The quotient and remainder of a type-level integer and a natural number. For a negative dividend, the remainder part is negative such that x = q*y + r @since 0.1.4

Equations

QuotRem ('Neg x) y = QuotRemFixup (DivMod ('Neg x) y) y

QuotRem x y = DivMod x y

type family Div (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7

The quotient of a type-level integer and a natural number.

Since: 0.1.4

Equations

Div x y = Fst (DivMod x y)

type family Mod (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7

The remainder of a type-level integer and a natural number For a negative number, behaves similarly to mod. @since 0.1.4

Equations

Mod x y = Snd (DivMod x y)

type family Quot (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7

The integer part of the result of dividing an integer by a natural number

Since: 0.1.4

Equations

Quot x y = Fst (QuotRem x y)

type family Rem (x :: k) (y :: Nat) :: IntDivK k where ... infixl 7

The remainder of the result of dividing an integer by a natural number

Since: 0.1.4

Equations

Rem x y = Snd (QuotRem x y)

type family GCD (x :: k1) (y :: k2) :: Nat where ...

The greatest common divisor of two type-level integers

Since: 0.1.4

Equations

GCD (x :: Nat) (y :: Nat) = GCDAux x y

GCD (x :: Nat) (y :: TInt) = GCDAux x (UnPos (Abs y))

GCD (x :: TInt) (y :: Nat) = GCDAux (UnPos (Abs x)) y

GCD (x :: TInt) (y :: TInt) = GCDAux (UnPos (Abs x)) (UnPos (Abs y))

type family IntLog (n :: Nat) (x :: k) :: TInt where ...

The floor of the logarithm of a type-level number NB. unlike Log2, Log n 0 here is a type error.

Since: 0.1.4

Equations

IntLog 0 _ = TypeError ('Text "Invalid IntLog base: 0")

IntLog 1 _ = TypeError ('Text "Invalid IntLog base: 1")

IntLog _ 0 = TypeError ('Text "IntLog n 0 is infinite")

IntLog _ ('Pos 0) = TypeError ('Text "IntLog n 0 is infinite")

IntLog _ ('Neg 0) = TypeError ('Text "IntLog n 0 is infinite")

IntLog _ (0 :% _) = TypeError ('Text "IntLog n 0 is infinite")

IntLog _ (_ :% 0) = TypeError ('Text "IntLog parameter has zero denominator")

IntLog _ ('Neg _) = TypeError ('Text "IntLog of a negative does not exist")

IntLog n (x :: Nat) = IntLog n ('Pos x)

IntLog n ('Pos x) = IntLogAux n ('Pos x)

IntLog n (x :: Rat) = If (Floor x == 'Pos 0) (NegLogFudge n x (Negate (IntLogAux n (Floor (Recip x))))) (IntLog n (Floor x))

type Log2 x = IntLog 2 x

The floor of the logarithm base 2 of a type-level number. Note that unlike Log2, this errors on Log2 0.

Since: 0.1.4

Symbols

data Symbol

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

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

Concatenation of type-level symbols.

Since: base-4.10.0.0

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

Comparison of type-level symbols, as a function.

Since: base-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: base-4.7.0.0

Minimal complete definition

symbolSing

symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String

Since: base-4.7.0.0

symbolVal' :: forall (n :: Symbol). KnownSymbol n => Proxy# n -> String

Since: base-4.8.0.0

data SomeSymbol

This type represents unknown type-level symbols.

Constructors

KnownSymbol n => SomeSymbol (Proxy n)

Since: base-4.7.0.0

Instances

Eq SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

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

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

Ord SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

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: base-4.7.0.0

Defined in GHC.TypeLits

Methods

readsPrec :: Int -> ReadS SomeSymbol

readList :: ReadS [SomeSymbol]

readPrec :: ReadPrec SomeSymbol

readListPrec :: ReadPrec [SomeSymbol]

Show SomeSymbol

Since: base-4.7.0.0

Defined in GHC.TypeLits

Methods

showsPrec :: Int -> SomeSymbol -> ShowS

show :: SomeSymbol -> String

showList :: [SomeSymbol] -> ShowS

someSymbolVal :: String -> SomeSymbol

Convert a string into an unknown type-level symbol.

Since: base-4.7.0.0

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

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

Since: base-4.7.0.0

User-defined type errors

type family TypeError (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: base-4.9.0.0

data ErrorMessage

A description of a custom type error.

Constructors

Text Symbol

Show the text as is.

ShowType t

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

ErrorMessage :<>: ErrorMessage infixl 6

Put two pieces of error message next to each other.

ErrorMessage :$$: ErrorMessage infixl 5

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