digitalmars.D - The NaN of types (in D)
- Stefan Koch (32/32) Oct 11 2020 Good Morning,
- Imperatorn (3/7) Oct 11 2020 Shouldn't this be the universe. The empty set is "there is no _",
- Stefan Koch (13/22) Oct 11 2020 The universe would be __type. (because it can hold any type in U)
- Imperatorn (2/21) Oct 11 2020 Oh, I see. I mis-read the question
- Paul Backus (5/16) Oct 11 2020 To me, this sounds more like an empty Optional!__type or a null
- Stefan Koch (9/27) Oct 11 2020 __type need an init value otherwise phobos breaks all over the
- Imperatorn (2/18) Oct 11 2020 Or have NaT = Not a Type, as NaN
- Paul Backus (9/12) Oct 11 2020 By definition, the init value of a type is part of that type's
- Stefan Koch (6/21) Oct 11 2020 Instantiating a template for just one more additional value?
- Paul Backus (6/11) Oct 11 2020 It doesn't have to be a template; it could be a __type*, or
- Stefan Koch (5/18) Oct 11 2020 ø is a special case that shouldn't happen to often.
- Paul Backus (9/13) Oct 11 2020 Given that null references for classes are widely considered a
- Stefan Koch (6/21) Oct 11 2020 I am going to give this talk a listen.
- Joseph Rushton Wakeling (5/15) Oct 12 2020 Is that really a valid comparison, though? Doesn't the issue
- Paul Backus (9/19) Oct 12 2020 The issue with null references is not related to memory safety.
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (6/8) Oct 12 2020 That depends. It is not uncommon to have two sets of floating
- Joseph Rushton Wakeling (3/10) Oct 12 2020 Right. I'm just not sure I follow why the ø Stefan is defining
- Paul Backus (6/17) Oct 12 2020 Since ø is not a type, I assume that you will get an error if you
- Stefan Koch (15/33) Oct 12 2020 You cannot create a variable of type ø.
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (13/21) Oct 12 2020 I think you need to ask yourself why you need this?
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (3/5) Oct 12 2020 supertype...
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (9/9) Oct 12 2020 But in general, I would just have made "type" a reference/pointer
- Stefan Koch (5/15) Oct 12 2020 That would never be merged though.
- Q. Schroll (45/59) Oct 12 2020 As I understand it, the NaN of types (call it NaT, not a type) is
- Imperatorn (3/7) Oct 11 2020 Btw, wouldn't this be solved if/when DIP1017 is passed?
- Imperatorn (4/8) Oct 11 2020 You have a typo here:
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (5/6) Oct 12 2020 It can be a return type, but you probably meant that a function
- Imperatorn (5/11) Oct 12 2020 "A function whose return type is bottom cannot return any value,
- Imperatorn (4/18) Oct 12 2020 https://docs.python.org/3/library/typing.html#typing.NoReturn
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (3/6) Oct 12 2020 It does not return using the normal path is what they mean, so
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (5/11) Oct 12 2020 Please note that the bottom type as a return type does not
- Imperatorn (6/12) Oct 12 2020 Yes. But to be obnoxiously technical, it depends on the
- Abdulhaq (3/18) Oct 12 2020 I'm wondering if brain exploding comments should have the title
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (28/35) Oct 12 2020 I think you need to find out what you need to prove the semantics
- Ola Fosheim =?UTF-8?B?R3LDuHN0YWQ=?= (4/8) Oct 12 2020 In case it wasn't clear. A bottom type contains no values, so it
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
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
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: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.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
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:Oh, I see. I mis-read the questionOn Sunday, 11 October 2020 at 12:18:59 UTC, Stefan Koch wrote: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.[...]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
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
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:__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.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
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:Or have NaT = Not a Type, as NaNOn Sunday, 11 October 2020 at 12:18:59 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. 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.[...]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
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
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: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.__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
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
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:ø 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.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
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
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: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.ø 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
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 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.ø 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.
Oct 12 2020
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: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.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
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
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
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: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.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
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: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.On Monday, 12 October 2020 at 14:11:22 UTC, Paul Backus wrote: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.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
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
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 yousupertype...
Oct 12 2020
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
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
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
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
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
On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote:The empty type cannot be a return typeIt 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
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:"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."The empty type cannot be a return typeIt 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
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: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.htmlOn Monday, 12 October 2020 at 06:41:26 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."The empty type cannot be a return typeIt 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
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
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: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."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
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: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.The empty type cannot be a return typeIt 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
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:I'm wondering if brain exploding comments should have the title prefixed with [BE] .....On Monday, 12 October 2020 at 06:41:26 UTC, Imperatorn wrote: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.The empty type cannot be a return typeIt 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
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
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