GHC.TypeNats

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

Kind Nat

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

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

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

type Nat = Natural Исходный код

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

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

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

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

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

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

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

natVal :: forall (n :: Nat) proxy. KnownNat n => proxy n -> Natural Исходный код

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

natVal' :: forall (n :: Nat). 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 :: 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) Источник

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

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

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

Начиная с: 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

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

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

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

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

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

Начиная с: 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

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

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 CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... Источник

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

Начиная с: base-4.7.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

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