# Ramblings about Void.

This is basically a slightly cleaned up version of my answer to

```
https://gitter.im/scalaz/scalaz?at=5b246f7a6b24803e845c6a17
Hey @emilypi @alexknvl , Can you guys provide me simple example code which uses Void type in Scala? I think that we use Void when we know for sure that some branch is never going to execute kinda situation . But I am confused with the method absurd which seem to doing nothing, It takes Void and returns Void. :confused: Need your help!
```

on Gitter.

# Why do we need absurd?

Consider `Void \/ A => A`

:

We need to insert something in the first case, but what? We have a value `x : Void`

in scope, so we know for sure that that case can never actually succeed. But we still need to convince the compiler of that!

In some compilers, impossible cases can actually be marked as `impossible`

, the compiler itself finds a value of type `Void`

in the current context and then does dead code elimination.

But if you don’t have such an option, you can use `absurd[A](v: Void): A`

to satisfy any result type.

# How do you use Void in practice?

Perhaps the most important use-case for `Void`

is also the most “useless”, or “computationally trivial”: proving that things are false. If you prove that you can derive `Void`

from some expression (or a logician would say assuming) `a : A`

, you know that `A`

has no inhabitants (no proofs). But that knowledge doesn’t allow you to actually compute anything.

I will assume that the reader is somewhat familiar with *propositions-as-types* or Curry-Howard-Lambek correspondence. It is often misunderstood in the programming community IMHO.

Under CHL, `(A => Void) => Void`

corresponds to `(A→⊥)→⊥`

or in other words `¬¬A`

. In classical logic it is the same as A, but in intuitionistic logic we can not remove the double negation.

You can try writing `((A => Void) => Void) => A`

in Scala, but I guarantee you that whatever tricks you use (mutability, exceptions), it is impossible to do for an arbitrary type `A`

without running into soundness issues:

```
type Void <: Nothing
type \/[+A, +B] = Either[A, B]
type ¬¬[+A] = (A => Void) => Void
final case class Return[A](tag: AnyRef, a: A) extends Throwable {
override def fillInStackTrace(): Throwable = this
}
def uncps[A](a: ¬¬[A]): A = {
val Tag: AnyRef = new AnyRef()
try a(a => throw Return[A](Tag, a)) catch {
case Return(Tag, a) => a.asInstanceOf[A]
}
}
// Law of excluded middle under double negation.
def either[A]: ¬¬[(A => Void) \/ A] =
k => k(Left(a => k(Right(a))))
println(uncps(either[Int])) // Left(<function>)
uncps(either[Int]) match {
case Left(f) => f(1) // throws an exception
case Right(x) => x
}
```

But it is still a very interesting type because we know that if someone managed to come up with `(A => Void) => Void`

without cheating, then `A`

must have at least one inhabitant.

Why? Let’s assume that someone gave us a `p: (A => Void) => Void`

without cheating (e.g. exceptions or non-termination). Let’s cheat ourselves, and pass it `na : a => ???`

. `p(na)`

must return a value of type `Void`

, so it either calls `na`

, or our language itself is unsound and it is possible to derive `a : Void`

without calling `na`

.

In some cases we have escape hatches that allow us to forcibly construct an `A`

, for example consider `A =:= B`

:

How do we know that this won’t crash our code with a `ClassCastException`

? What if someone gave us `((A =:= B) => Void) => Void`

? We would know that `A =:= B`

is inhabited by at least one value, which means that `A`

is indeed the same type as `B`

and `implicitly[A =:= A].asInstanceOf[A =:= B]`

is perfectly safe.

So in *some cases for some types* `A`

it is perfectly legal to do `((A => Void) => Void) => A`

.

Logically, it is `¬¬A→A`

, proof by contradiction: you assume that `A`

is false, prove absurdity from that, and by contradiction you prove `A`

.

## Void in category theory.

I’ll assume that the reader is familiar with `Scal`

or `Hask`

as categories with types as objects and functions as morphisms.

Categories without any extra structures are very very boring. Luckily, `Scal`

has lots of interesting things in it, e.g. it is both a cartesian and a co-cartesian category.

