GHC.TypeLits

Безопасный Haskell	Safe
Язык	Haskell2010

Виды

data Natural Источник

Натуральное число

Инвариант: числа <= 0xffffffffffffffff используют конструктор NS

type Nat = Natural Источник

Синоним типа для Natural.

Ранее это был непрозрачный тип данных, но его заменили синонимом типа.

Начиная с: base-4.16.0.0

data Symbol Источник

(Род) Это род символов на уровне типов.

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

class KnownNat (n :: Nat) where Источник

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

Начиная с: base-4.7.0.0

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Integer Источник

Начиная с: base-4.7.0.0

natVal' :: forall (n :: Nat). KnownNat n => Proxy# n -> Integer Источник

Начиная с: base-4.8.0.0

class KnownSymbol (n :: Symbol) where Источник

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

Начиная с: base-4.7.0.0

symbolVal :: forall (n :: Symbol) proxy. KnownSymbol n => proxy n -> String Источник

Начиная с: base-4.7.0.0

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

Начиная с: base-4.8.0.0

class KnownChar (n :: Char) where Исходный код

Начиная с: base-4.16.0.0

charVal :: forall (n :: Char) proxy. KnownChar n => proxy n -> Char Исходный код

charVal' :: forall (n :: Char). KnownChar n => Proxy# n -> Char Исходный код

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

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

Начиная с: base-4.10.0.0

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

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

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

someNatVal :: Integer -> Maybe SomeNat Исходный код

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

Начиная с: base-4.7.0.0

someSymbolVal :: String -> SomeSymbol Исходный код

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

Начиная с: base-4.7.0.0

someCharVal :: Char -> SomeChar Исходный код

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

Начиная с: base-4.16.0.0

sameNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) Исходный код

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

Начиная с: base-4.7.0.0

sameSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) Исходный код

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

Начиная с: base-4.7.0.0

sameChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Maybe (a :~: b) Исходный код

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

Начиная с: base-4.16.0.0

decideNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Исходный код

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

Начиная с: base-4.19.0.0

decideSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Исходный код

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

Начиная с: base-4.19.0.0

decideChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> Either ((a :~: b) -> Void) (a :~: b) Исходный код

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

Начиная с: base-4.19.0.0

data OrderingI (a :: k) (b :: k) where Исходный код

Тип данных Ordering для типовых литералов, предоставляющий доказательство их порядка.

Начиная с: base-4.16.0.0

cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b Исходный код

Подобно sameNat, но если числа не равны, функция также предоставляет доказательство LT или GT.

Начиная с: base-4.16.0.0

cmpSymbol :: forall (a :: Symbol) (b :: Symbol) proxy1 proxy2. (KnownSymbol a, KnownSymbol b) => proxy1 a -> proxy2 b -> OrderingI a b Исходный код

Подобно sameSymbol, но если символы не равны, функция также предоставляет доказательство LT или GT.

Начиная с: base-4.16.0.0

cmpChar :: forall (a :: Char) (b :: Char) proxy1 proxy2. (KnownChar a, KnownChar b) => proxy1 a -> proxy2 b -> OrderingI a b Исходный код

Подобно sameChar, но если символы Char не равны, функция также предоставляет доказательство LT или GT.

Начиная с: base-4.16.0.0

Синглетонные значения

data SNat (n :: Nat) Исходный код

Свидетельство на уровне значений для натурального числа на уровне типов. Этот тип обычно называют синглетонным, поскольку для каждого n существует единственное значение, принадлежащее типу SNat n (кроме нижнего значения).

Определение SNat намеренно оставлено абстрактным. Чтобы получить значение SNat, используйте один из следующих способов:

1. Метод natSing класса KnownNat.
2. Синоним шаблона SNat.
3. Функцию withSomeSNat, создающую SNat из числа Natural.

Начиная с: base-4.18.0.0

data SSymbol (s :: Symbol) Источник

Значение-свидетель для символа на уровне типов. Обычно такой тип называют синглтонным: для каждого s существует единственное значение, принадлежащее типу SSymbol s (за исключением bottom).

Определение SSymbol намеренно оставлено абстрактным. Чтобы получить значение SSymbol, используйте один из следующих вариантов:

1. Метод symbolSing класса KnownSymbol.
2. Синоним шаблона SSymbol.
3. Функцию withSomeSSymbol, которая создаёт SSymbol из String.

Начиная с: base-4.18.0.0

data SChar (s :: Char) Источник

Значение-свидетель для символа на уровне типов. Обычно такой тип называют синглтонным: для каждого c существует единственное значение, принадлежащее типу SChar c (за исключением bottom).

Определение SChar намеренно оставлено абстрактным. Чтобы получить значение SChar, используйте один из следующих вариантов:

1. Метод charSing класса KnownChar.
2. Синоним шаблона SChar.
3. Функцию withSomeSChar, которая создаёт SChar из Char.

Начиная с: base-4.18.0.0

pattern SNat :: () => KnownNat n => SNat n Источник

Явный двунаправленный синоним шаблона, связывающий SNat с ограничением KnownNat.

Как выражение: создает явное значение SNat n из неявного ограничения KnownNat n:

SNat @n :: KnownNat n => SNat n

Как шаблон: сопоставляет явное значение SNat n, вводя неявное ограничение KnownNat n в область видимости:

f :: SNat n -> ..
f SNat = {- KnownNat n in scope -}

Начиная с: base-4.18.0.0

pattern SSymbol :: () => KnownSymbol s => SSymbol s Источник

