The NaN of types (in D)

[Ola Fosheim Grøstad]

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)

I think you need to find out what you need to prove the semantics 
of the language to be sound (or which constructs you need to 
exclude to make it sound). Or just hack together something that 
isn't exposed to the programmer. Maybe you need to tune the 
existing language.

So, for instance, if the following was legal "i<j ? true : 
break". Then break would have the bottom type, never returns 
anything. So the bottom type has no values. So the conditional 
expression is of type boolean as the bottom type is included in 
the type boolean.

A function that is "void f()", on the other can be viewed as 
returning only one value "void()". So if you allow "i<=j ? (i==j) 
: f()" the type of the conditional expression would be 
void|boolean, so it has 3 values I guess. "no value" is exactly 
one value... :^)

On the other hand, a bottom-value represents situations where you 
at run time want to represent that a computation is inconclusive. 
For instance if you spawn two threads to compute f() and g(), and 
have the expression "f()||g()" then you can continue if either 
f() or g() succeeds, but you can allow the other one to fail or 
go into an infinite loop.  If both fail I guess you could assign 
it a bottom-value.

But you might want to distinguish between "inconclusive" and 
"contradiction"...

Anyway, it all boils down to the semantics and capabilities of 
the existing language, if you expose it externally it should not 
be driven by the compiler implementation.