8

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

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

4

2 回答 2

11
于 2013-09-11T02:24:45.640 回答
1

简短的回答是 FiniteNum Zero 类型为空，因为两个构造函数都返回 FiniteNum 索引为非零自然数。现在尝试回答以下问题：FiniteNum（Succ Zero）有多少个元素？他们看起来怎么样？重复 2,3,4...

于 2013-09-10T19:30:50.843 回答