Bottom Type--Type Theory

[H. S. Teoh]

On Thu, Jan 17, 2019 at 01:20:20PM +0000, Olivier FAURE via Digitalmars-d wrote:
[...]
> I think I'm confused.
> 
> Actually, I think I have a pretty good question. Let's imagine we
> implement two types in D, Unit and Top, so that they match their type
> theory concepts as best as they can.
> 
> Given this code:
> 
>     int foo(Unit u) {
>         ...
>     }
> 
>     int bar(Top t) {
>         ...
>     }
> 
> what could you do in `bar` that you couldn't do in `foo`?
> 
> (I'd appreciate if you could answer with pseudocode examples, to help
> communication)

For one thing, Top would be the supertype of every other type, so you
could pass in values of any type to bar:

	bar(123);
	bar("abc");
	bar(null);
	bar(Unit.init);

Whereas the only type that foo will accept is the unique value of Unit:

	foo(Unit.init);

You can't pass anything else to foo, because the only value it accepts
is the unique value of Unit, and nothing else.

As to what you can *do* inside the functions: since Unit has only one
value, every operation on it is vacuous:

	int foo(Unit u) {
		assert(u == u); // always true
		auto v = u;	// basically no-op
		assert(is(typeof(v) == Unit));
		...
		return 0;	// N.B.: cannot return u because Unit
				// does not convert to int (Unit is not
				// a subtype of int).
	}

With Top, the value can literally be *any* type, which means there's
also very little you can actually do with it, because you cannot assume
anything about it -- the only assumptions you can make are those that
are true for *all* types in the language.  You could take its address,
or assign a new value to it (of any type):

	int bar(Top t) {
		Top* p = &t;
		t = 123;
		t = "abc";
		t = null;
		t = Unit.init;
		...
		return 0;	// again, cannot return t, because Top is not
				// a subtype of int (int is a subtype of
				// Top, though, but it doesn't go the
				// other way)
	}

But as to actually operating on the value of t, there's really not much
that can be done, since it encompasses too much, and there are very few
operations that are common to *all* types.

A Top* would be the same as today's void*, in that any pointer
implicitly converts to it:

	int i = 123;
	float x = 1.0;
	string s = "abc";
	Unit u;
	Top* ptr;

	ptr = &i;
	ptr = &x;
	ptr = &s;
	ptr = &u;

Dereferencing ptr would give you a value of type Top, but then, barring
further language support, you wouldn't know which underlying type it is,
so there wouldn't be very much you could meaningfully do with it. This
means that you can't meaningfully assign anything via ptr, for example:

	*ptr = 123; // error: not every type supports opAssign(int)
	*ptr = "abc"; // error: not every type supports opAssign(string)
	... // etc.

Which ultimately makes sense, because we could have gotten ptr from
taking the address of a float, for example, and it would be UB to assign
a string to *ptr.

You could cast the Top* to something else, but that gets into the realm
of implementation-defined behaviour (it could be just UB), and no longer
something under the auspices of type theory.

Basically, Top behaves more-or-less like std.variant.Variant, maybe
excepting some corner cases.


T

-- 
People walk. Computers run.