37

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?

J. Abrahamson
  • 72,246
  • 9
  • 135
  • 180
  • 4
    What danger do you speak of? That a purist might recoil at the horror? – Robert Harvey Feb 05 '13 at 15:27
  • good question, seems like this could be really useful. – Adam Gordon Bell Feb 05 '13 at 15:28
  • 9
    @RobertHarvey Might not be any danger whatsoever, but oftentimes you find that violations of purity lead to incorrect expectations about behavior or tricks to get around module encapsulation. I'd be more than happy to use `spoon` in real code (I already do) but I noticed today that it violates Haskell semantics. – J. Abrahamson Feb 05 '13 at 15:30
  • And I guess that in some sense it's actually "more pure" since it allows you to "totalify" some potentially partial code. – J. Abrahamson Feb 05 '13 at 15:33
  • 6
    Can you really distinguish `undefined` and `(let x = x in x)` this way? Perhaps the latter does return `Nothing` if you wait long enough. – Sjoerd Visscher Feb 05 '13 at 15:44
  • 8
    @SjoerdVisscher: I checked, it doesn't. – Tom Crockett Feb 05 '13 at 15:51
  • @pelotom But you can't detect that in a pure program. – Sjoerd Visscher Feb 05 '13 at 16:01
  • 2
    It's `unsafePerformIO` and `deepseq` under the hood. – AndrewC Feb 05 '13 at 16:04
  • 5
    Note: If you like using return types like `Maybe a` instead of partial functions, the [safe package](http://hackage.haskell.org/package/safe) might be more your kind of thing. – AndrewC Feb 05 '13 at 16:06
  • 3
    This library basically adds Java's `null` semantics to Haskell. We can return `undefined` to indicate "no result", with the understanding that the client will check for this condition using spoon :P – Tom Crockett Feb 05 '13 at 16:15
  • Ha, that's a good point. I suppose the "erosion of confidence" happened already in any code I'm interested in spooing. – J. Abrahamson Feb 05 '13 at 16:16
  • 2
    @SjoerdVisscher I took your initial remark as a joke in context with @pelotom's but now I think you've got a good point that I need to think about more—semantically, `spoon` is making a promise to take `_|_` to `Nothing` and it might just take an observably infinite amount of time. I think this really drives home some questions I have about denotational semantic models. Would you like to write it out as an answer to document this more? – J. Abrahamson Feb 05 '13 at 22:16
  • @tel I couldn't quite figure out the details for a proper answer. But thankfully luqui already did a great job answering this question! – Sjoerd Visscher Feb 06 '13 at 09:41

2 Answers2

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)

luqui
  • 59,485
  • 12
  • 145
  • 204
  • 3
    This is more of what I was looking for. I didn't connect it to the non-monotonicity property—it sort of implies that part of the discipline for using it should be to always consider `Nothing` responses as the kinds of subsystem failures that they are. – J. Abrahamson Feb 05 '13 at 23:05
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.

dave4420
  • 46,404
  • 6
  • 118
  • 152
sclv
  • 38,665
  • 7
  • 99
  • 204
  • 1
    Yes, knowing there's no way to write `unsafeCoerce` is good, though not so worrisome. It's more that I wanted to know if there was a way to violate module boundaries or the like through it. Something that could come up and be misconstrued accidentally less intentionally malicious code... though I did write that in the question, sort of tongue in cheek. – J. Abrahamson Feb 05 '13 at 16:10