有限的数字如何运作？ （依赖类型）

我对依赖类型语言感兴趣。有限数对我来说似乎非常有用。例如，安全地索引固定大小的数组。但这个定义对我来说并不清楚。

Idris 中有限数的数据类型可以如下：（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 是什么意思？为什么类型检查器接受第一个实现并拒绝第二个实现？

将索引视为上限对于任何可以表示为的数字Fin n。例如，Fin 4包含所有小于的自然数4。这是一个数据声明：

data Fin : ℕ → Set where

这个定义与此有何关系？自然数的定义有两部分：zero and suc; for Fin，我们称之为fzero and fsuc.

根据我们的上限解释，fzero可以给定任何上限，只要它不是zero（0≮0）。我们如何表示边界可以是除zero？我们可以简单地通过应用来强制执行suc:

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

这正是我们所需要的：没有人可以写fzero其类型为Fin 0.

Now the fsuc情况：我们有一个有上限的数字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（代表为?, a hole) 有一个类型Fin (suc zero) (since k = suc zero）。当我们填写fzero，Agda试图统一suc zero with suc k₂，当然解决方案会成功k₂ = zero.

如果我们决定再投入一个fsuc:

test = fsuc (fsuc ?)

然后使用与上面相同的统一，我们得到孔的类型必须是Fin zero。到目前为止，这种类型检查得很好。然而，当你尝试填充时fzero在那里，Agda 必须统一zero with suc k₃- 无论其价值k₃, suc某事永远不可能zero，因此失败并出现类型错误。

有限数的另一种表示形式（可以说不太好用）是一对自然数和它小于界限的证明。

open import Data.Product

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

原本的Fin可以被认为是一个版本Fin'证明被直接烘焙到构造函数中。