proposed @noreturn attribute

Walter Bright via Digitalmars-d digitalmars-d at puremagic.com
Sat Jul 8 19:25:50 PDT 2017


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

(D already has a `void` type, so can't use Haskell's word.)


More information about the Digitalmars-d mailing list