【发布时间】:2016-07-03 03:50:22
【问题描述】:
我在搞乱fix,搞砸之后我遇到了一些奇怪的行为,即0 * undefined 是*** Exception: Prelude.undefined 和undefined * 0 是0。这也意味着fix (0 *) 是*** Exception: <<loop>> 而fix (* 0) 是0。
在玩弄它之后,似乎原因是因为让它在两个方向上都短路并不是一件容易的事,因为这并没有多大意义,没有某种奇怪的并行计算并从第一个非底部返回。
这种事情是否在其他地方看到过(反身函数对底值不反身),我可以放心地依赖它吗?还有一种实用的方法可以使 (0 *) 和 (* 0) 无论传入的值如何都计算为零。
【问题讨论】:
-
什么?太棒了!
-
这正是使得denotational semantics 不完全等同于operational semantics,即不完全抽象。前者可以用
f undefined 0 = 0和f 0 undefined = 0表示函数f,而后者不能。语言实现遵循操作语义,因此无法在没有一些技巧的情况下定义这样的f。