haskell - 无法在 C 中添加自然数的后果

Question

在系统 F 中，我可以使用 Church 数字定义真正的总加法函数。

在 Haskell 中，由于底值，我无法定义该函数。例如，在haskell 中，如果x + y = x，那么我不能说y 为零-如果x 是底部，则对于任何y，x + y = x。所以加法不是真正的加法，而是它的近似。

在 C 中，我无法定义该函数，因为 C 规范要求所有内容都具有有限大小。所以在 C 中可能的近似值甚至比 Haskell 更糟糕。

所以我们有:

在 System F 中，可以定义加法，但不可能有完整的实现(因为没有无限的硬件)。

在 Haskell 中，不可能定义加法(因为底部)，并且不可能有完整的实现。

在 C 中不可能定义总加法函数(因为一切的语义都是有界的)但兼容的实现是可能的。

因此，所有 3 个正式系统(Haskell、System F 和 C)似乎都有不同的设计权衡。

那么选择一个而不是另一个的后果是什么？

Answer 1

Haskell

这是一个奇怪的问题，因为您正在使用 = 的模糊概念。 _|_ = _|_ 仅在域语义级别“保持”(即使如此，您也应该真正使用 ⊑ )。如果我们区分域语义级别的可用信息和语言本身的相等性，那么说 True ⊑ x + y == x --> True ⊑ y == 0 是完全正确的。

问题不是加法，自然数也不是问题——问题只是区分语言中的相等性和语言语义中关于相等性或信息的陈述。如果没有底部问题，​​我们通常可以使用朴素的等式逻辑来推理 Haskell。对于底部，我们仍然可以使用等式推理——我们只需要更复杂地使用我们的等式。

优秀论文“Fast and Loose Reasoning is Morally Correct”中更全面、更清晰地阐述了总语言和通过提升它们定义的部分语言之间的关系。

C

您声称 C 要求所有内容(包括可寻址空间)都具有有限大小，因此 C 语义对可表示的自然数的大小“施加了限制”。并不真地。 C99 standard 表示如下:“任何指针类型都可以转换为整数类型。除非之前指定，否则
结果是实现定义的。如果结果不能用整数类型表示，
行为未定义。结果不必在任何整数的值范围内
类型。” 基本原理文件进一步强调“C 现在已经在广泛的体系结构上实现。虽然其中一些
体系结构具有统一的指针，这些指针是某种整数类型的大小，最大
可移植代码不能假设不同指针类型和整数类型之间有任何必要的对应关系。在某些实现中，指针甚至可以比任何整数类型都宽。”

如您所见，没有明确假设指针必须具有有限大小。