On Fri, Jan 18, 2019 at 01:04:58AM +0000, Q. Schroll via Digitalmars-d wrote:
> On Thursday, 17 January 2019 at 22:13:13 UTC, H. S. Teoh wrote:
> > [...]
> > This also lets us write sanity-checking expressions such as:
> > 
> > 	float sqrt(float x) {
> > 		return (x >= 0.0) ? ... /* implementation here */
> > 			: Bottom.init;
> > 	}
> > 
> > This is valid since Bottom converts to any type. Then at runtime, if x < 0.0, assert(0) gets triggered.
> 
> While unrelated to the DIP discussion, I will insist that x >= 0.0 and x < 0.0 can both be wrong: x can be NaN.

`NaN >= 0.0` evaluates to false, so the assert will still trigger.


T

-- 
English is useful because it is a mess. Since English is a mess, it maps well onto the problem space, which is also a mess, which we call reality. Similarly, Perl was designed to be a mess, though in the nicest of all possible ways. -- Larry Wall

On 1/17/2019 2:13 PM, H. S. Teoh wrote:
> Nice, well-rounded-out semantics.

I'm loving this discussion!

On Friday, 18 January 2019 at 01:46:10 UTC, Walter Bright wrote:
> On 1/17/2019 2:13 PM, H. S. Teoh wrote:
>> Nice, well-rounded-out semantics.
>
> I'm loving this discussion!

This is draft-review level discussion, not final review discussion.

On Friday, 18 January 2019 at 01:31:47 UTC, H. S. Teoh wrote:
> I don't argue that it's not a unit type.  But that's not the same thing as saying it's *the* unit type.  There may be multiple, distinct unit types, because D types are not structural types in the type theoretic sense; for example:
>
> 	struct A { int x; }
>
> is a distinct type from:
>
> 	struct B { int x; }
>
> in spite of being identical product types according to type theory.

The official term for this is "nominal typing" [1]. In a nominally-typed language, it is perfectly normal for there to be many distinct types that are structurally identical. In fact, the entire *point* of a nominal type system is to allow the programmer to distinguish between types that are structurally identical. For example, without nominal typing, it would be impossible to write code like this:

struct XY { double x, y; }
struct Polar { double r, theta; }

Polar xyToPolar(XY src) {
    return PolarCoords(
        sqrt(src.x^^2 + src.y^^2),
        atan2(src.y, src.x)
    );
}

// In a structurally-typed language, this assertion would fail
assert(!__traits(compiles, xyToPolar(Polar(1, 3.14))));

The downside of a nominal type system is, as you've noticed, that one cannot speak of "the" unit type, or indeed "the" type with any particular structure.

However, even if there are many possible unit types in D, that does not mean we cannot single one out for special treatment--indeed, we *do* single one out, already. `void`, in its role as a function return type, is different from all other (structurally-equivalent) unit types in that it is the only one that can be returned implicitly:

struct Unit {}

void foo() { return; } // Implicitly, `return void();`
Unit bar() { return Unit(); } // Can't just write `return;` here

So, even though `void` is not "the" unit type in the sense of uniqueness, it is still "special" in a way that no other unit type in D is.

Another way to think of it is that, in a nominally-typed language, it is not enough for "the" unit type (if such a thing is to exist) to have a canonical structure. It must also have a canonical *name*.

[1] https://en.wikipedia.org/wiki/Nominal_type_system

On Fri, Jan 18, 2019 at 03:55:40AM +0000, Paul Backus via Digitalmars-d wrote:
> On Friday, 18 January 2019 at 01:31:47 UTC, H. S. Teoh wrote:
> > I don't argue that it's not a unit type.  But that's not the same thing as saying it's *the* unit type.  There may be multiple, distinct unit types, because D types are not structural types in the type theoretic sense; for example:
> > 
> > 	struct A { int x; }
> > 
> > is a distinct type from:
> > 
> > 	struct B { int x; }
> > 
> > in spite of being identical product types according to type theory.
> 
> The official term for this is "nominal typing" [1]. In a nominally-typed language, it is perfectly normal for there to be many distinct types that are structurally identical. In fact, the entire *point* of a nominal type system is to allow the programmer to distinguish between types that are structurally identical.

Thank you. That's the gist of it.


[...]
> The downside of a nominal type system is, as you've noticed, that one cannot speak of "the" unit type, or indeed "the" type with any particular structure.
> 
> However, even if there are many possible unit types in D, that does not mean we cannot single one out for special treatment--indeed, we *do* single one out, already. `void`, in its role as a function return type, is different from all other (structurally-equivalent) unit types in that it is the only one that can be returned implicitly:
[...]
> Another way to think of it is that, in a nominally-typed language, it is not enough for "the" unit type (if such a thing is to exist) to have a canonical structure. It must also have a canonical *name*.
[...]

So now we're clearer about what exactly is involved here.  If we want to "clean up" the "messy" meaning of `void`, we should first recognize that it's an overloaded keyword with at least 3 or 4 different meanings:

1) A unit type -- in the context of a function return type.

2) A bottom type -- in the context of a variable declaration, which makes said declaration illegal (though this latter point is not mandatory and could possibly be altered as part of introducing an explicit bottom type to D).

3) The top type -- when used in its pointer form as void*, where it really means Any* where Any is the top type.

