proposed @noreturn attribute

[Andrei Alexandrescu via Digitalmars-d]

On 07/08/2017 10:25 PM, Walter Bright wrote:
> On 7/8/2017 7:01 PM, sarn wrote:
>> On Sunday, 9 July 2017 at 00:16:50 UTC, Walter Bright wrote:
>>> We have types that cannot be named (Voldemort types), types that have 
>>> no type (void), I suppose that types that cannot exist will fill out 
>>> the edge cases of the menagerie.
>>>
>>> I assume there is a standard jargon for this - does anyone know Type 
>>> Theory?
>>>
>>> Are there any other interesting uses for a type that cannot exist?
>>
>> In pure functional languages, that's what "bottom" or Haskell's Void is.
>>
>> In Curry–Howard "programs are proofs" theory, a type is a proposition 
>> and an instance is a proof.  A type with no instance is a proposition 
>> that can't be proved.
>>
>> https://codewords.recurse.com/issues/one/type-systems-and-logic
>>
>> I'm not sure how much impact this has on everyday D programming, but 
>> hey, it's a thing.
> 
> Thanks, it looks like we won't get any help from type theory. We're on 
> our own :-)

How does the information provided lead to such a conclusion? There's 
established theory and practice on that.

https://en.wikipedia.org/wiki/Bottom_type

The "Bottom" type (bottom of the type hierarchy lattice) is what's 
needed. If "Object" is the total set i.e. the top of the lattice i.e. 
the type that is so general all types are a subset of it, then "Bottom" 
is the type that is a subtype of all types and is so particular it can't 
be even instantiated. It implicitly converts to everything because it's 
a subtype of everything. Obviously conversion doesn't need to be honored 
because the function never returns.


Andrei