Как могут работать конечные числа? (зависимые типы)

Question

Я интересуюсь зависимыми языками. Конечные числа кажутся мне полезными. Например, чтобы безопасно индексировать массивы фиксированного размера. Но определение для меня не ясное.

Тип данных для конечных чисел в Идриса могут быть следующие: (И, наверное, похож на Agda)

data FiniteNum : Natural -> Type where 
    FZero : FiniteNum (Succ k) 
    FSucc : FiniteNum k -> FiniteNum (Succ k) 

И это, кажется, работает:

exampleFN : FiniteNum (Succ (Succ Zero)) 
exampleFN = FSucc FZero -- typechecks 
-- exampleFN = FSucc (FSucc FZero) -- won't typecheck 

Но как это работает? Что означает k? И как получилось, что контролер типа принимает первую реализацию и отклоняет вторую?

Answer 1

Подумайте об индексе как верхняя граница для любого числа, которое может быть представлено Fin n. Например, Fin 4 содержит все натуральные числа менее 4. Вот заявление данных:

data Fin : ℕ → Set where 

Как это определение относится к этому вопросу? Определение натуральных чисел состоит из двух частей: zero и suc; для Fin, мы назовем их fzero и fsuc.

С нашей интерпретацией верхней границы fzero можно получить любую верхнюю границу, если она не zero (0 ≮ 0). Как мы представляем, что граница может быть чем-то отличным от zero? Мы можем заставить что просто применив suc:

fzero : {k : ℕ} → Fin (suc k) 

Это дает нам именно то, что нам нужно: никто не может написать fzero таким образом, что его тип Fin 0.

В настоящее время fsuc case: у нас есть номер с верхней границей k, и мы хотим создать преемника. Что мы можем сказать о верхней границе? Это, безусловно, возрастает, по крайней мере, одно:

fsuc : {k : ℕ} → Fin k → Fin (suc k) 

В качестве упражнения, убедить себя, что все числа меньше n могут быть представлены Fin n (только один из возможных способов).

---

Как проверка типа принимает одно и отклоняет другое? В этом случае это простое объединение. Давайте посмотрим на этот код:

test : Fin (suc (suc zero)) 
test = ? 

Когда мы пишем fsuc, Agda должен выяснить значение k. Для этого нужно посмотреть на конструктор fsuc: он строит значение типа Fin (suc k) и нам нужно suc k = suc (suc zero); объединив эти два, получим, что k = suc zero.Так следующий:

test = fsuc ? 

Теперь выражение, следующее fsuc (в лице ?, отверстие) имеет тип Fin (suc zero) (так k = suc zero). Когда мы заполняем fzero, Agda пытается объединить suc zero с suc k₂, что, конечно же, успешно с решением k₂ = zero.

Если мы решили бросить в другой fsuc:

test = fsuc (fsuc ?) 

Затем с помощью того же объединения, как и выше, мы получаем, что тип отверстия должен быть Fin zero. Пока этот тип отлично проверяется. Тем не менее, когда вы пытаетесь набить fzero, Agda должна объединить zero с suc k₃ - независимо от того, что значение k₃, suc чего-то никогда не может быть zero, так что сбой и вы получите ошибку типа.

---

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

open import Data.Product 

Fin' : ℕ → Set 
Fin' n = Σ ℕ (λ k → k < n) 

оригинальный Fin можно рассматривать как вариант Fin' где доказательство запеченный непосредственно в конструкторах.

Answer 2

Короткий ответ заключается в том, что тип нулевого типа FiniteNum пуст, поскольку оба конструктора возвращают FiniteNum, индексированный с ненулевым натуральным числом. Теперь попробуйте ответить на следующее: сколько элементов имеет FiniteNum (Succ Zero)? Как они выглядят? Повторите для 2,3,4 ...