Is spoon unsafe in Haskell?
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; eg using undefined the way Java programmers use null )
You can't write unsafeCoerce with spoon , if that's what you're getting at. It is precisely as unsound as it looks, and violates Haskell semantics precisely as much as it appears to. However, you can't use it to create a segfault or anything of the like.
However, by violating Haskell semantics, it does make code harder to reason about in general, and also, eg a safeHead with spoon is necessarily going to be less efficient than a safeHead written directly.
下一篇: 在哈斯克尔勺不安全？