在哈斯克尔勺不安全？ [英] Is spoon unsafe in Haskell?

问题描述

因此，Haskell中有一个库叫做勺子，它可以让我做到这一点。

  safeHead :: [a]  - >也许是
 safeHead =汤匙。头部
  

但它也让我做到这一点

 >>>勺True：可能Bool 
只是真
>>>勺（错误叉）::也许Bool 
没有
>>>勺子undefined ::也许布尔
没有
>>>勺（让x = x in x）::可能Bool 
 <...让我们继续等待...> 
  

这在某些情况下似乎非常有用，但它也违反指称语义（据我的理解），因为它让我在⊥的语义原像中区分不同的事物。这比 throw / catch 强大得多，因为它们可能具有由continuations定义的语义。

 >>>尝试使用$ return（errorthimble）:: IO（SomeException Bool）
 Right ***异常：顶针
  

所以我的问题是：有人可以使用勺子恶意破坏类型安全吗？便利是否值得冒险？或者，更现实的说，是否有一种合理的方式，使用它可能侵蚀别人对程序意义的信心？

是一个棘手的问题，如果使用它，做一个看起来像无辜的重构可以改变程序的行为。没有任何花里胡哨的事情，它是这样的：

  fhx = hx 
 isJust（spoon（f undefined）） -  - >真正的
  

但可能是本书中最常见的haskell转换，即eta收缩，为<$ c $给出

  fh = h 
 isJust（spoon（f undefined） ） - > False 
  

由于存在 seq ;但没有匙eta收缩只能将终止程序更改为错误;用勺子收缩可以将终止程序变成不同的终止程序。

$ b 形式上， spoon 不安全的方式是域名上的非单调性（因此可以用它来定义函数）;而没有勺子，每个函数都是单调的。所以在技术上你失去了正式推理的有用属性。

作为一个现实生活中的例子， （阅读：我认为现实生活中不太可能重要 - 除非开始滥用它;例如使用未定义 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)

这篇关于在哈斯克尔勺不安全？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！