How would a Void let you produce, or do, anything?

Question

In Type-Driven Development with Idris, Brady says

If you were able to provide a value of the empty type, you'd be able to produce a value of any type. In other words, if you have a proof that an impossible value has happened, you can do anything. The Prelude provides a function, void, that expresses this:

void : Void -> a

I'm having difficulty getting what this means. How could you produce a value of any type from a Void? And how does that mean you could do anything? Would be particularly helpful if you could explain this with reference to void

Answer 1

Every type has a set of introduction rules and an elimination rule. Void is kind of special. It has no introduction rule by itself. However other types come with extra introduction rules for Void. For example, equality of Nat has an introduction rule for Void:

n: Nat -> 0 = S(n) -> Void

(Idris generates these rules from its own internal rules for determining that different terms cannot be pattern-matched.)

The elimination rule lets you go the other way, eg:

Void -> n: Nat -> 0 = S(n)

In effect it says that all impossible things are equivalently impossible - if you have one impossible thing, then you can have any other impossible thing.

The deeper question is: what would happen if we didn't have this elimination rule? Would we end up with different categories of impossible things, with different non-equivalent types of impossibility?

I don't know the answer to that question.

However, if you assume 0=1 then it's easy to prove that anything is equal to anything else (because you can prove that repeat(1,f,x) = repeat(0,f,x) so therefore f(x) = x for all x and f, so define f where f(a) = y, and you have that x = y).

So, if we know that all introduction rules for Void are derived from inequalities, then a more limited elimination rule like the following would be equivalent to the more general rule:

Void -> 0 = 1