haskell - 勺子在 Haskell 中不安全吗？

Question

Haskell 中有一个名为 spoon 的库这让我可以做到这一点

safeHead :: [a] -> Maybe a
safeHead = spoon . head

但它也让我可以这样做

>>> spoon True             :: Maybe Bool
Just True
>>> spoon (error "fork")   :: Maybe Bool
Nothing
>>> spoon undefined        :: Maybe Bool
Nothing
>>> spoon (let x = x in x) :: Maybe Bool
<... let's just keep waiting...>

这在某些情况下似乎非常有用，但它也违反了指称语义(据我的理解)，因为它让我区分 ⊥ 语义原像中的不同事物。这比 throw/catch 严格来说更强大，因为它们可能具有由延续定义的语义。

>>> try $ return (error "thimble") :: IO (Either SomeException Bool)
Right *** Exception: thimble

所以我的问题是:有人可以恶意使用 Spoon 来破坏类型安全吗？为了方便值得冒危险吗？或者，更现实地说，是否有一种合理的方式可以使用它来削弱某人对程序含义的信心？

Answer 1

有一个棘手的问题，如果您使用它，做一些看似无害的重构可能会改变程序的行为。没有任何花哨的东西，就是这样的:

f h x = h x
isJust (spoon (f undefined)) --> True

但是，将书中最常见的 Haskell 变换(eta 收缩)转换为 f，得到

f h = h
isJust (spoon (f undefined)) --> False

由于seq的存在，Eta收缩已经不保留语义；但如果没有 Spoon eta 收缩，只能将终止程序变成错误；使用 Spoon eta 收缩可以将终止程序更改为不同的终止程序。

正式来说，spoon 不安全的原因是它是 non-monotone on domains (因此可以用它来定义函数)；而如果没有spoon，每个功能都是单调的。因此，从技术上讲，你失去了形式推理的有用属性。

举一个现实生活中的例子来说明何时这很重要，作为读者的练习(阅读:我认为这在现实生活中不太可能重要 - 除非你开始滥用它；例如，像 Java 程序员使用 null 一样使用 undefined)