haskell - 交换函数的意外性质？

Question

我得出了一个令我困惑的陈述(定理？)。我想知道我的逻辑是否合理。

Any commutative non-strict function f :: a -> a -> b is a constant.

交换性被理解为包括底部，即 f x y和 f y x要么都终止，要么都没有。
我的非正式推理如下。假设 f是一个非严格函数。那么存在 a使得 f a ⊥或 f ⊥ a终止。如 f是可交换的，那么两者都应该终止。但随后 f不能仔细审查它的任何一个论点。 (如果它首先检查第一个参数，那么 f ⊥ a 必须是 ⊥ ，反之亦然)。所以它必须是一个常数函数。
这个推理正确吗？
如果 f 显然会失败允许同时检查两个参数，如果其中一个不是 ⊥ 则成功。 .但是在(一些相当保守的扩展)Haskell 中允许这样的函数吗？

Answer 1

志写

One could argue that

f :: Int -> Int -> [Int]
f x y = [x+y]

is commutative, non-strict, and non-constant. This relies on [ _|_ ] being distinct from _|_. If you for some reason consider this to be strict, you should more precisely define your strictness notion.

确实，是这样的!给定任何非常量的交换函数 f ，您可以通过包装 f 的应用程序来编写一个非严格的、非常量的、可交换的函数。在一个或多个惰性构造函数中。