GHC.TypeNats

Safe Haskell	Safe
Language	Haskell2010

Тип Nat

data Natural

type Nat = Natural Source

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

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

С момента: base-4.16.0.0

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

class KnownNat (n :: Nat) where Source

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

С момента: base-4.7.0.0

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

С момента: base-4.10.0.0

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

С момента: base-4.10.0.0

data SomeNat Source

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

С момента: base-4.10.0.0

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

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

С момента: base-4.10.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

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

Значения-синглетоны

data SNat (n :: Nat) Source

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

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

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

Since: base-4.18.0.0

pattern SNat :: () => KnownNat n => SNat n Source

Явно двунаправленный синоним шаблона, связывающий 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 -}

Since: base-4.18.0.0

fromSNat :: forall (n :: Nat). SNat n -> Natural Source

Возвращает число, соответствующее n, в значении SNat n.

С момента: base-4.18.0.0

withSomeSNat :: Natural -> (forall (n :: Nat). SNat n -> r) -> r Source

Преобразует число Natural в значение SNat n, где n - это свежее натуральное число на уровне типов.

С момента: base-4.18.0.0

withKnownNat :: forall (n :: Nat) r. SNat n -> (KnownNat n => r) -> r Source

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

С момента: base-4.18.0.0

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

type (<=) (x :: t) (y :: t) = Assert (x <=? y) (LeErrMsg x y :: Constraint) infix 4 Source

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

С момента: base-4.16.0.0

type (<=?) (m :: k) (n :: k) = OrdCond (Compare m n) 'True 'True 'False infix 4 Source

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

С момента: base-4.16.0.0

type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 Source

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

С момента: base-4.7.0.0

type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 Source

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

С момента: base-4.7.0.0

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

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

С момента: base-4.7.0.0

type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 Source

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

С момента: base-4.7.0.0

type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Source

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

С момента: base-4.7.0.0

cmpNat :: forall (a :: Nat) (b :: Nat) proxy1 proxy2. (KnownNat a, KnownNat b) => proxy1 a -> proxy2 b -> OrderingI a b Source

Аналогично sameNat, но если числа не равны, дополнительно предоставляет доказательство LT или GT.

С момента: base-4.16.0.0

type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 Source

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

С момента: base-4.11.0.0

type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 Source

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

С момента: base-4.11.0.0

type family Log2 (a :: Natural) :: Natural where ... Source

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

С момента: base-4.11.0.0