Void is the uninhabited type, Unit is the singleton type. Void != Unit

a1369209993 · on Nov 27, 2022

No, as previously mentioned, `void` is the singleton type (the same type haskell calls `()`[0], and some other languages call `Unit`). Eg:

  void foo(int x) {
    printf("%i\n",x);
    return; /* <- inhabited */ }

0: Give or take some pedantry about `TYPE 'LiftedRep`.

louthy · on Nov 28, 2022

The example you give is a statement, not an expression. There is no value returned, and the return-type is void, which can't be constructed. Only imperative languages, that can ignore the lack of a value from an expression (by simply moving on to the next statement), can deal with void returning functions. In Haskell this causes the end-of-the-program because it works solely with expressions, and an expression must have a value.

It's been a good 30 years since I've written any C, and I know its type-system is compromised at best, but I'm fairly sure you can't do something like this?

    void x = new void();

Or, using your foo example:

    void x = foo();

If you can then void is inhabited (and incorrectly named). I realise you could create void* and other elaborate means of claiming you have an inhabited void, but really can you legally construct one, not hack any underlying value to pretend to have one - there is a difference. If you can construct one and assign it to a variable, then it's inhabited.

Railing against Haskell when its implementation actually works correctly is a very strange position to take. The clue really is in the name empty-set = void, singleton-set = unit.