共有Idris新手问题，对不起。
我在学校曾教过自然数（N）和零自然数（N0）。
在Idris中，存在数据类型Nat，其定义与N0相对应。
如果将Nat定义如下，将会发生什么变化：
data Nat = One | S Nat
data Nat0 = Zero | Nat
我想现在比较容易，但是主要是编译器实现问题还是正式的问题？
在某些情况下，0毫无意义，我想现在更难于正确定义。
或不？
我已经看到它定义了两种方式，但是在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
本文收集自互联网，转载请注明来源。
如有侵权，请联系 [email protected] 删除。
我来说两句