www.digitalmars.com         C & C++   DMDScript  

digitalmars.D - The NaN of types (in D)

reply Stefan Koch <uplink.coder googlemail.com> writes:
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
Oct 11 2020
next sibling parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
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?
Oct 11 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
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.
Oct 11 2020
parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
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
Oct 11 2020
prev sibling next sibling parent reply Paul Backus <snarwin gmail.com> writes:
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.
Oct 11 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
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.
Oct 11 2020
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
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
Oct 11 2020
prev sibling parent reply Paul Backus <snarwin gmail.com> writes:
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.
Oct 11 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
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.
Oct 11 2020
parent reply Paul Backus <snarwin gmail.com> writes:
On Sunday, 11 October 2020 at 18:09:28 UTC, Stefan Koch wrote:
 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.
It doesn't have to be a template; it could be a __type*, or something else built-in. The point is that code working with __type variables shouldn't be *required* to add null checks everywhere to account for the possibility of ø. Nullability should be opt-in.
Oct 11 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
On Sunday, 11 October 2020 at 18:18:24 UTC, Paul Backus wrote:
 On Sunday, 11 October 2020 at 18:09:28 UTC, Stefan Koch wrote:
 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.
It doesn't have to be a template; it could be a __type*, or something else built-in. The point is that code working with __type variables shouldn't be *required* to add null checks everywhere to account for the possibility of ø. Nullability should be opt-in.
ø is a special case that shouldn't happen to often. You are free to ignore the possibility of it being null. Just like with classes which almost no one checks with class is null.
Oct 11 2020
parent reply Paul Backus <snarwin gmail.com> writes:
On Sunday, 11 October 2020 at 19:45:06 UTC, Stefan Koch wrote:
 ø is a special case that shouldn't happen to often.

 You are free to ignore the possibility of it being null.
 Just like with classes which almost no one checks with class is 
 null.
Given that null references for classes are widely considered a "billion dollar mistake" [1], the comparison does not exactly fill me with confidence. Is there a serious problem with using __type* when you need something nullable, and __type otherwise? It seems like the best of both worlds to me. [1] https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/
Oct 11 2020
next sibling parent Stefan Koch <uplink.coder googlemail.com> writes:
On Sunday, 11 October 2020 at 20:37:56 UTC, Paul Backus wrote:
 On Sunday, 11 October 2020 at 19:45:06 UTC, Stefan Koch wrote:
 ø is a special case that shouldn't happen to often.

 You are free to ignore the possibility of it being null.
 Just like with classes which almost no one checks with class 
 is null.
Given that null references for classes are widely considered a "billion dollar mistake" [1], the comparison does not exactly fill me with confidence. Is there a serious problem with using __type* when you need something nullable, and __type otherwise? It seems like the best of both worlds to me. [1] https://www.infoq.com/presentations/Null-References-The-Billion-Dollar-Mistake-Tony-Hoare/
I am going to give this talk a listen. __type can always be invalid, getting the super type of "object" or "int" for example would yield a type which is not a type. I could have them return __type* .... I need to experiment with this.
Oct 11 2020
prev sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On Sunday, 11 October 2020 at 20:37:56 UTC, Paul Backus wrote:
 On Sunday, 11 October 2020 at 19:45:06 UTC, Stefan Koch wrote:
 ø is a special case that shouldn't happen to often.

 You are free to ignore the possibility of it being null.
 Just like with classes which almost no one checks with class 
 is null.
Given that null references for classes are widely considered a "billion dollar mistake" [1], the comparison does not exactly fill me with confidence.
Is that really a valid comparison, though? Doesn't the issue with null references for classes stem from memory safety concerns? I don't quite see how that applies in the case of types, any more than NaN is a safety issue for floating point numbers.
Oct 12 2020
parent reply Paul Backus <snarwin gmail.com> writes:
On Monday, 12 October 2020 at 07:57:11 UTC, Joseph Rushton 
Wakeling wrote:
 On Sunday, 11 October 2020 at 20:37:56 UTC, Paul Backus wrote:
 Given that null references for classes are widely considered a 
 "billion dollar mistake" [1], the comparison does not exactly 
 fill me with confidence.
