有限数字如何工作？(依赖类型)

Question

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

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是什么意思？为什么类型检查器接受第一个实现并拒绝第二个？

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情况是:我们有一个上限的数字,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,阿格达试图统一suc zero使用suc k?,这当然与解决方案成功k? = zero.

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

test = fsuc (fsuc ?)

然后使用与上面相同的统一,我们得到孔的类型必须Fin zero.到目前为止,这种类型检查很好.但是,当你尝试的东西fzero在里面,阿格达有统一zero与suc k?-的,不管价值k?,suc东西绝不可能zero,所以失败,你会得到一个类型的错误.

有限数的另一种表示(可以说是不太适合使用)是一对自然数并证明它小于界限.

open import Data.Product

Fin' : ? ? Set
Fin' n = ? ? (? k ? k < n)

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