2
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ I think that there is a confusion of two notions of "$A$ is a subtype of $B$": (1) There is a function of type $A\to B$. (2) There is an injective function of type $A\to B$. Any type is a subtype of $Top$ for both notions (1) and (2), and all types are subtypes of $unit$ for (1) but most types are not subtypes of $unit$ for (2). I'd say that (2) is the right definition. $\endgroup$ – xavierm02 Jan 17 at 12:53
  • $\begingroup$ The function from any $A$ to $unit$ could be named $ignore$ and defined by $ignore(x):=()$ with $()$ being the only inhabitant of $unit$. In C++, this function $ignore$ is a coercion and is added implicitly. Because of this, any expression of any type can also be seen as being of type $unit$. Void pointers are more of a hack: If you only did things that respected the type system with them, they would be useless. To use them, at some point, you cast them to pointers to some other type before using them. I'd guess that most (or even all?) occurrences of void* could be Top* if Top existed in C++. $\endgroup$ – xavierm02 Jan 17 at 12:58
  • $\begingroup$ @xavierm02: your comments are off the mark. To say that "any expresions of any type can be seen as being of type $unit$" is highly misleading. By the same reasoning any expression of any type can be seen as being of any other type". $\endgroup$ – Andrej Bauer Jan 17 at 13:37
  • $\begingroup$ @AndrejBauer I maybe should've said "can be coerced to unit". But since the coercion to unit is implicit, I think that the "can be seen as" formulation is fine. And yes, you can coerce anything to any non empty type. But the coercion to unit is often made implicit while others are not. $\endgroup$ – xavierm02 Jan 17 at 16:42
  • $\begingroup$ In C and C++, void as a function return type has a completely different meaning from void in void*. The language designers used the same keyword for two different things. See cs.stackexchange.com/questions/63203/… (which is almost a duplicate of your question — almost because it doesn't deal with something being a unit type vs something being coercible to/from a unit type). $\endgroup$ – Gilles 'SO- stop being evil' Jan 21 at 16:58
5
$\begingroup$

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.

$\endgroup$
  • $\begingroup$ "NB: We can only have a map S→∅ when S itself is the empty set." Can you explain this? Do you mean an injective map? $\endgroup$ – Narrateur du chaos Jan 22 at 12:03
  • $\begingroup$ So, if I'm understanding your post correctly, the answer is "it depends on the subtyping rules, and there's no unanimous rules for what subtyping is or should be?" $\endgroup$ – Narrateur du chaos Jan 22 at 12:07
  • $\begingroup$ No, I mean any map. It's a basic mathematical fact that a map $S \to \emptyset$ exists if, and only if, the set $S$ is empty. NB: a map by definition must be defined everywhere, or else it is not a map. $\endgroup$ – Andrej Bauer Jan 22 at 14:20
  • $\begingroup$ Well, you asked about the difference between the unit and the top type, and I explained that right at the beginning. As to whether the unit and the top type may happen to be equal, that part depends on what notion of subtyping we have. $\endgroup$ – Andrej Bauer Jan 22 at 14:22

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.