Is that really a valid comparison, though? Doesn't the issue with null references for classes stem from memory safety concerns? I don't quite see how that applies in the case of types, any more than NaN is a safety issue for floating point numbers.
The issue with null references is not related to memory safety. NullPointerException in Java is not a memory-safety error, for example. The issue with nullable references is that you have to check every reference for null before you use it, or your program will crash. By contrast, NaN will not crash your program if you forget to check for it before using it in an expression.
Oct 12 2020
next sibling parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 14:11:22 UTC, Paul Backus wrote:
 By contrast, NaN will not crash your program if you forget to 
 check for it before using it in an expression.
That depends. It is not uncommon to have two sets of floating point operations with/without exceptions. You also have something called signalling NaN (sNaN). Anyway, the correctness issues in floating point expressions are quiet complicated in reality.
Oct 12 2020
prev sibling parent reply Joseph Rushton Wakeling <joseph.wakeling webdrake.net> writes:
On Monday, 12 October 2020 at 14:11:22 UTC, Paul Backus wrote:
 The issue with null references is not related to memory safety. 
 NullPointerException in Java is not a memory-safety error, for 
 example. The issue with nullable references is that you have to 
 check every reference for null before you use it, or your 
 program will crash.

 By contrast, NaN will not crash your program if you forget to 
 check for it before using it in an expression.
Right. I'm just not sure I follow why the ø Stefan is defining wouldn't behave more like NaN than a null pointer.
Oct 12 2020
parent reply Paul Backus <snarwin gmail.com> writes:
On Monday, 12 October 2020 at 14:46:14 UTC, Joseph Rushton 
Wakeling wrote:
 On Monday, 12 October 2020 at 14:11:22 UTC, Paul Backus wrote:
 The issue with null references is not related to memory 
 safety. NullPointerException in Java is not a memory-safety 
 error, for example. The issue with nullable references is that 
 you have to check every reference for null before you use it, 
 or your program will crash.

 By contrast, NaN will not crash your program if you forget to 
 check for it before using it in an expression.
Right. I'm just not sure I follow why the ø Stefan is defining wouldn't behave more like NaN than a null pointer.
Since ø is not a type, I assume that you will get an error if you try to use it for anything that requires a type--for example, declaring a variable, or asking for its .sizeof. If this is not the case, I invite Stefan to correct me.
Oct 12 2020
parent reply Stefan Koch <uplink.coder googlemail.com> writes:
On Monday, 12 October 2020 at 15:03:07 UTC, Paul Backus wrote:
 On Monday, 12 October 2020 at 14:46:14 UTC, Joseph Rushton 
 Wakeling wrote:
 On Monday, 12 October 2020 at 14:11:22 UTC, Paul Backus wrote:
 The issue with null references is not related to memory 
 safety. NullPointerException in Java is not a memory-safety 
 error, for example. The issue with nullable references is 
 that you have to check every reference for null before you 
 use it, or your program will crash.

 By contrast, NaN will not crash your program if you forget to 
 check for it before using it in an expression.
Right. I'm just not sure I follow why the ø Stefan is defining wouldn't behave more like NaN than a null pointer.
Since ø is not a type, I assume that you will get an error if you try to use it for anything that requires a type--for example, declaring a variable, or asking for its .sizeof. If this is not the case, I invite Stefan to correct me.
You cannot create a variable of type ø. ø myVar; is invalid. You cannot ø as a returnType or as a parameter type. So a functiondeclatation like ø fn(int x) or int fn(ø x) is invalid. But you can ask for it's size. ø.sizeof == 0. For it's members __traits(allMembers, ø) == [] .... And I think that's all of the introspection I currently support. __traits(getAttributes) is currently not available anymore as I need to define, a type which can hold anything (and not just types) for that to work.
Oct 12 2020
next sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 15:10:55 UTC, Stefan Koch wrote:
 ø.sizeof == 0.
 For it's members
 __traits(allMembers, ø) == []
 ....
 And I think that's all of the introspection I currently support.

 __traits(getAttributes) is currently not available anymore as I 
 need to define, a type which can hold anything  (and not just 
 types) for that to work.
I think you need to ask yourself why you need this? You can also look at how other languages do type variables. One clean solution is to bind them to Object and subclasses of Object, but since Object is not a subtype of all D types you could use __bottom__. I don't really see a good argument for why __bottom__ cannot be used? You cannot instantiate __bottom__. If you went for something more generic like AST-node pointers then it would make sense, but then you could just go with null... basically representing "is waiting for a value" or "under construction". But then you also need to figure out if you want to represent incomplete types.
Oct 12 2020
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 15:44:44 UTC, Ola Fosheim Grøstad 
wrote:
 One clean solution is to bind them to Object and subclasses of 
 Object, but since Object is not a subtype of all D types you
