Search code examples
haskellcategory-theory

Inverse of the absurd function

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

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

Solution

  • 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.