Явный двунаправленный синоним шаблона, связывающий SSymbol с ограничением KnownSymbol.

Как выражение: создает явное значение SSymbol s из неявного ограничения KnownSymbol s:

SSymbol @s :: KnownSymbol s => SSymbol s

Как шаблон: сопоставляет явное значение SSymbol s, вводя неявное ограничение KnownSymbol s в область видимости:

f :: SSymbol s -> ..
f SSymbol = {- KnownSymbol s in scope -}

Начиная с: base-4.18.0.0

pattern SChar :: () => KnownChar c => SChar c Источник

Явный двунаправленный синоним шаблона, связывающий SChar с ограничением KnownChar.

Как выражение: создает явное значение SChar c из неявного ограничения KnownChar c:

SChar @c :: KnownChar c => SChar c

Как шаблон: сопоставляет явное значение SChar c, вводя неявное ограничение KnownChar c в область видимости:

f :: SChar c -> ..
f SChar = {- KnownChar c in scope -}

Начиная с: base-4.18.0.0

fromSNat :: forall (n :: Nat). SNat n -> Integer Источник

Возвращает Integer, соответствующее n, в виде значения SNat n. Возвращаемое Integer всегда неотрицательно.

Версию этой функции, возвращающую Natural вместо Integer, см. в fromSNat в GHC.TypeNats.

Начиная с: base-4.18.0.0

fromSSymbol :: forall (s :: Symbol). SSymbol s -> String Источник

Возвращает строку, соответствующую s, в виде значения SSymbol s.

Начиная с: base-4.18.0.0

fromSChar :: forall (c :: Char). SChar c -> Char Источник

Возвращает Char, соответствующий c, в виде значения SChar c.

Начиная с: base-4.18.0.0

withSomeSNat :: Integer -> (forall (n :: Nat). Maybe (SNat n) -> r) -> r Источник

Пытается преобразовать Integer в значение SNat n, где n — новое натуральное число на уровне типов. Если аргумент Integer неотрицателен, вызывает продолжение с Just sn, где sn — значение SNat n. Если аргумент Integer отрицателен, вызывает продолжение с Nothing.

Версию этой функции, в которой продолжение использует 'SNat n instead of Maybe (SNat n)@, см. в withSomeSNat в GHC.TypeNats.

Начиная с: base-4.18.0.0

withSomeSSymbol :: String -> (forall (s :: Symbol). SSymbol s -> r) -> r Источник

Преобразует String в значение SSymbol s, где s — новый символ на уровне типов.

Начиная с: base-4.18.0.0

withSomeSChar :: Char -> (forall (c :: Char). SChar c -> r) -> r Источник

Преобразует Char в значение SChar c, где c — новый символ на уровне типов.

Начиная с: base-4.18.0.0

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r Источник

Преобразует явное значение SNat n в неявное ограничение KnownNat n.

Начиная с: base-4.18.0.0

withKnownSymbol :: forall (s :: Symbol) r. SSymbol s -> (KnownSymbol s => r) -> r Источник

Преобразует явное значение SSymbol s в неявное ограничение KnownSymbol s.

Начиная с: base-4.18.0.0

withKnownChar :: forall (c :: Char) r. SChar c -> (KnownChar c => r) -> r Источник

Преобразует явное значение SChar c в неявное ограничение KnownChar c.

Начиная с: base-4.18.0.0

Функции для типовых литералов

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Источник

Сравнение (<=) сравнимых типов в виде ограничения.

Начиная с: base-4.16.0.0

type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 Источник

Сравнение (<=) сравнимых типов в виде функции.

Начиная с: base-4.16.0.0

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Источник

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

Начиная с: base-4.7.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Источник

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

Начиная с: base-4.7.0.0

type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 Источник

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

Начиная с: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 Источник

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

Начиная с: base-4.7.0.0

type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 Источник

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

Начиная с: base-4.11.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 Источник

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

Начиная с: base-4.11.0.0

type family Log2 (a :: Natural) :: Natural where ... Источник

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

Начиная с: base-4.11.0.0

type family AppendSymbol (a :: Symbol) (b :: Symbol) :: Symbol where ... Источник

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

Начиная с: base-4.10.0.0

type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Источник

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

Начиная с: base-4.7.0.0

type family CmpSymbol (a :: Symbol) (b :: Symbol) :: Ordering where ... Источник

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

Начиная с: base-4.7.0.0

type family CmpChar (a :: Char) (b :: Char) :: Ordering where ... Источник

Сравнение символов на уровне типов.

Начиная с: base-4.16.0.0

type family ConsSymbol (a :: Char) (b :: Symbol) :: Symbol where ... Источник

Добавление символа на уровне типов в начало символа на уровне типов

Начиная с: base-4.16.0.0

type family UnconsSymbol (a :: Symbol) :: Maybe (Char, Symbol) where ... Источник

Это семейство типов возвращает значение Just на уровне типов, содержащее первый символ символа и его хвост, если оно определено, и Nothing в противном случае.

Начиная с: base-4.16.0.0

type family CharToNat (a :: Char) :: Natural where ... Источник

Преобразует символ в его кодовую точку Unicode (ср. ord)

Начиная с: base-4.16.0.0

type family NatToChar (a :: Natural) :: Char where ... Источник

Преобразует кодовую точку Unicode в символ (ср. chr)

Начиная с: base-4.16.0.0

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

type family TypeError (a :: ErrorMessage) :: b where ... Источник

Эквивалент 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 Источник

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