On Wednesday, 16 January 2019 at 22:32:33 UTC, Walter Bright wrote:
> The thing is, I know little about formal type theory. As far as I can tell, nobody in this community does either, aside from Timon Gehr.

I shows, the rationale for this DIP as it stands is wafer thin.
You should try to recruit Timon as a co-author and send the whole thing back to draft.
There is zero reason this for the DIP to have got this far through the process.

> Back to the bottom type. C's ability to manipulate types is so primitive nobody misses type calculus. But D can do type calculus, and I worry that the lack of a bottom type, far from creating corner cases, causes corner cases and awkward problems analogous to what the lack of an identity function causes.

Please point me to the section of the DIP where it says this, 'cause I'm not seeing it.
This is an interesting potential  but needs to be discussed in the draft phase.

> The trouble is, I don't know enough about type theory to know if this is the case or not. I only know analogies to problems other systems have when the boundary cases are not expressible.

You need examples to give the DIP any credibility, as it stands the DIP makes two arguments : documentation and optimisation. Both of these exist already for LDC and GDC as attributes and it takes all of _6 lines+ to unify them and make the documentation aspect available to DMD.

> An example of an awkward corner case caused by lack of a bottom type:
>
>    @noreturn int betty();
>
> How can it return an int yet not return? It makes no sense.

Yes that is stupid. Does anyone write it now, given that it is already possible with LDC/GDC? No, because D is a pragmatic language, just because you can write something non-sensical doesn't mean that anyone will, especially when you have to go out of your way to do it.
_We shouldn't be designing around the fact that you can do stupid things_.

>And
> if one was doing type calculus on the return value of betty(), it would show up as 'int' and botch everything up.

