DIP 1017--Add Bottom Type--Final Review

[H. S. Teoh]

On Thu, Jan 17, 2019 at 11:52:02PM +0100, Johannes Loher via Digitalmars-d wrote:
> Am 17.01.19 um 23:33 schrieb H. S. Teoh:
> > I'm not so sure about that.  A true Unit type conveys no
> > information, yet TBottom* conveys at least this information: that
> > it's a pointer, and that the pointer cannot be dereferenced.  A true
> > Unit type would be the return type of a void function; would you
> > equate TBottom* with the return type of a void function?  That would
> > be very strange indeed.
> 
> I suggested this earlier in this thread, i.e.
> 
> ```
> alias void = Tbottom*;
> ```
> 
> This would make `null` the single value `void`.
> 
> If we were to follow type theory rigorously, we would not even have
> another choice than doing this because all types which have exactly
> one value are naturally isomorphic and this means they are equal from
> a type theory perspective.

This is where I wish someone who actually knows type theory would step
up and clear up the situation, because in my mind, the type system we
have in D contains an inherent, additional layer of complexity beyond
what you're describing, and this is related to what you say below:


> This is not the case in D (in particular while struct A {} and struct
> B {} are of the same type from a rigorous type theory perspective,
> they are not in D). So we don't actually have to do it like this, but
> it would be an option (if we fixed void to be a proper unit type).

I don't think we can realistically force empty structs `struct A {}` and
`struct B {}` to be the same type, because even though they are arguably
both unit types, they can still be distinguished from each other by
name. This distinction is also more than just mere convention; it plays
a crucial role in UDAs, for example:

	struct DontSerialize {}
	struct SerializeAsBytes {}

	struct Data {
		@DontSerialize uint runtimeId;
		@SerializeAsBytes int payload;
	}

If we collapsed both structs into a single Unit type, the UDA mechanism
would completely fall apart.

Furthermore, types in D cannot be identified merely by their constituent
parts.  For example:

	struct CartesianCoors {
		float x;
		float y;
	}

	struct PolarCoors {
		float theta;
		float radius;
	}

Technically, both structs are products of two floats, but that does not
make them the same thing, because the values of their constituent
components are interpreted differently and should not be confused one
for another.

At the very least, it would seem that the *name* of the type plays an
essential role in its identification.  I.e., it's almost as if a struct
declaration is actually defining a type that, in addition to the types
of its fields, contains also an implicit string type identifying the
name of the struct. Or alternatively, we're dealing with a type system
where types are additionally decorated with string identifiers that
distinguish otherwise-identical types from each other.  (Or it could be
that I've no idea what I'm talking about, and this is the consequence of
this community having very few people who actually know type theory
thoroughly enough to be able to work out a sane solution to all of these
issues. :-P)


In any case, coming back to TBottom*, another issue that makes me wary
of defining TBottom* == void is the top pointer `void*`.  Since any
pointer implicitly converts to `void*`, this means TBottom* implicitly
converts to `void*` too, which in turn means `void` should also
implicitly convert to `void*`:

	void procedure(...) { }

	void* ptr = procedure(...); // valid if TBottom* == Unit == void

I think the problems that such a construct would cause would far
outweigh whatever benefits that we may have reaped from introducing Unit
and Bottom types!


T

-- 
Life is complex. It consists of real and imaginary parts. -- YHL