How is Data.Void.absurd different from ⊥?

Question

I saw Inverse of the absurd function earlier today, and while it's clear to me that any possible implementation of drusba :: a -> Void will never terminate (after all, it's impossible to construct Void), I don't understand why the same isn't true of absurd :: Void -> a. Consider the GHC implementation:

newtype Void = Void Void

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

spin, it seems to me, is endlessly unraveling the infinite series of Void newtype wrappers, and would never return even if you could find a Void to pass it. An implementation that would be indistinguishable would be something like:

absurd :: Void -> a
absurd a = a `seq` undefined

Given that, why do we say that absurd is a proper function that deserves to live in Data.Void, but

drusba :: a -> Void
drusba = undefined

is a function that cannot possibly be defined? Is it something like the following?

absurd is a total function, giving a non-bottom result for any input in its (empty) domain, whereas drusba is partial, giving bottom results for some (indeed all) inputs in its domain.

Answer 1

For historical reasons, any Haskell data type (including newtype) must have at least one constructor.

Hence, to define the Void in "Haskell98" one needs to rely on type-level recursion newtype Void = Void Void. There is no (non-bottom) value of this type.

The absurd function has to rely on (value level) recursion to cope with the "weird" form of the Void type.

In more modern Haskell, with some GHC extensions, we can define a zero constructor data type, which would lead to a saner definition.

{-# LANGUAGE EmptyDataDecls, EmptyCase #-}
data Void
absurd :: Void -> a
absurd x = case x of { }    -- empty case

The case is exhaustive -- it does handle all the constructors of Void, all zero of them. Hence it is total.

In some other functional languages, like Agda or Coq, a variant of the case above is idiomatic when dealing with empty types like Void.

Answer 2

Data.Void moved from the void package to base in base version 4.8 (GHC 7.10). If you look at the Cabal file for void you'll see that it only includes Data.Void for old base versions. Now, Void is defined as chi suggests:

data Void

absurd :: Void -> a
absurd a = case a of {}

which is perfectly valid.

---

I think the idea behind the old definition is something like this:

Consider the type

data BadVoid = BadVoid BadVoid

This type doesn't get the job done, because it's actually possible to define a non-bottom (coinductive) value with that type:

badVoid = BadVoid badVoid

We can fix that problem by using a strictness annotation, which forces the type to be inductive:

data Void = Void !Void

Under assumptions that may or may not actually hold, but at least morally hold, we can legitimately perform induction on any inductive type. So

spin (Void x) = spin x

will always terminate if, hypothetically, we have something of type Void.

The final step is replacing the single-strict-constructor datatype with a newtype:

newtype Void = Void Void

This is legitimate too; it's impossible to construct a non-bottom value of this Void type. The advantage of doing it this way is that it sometimes lets GHC recognize a little code as dead. But it's not a big advantage, and it introduces some unfortunate complications. The definition of spin, has changed meaning because of the different pattern matching semantics between data and newtype. To preserve the meaning precisely, spin should probably have been written

spin !x = case x of Void x' -> spin x'

(avoiding spin !(Void x) to skirt a now-fixed bug in the interaction between newtype constructors and bang patterns; but for GHC 7.10 (ha!) this form doesn't actually produce the desired error message because it's "optimized" into an infinite loop) at which point absurd = spin.

Thankfully, it doesn't actually matter in the end, because the whole old definition is a bit of a silly exercise.