supertype...
Oct 12 2020
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
But in general, I would just have made "type" a reference/pointer 
to a virtual object which an hierarchy along the lines of:

CompilerNode :> CompilerType

By virtual object I mean an object that does not have to exist in 
memory. Kinda like DOM objects in the browser.

Then you can later introduce

CompilerNode :> ASTNode

ASTNode does not have to correspond to what the compiler does 
internally.
Oct 12 2020
parent Stefan Koch <uplink.coder googlemail.com> writes:
On Monday, 12 October 2020 at 16:03:58 UTC, Ola Fosheim Grøstad 
wrote:
 But in general, I would just have made "type" a 
 reference/pointer to a virtual object which an hierarchy along 
 the lines of:

 CompilerNode :> CompilerType

 By virtual object I mean an object that does not have to exist 
 in memory. Kinda like DOM objects in the browser.

 Then you can later introduce

 CompilerNode :> ASTNode

 ASTNode does not have to correspond to what the compiler does 
 internally.
That would never be merged though. which is why I only expose that which is already exposed thorough template means.
Oct 12 2020
prev sibling parent Q. Schroll <qs.il.paperinik gmail.com> writes:
On Monday, 12 October 2020 at 15:10:55 UTC, Stefan Koch wrote:
 You cannot create a variable of type ø.
 ø myVar; is invalid.
 You cannot ø as a returnType or as a parameter type.
 So a functiondeclatation like ø fn(int x) or int fn(ø x) is 
 invalid.

 But you can ask for it's size.
 ø.sizeof == 0.
 For it's members
 __traits(allMembers, ø) == []
 ....
 And I think that's all of the introspection I currently support.

 __traits(getAttributes) is currently not available anymore as I 
 need to define, a type which can hold anything  (and not just 
 types) for that to work.
As I understand it, the NaN of types (call it NaT, not a type) is only vaguely similar to NaN in the regard that is(NaT == NaT) would return false. NaT's only purpose is to be __type.init because __type.init is needed. For that matter, __type.init could be int, but there are reasons not to do that; the same as there are reasons not to make double.init 0.0, but double.nan. Having a __type.init that, for all intents and purposes is a type, i.e. __type.init binds to type-parameters in templates, but whenever it bubbles up to the point of an `is` expression or the point where the type is used, it will be special cased so that to the user it appears as it just isn't a type. In that way, it would be totally different from a bottom type. A bottom type will always look like a type to the user. Making __type.init be __bottom is on par with making it int. To be honest, __type.init does not even need a name; it could be referred to by `__type.init` similar to `typeof(null)` hasn't a name. You could alias it, sure. However, I'm not entirely convinced that making is(NaT == NaT) return false is a good idea. It makes things complicated and confuses the heck out of meta-programmers when debugging stuff. Just make NaT a type. "Using" it computationally, i.e. getting its .init, declaring a variable of it, make a function return values from it, that would be an error because the type doesn't actually exist. (Mathematically speaking, the bottom type is the empty set. You can ask if some potential element is in a type; for the bottom type, the answer is no every time. But __type.init isn't a real type. The question if something is an element of __type.init makes no sense. In that regard, __type.init kind of is like an element of the empty set: It does not exist! Still we can "let x be an element of the empty set" and talk about x. But that x cannot have a value.) Because types must be resolved at compile-time (versus values that are resolved at run-time), double's NaN has to be dealt with in the running program. It would be great if double.init would be NaN, but the magical compiler could keep that value from ever be part of a running program rendering it unnecessary to realize NaN in the machine. However, we can do that with NaT. The programmer may have to deal with NaT on the meta-level, but the meta-resolved program *must* be free of it, otherwise it's an error. (In all the suggestions, having a bottom type meant that declaring a variable of it is equivalent to assert(0);. This is a huge difference. The bottom type is realized and this is part of its semantics.)
Oct 12 2020
prev sibling next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
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));
Oct 11 2020
prev sibling next sibling parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
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.

 [...]
You have a typo here: But Ø cannot be ⊥, because ⊥ can be a valid return type The empty type cannot be a return type
Oct 11 2020
parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:
 The empty type cannot be a return type
