Определение конечных множеств в Агда

Я новичок в Агда. Я читаю статью "Зависимые типы на работе" Ана Бове и Питера Дибьера. Я не понимаю обсуждения конечных наборов (на странице 15 в моей копии).

В документе определяется тип Fin:

data Fin : Nat -> Set where
    fzero : {n : Nat} -> Fin (succ n)
    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

Я должен упустить что-то очевидное. Я не понимаю, как это определение работает. Может ли кто-то просто перевести определение Fin в повседневный английский? Это может быть все, что мне нужно, чтобы понять эту часть статьи.

Спасибо, что нашли время, чтобы прочитать мой вопрос. Я ценю это.

Ответ 1

data Fin : Nat -> Set where

Fin - тип данных, параметризованный натуральным числом (или: Fin - это функция уровня типа, которая принимает Nat и возвращает a Set (базовый тип), то есть для любого натурального числа n Fin n является Set).

    fzero : {n : Nat} -> Fin (succ n)

Для всех натуральных чисел n fzero является членом типа /set Fin (succ n) (из которого следует, что для всех положительных чисел (т.е. всех naturals, кроме нуля) n fzero является членом Fin n).

    fsucc : {n : Nat} -> Fin n -> Fin (succ n)

Для всех натуральных чисел n и всех значений m типа Fin n, fsucc m является членом типа Fin (succ n).

Итак, fzero является членом Fin n для всех n, кроме нуля, и fsucc m является членом Fin n для всех n, которые представляют число, большее чем fsucc m.

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