GHC.TypeNats

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

Тип Nat

data Nat Источник

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

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

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

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

С версии: base-4.7.0.0

natVal :: forall n proxy. KnownNat n => proxy n -> Natural Источник

С версии: base-4.10.0.0

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

С версии: base-4.10.0.0

data SomeNat Источник

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

С версии: base-4.10.0.0

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

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

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

sameNat :: (KnownNat a, KnownNat 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 Исходный код

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

type family (m :: Nat) + (n :: Nat) :: Nat infixl 6 Исходный код

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

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

type family (m :: Nat) * (n :: Nat) :: Nat infixl 7 Исходный код

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

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

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

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

Since: base-4.7.0.0

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

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

Since: base-4.7.0.0

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

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

Since: base-4.7.0.0

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

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

Since: base-4.11.0.0

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

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

Since: base-4.11.0.0

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

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

Since: base-4.11.0.0