Section missing id

Consider Void \/ A => A:

def coidr[A]: Void \/ A => A = {
  case -\/(x) => ...
  case \/-(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.

Section missing id

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(&lt;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:

def equal[A, B]: A =:= B =
  implicitly[A =:= A].asInstanceOf[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.

Section missing id

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.

Section missing id

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 an function with type (A \/ B) \/ C => A \/ (B \/ C) 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.

Section missing id

Finally, I hear you say "absurd seems to do nothing, it takes Void and returns Void". The reader must have looked at the implementation of absurd rather than its interface:

def absurd[A]: Void => A = v => v

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.