37
4

2 回答 2

37

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)

于 2013-02-05T22:41:37.637 回答
13

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.

于 2013-02-05T16:00:41.183 回答