Haskell中的勺子不安全吗？答案

【问题标题】：Is spoon unsafe in Haskell?Haskell中的勺子不安全吗？
【发布时间】：2013-02-05 15:24:19
【问题描述】：

所以在 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

所以我的问题是：有人可以恶意使用勺子来破坏类型安全吗？便利值得冒险吗？或者，更现实地说，是否有合理的方式使用它会削弱人们对程序含义的信心？

【问题讨论】：

你说什么危险？一个纯粹主义者可能会因恐惧而退缩？
@RobertHarvey 可能不会有任何危险，但您经常会发现违反纯度会导致对绕过模块封装的行为或技巧的错误预期。我非常乐意在实际代码中使用 spoon（我已经这样做了），但我今天注意到它违反了 Haskell 语义。
你真的能这样区分undefined和(let x = x in x)吗？如果您等待的时间足够长，也许后者确实会返回 Nothing。
@SjoerdVisscher：我查过了，没有。
注意：如果你喜欢使用像 Maybe a 这样的返回类型而不是部分函数，safe package 可能更适合你。

标签： haskell

【解决方案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，每个功能都是单调的。所以技术上你失去了形式推理的有用属性。

想出一个现实生活中的例子，说明何时这很重要，留给读者作为练习（阅读：我认为这在现实生活中不太重要——除非你开始滥用它；例如使用 undefined 就像 Java 程序员使用 null)

【讨论】：

这更多是我想要的。我没有将它与非单调性属性联系起来——它有点暗示使用它的部分原则应该是始终将Nothing 响应视为子系统故障的种类。

【解决方案2】：

你不能用spoon 写unsafeCoerce，如果那是你的意思。它就像它看起来一样不健全，并且与它看起来一样违反了 Haskell 语义。但是，您不能使用它来创建段错误或类似的东西。

但是，通过违反 Haskell 语义，它确实使代码更难推理，而且，例如带勺子的safeHead 的效率必然低于直接编写的safeHead。

【讨论】：

是的，知道没有办法写unsafeCoerce 很好，虽然不是那么令人担忧。我更想知道是否有办法通过它违反模块边界等。可能会出现并被误解的东西，而不是故意的恶意代码......虽然我确实在问题中写了这个，有点开玩笑。