proposed @noreturn attribute

[Timon Gehr via Digitalmars-d]

On 19.07.2017 17:14, Moritz Maxeiner wrote:
> On Wednesday, 19 July 2017 at 14:52:28 UTC, Timon Gehr wrote:
>> On 19.07.2017 16:47, Moritz Maxeiner wrote:
>>> On Wednesday, 19 July 2017 at 14:32:24 UTC, Timon Gehr wrote:
>>>> On 19.07.2017 14:13, Moritz Maxeiner wrote:
>>>>> On Wednesday, 19 July 2017 at 11:35:47 UTC, Timon Gehr wrote:
>>>>>> a value of type bottom can be used to construct a value for any 
>>>>>> other type.
>>>>>
>>>>> AFAIK from type theory, bottom is defined as having no values (so 
>>>>> one can't reason about the relationship of such non-existent 
>>>>> value(s) to values of other types).
>>>> https://en.wikipedia.org/wiki/Principle_of_explosion
>>>
>>> I am aware, but once a statement (and its negation) can be inferred 
>>> from the same (false) proposition, one isn't reasoning anymore - and 
>>> more importantly its not useful w.r.t. explaining what the bottom 
>>> type is.
>>
>> I disagree with both of those statements, but I'm not sure how any of 
>> this relates to the true sentence I wrote that you seemed to criticize.
> 
> The sentence I quoted states you can use a value of type bottom to 
> construct a value of any other type; this means the existence of such a 
> value of type bottom becomes an implicit premise.

Not really; see below.

> As the bottom type is 
> defined as having no values that premise does not hold, i.e. you can 
> infer both
> "a value of type bottom can be used to construct a value for any other 
> type."
> and
> "a value of type bottom cannot be used to construct a value for any 
> other type."
> from it (principle of explosion, as you quoted). My original criticism 
> was meant to convey that I do not consider the quoted sentence as being 
> helpful w.r.t. explaining what the bottom type is (which the rest of the 
> post I quoted the sentence from did quite well).

What I said does not /use/ the principle of explosion; it states it.

What I am saying is: in a language with a bottom type, we can create a 
function:

T f(T)(Bottom b){
     return b; // assuming b converts to all types implicitly.
}

Within the function body, b is a value of type Bottom.
We use a value of type Bottom to create a value of any type we want.

The reason why I included that part of the sentence was: Not all 
programming languages have subtyping, but all programming languages with 
a bottom type allow a function of the above type to be constructed. 
(It's the induction principle for empty algebraic data types.)

For any T, the type of &f!T is T delegate(Bottom), or in different notation:
f: ∀a. ⊥ → a.

I.e., the type of f is the principle of explosion.