为什么Idris中的Nat数据类型从0开始而不是1？

Question

总的伊德里斯新手问题,对不起.

我在学校被教过有自然数(N)和自然数(零)(N0).
在Idris中,存在数据类型Nat,其根据定义对应于N0.

如果将Nat定义如下,会发生什么变化:

data Nat = One | S Nat
data Nat0 = Zero | Nat

我想现在更容易,但主要是编译器实现问题还是正式问题？

必须有0没有意义的情况,我想现在正确定义这些更复杂.
或不？

Answer 1

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

使用你的定义很好,只是在使用Nat谈论其他结构的属性时不必要的繁琐.

如果零没有意义,您可以定义数据类型,使其不可能将零作为索引.这是一个(设计和未经测试的)示例,其中零没有意义,树由元素数量索引,元素存储在叶子:

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