Now, one might say “But Alex, `Scal`

is not really a category and eager languages do not have products”.

And to that I say “Bite me”. Yes, everything I said so far is true only under rather severe assumptions (totality, purity, parametricity, no `null`

, no compiler weirdness, infinite stack, preferably TCO, language soundness, well-defined operational semantics, well-defined function equality, etc), but we make them all the time when doing functional programming anyway.

Anyway, let’s unpack “cartesian” and “cocartesian”. First of all they require *initial and terminal objects*.

Terminal objects have unique incoming morphisms from every other object.

Is `Int`

a terminal object? Clearly not, because there are many functions `Int => Int`

.

Is `Unit`

a terminal object? Yes, because there is only one arrow `A => Unit`

, that’s `_ => ()`

.

Conversely, initial objects have unique outgoing morphisms to every other object.

Is `Unit`

an initial object? No, because there are many functions of type `Unit => Int`

, for example `_ => 42`

or `_ => -1`

.

Now, it might not be exactly clear why, but `Void`

is an initial object in `Scal`

.

There is certainly a function from `Void`

to every other `A`

, `absurd`

. But why is it unique? That’s far less clear. It doesn’t have any observable properties, we can not call an `f : Void => A`

. There is no way to distinguish two `f, g : Void => A`

.

You could say that precisely because they *have no observable properties that are different, we should identify them*.

Notice that when I say “Void is an initial object”, I say `an`

rather than `the`

. That’s because any type with no inhabitants would serve equally well as an initial object. In fact, in category theory you prove that they are all isomorphic.

### Cartesian categories are monoidal

Okay, back to cartesian and cocartesian. Cartesian categories also have to be monoidal, with terminal object as a unit. Monoidal categories are those that have a special `⊗[_, _]`

such that `(A ⊗ B) ⊗ C`

is isomorphic to `A ⊗ (B ⊗ C)`

, an identity object `I`

such that `A ⊗ I`

is isomorphic to `A`

and `I ⊗ A`

is isomorphic to `A`

, and some other laws that are not important right now.

What if we take `⊗[A, B] = (A, B)`

? Clearly `((A, B), C)`

is isomorphic to `(A, (B, C))`

. But what do we need to substitute for `I`

in `(A, I)`

so that it is isomorphic to `A`

?

`Unit`

, which is a terminal object! Which means `Scal`

is a cartesian category.

Now, if you know a bit of category theory, you might say “`(,)`

is a product, what about co-products”?

Turns out that if you take `⊗[A, B] = A \/ B`

, it also satisfies `(A ⊗ B) ⊗ C = A ⊗ (B ⊗ C)`

(please take some time to write a `(A \/ B) \/ C => A \/ (B \/ C)`

on ScalaFiddle to convince yourself). Now we need an `I`

such that `A \/ I`

is isomorphic to `A`

.

We have `absurd`

, so we can easily write `A \/ Void => A`

, in fact we already have a mostly complete implementation at the beginning of this page. And `A => A \/ Void`

is just `-\/`

. So `Void`

makes `Scal`

into a cocartesian category

## But how does absurd work in Scala?

Finally,

absurd which seem to doing nothing, It takes Void and returns Void

the reader must have looked at the implementation of `absurd`

rather than its interface.

Indeed, it takes a `v: Void`

and returns it, because in Scala we have subtyping and a bottom type of the subtyping lattice `Nothing`

. `Nothing <: A`

for any `A`

, and if `A <: B`

, then `(a : A) : B`

upcasts `a`

to type `B`

.

`Nothing`

is actually the same type as `Void`

, with the exact same semantics from the logical / categorical point of view.

**But we work in Scala**, and Scala is a massive PITA sometimes, especially when it comes to `Nothing`

. it really dislikes `Nothing`

in implicits and it is overly eager to report any use of `Nothing`

as “dead code” and issue a warning if you have -Ywarn:unused (or whatever the flag).

So instead we hide `Nothing`

behind an opaque newtype and export only the parts of its behavior we care about - `absurd`

(and maybe `Void === Nothing`

). This makes Scala happy and we can use `Nothing`

without all of the bugs.