Good Morning,

today I would like to write about something which came up while implementing type functions.

It turns out that it is useful, to have a .init value for __type.
The language expects it, phobos' std.algorithm breaks in horrible ways when this is violated.
So that poses the question, what should this value be.
It cannot really be a valid type.
One option would be to use the internal error type called Terror.
It turns out that type is aptly named.
Using it will make every mention of the __type.init value an error.
We do not want this.
It's fine to return the init value as long as is(type.init) does return false.

So we need a type that behaves just like Terror (i.e. is not considered a type by the is expression) but is not an error.

This type is the empty type (Ø).
It is emptier than void and on the same level as bottom (⊥).
But Ø cannot be ⊥, because ⊥ can be a valid return type of a function.
(At least once we have the ⊥ type)

Ø not being a valid type as far as the is expression is concerned.
(is(Ø) yields false)
Also means that is(Ø == Ø) also yields false.

And this is where the similarity to NaN comes from, which allowed me to give the post this fancy title.

Please ask me anything, about Ø or type functions.
I am happy to answer questions, and maybe we find more contradictions that we can resolve.

Cheers,

Stefan

On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
> Good Morning,
>
> today I would like to write about something which came up while implementing type functions.
>
> [...]

Shouldn't this be the universe. The empty set is "there is no _", while the "opposite" ¬∅ of the empty set is the universe?

On Sunday, 11 October 2020 at 12:46:53 UTC, Imperatorn wrote:
> On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
>> Good Morning,
>>
>> today I would like to write about something which came up while implementing type functions.
>>
>> [...]
>
> Shouldn't this be the universe. The empty set is "there is no _", while the "opposite" ¬∅ of the empty set is the universe?

The universe would be __type. (because it can hold any type in U)
If you set the __type.init to be __type; (And that's how it used to be)

The that means you cannot distinguish between a function returning __type.
(Assuming your type function gives you the return type of a function)
And the programmer having messed up the and forgot to set the value.

Therefore you need an initial value which cannot possibly be a valid type anywhere.
Hence a type which is no valid type is needed.

On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
> So we need a type that behaves just like Terror (i.e. is not considered a type by the is expression) but is not an error.
>
> This type is the empty type (Ø).
> It is emptier than void and on the same level as bottom (⊥).
> But Ø cannot be ⊥, because ⊥ can be a valid return type of a function.
> (At least once we have the ⊥ type)
>
> Ø not being a valid type as far as the is expression is concerned.
> (is(Ø) yields false)
> Also means that is(Ø == Ø) also yields false.

To me, this sounds more like an empty Optional!__type or a null __type* than a NaN. Maybe it would be better to leave __type as the non-nullable version, and use something like __type* to represent a type that may be absent.

On Sunday, 11 October 2020 at 15:19:17 UTC, Paul Backus wrote:
> On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
>> So we need a type that behaves just like Terror (i.e. is not considered a type by the is expression) but is not an error.
>>
>> This type is the empty type (Ø).
>> It is emptier than void and on the same level as bottom (⊥).
>> But Ø cannot be ⊥, because ⊥ can be a valid return type of a function.
>> (At least once we have the ⊥ type)
>>
>> Ø not being a valid type as far as the is expression is concerned.
>> (is(Ø) yields false)
>> Also means that is(Ø == Ø) also yields false.
>
> To me, this sounds more like an empty Optional!__type or a null __type* than a NaN. Maybe it would be better to leave __type as the non-nullable version, and use something like __type* to represent a type that may be absent.

__type need an init value otherwise phobos breaks all over the place.
and it's much nicer if that value is not part of the domain.
you can compare it 0.
You can do calculations without 0 but it gets very complicated very fast.
The empty type is awesome! I love it!
It allows me to simplify proofs so much.

On Sunday, 11 October 2020 at 13:11:28 UTC, Stefan Koch wrote:
> On Sunday, 11 October 2020 at 12:46:53 UTC, Imperatorn wrote:
>> On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
>>> [...]
>>
>> Shouldn't this be the universe. The empty set is "there is no _", while the "opposite" ¬∅ of the empty set is the universe?
>
> The universe would be __type. (because it can hold any type in U)
> If you set the __type.init to be __type; (And that's how it used to be)
>
> The that means you cannot distinguish between a function returning __type.
> (Assuming your type function gives you the return type of a function)
> And the programmer having messed up the and forgot to set the value.
>
> Therefore you need an initial value which cannot possibly be a valid type anywhere.
> Hence a type which is no valid type is needed.

Oh, I see. I mis-read the question

On Sunday, 11 October 2020 at 15:23:45 UTC, Stefan Koch wrote:
> On Sunday, 11 October 2020 at 15:19:17 UTC, Paul Backus wrote:
>> On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
>>> [...]
>>
>> To me, this sounds more like an empty Optional!__type or a null __type* than a NaN. Maybe it would be better to leave __type as the non-nullable version, and use something like __type* to represent a type that may be absent.
>
> __type need an init value otherwise phobos breaks all over the place.
> and it's much nicer if that value is not part of the domain.
> you can compare it 0.
> You can do calculations without 0 but it gets very complicated very fast.
> The empty type is awesome! I love it!
> It allows me to simplify proofs so much.

Or have NaT = Not a Type, as NaN

On Sunday, 11 October 2020 at 15:23:45 UTC, Stefan Koch wrote:
>
> __type need an init value otherwise phobos breaks all over the place.
> and it's much nicer if that value is not part of the domain.

By definition, the init value of a type is part of that type's domain. What adding ø does is extend the domain of __type from "all types" to "all types, plus one additional value that isn't a type." Thus the comparison to Optional, which does the same thing.

Both __type and Optional!__type are useful and worth having, but I think it would be better to keep them separate than to make all __type variables implicitly nullable. Optional!__type's init value can be "not a type", and __type's init value can be bottom.

On Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote:
> Good Morning,
>
> today I would like to write about something which came up while implementing type functions.
>
> [...]

Btw, wouldn't this be solved if/when DIP1017 is passed?

alias Tbottom = typeof(assert(0));

On Sunday, 11 October 2020 at 17:18:20 UTC, Paul Backus wrote:
> On Sunday, 11 October 2020 at 15:23:45 UTC, Stefan Koch wrote:
>>
>> __type need an init value otherwise phobos breaks all over the place.
>> and it's much nicer if that value is not part of the domain.
>
> By definition, the init value of a type is part of that type's domain. What adding ø does is extend the domain of __type from "all types" to "all types, plus one additional value that isn't a type." Thus the comparison to Optional, which does the same thing.
>
> Both __type and Optional!__type are useful and worth having, but I think it would be better to keep them separate than to make all __type variables implicitly nullable. Optional!__type's init value can be "not a type", and __type's init value can be bottom.

Instantiating a template for just one more additional value?
Having to drag this bool around in ctfe?
Having to check it every time when you do an is-exp?

that's crazy.
Especially when I have to choice to define an empty type.