proposed @noreturn attribute

Timon Gehr via Digitalmars-d digitalmars-d at puremagic.com
Wed Jul 19 07:52:28 PDT 2017


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.


More information about the Digitalmars-d mailing list