It can be a return type, but you probably meant that a function with a bottom type as a return value does to return normally. A function that always returns by exception would have a bottom type as the return type.
Oct 12 2020
next sibling parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 12 October 2020 at 08:52:22 UTC, Ola Fosheim Grøstad 
wrote:
 On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:
 The empty type cannot be a return type
It can be a return type, but you probably meant that a function with a bottom type as a return value does to return normally. A function that always returns by exception would have a bottom type as the return type.
"A function whose return type is bottom cannot return any value, not even the zero size unit type. Therefore a function whose return type is the bottom type cannot return."
Oct 12 2020
next sibling parent Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 12 October 2020 at 11:55:38 UTC, Imperatorn wrote:
 On Monday, 12 October 2020 at 08:52:22 UTC, Ola Fosheim Grøstad 
 wrote:
 On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:
 The empty type cannot be a return type
It can be a return type, but you probably meant that a function with a bottom type as a return value does to return normally. A function that always returns by exception would have a bottom type as the return type.
"A function whose return type is bottom cannot return any value, not even the zero size unit type. Therefore a function whose return type is the bottom type cannot return."
https://docs.python.org/3/library/typing.html#typing.NoReturn https://kotlinlang.org/api/latest/jvm/stdlib/kotlin/-nothing.html https://doc.rust-lang.org/std/primitive.never.html
Oct 12 2020
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 11:55:38 UTC, Imperatorn wrote:
 "A function whose return type is bottom cannot return any 
 value, not even the zero size unit type. Therefore a function 
 whose return type is the bottom type cannot return."
It does not return using the normal path is what they mean, so the expression takes no value.
Oct 12 2020
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 12:10:39 UTC, Ola Fosheim Grøstad 
wrote:
 On Monday, 12 October 2020 at 11:55:38 UTC, Imperatorn wrote:
 "A function whose return type is bottom cannot return any 
 value, not even the zero size unit type. Therefore a function 
 whose return type is the bottom type cannot return."
It does not return using the normal path is what they mean, so the expression takes no value.
Please note that the bottom type as a return type does not describe what the function does. It describes what the type of the expression is at the call-site.
Oct 12 2020
prev sibling parent reply Imperatorn <johan_forsberg_86 hotmail.com> writes:
On Monday, 12 October 2020 at 08:52:22 UTC, Ola Fosheim Grøstad 
wrote:
 On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:
 The empty type cannot be a return type
It can be a return type, but you probably meant that a function with a bottom type as a return value does to return normally. A function that always returns by exception would have a bottom type as the return type.
Yes. But to be obnoxiously technical, it depends on the interpretation of constructive vs classical logic https://www.google.com/url?sa=t&source=web&cd=&ved=2ahUKEwjg4tKDuq_sAhXu-SoKHTk8B8AQFjAAegQIAxAB&url=https%3A%2F%2Fwww.cl.cam.ac.uk%2F~tgg22%2Fpublications%2Fpopl90.pdf&usg=AOvVaw2-3Zw1cFaj12LRblFfcgvL But yes.
Oct 12 2020
parent Abdulhaq <alynch4047 gmail.com> writes:
On Monday, 12 October 2020 at 16:29:16 UTC, Imperatorn wrote:
 On Monday, 12 October 2020 at 08:52:22 UTC, Ola Fosheim Grøstad 
 wrote:
 On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:
 The empty type cannot be a return type
It can be a return type, but you probably meant that a function with a bottom type as a return value does to return normally. A function that always returns by exception would have a bottom type as the return type.
Yes. But to be obnoxiously technical, it depends on the interpretation of constructive vs classical logic https://www.google.com/url?sa=t&source=web&cd=&ved=2ahUKEwjg4tKDuq_sAhXu-SoKHTk8B8AQFjAAegQIAxAB&url=https%3A%2F%2Fwww.cl.cam.ac.uk%2F~tgg22%2Fpublications%2Fpopl90.pdf&usg=AOvVaw2-3Zw1cFaj12LRblFfcgvL But yes.
I'm wondering if brain exploding comments should have the title prefixed with [BE] .....
Oct 12 2020
prev sibling parent reply Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
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.
Oct 12 2020
parent Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= <ola.fosheim.grostad gmail.com> writes:
On Monday, 12 October 2020 at 08:13:57 UTC, Ola Fosheim Grøstad 
wrote:
 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"...
In case it wasn't clear. A bottom type contains no values, so it cannot contain bottom values...
Oct 12 2020