Re: 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.