Kotlin made this explicit by calling the void type Unit, where it is a class that has a single instance with the same name.

So when you define a function:

    fun foo(a: Int): Unit {
        ...
    }

You can actually assign a value to the result:

    val x = foo()  // x now contains the value Unit

There is another type which does not have any instances, called Nothing. Declaring a function to return Nothing indicates that the function will never return. Other than that, Nothing is a regular type, but code that uses it will be unreachable (and flagged as such by the IDE) because you can never create an instance of it.

    fun foo(): Nothing {
        throw SomeException()
    }

This leads me to the question. Unit is obviously the mathematical Unit type, but is there a way to model the Nothing type in mathematically?

Yeah, it's called Bottom (⊥)

    fun foo(): ⊥ {
        return foo();
    }

In Rust it's called !, and you can write

    fn will_panic() -> ! {
        panic!("uh oh");
    }

This is actually useful for some embedded systems, where the main function isn't allowed to return, and gets declared with the Nothing / Bottom / ! type.

The compiler is also smart enough to say that an infinite loop has type !, so you can have

    fn main() -> ! {
        let setup = ...;
        loop {
            blink_led();
            sleep(100);
        }
    }

and it'll complain if you put a break statement in the loop.

Cool. So `void f (double a, double b)` is like `f : R^2 -> R^0`, where R^0 is a singleton set.

In C and C++, where this void kludge from, the void type is an incomplete type which cannot be completed and contains no values.