GHC.TypeLits

Safe Haskell	Надёжный
Язык	Haskell2010

Типы

data Nat Исходный код

(Тип) Это тип натуральных чисел на уровне типов.

data Символ Исходный код

(Тип) Это тип символов на уровне типов. Объявлен здесь, потому что класс IP нуждается в нём

Связывание уровня типов и значений

class KnownNat (n :: Nat) Исходный код

Этот класс предоставляет целое число, ассоциированное с натуральным числом на уровне типов. Существуют экземпляры класса для каждого конкретного литерала: 0, 1, 2 и т.д.

С момента выпуска: base-4.7.0.0

natVal :: forall n proxy. KnownNat n => proxy n -> Integer Исходный код

С момента выпуска: base-4.7.0.0

natVal' :: forall n. KnownNat n => Proxy# n -> Integer Исходный код

С момента выпуска: base-4.8.0.0

class KnownSymbol (n :: Символ) Исходный код

Этот класс предоставляет строку, ассоциированную со символом на уровне типов. Существуют экземпляры класса для каждого конкретного литерала: "hello" и т.д.

С момента выпуска: base-4.7.0.0

symbolVal :: forall n proxy. KnownSymbol n => proxy n -> String Исходный код

С момента выпуска: base-4.7.0.0

symbolVal' :: forall n. KnownSymbol n => Proxy# n -> String Исходный код

С момента выпуска: base-4.8.0.0

data SomeNat Исходный код

Этот тип представляет неизвестные натуральные числа на уровне типов.

С момента выпуска: base-4.10.0.0

тип SomeSymbol Исходный код

Этот тип представляет неизвестные символы уровня типов.

someNatVal :: Integer -> Maybe SomeNat Источник

Преобразовать целое число в неизвестное число типа.

С момента выпуска: base-4.7.0.0

someSymbolVal :: String -> SomeSymbol Источник

Преобразовать строку в неизвестный символ типа.

С момента выпуска: base-4.7.0.0

sameNat :: (KnownNat a, KnownNat b) => Proxy a -> Proxy b -> Maybe (a :~: b) Источник

Мы либо получаем доказательство, что эта функция была вызвана с одинаковыми числовыми значениями типа, либо Nothing.

С момента выпуска: base-4.7.0.0

sameSymbol :: (KnownSymbol a, KnownSymbol b) => Proxy a -> Proxy b -> Maybe (a :~: b) Источник

Мы либо получаем доказательство, что эта функция была вызвана с одинаковыми символами типа, либо Nothing.

С момента выпуска: base-4.7.0.0

Функции над литералами типов

type (<=) x y = (x <=? y) ~ 'True infix 4 Источник

Сравнение натуральных чисел типа в качестве условия.

С момента выпуска: base-4.7.0.0

type family (m :: Nat) <=? (n :: Nat) :: Bool infix 4 Source

Сравнение натуральных чисел на уровне типов, как функция. ПРИМЕЧАНИЕ: Функциональность этой функции должна быть включена в CmpNat, поэтому она может быть удалена в будущем. Пожалуйста, сообщите нам, если вы обнаружите расхождения между этими двумя функциями.

type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Source

Сложение натуральных чисел на уровне типов.

С версии: base-4.7.0.0

type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Source

Умножение натуральных чисел на уровне типов.

С версии: base-4.7.0.0

type family (m :: Nat) ^ (n :: Nat) :: Nat infixr 8 Source

Возведение в степень натуральных чисел на уровне типов.

С версии: base-4.7.0.0

type family (m :: Nat) - (n :: Nat) :: Nat infixl 6 Source

Вычитание натуральных чисел на уровне типов.

С версии: base-4.7.0.0

type family Div (m :: Nat) (n :: Nat) :: Nat infixl 7 Source

Деление натуральных чисел (округление вниз). Div x 0 не определено (т.е. его нельзя упростить).

С версии: base-4.11.0.0

type family Mod (m :: Nat) (n :: Nat) :: Nat infixl 7 Source

Остаток от деления натуральных чисел. Mod x 0 не определено (т.е. его нельзя упростить).

С версии: base-4.11.0.0

type family Log2 (m :: Nat) :: Nat Source

Логарифм по основанию 2 (округление вниз) натуральных чисел. Log 0 не определено (т.е. его нельзя упростить).

С версии: base-4.11.0.0

type family AppendSymbol (m :: Symbol) (n :: Symbol) :: Symbol Source

Конкатенация символов на уровне типов.

С версии: base-4.10.0.0

type family CmpNat (m :: Nat) (n :: Nat) :: Ordering Source

Сравнение натуральных чисел на уровне типов, как функция.

С версии: base-4.7.0.0

type family CmpSymbol (m :: Symbol) (n :: Symbol) :: Ordering Source

Сравнение символов на уровне типов, как функция.

С версии: base-4.7.0.0

Пользовательские ошибки типов

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

Эквивалент error на уровне типов.

Полиморфный тип позволяет использовать его в различных сценариях. Например, он может быть использован как ограничение, например, для предоставления лучшего сообщения об ошибке для отсутствующего экземпляра.

-- in a context
instance TypeError (Text "Cannot Show functions." :$$:
                    Text "Perhaps there is a missing argument?")
      => Show (a -> b) where
    showsPrec = error "unreachable"

Его также можно разместить в правой части функции на уровне типов, чтобы получить ошибку для недопустимого случая.

type family ByteSize x where
   ByteSize Word16   = 2
   ByteSize Word8    = 1
   ByteSize a        = TypeError (Text "The type " :<>: ShowType a :<>:
                                  Text " is not exportable.")

С версии: base-4.9.0.0

data ErrorMessage Source

Описание пользовательской ошибки типа.