勺子在 Haskell 中不安全吗?

问题描述

Haskell 中有一个名为 spoon 的库，它让我可以这样做

safeHead :: [a] ->也许一个安全头 = 勺子.头

但它也让我这样做

>>>勺子真的 :: 也许布尔只是真的>>>勺子(错误叉子"):: 也许布尔没有什么>>>勺子未定义::也许布尔没有什么>>>勺子(让 x = x in x):: 也许布尔<...让我们继续等待...>

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

>>>try $ return (error "thimble") :: IO (Either SomeException Bool)右***例外:顶针

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

解决方案

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

f h x = h xisJust (spoon (f undefined)) -->真的

但可能是书中最常见的haskell转换，eta收缩，到f，给出

f h = hisJust (spoon (f undefined)) -->错误的

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

形式上，spoon 不安全的方式是它是 非-域上的单调(因此可以根据它定义函数)；而如果没有 spoon，每个功能都是单调的.所以技术上你失去了形式推理的有用特性.

想出一个现实生活中的例子来说明什么时候这很重要，留给读者练习(阅读:我认为这在现实生活中不太可能重要——除非你开始滥用它；例如使用 undefined Java 程序员使用 null) 的方式

So there's a library in Haskell called spoon which lets me do this

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

but it also lets me do this

>>> 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...>

which seems really useful in certain cases, but it also violates denotational semantics (to my understanding) since it lets me distinguish between different things in the semantic preimage of ⊥. This is strictly more powerful than throw/catch since they probably have a semantics defined by continuations.

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

So my question is: can someone use spoon maliciously to break type safety? Is the convenience worth the danger? Or, more realistically, is there a reasonable way that using it could erode someone's confidence in the meaning of a program?

解决方案

There is one tricky point where, if you use it, doing what seems like an innocent refactor can change the behavior of a program. Without any bells and whistles, it is this:

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

but doing perhaps the most common haskell transformation in the book, eta contraction, to f, gives

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

Eta contraction is already not semantics preserving because of the existence of seq; but without spoon eta contraction can only change a terminating program into an error; with spoon eta contraction can change a terminating program into a different terminating program.

Formally, the way spoon is unsafe is that it is non-monotone on domains (and hence so can be functions defined in terms of it); whereas without spoon every function is monotone. So technically you lose that useful property of formal reasoning.

Coming up with a real-life example of when this would be important is left as an exercise for the reader (read: I think it is very unlikely to matter in real life -- unless you start abusing it; e.g. using undefined the way Java programmers use null)

这篇关于勺子在 Haskell 中不安全吗?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！