What is the difference between a Top type and a Unit type

Question

Wikipedia defines a Top type: (edited for readability)

The Top type [...] is the universal supertype, as all other types in any given type system are subtypes of Top

However, the article goes on to say:

In C++: The pointer to void type can accept any non-function pointer, even though the void type itself is not the universal type but the unit type.

I don't understand this. In particular, given these two functions:

void foo(T1, T2, T3);
SomeType bar(T1, T2, T3);

I'd expect bar to be accepted wherever foo is accepted (in function pointers, as virtual methods, etc); which makes me think void is being treated as a supertype of SomeType.

Leaving C++ aside, I'd expect the same semantics from any language: any logic that expects a void could logically accept any other type.

---

So, given its properties, why is void usually called a Unit type, and how is it different from a Top type?

Answer 1

Let me first give the mathematical counterparts of the unit and the top type:

• the unit type is the type $U$ such that for every type $X$ there is a unique map $X \to U$

• the top type is the type $T$ such that every type $X$ is a subtype of $T$, written $X \leq T$

Thus we cannot speak of the top type unless we have subtyping. Not all type systems have subtyping, and in those there is no top type to speak of.

The unit type $U$ must be very small: since there is only one map $U \to U$, if we have $a, b: U$ then the two maps $x \mapsto a$ and $x \mapsto b$ must be equal, whence $a = b$. We should be more precise about what "equal" means, and we should discuss non-terminating computations, but let's keep things simple. On the other hand, there must be at least one element of $U$, or else there can be no map $\mathtt{int} \to U$. (NB: We can only have a map $S \to \emptyset$ when $S$ itself is the empty set.)

The type called $\mathtt{void}$ isn C/C++ has the property of the unit type. It is a mistake to think that a function returning $\mathtt{void}$ "returns nothing". It actually returns precisely one thing, but because the unique thing that it returns is unique and does not carry any information beyond the fact that the function actually returned, we never make the thing explicit. Thus programmers never see it, and so they end up thinking it isn't there. There are programming languages in which the unique element of the unit type can be made explicit. Can there be a function that returns nothing? Yes, it's a function that does not return at all (if it did, it would have to return something) – it is a function which raises an exception! Raising an exception is not "returning".

The top type $T$ must be in some sense very large because every other type is a subtype of $T$. Note that $X \leq T$ does not necessarily mean that there is an injective map $X \to T$, nor does the fact that there is a map $X \to T$ imply $X \leq T$. There are many kinds of subtyping and it is really quite impossible to tell more precisely what "large" means without knowing what sort of subtyping we are talking about.

For example, in some languages there is subtyping between numerical types, so that for instance $\mathtt{byte} \leq \mathtt{int} \leq \mathtt{float}$. Here $\mathtt{float}$ could be the top type, and it is the "largest" numerical type.

On the other hand, structural record subtyping says that the record type $R = \{\ell_1 : X_1, \ldots, \ell_m : X_m\}$ is a subtype of $Q = \{k_1 : Y_1, \ldots, k_n : Y_n\}$ when every field $k_j : Y_i$ has a corresponding field $\ell_i : X_i$ such that $k_j = \ell_i$ and $X_i \leq Y_j$. In words, $R \leq Q$ means that an $R$-record may be seen as a $Q$-record because it has all the fields that a $Q$-record should have, and possibly more. Under this view the top type is the empty record $\{\}$, which is isomorphic to the unit type!

You asked concretely about subtyping of functions. The basic rule there is: if $X_2 \leq X_1$ and $Y_1 \leq Y_2$ then $(X_1 \to Y_1) \leq (X_2 \to Y_2)$ (notice the reversal of inequality for $X_1$ and $X_2$). In your particular case we have $X_1 = X_2 = T_1 \times T_2 \times T_3$, $Y_1 = \mathtt{SomeType}$ and $Y_2 = \mathtt{unit}$ (I refuse to write "void" for something that is not the empty type and C/C++ can go sulk in the corner). So the question comes down to $\mathtt{SomeType} \leq \mathtt{unit}$, i.e., should the unit type be the top type? Well, this depends on what "subtype" means, as I tried to explain above. In C and C++ subtyping is expressed through a system of implicit coercions, so you'd have to open a book on C and find out whether there is supposed to be an implicit coercion from an arbitrary type to the unit type. It's a matter of language definition.