为什么不是 (20 >) 。长度。取 10 === const True答案

【问题标题】：Why isn't (20 >) . length . take 10 === const True为什么不是 (20 >) 。长度。取 10 === const True
【发布时间】：2022-07-08 03:14:50
【问题描述】：

tl;博士

20 < length $ take 10 $ whatever 需要whatever 才能成功地对列表（至少是[] 或(_:_)）进行模式修补，这难道不是“缺乏”懒惰吗？

或者，换句话说，为什么不是(20 >) . length . take 10 === const True，所以将它们中的任何一个应用于任何东西都不需要对参数进行任何评估？

(20 >) . length . take 10 !== const True 是必需品吗？还是设计选择？无论哪种情况，为什么？

前言

这是对my previous question的跟进。

在那里我问为什么@987654322@ error 会反复无限地打印*** Exception: 。

答案令人满意。

我的运气

但是，我玩了一下ghci，发现take 0 $ fix error 预期会返回""，而length $ take 0 $ fix error 会返回0。

另一方面，以下打印*** Exception: 无限流：

20 > (length $ take 10 $ fix error)

我了解如果甚至计算了 fix error 的一个元素（实际上是尝试），结果就是这样，但我的问题是：为什么首先需要对它们中的任何一个进行评估，在那个特定的表达式中？毕竟，length $ take 10 $ whatever 不能是 <= 10，因此是 < 20，所以表达式的计算结果应该是 True。

实际上，我看到20 > (length $ take 10 $ [fix error]) 立即返回True。可能整点是take 10 期望在[a] 上工作，所以length $ take 10 $ [fix error] 不需要评估fix error 以确保它在[a] 上工作。事实上，我也验证了 20 > (length $ take 10 $ undefined) 错误（即使没有无限重复错误），而 20 > (length $ take 10 $ [undefined]) 返回 True。

也许这就是Willem Van Onsem meant in this comment。

不管怎样，因为我可以把上面的表达式写成

((20 >) . length . take 10) $ fix error

我很想说

(20 >) . length . take 10 === const True

因此我会说((20 >) . length . take 10) $ fix error 返回True 是合理的，就像const True $ fix error 返回True。

但事实并非如此。为什么？

【问题讨论】：

您是在问为什么要观察自己在 Haskell 中所做的事情，还是在问如果我们从头开始设计一种新的类似 Haskell 的语言，原则上会存在什么行为？
@DanielWagner 后者。
好的。假设我们已经制定了一个对程序含义足够灵活的假设规范，允许编译器执行重写 length (take 10 x) < 20 -> True 如果它可以发现它。为了使编译器能够发现和执行重写，您的实施计划是什么？
目标是符号计算还是证明某些程序的属性？如果是这样，那么在某些范式中，声明 (20 >) . length . take 10 === const True 是可证明的和机器可验证的（例如 Agda、Coq）。还是您希望编译器为您“修复”某些类型的程序？如果是这样，那么对您的问题的真正无聊的答案是：它以这种方式工作，因为该语言为程序分配了一致且可预测的操作语义，并且这种具有take 10 undefined = undefined 的操作语义的选择还允许使用真实世界的广泛类程序使用。
... 然而，在今天的 Haskell 中，您可以使用名称 length 和 take 定义不同的符号，这样 length . take 10 $ [1,2, ...] 计算为 10 和 @987654368 并不是不可想象的@ 计算为 True。但是没有规范或通用的方法可以做到这一点。如何定义这些符号完全取决于你想要完成什么。

标签： haskell functional-programming pattern-matching lazy-evaluation

【解决方案1】：

take 10 必须确定其参数是 [] 还是 (:) 值。

const True 没有。

length 是严格的，因为它必须遍历其整个参数。组合并不意味着它只需要迭代足够多的值以获得足够大的数字来伪造(20 >)。

【讨论】：

因此这两个函数在表示上是不同的。通常，在程序员背后执行程序修改以改变程序的含义并不是一个好主意，即使您所做的只是使程序更加明确。

【解决方案2】：

毕竟，长度 $ 取 10 $ 不能是

在 Haskell 中不正确。长度函数通常可能会崩溃或进入无限循环。在这两种情况下，它都不会给出有效整数作为结果，并且无法将缺少有效整数与 10 进行比较。通常，评估任意表达式可能会产生一个值，例如 (1::Int) 或 @987654321 @。其中bottom概括了表达式可能不会产生值的所有原因。

表达式20 < length $ take 10 $ whatever，因此必须计算为True 或底部，对于编译器False 甚至是一个选项。正如您所见，True 和 bottom 都是有效结果。相比之下，const True whatever 则不同，因为它总是在 True 中求值而不求 whatever。

【讨论】：

【解决方案3】：

您看到的行为更多地与 length 和 > 相关，而不是与 take 相关。 length 必须返回一个特定数字，而(20 >) 只能在提供特定数字时运行。您认为流水线中正在处理的数字是多少？

您承认length $ take 10 $ fix error 是（并且应该是）底部。在遇到错误之前，列表fix error 中甚至没有一个元素可以查看，因此没有可以返回的数字可以准确测量列表的长度。（可能很容易说它的长度可能为零，因为那里没有任何元素，但这意味着fix error 等于[]，这也不是真的。真正要求它的长度很简单一个错误。）

但是，您现在希望将该底部值输入(20 >) 并期望得到结果True。但是底部是可以互换的，所以这需要20 > undefined 也是True。事实上，它需要length $ take 50 $ fix error 也是True。

您的直觉似乎是 length . take 10 无法返回大于 10 的值，因此 (20 >) . length . take 10 应该是 const True，因此不需要检查其输入。您显然已经注意到这对于当前的 Haskell 来说是不准确的，但我认为这无论如何都不是可取的行为。我的直觉是(20 >) 需要一个小于20 的特定输入数字才能返回True；一个模糊的概念认为它的输入不能是一个更大的数字是不够的。如果它的输入是错误（任何错误），那么True 和False 都不是准确的返回值。

请注意，length $ take 0 $ fix error 是一个非常不同的情况。 take 的定义等价于：

take n _
  | n <= 0  = []
take _ [] = []
take n (x:xs) = x : take (n - 1) xs

它检查要获取的元素的数量是否为零（或更少）在它检查任何列表，如果是，它可以返回一个特定的具体列表[]而不检查输入列表（因此不会从fix error 或undefined 触发任何错误）。那么length可以测量[]并返回0，小于20。

同样，length $ take 10 $ [fix error] 有效，因为take 10 可以返回长度为 1 的列表，而无需检查列表内部的任何元素（并且该位会触发错误），而 length 可以测量该列表并返回1，它小于20。

这两种情况实际上都不需要任何未定义的属性的特定值，但您的原始情况需要（错误的length）。这与“确保我们正在处理[a]”无关，只是您的答案是否取决于未定义的值。

【讨论】：