4) An uninitialized value -- when used in variable declarations of the form `T x = void;`.

So in some sense, D already *has* a distinguished unit type, a bottom type (of sorts), and even a top type. (For our purposes, (4) is not really relevant.)  It's just that they are currently not treated as first-class citizens, and therefore can only be used in certain, constrained contexts, and cannot be freely combined with other types as one might desire to.  Our "arithmetic system", so to speak, already has the necessary concepts of 0, 1, and infinity, but they are just inconsistently lumped together under a single name and consequently arbitrarily restricted.

So the course of action seems quite obvious, at least at a high level:

a) Rename the various usages of `void` into distinct names reflecting their actual meaning;

b) Remove the arbitrary restrictions on their usage.

We cannot do (b) before doing (a), because it will end up with a mess where `void` means multiple things in the *same* context, which is unworkable. (And besides, continuing to use `void` only prolongs the conflation of incompatible concepts in users' minds, which will only lead to misunderstanding and wrong usage -- i.e., bad UI design.)

Of course, there's a lot of details omitted in this simple plan of action.  Before we can remove the restrictions on the unit / top / bottom types, we better be clear exactly what kind of semantics we expect when we combine them with other types in the existing system. We have to worry about backward-compatibility, migration schedules, and so on.  It will be a pretty big change, more than what the DIP in question appears to be suggesting.


T

-- 
Right now I'm having amnesia and deja vu at the same time. I think I've forgotten this before.

On Thursday, 17 January 2019 at 09:24:26 UTC, Walter Bright wrote:
> On 1/16/2019 8:52 PM, Johannes Loher wrote:
>> 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?
>
> Too much water under that bridge.

I suppose `bottom`, `top`, and `unit` types can be added to the language while maintaining current `void` semantics.  Then, in time, the uses of `void` masquerading as `bottom`, `top`, and `unit` will diminish to a point where it wouldn't be all that disruptive to deprecate it.  This just needs someone with the skill and time to implement it, which is probably the real blocker.

Mike

On Sat, Jan 19, 2019 at 03:40:57AM +0000, Mike Franklin via Digitalmars-d wrote:
> On Thursday, 17 January 2019 at 09:24:26 UTC, Walter Bright wrote:
> > On 1/16/2019 8:52 PM, Johannes Loher wrote:
> > > 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?
> > 
> > Too much water under that bridge.
> 
> I suppose `bottom`, `top`, and `unit` types can be added to the language while maintaining current `void` semantics.  Then, in time, the uses of `void` masquerading as `bottom`, `top`, and `unit` will diminish to a point where it wouldn't be all that disruptive to deprecate it.  This just needs someone with the skill and time to implement it, which is probably the real blocker.
[...]

There would have to be some incentive for people to stop writing `void` and `void*` and start writing `top*`, `bottom`, `unit`, though. Otherwise we'll just end up with 3 more keywords that nobody uses cluttering the language.


T

-- 
Long, long ago, the ancient Chinese invented a device that lets them see through walls. It was called the "window".

H. S. Teoh <hsteoh@quickfur.ath.cx> wrote:
> On Thu, Jan 17, 2019 at 09:48:52PM +0100, Johannes Loher via Digitalmars-d wrote: [...]
>> This would still allow things like
>> ```
>> Bottom var = assert(0);
>> ```
> 
> Yes.  Though *why* you'd want to declare a variable of type Bottom -- as
> opposed to just writing the expression of type Bottom -- is a good
> question that I don't have a good answer to.
> [...]

That could be useful in generic code that is instatiated with 'Bottom'

Tobi

On 17.01.19 03:32, Q. Schroll wrote:
> 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.

No, you cannot have _variables_ of this type. There is nothing like this in type theory. If you can't have a variable of a certain "type", it's not a type.

> 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.

No, that has different low-level semantics.

> 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.
> ...

No, this is the "untyped block of memory" usage of 'void'. This does not have a parallel in type theory because _untyped_ and only useful if used in an unsafe manner.

> 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*.

See 2.

On Thursday, 17 January 2019 at 23:05:58 UTC, H. S. Teoh wrote:
> It does lead to other corner cases like structs that contain Bottom fields -- instantiating such a struct should abort at runtime, and void initialization should be illegal -- so this special case is infectious and may lead to increased compiler complexity. OTOH, maybe this complexity can be nipped in the bud by stipulating that any aggregate that contains Bottom reduces to Bottom, i.e., any struct or class that contains a Bottom field will be defined to be Bottom itself (since it would be impossible to create an instance of such a struct or class without also creating an instance of Bottom).

I think this solution would also create its own corner cases.

For instance, if you were to write:

    auto callEach(Functions...)(Functions functions) {
        ReturnTypesOf!Functions returnValues;

        static forearch(i, f; functions) {
            returnValues[i] = f();
        }

        return returnValues;
    }

    // Later...
    auto handleError = () => throw SomeException;
    callEach(&foo, &bar, &handleError);

The function would abort near the beginning with no error message, instead of throwing when handleError is called.

I think there are two solutions to this problem:
- Forbid any aggregate to include a Bottom type, which would severely limit Bottom's use as a first-class type.
- Rework the type system to gracefully handle types with no .init value.

In the second case, Bottom, Bottom[10] and struct Foobar { Bottom x; } would all be legal, distinct types. Their only common point would be that they would all have a "no .init" trait.