npo*_*cop 4 haskell types language-design turing-complete
在System FI中,可以使用Church数字定义真正的总加法函数.
在Haskell中,由于底值,我无法定义该函数.例如,在haskell中,如果x + y = x,那么我不能说y为零 - 如果x是底部,x + y = x表示任何y.因此,加法不是真正的加法,而是对它的近似.
在CI中无法定义该函数,因为C规范要求所有内容都具有有限的大小.所以在C中,可能的近似值甚至比Haskell更差.
所以我们有:
在系统F中,可以定义添加,但不可能有完整的实现(因为没有无限的硬件).
在Haskell中,不可能定义添加(因为底部),并且不可能有完整的实现.
在C中,不可能定义总加法函数(因为所有内容的语义都是有界的),但是可以实现兼容的实现.
因此,所有3个正式系统(Haskell,System F和C)似乎都有不同的设计权衡.
那么选择一个而不是另一个的后果是什么？
哈斯克尔
这是一个奇怪的问题,因为你正在处理一个模糊的概念=.在域语义级别_|_ = _|_只能"保持"(甚至那时你应该真正使用?).如果我们区分域语义级别的可用信息和语言本身的相等性,那么说True ? x + y == x- > 是完全正确的True ? y == 0.
这不是问题的补充,也不是自然数也是问题 - 问题只是区分语言中的相等性和语言语义中的相等或语句信息.如果没有底部问题,我们通常可以使用天真的等式逻辑推理Haskell.对于底部,我们仍然可以使用等式推理 - 我们只需要使用我们的方程更复杂.
通过优秀论文" 快速宽松的推理在道德上正确 "中,可以更全面,更清晰地阐述总语言与提升语言所定义的部分语言之间的关系.
C
你声称C要求所有东西(包括可寻址空间)具有有限的大小,因此C语义"对可表示的自然的大小施加限制".并不是的.的C99标准说以下内容:".任何指针类型可被转换为整数型除先前SPECI音响ED,结果是实施德音响定义如果结果不能在整数类型来表示,则该行为定义的结果需要理解过程网络连接.不在任何整数类型的值范围内." 理论文档进一步强调"C已经在各种体系结构上实现.虽然这些体系结构中的一些具有统一指针,这些指针是某种整数类型的大小,但是最大可移植代码不能假设不同指针类型之间的任何必要的对应关系.整数类型.在某些实现中,指针甚至可以比任何整数类型都宽."
正如您所看到的,显然没有假设指针必须是有限大小的.