> The most straightforward way to represent the proposition
    > “not A” with the type A -> ⊥, where ⊥ is what’s called an
    > empty type – a type with no values. (This type’s symbol
    > comes from mathematics. It is usually pronounced
    > “bottom.”) A -> Void can be read as “if we have an A, we
    > can use it to make something that doesn’t exist”

Unless the author means something different from what I think, using "void" here is very confusing. "void", as it appears in C, Java, et. al. is not all like a bottom type. A bottom type means "there can be no value here". In other words, a function whose return type was bottom could not return. Coming from an imperative mindset, one way to understand that is to consider this function:

    foo() { throw "!"; }

You can never get a value out of this function. If you do:

    var result = foo();

result will never get assigned. So, here, foo's return type really is "bottom". This is different from void—a function that returns successfully but emits no value.

Instead of corresponding to "bottom", void maps to the unit type: the empty tuple.