为什么Idris中的Nat数据类型以0开头而不是1?

我看到它有两种定义方式,但我们更喜欢在Idris中从零开始的一个原因是,它对于描述其他结构的大小很有用,例如列表或树。列表中可以有零个内容,树的高度可以为零,附加两个零长度列表会导致一个零长度的列表。

在零没有意义的情况下,可以定义数据类型,使其不可能将零作为索引。这里有一个(人为的和未经测试的)示例,其中零没有意义,树由元素数量索引,元素存储在叶子上:

data Tree : Nat -> Type -> Type where
     Leaf : ty -> Tree 1 ty
     Node : Tree n ty -> Tree m ty -> Tree (n + m) ty

考虑到这些构造函数,您将永远无法生成 Tree 0 Int 但你可以做一个 Tree 1 Int 或 Tree 2 Int 或 Tree n Int 对于任何 n > 0

test1 : Tree 1 Int
test1 = Leaf 94

test2 : Tree 2 Int
test2 = Node test1 test1

test3 : Tree 3 Int
test3 = Node test1 test2

test0 : Tree 0 Int
test0 = ?no_chance