Is spoon unsafe in Haskell?

Question

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?

Answer 1

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)

Answer 2

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, e.g. a safeHead with spoon is necessarily going to be less efficient than a safeHead written directly.