Haskell Data.Void: undefined turns into infinite loop

Question

I noticed one thing about the Void type in the haskell Data.Void module, which is weird and I'd very much like to know why it is the way it is. Undefined is supposed to be a value that exists for every type (in my understanding), and

undefined :: Type

is supposed to yield

*** Exception: Prelude.undefined

which works for every data type I have tried, except for Void. undefined :: Void does not terminate at all, same for absurd undefined. Now I don't think that's really much of an issue since Void represents a value that is not going to happen anyway, but I would still like to know what causes this behavior.

Answer 1

After a bit more investigation, I think I understand how this can happen, and how it depends on optimization choices by GHC. In void-0.7, we have the following relevant definitions:

newtype Void = Void Void

absurd :: Void -> a
absurd a = a `seq` spin a where
   spin (Void b) = spin b

instance Show Void where
  showsPrec _ = absurd

Note that the Show instance delegates to absurd, which explains why undefined :: Void in GHCi gives the same result as absurd undefined.

Now looking at the definition of absurd a, it uses seq to "ensure" that a is actually evaluated, so you would think that should trigger the undefined exception. However, subtly seq doesn't actually work that way. a `seq` b only guarantees that both a and b will be evaluated before the whole expression returns, but not in which order. It is entirely up to the choice of the implementation which part is evaluated first.

This means that GHC is free to either evaluate the a first, triggering the exception; or else to evaluate spin a first. If it evaluates spin a first, then you get an infinite loop, because the Void constructor is a newtype constructor, and by design, unwrapping those doesn't actually evaluate anything.

So therefore, by the semantics of seq, both options are actually equally legal Haskell behavior.

As a final note, the exception semantics in GHC have been defined as explicitly nondeterministic: If an expression could give bottom in several different ways, GHC can choose any of them. Since the only way to distinguish different bottoms is in IO, this is considered acceptable.