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

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

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? И как получилось, что средство проверки типов принимает первую реализацию и отклоняет вторую?