haskell - Haskell中整数的非整数居民

Question

Haskell 中定义的 Peano 自然数data Peano = Zero | Succ Peano是非常奇怪的野兽：除了普通的自然数和底值之外，其中还有一个“无限整数” inf = Succ inf。

有没有其他这种Peano类型的居民？这个无限数有名字吗？

Answer 1

它们并不奇怪，它们只是简单的自然叠加。撇开 ⊥ 的问题不谈，我们可以在这里定义自然数类型为由 或 组成Zero，或Succ应用于自然数。归纳定义将假定一个明确定义的结束，即任何数字都从Zero构造函数开始。协约定义只是说给定任何自然数，它要么是，Zero要么我们可以删除外部Succ以获得另一个自然数。

看似细微的区别在于，共归纳定义包括无穷无尽的Succ构造函数系列，这确实是无穷大的真实表示。这是有意义的，因为虽然归纳定义是关于确保递归将达到一个明确定义的基本情况，但归纳定义是关于确保始终有一个明确定义的下一步可用。

由于数据构造函数是懒惰的，所以在 Haskell 中，协约解释很方便，并且在某些方面是强制性的。

因此，正如 Daniel Fischer 所说，这个无限数确实是无穷大，或者如果您需要指定哪个无穷大，则为 ω。它只是一个共归纳无穷，很像更常见的无穷列表。

如果您通过其教堂编码来考虑自然数，则有限数意味着“将此函数迭代 N 次”；ω 的意思是“无限期地迭代这个函数”。

Answer 2

嗯，有Succ _|_，Succ (Succ _|_)等等。不过，您可能已经将这些包含在“底部值”中。inf = Succ inf通常称为infinity或omega（作为自然数的序数）。