dependent-type - 为什么 Idris 中的 Nat 数据类型以 0 而不是 1 开头？

Question

总 Idris 新手问题，抱歉。

我在学校里被教导有自然数(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