proposed @noreturn attribute
sarn via Digitalmars-d
digitalmars-d at puremagic.com
Sat Jul 8 19:01:26 PDT 2017
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.
More information about the Digitalmars-d
mailing list