proposed @noreturn attribute

[Timon Gehr via Digitalmars-d]

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.