Inverse of the absurd function

Question

Is there an inverse to the absurd function from Data.Void?

If it exists, how is it implemented and what is it used for?

Answer 1

This function does not exist. (assuming strict semantics)

Looking at the algebra of types, the function type is equivalent to exponentiation.

Now the function absurd, which has the type Void -> a corresponds to the operation a ^ 0 which equals 1. This means that there is exactly one implementation of absurd, which can be found in Data.Void.

Reversing the arrow, you get the type a -> Void, which corresponds to 0 ^ a or 0, which means the desired function does not exist.

---

You could also prove this using the Curry-Howard isomorphism. Since the function type corresponds to the boolean function 'implies', you get the following term:

True -> False

which is false, and therefore no function a -> Void can exist.

Corrections due to imprecise language are encouraged since I just started learning category theory.

Answer 2

It depends what you mean. absurd witnesses one side of the isomorphism Void = forall a.a and from that view, has an inverse

void :: (forall a.a) -> Void
void x = x

that is really an isomorphism.

There is no total function of the type

 forall a.a -> Void

nor any inverse to absurd with that type among partial functions.

Answer 3

Quite intuitively, that function cannot possibly exist^†. Say we had such a function:

drusba :: a -> Void

then you could do

GHCi> drusba (5 :: Int)

...thereby creating a value of type Void. Well, that's exciting... also, congratulations, you're dead!

Hask (the category of Haskell types, with Haskell functions as morphisms) is a bicartesian closed category with initial object Void. The definition of an initial object is that, for any type A, there exists exactly one function Void -> A – these functions are the instantiations of absurd :: Void -> a. Dually, there exists exactly one function B -> (), since () is the terminal object – any such function is equivalent to const ().

Now, assuming drusba :: () -> Void, we would have

drusba . absurd :: Void -> Void
drusba . absurd ≡ id

because there can only be one function Void -> Void, and we know id is one; and

absurd . drusba :: () -> ()
absurd . drusba ≡ id

for the same reason. IOW, drusba and absurd are indeed proper inverses to each other, which means () and Void are isomorphic.

But from this it would follow that any type A is actually isomorphic to both () and Void, because there would exist precisely one function () -> A and A -> ().

So basically, if there existed a function drusba :: a -> Void, it would mean that Haskell had only one type, which would contain no values. That wouldn't be a particularly useful programming language, would it?

---

^†_{Of course, all of this only holds if you disregard ⊥.}