Ivory: Void

The torture at last
Will be gone with the past
Infinity. Where will I go?

— Blind Guardian, Tanelorn (Into the Void)

The simplest number system appears at the very top of Ivory’s numerical tower: void. In fact, it is so simple that it doesn’t contain any values at all!

;; Given any value 'n', it's not an element of 'void'
(define (void? n) #f)

void is an empty type, equivalent to Nothing in Typed Racket. It is an initial object, meaning we can transform an element of void into an element of anything: we just do a cast, safe in the knowledge that it can never go wrong, since it can never actually be executed (due to there being no elements of void to call it on)!

Nevertheless, we can use such casts to implement arithmetic operations for void (like +, ×, /, max, min, gcd, lcm, etc.) which vacuously obey their associated laws.

It’s rare to need void, but it can be handy on occasion. Its dual is a unit type, like zero.