On 18.07.2017 14:19, Stefan Koch wrote:
On Tuesday, 18 July 2017 at 12:15:06 UTC, Timon Gehr wrote:
On 18.07.2017 12:17, John Colvin wrote:
Better to just not define it.
That's not an option. Bottom is a subtype of all types. It cannot
remove members, even static ones.
Timon, how important is it to actually have bottom ?
D has a C-inspired first-order type system, so it is not necessarily
crucial to have it in D. (The reason I got involved in this thread is
that it was proposed to add Bottom as a type that is not really a type;
'void' is annoying enough as the 'null' of types. We don't really need
another one of those.)
Bottom is the most principled way to encode noreturn (but the D type
system does not have a tradition of being very principled, so
introducing it has a cost that does not really exist the same way in
more orthogonal designs: it falls out of them naturally).
If you have a very expressive type system, it is important to have empty
types, because there you cannot actually decide algorithmically whether
any given type is in fact empty. Another reason why one might want an
empty type is that it is the neutral element for disjoint union (up to
isomorphism). (But D does not have those built-in.)
... and what does it actually represent ?
It's a type that has no instances. If I say
int foo();
this means foo returns one of {0,1,-1,2,-2,3,-3,...,int.max,int.min}.
If I say
Bottom foo();
this means foo returns one of {}.
I.e., there is no value which foo might return. Hence it cannot return.
It can be argued that it is a bit silly to say:
int foo()@noreturn;
I.e., this function returns one of
{0,1,-1,2,-2,3,-3,...,int.max,int.min}, but actually, it does not return
anything. The first piece of information is redundant.
The closure of all possible types ?
like auto but if auto where not replaced ?
Your intuition is correct. In a higher-order type system, you can have:
(∀a. a) foo();
This says that foo returns a value that has any type you wish it to have.
Of course, there is no single value that has all types (ignoring e.g.
full OO languages that have null references), hence we have no way to
actually construct a value satisfying the constraints, so (∀a. a) is an
empty type.
In languages with subtyping, Bottom is often just a subtype of all other
types. (The name "Bottom" stems from here:
https://en.wikipedia.org/wiki/Lattice_(order)#Bounded_lattice . The
bounded lattice in question is the subtyping lattice, where A ≤ B means
A is a subtype of B.)
One reason why it is nice to have a bounded subtyping lattice is that
then, you can express subtyping constraints uniformly: A≤B does not
constraint B if A is Bottom, and it does not constrain A if B is Top.
