DIP 1017--Add Bottom Type--Final Review

[H. S. Teoh]

On Fri, Jan 18, 2019 at 12:54:52AM +0000, Jonathan Marler via Digitalmars-d wrote:
> On Thursday, 17 January 2019 at 22:33:35 UTC, H. S. Teoh wrote:
> > On Thu, Jan 17, 2019 at 09:43:52PM +0000, Jonathan Marler via
> > Digitalmars-d wrote:
[...]
> > > That's conceptually the same thing.  Saying that TBottom* is
> > > "always equal to null" is the same as saying it's a Unit Type,
> > > which is the same as saying that it contains no information so the
> > > storage needed is 0 (same as void).
> > 
> > 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.
[...]
> You're mixing up what you know about programming languages like C/C++
> and D with type theory.  TBottom* by definition is a unit type.  It is
> a pointer to nothing, which can only ever have one value.  It may not
> "seem" like a unit type, but when you spend enough time in set theory
> and logic you'll find most things are not what they seem.
[...]

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.  And
indeed,

	struct C { }

is distinct from:

	struct D { }

in spite of both C and D being, ostensibly, "unit types".

Similarly:

	enum E1 { A }

is distinct from

	enum E2 { A }

even though they are supposedly "unit types" inhabited by the same,
identical value.  (Well, actually they are logically distinct values,
E1.A and E2.A according to the language spec, even if they are
represented in machine code as the same integer value 0, and even if
they are the only value of their respective types.)

So the mapping from the concepts of type theory to D is not as
straightforward as it might appear at first glance -- at least not if
you want to retain any semblance of backward compatibility. You could, I
suppose, gut the entire existing system and replace it with something
directly derived from type theory, with a single, unique unit type that
encompassess all unit types in the language. But that would also
basically break all D code in existence, which makes it not a viable
approach.

At the very least, to account for the distinctness of differently-named
(D) types with identical contents you'd have to decorate the
(type-theoretic) type with some kind of distinguishing feature, such as
something that encodes the name of the struct / enum.  Once you have
that, it's not so unreasonable to also say that pointer types are
inherently distinct from non-pointer types, even if a particular pointer
type happens to only ever allow 1 value, just as a particular
non-pointer type also only ever allows 1 value.  Nothing dictates that
this single value must be the same value across the two types (I could
have `enum F { A=1 }` and `enum G { A=2 }` for example).  There may
exist multiple unit types that are not necessarily compatible with each
other.

Which makes the idea of Tbottom* and void being distinct types a
definite, well-founded possibility.  (Though whether or not it's a good
idea remains to be seen.)


T

-- 
Without outlines, life would be pointless.