First of all, the return type would canonically be void, not int (if you've gone out of your way to do something stupid  its your fault).
Second, I suspect the frequency of functions that always never return are a minute fraction of the total functions of a program, who is .
Third even if bottom coverts to everything else functions of bottom won't, so, from what I can see that breaks a lot of its supposed advantages anyway.
Finally, the addition of bottom its going to botch up a whole lot of existing code that isn't expecting it/doesn't care about it.

> The trouble with 'void' as a bottom type is it is only half done. For example, 'void' functions are procedures, and certainly do return. A void* is certainly a pointer to something, not nothing. 'void' is the one with awkward corner cases, it's just we're so used to them we don't see them, like few C++ people recognized the identity function problem.

Links please?

> My trouble explaining the immediate value of a bottom type stems from my poor knowledge of type theory. Other languages aren't necessarily good role models here, as few language designers seem to know much about type calculus, either. I was hoping that someone who does understand it would help out!
>
> (I.e. it's not just about functions that don't return. That's just an obvious benefit.)

That DIP doesn't make that point at all! If you don't know what you're talking about, you should find out _before_ you waste everyones time reviewing it!

This whole DIP needs to be sent back to draft. You need to come up with convincing ideas as to why a type is _practically_ more useful than an attribute that takes into account the fact that the claimed benefits already exist and that the implementation, learning curve and other external costs don't outweigh doing it.

On Thu, Jan 17, 2019 at 12:44:32AM +0000, Nicholas Wilson via Digitalmars-d wrote:
> On Wednesday, 16 January 2019 at 22:32:33 UTC, Walter Bright wrote:
[...]
> > An example of an awkward corner case caused by lack of a bottom type:
> > 
> >    @noreturn int betty();
> > 
> > How can it return an int yet not return? It makes no sense.
> 
> Yes that is stupid. Does anyone write it now, given that it is already possible with LDC/GDC? No, because D is a pragmatic language, just because you can write something non-sensical doesn't mean that anyone will, especially when you have to go out of your way to do it.

Actually, there *are* some cases where people might try to write something like this (not saying it's a good idea, but it's not as crazy as it might sound at first). To wit:

	// thirdpartylib.d
	class Base {
		int method() { ... }
	}

	// usercode.d
	class Derived : Base {
		override int method() {
			throw new Exception("Not implemented yet");
		}
	}

You cannot write Derived.method as void, because then it wouldn't override Base.method.


[...]
> > My trouble explaining the immediate value of a bottom type stems from my poor knowledge of type theory. Other languages aren't necessarily good role models here, as few language designers seem to know much about type calculus, either. I was hoping that someone who does understand it would help out!
> > 
> > (I.e. it's not just about functions that don't return. That's just
> > an obvious benefit.)
> 
> That DIP doesn't make that point at all! If you don't know what you're talking about, you should find out _before_ you waste everyones time reviewing it!
> 
> This whole DIP needs to be sent back to draft. You need to come up with convincing ideas as to why a type is _practically_ more useful than an attribute that takes into account the fact that the claimed benefits already exist and that the implementation, learning curve and other external costs don't outweigh doing it.

Yeah, how did this DIP get so far when it's standing on such shaky foundations?  Shouldn't somebody of Timon's calibre have been recruited to iron out the kinks before "final review"? Actually, this should have been done for the *initial* draft.  This DIP as it stands is far too crude and incomplete to be this far along in the process.


T

-- 
Tech-savvy: euphemism for nerdy.

On 1/16/2019 3:11 PM, luckoverthere wrote:
> So you want to add something you don't fully understand and aren't sure if there is even any benefit at all. You just presume there to be a benefit? I don't think you should think of void and void* as the same thing. Pointers are their own type, if all you have is a void* and no other information, you might as well be pointing at nothing. I suggest you figure out what it is you actually want to implement, this is no better than cowboy programming. Hell might even be worse than a pilot wearing a blindfold with someone whispering in his ear that he is going the right direction. Don't implement something you obviously don't know enough about. I can only imagine what kind of disaster this is going to be in comparison to auto-encoding.

A fair point, though the rudeness is disappointing. I'd appreciate help with it. I hope this DIP stimulates something more positive than excoriation. Consider it a challenge!

On 1/16/2019 2:59 PM, Dukc wrote:
> Isn't `void` in fact analogous to the TOP type? With a bit additional features, it could be used as one, as I understand it.

I think H.S. Teoh's reply helps with that. 'void' is symptomatic of poor design inherited from C along with my non-CS background.

My interest in a bottom type comes from wanting a sounder mathematical basis for types in D, but sadly nobody else seems interested, and this DIP is pretty much DOA.

On 1/16/2019 5:21 PM, H. S. Teoh wrote:
> Yeah, how did this DIP get so far when it's standing on such shaky
> foundations?  Shouldn't somebody of Timon's calibre have been recruited
> to iron out the kinks before "final review"?

The idea originally came up here:
https://digitalmars.com/d/archives/digitalmars/D/proposed_noreturn_attribute_303875.html

Timon was asked:
https://digitalmars.com/d/archives/digitalmars/D/proposed_noreturn_attribute_303875.html

There's a fair amount of good commentary from Timon about it, he's obviously the right person to write the DIP.

On Thursday, 17 January 2019 at 01:45:13 UTC, Walter Bright wrote:
> On 1/16/2019 2:59 PM, Dukc wrote:
>> Isn't `void` in fact analogous to the TOP type? With a bit additional features, it could be used as one, as I understand it.
>
> I think H.S. Teoh's reply helps with that. 'void' is symptomatic of poor design inherited from C along with my non-CS background.

OTOH, it gets us easy compatibility and familiarity.

> My interest in a bottom type comes from wanting a sounder mathematical basis for types in D, but sadly nobody else seems interested, and this DIP is pretty much DOA.

Its not that we're not interested, its that the DIP needs to show tangible practical benefits (which are low) that clearly outweigh the risks and costs (which are very high), and shows clear benefits relative to the other solutions to the problems (which already exist), which it doesn't.

If this DIP is DOA, how has it managed to get all the way to final review? It should either be dropped, or still be in draft.

On Tuesday, 15 January 2019 at 16:23:57 UTC, Timon Gehr wrote:
> [...]
> It makes little sense to define a type "void" that has "no values" and then say "but as a special case, a function with return type void is a procedure instead", because you can just have a unit type. The whole "variables cannot be of type void"-nonsense is also nothing but annoying.

The void type is one of *three* type-theoretically different types:
1. For any variables (local, parameter, field, ...), it *is* the bottom type: You cannot have values of it.
2. For function returns, it is a unit type. In D, we have another one: typeof(null). In fact, we could deprecate void returning functions and use typeof(null) instead.
3. For pointer (i.e. void*) (and arrays (void[n]) and slices (void[])), void is neither of the above. It's rather a top type (or any, or unknown in TypeScript) which can hold any value. As it is with Object, you cannot do anything (meaningful) with it without explicit downcast.

This is not new -- it's inherited from C. If we get a bottom type, void in the sense of 2. can be defined as void = bottom*.

On Thursday, 17 January 2019 at 00:41:54 UTC, Jonathan Marler wrote:
> On Thursday, 17 January 2019 at 00:09:50 UTC, H. S. Teoh wrote:
>> On Wed, Jan 16, 2019 at 02:32:33PM -0800, Walter Bright via Digitalmars-d wrote: [...]
>>> [...]
>> [...]
>>
>> Actually, the *real* problem with `void` is that it has been overloaded to mean multiple, context-dependent things that are somewhat but not really the same, and aren't really compatible with each other.
>>
>> [...]
>
> A good summary of the issues with void. Maybe adding a bottom type enables some new clever semantics, but I would venture to guess that adding a real unit type would be even more helpful than a bottom type. I've had cases where being able to use void as a function parameter or a field would have made some of my templates much cleaner. Maybe we should focus on making void a real unit type before we try to add a bottom type?

D has a couple of different unit types which all behave differently:

typeof(null), its sole value being null. It also happens to be the bottom type for all objects, pointers and arrays.


void, which actually *does* have a single value - you just can't declare a variable with type void:

void main()
{
    auto v = new void[1];
    pragma(msg, typeof(v[0])); // Prints "void"
    import std.stdio;
    writeln(v[0]); // Error: template std.stdio.writeln cannot deduce function from argument types !()(void)
}

This may actually be a compiler bug/quirk; I'm not completely sure.


Any enum with only 1 element:

enum Unit
{
    val
}

As an aside, the empty enum:

enum Empty
{
}

Is an uninhabited type similar to Bottom, but is not implicitly convertible to any other type, unlike Bottom.


The empty struct:

struct Unit
{
}

Unit u;
writeln(u); // Prints Unit()


And probably more that I have missed.

On Thursday, 17 January 2019 at 00:44:32 UTC, Nicholas Wilson wrote:
> That DIP doesn't make that point at all! If you don't know what you're talking about, you should find out _before_ you waste everyones time reviewing it!

IMO, this tone is uncalled for. Let's all try to be civil and criticize the DIP, not the person.

Am 16.01.19 um 23:32 schrieb Walter Bright:> [...]
> The trouble with 'void' as a bottom type is it is only half done. For example, 'void' functions are procedures, and certainly do return. A void* is certainly a pointer to something, not nothing. 'void' is the one with awkward corner cases, it's just we're so used to them we don't see them, like few C++ people recognized the identity function problem. [...]
In a later post, H. S. Theo describes some of the problems with void in more detail. What is your stance on actually fixing void from a type theoretical perspective? Do you think that is practical?