On Sunday, 9 July 2017 at 04:23:15 UTC, Meta wrote:
> 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.

In C++/D terms, the unit type could be expressed as `enum Unit { unit }` while the bottom type would be `enum Bottom {}` (although only conceptually because in C++/D you can still do `Bottom b;`).

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

On 07/08/2017 05:03 PM, Vladimir Panteleev wrote:
> 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.

Eh, interesting. Indeed this doesn't compile anymore:

struct None
{
    @disable this();
    @disable this(this);
	@disable ~this();
    @disable static @property None init();
}

None fun()
{
	None none = void;
	return none;
}

void main()
{
    fun();
}

The type None would then go in object.d.

The compiler detects the pattern and make None implicitly convertible to anything so people can write things like:

int x = y ? 100 / y : fun();

Without the conversion, None is a less useful artifact.


Andrei

On 7/8/2017 9:23 PM, Meta wrote:
> 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.).

Thanks for the explanation.


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

That is indeed an interesting idea. Thanks!

(This thread is turning out to be more productive than I anticipated.)

On 7/8/2017 9:32 PM, Meta wrote:
> On Sunday, 9 July 2017 at 04:23:15 UTC, Meta wrote:
>> 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).

I read that a Void function in Haskell does not return. Is that incorrect? I'm not sure how Void relates to _|_

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

says Haskell does not support empty (i.e. bottom) types.

>> 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.
> 
> In C++/D terms, the unit type could be expressed as `enum Unit { unit }` while the bottom type would be `enum Bottom {}` (although only conceptually because in C++/D you can still do `Bottom b;`).

In D, void is used to signify a function doesn't return a value, but it still returns. It also means untyped data, and no initializer.

On Saturday, 8 July 2017 at 10:15:39 UTC, Walter Bright wrote:

> Has anyone a better idea?

What about

scope(exit) assert(0);

?

On 09.07.2017 07:44, Walter Bright wrote:
> On 7/8/2017 9:32 PM, Meta wrote:
>> On Sunday, 9 July 2017 at 04:23:15 UTC, Meta wrote:
>>> 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).
> 
> I read that a Void function in Haskell does not return. Is that incorrect?

It is indeed incorrect, but this has little relevance for D. In Haskell, non-termination and exceptions are values that you can store in a variable (due to lazy evaluation). A function can return non-termination or exceptions non-evaluated. When those values are finally lazily evaluated, you get actual non-termination or a thrown exception. This is why Haskell has no empty type. If evaluation in Haskell was strict (as D's is), a function with return type Void would not be able to return. (BTW: it makes more sense to return a polymorphic value, i.e. x :: t instead of using the Void type, because Haskell does not have subtyping. This still implies that x does not contain a 'real' value, because we can instantiate t with Void.)

> I'm not sure how Void relates to _|_
> 
>    https://en.wikipedia.org/wiki/Bottom_type#In_programming_languages
> 
> says Haskell does not support empty (i.e. bottom) types.
> ...

On Sunday, 9 July 2017 at 10:31:47 UTC, Mr.D wrote:
> On Saturday, 8 July 2017 at 10:15:39 UTC, Walter Bright wrote:
>
>> Has anyone a better idea?
>
> What about
>
> scope(exit) assert(0);
>
> ?

void func()
out { assert(0); }
body
{
}

On Sunday, 9 July 2017 at 10:51:50 UTC, Daniel N wrote:
> On Sunday, 9 July 2017 at 10:31:47 UTC, Mr.D wrote:
>> On Saturday, 8 July 2017 at 10:15:39 UTC, Walter Bright wrote:
>>
>>> Has anyone a better idea?
>>
>> What about
>>
>> scope(exit) assert(0);
>>
>> ?
>
> void func()
> out { assert(0); }
> body
> {
> }

Yes, this!

-Steve

On Sunday, 9 July 2017 at 10:59:43 UTC, Steven Schveighoffer wrote:
> On Sunday, 9 July 2017 at 10:51:50 UTC, Daniel N wrote:
>> On Sunday, 9 July 2017 at 10:31:47 UTC, Mr.D wrote:
>>> On Saturday, 8 July 2017 at 10:15:39 UTC, Walter Bright wrote:
>>>
>>>> Has anyone a better idea?
>>>
>>> What about
>>>
>>> scope(exit) assert(0);
>>>
>>> ?
>>
>> void func()
>> out { assert(0); }
>> body
>> {
>> }
>
> Yes, this!
>
> -Steve

That certainly signals intention, but I still think that an attribute is a whole lot simpler than compiler voodoo like this or the "None" discussed earlier.