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.