On Saturday, 8 July 2017 at 12:17:57 UTC, Andrei Alexandrescu wrote:
>     @disable @property None init();

You meant static here I guess.

> The compiler detects (without having anything hardwired about the particular type "None") that the type None is impossible to create and copy/move from a function, and therefore decrees the function will never return.

Cheat: https://is.gd/pf25nP

Works because of NRVO I guess. This particular one is countered by also adding a disabled destructor.

On Saturday, 8 July 2017 at 21:03:57 UTC, Vladimir Panteleev wrote:
> This particular one is countered by also adding a disabled destructor.

Oops, never mind that - this makes the function uncallable.

On 7/8/2017 1:20 PM, H. S. Teoh via Digitalmars-d wrote:
> Hmmm. Just to clarify, what exactly does @noreturn include? If I have a
> function that calls exit(), that's @noreturn? What about a function that
> always throws? Or a function that calls exec()? A function that always
> ends in assert(0)? A function that context-switches to a different
> thread / fibre and terminates this one?

There's no subtlety to it. It's a function that never returns. I.e. it doesn't execute a 'RET' instruction.


> As for Andrei's idea, it's pretty clever but we would need to
> standardize the None type, otherwise we risk hard-to-read code when
> everyone rolls their own None type with different names. An attribute
> has the advantage that it will be universally understood.

It would be like `size_t`.

On Saturday, 8 July 2017 at 12:17:57 UTC, Andrei Alexandrescu wrote:
> struct None
> {
>     @disable this();
>     @disable this(this);
>     @disable @property None init();
> }
>
> None ThisFunctionExits();
>
> The compiler detects (without having anything hardwired about the particular type "None") that the type None is impossible to create and copy/move from a function, and therefore decrees the function will never return.

That's a lot more complex (for the compiler and to explain) than using a simple magic @noreturn attribute.
Agreed that this is rarely needed but sometimes nice to have. Far from being important though ;).

On 7/8/2017 4:36 PM, Martin Nowak wrote:
> That's a lot more complex (for the compiler and to explain) than using a simple magic @noreturn attribute.
> Agreed that this is rarely needed but sometimes nice to have. Far from being important though ;).

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?

On Sunday, 9 July 2017 at 00:16:50 UTC, Walter Bright wrote:
> I assume there is a standard jargon for this - does anyone know Type Theory?
I'm afraid it's perpendicular to type theory - every type including Nothing can be returned. Most simple solution - just to remove '@' and call this type 'noreturn'.

noreturn functionFoo(bla-bla-bla);

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.

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

On Sun, Jul 09, 2017 at 02:01:26AM +0000, sarn via Digitalmars-d 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?

Technically, the *type* itself exist, it's just that you cannot create any instances of it. :-P  From the POV of types as sets of possible values, it's a type that corresponds with an empty set.  However, then we cannot distinguish between void (which is also by definition a type that has no instances) and noreturn.  I'm not sure how to interpret noreturn in this framework... perhaps a set that doesn't exist? :-P  We could call it a RussellsParadox set. :-D


> In pure functional languages, that's what "bottom" or Haskell's Void is.
[...]

Are you sure?  IIRC, it's legal to return bottom; it just signifies that the value is invalid, and that any operation on it will also result in bottom.  Sortof like NaN.  That's not the same thing as "this function never returns".


T

-- 
The computer is only a tool. Unfortunately, so is the user. -- Armaphine, K5

On Sunday, 9 July 2017 at 02:25:50 UTC, Walter Bright wrote:
> (D already has a `void` type, so can't use Haskell's word.)

Just so we are all on the same page, from a type-theory perspective void is a unit type (it has 1 value), not an uninhabited type (it has no values, i.e. Haskell's _|_ (bottom) type).

A function with a return type of unit means "this function returns no useful information", because the type only has one possible value anyway. A function with a return type of bottom means "this function can never return", because there is no value of type bottom that could be returned. All that can be done is for the function to diverge (throwing an exception, ending the program, looping forever, etc.).

We sort of have this already with `assert(0)`. The compiler knows that no execution can take place after an `assert(0)` is encountered (in other words, it knows that the function diverges). We just don't have a corresponding type to represent this (Rust uses ! but if I remember correctly it's not quite a first class type).

If we wanted to be cute we could use `typeof()` to represent this type as there is no value you can give to typeof such that it returns the bottom type. It also avoids having to come up with some special symbol or name for it.