proposed @noreturn attribute

Moritz Maxeiner via Digitalmars-d digitalmars-d at puremagic.com
Wed Jul 19 08:14:32 PDT 2017


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. 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).


More information about the Digitalmars-d mailing list