Bottom Type--Type Theory

[Johannes Loher]

Am 17.01.19 um 19:47 schrieb Olivier FAURE:
> On Thursday, 17 January 2019 at 18:38:54 UTC, Olivier FAURE wrote:
>> For instance, I think it would make sense to call a function `int
>> foobar(void, void)` with as `foobar(1, "abd")`, which is basically the
>> function saying it will ignore these parameters.
> 
> To expand on this, I'm understanding supertyping (at least in D and
> similar languages) as the *discarding* of type information. Eg, A is the
> supertype of B if B has more specific information about what values it
> can hold than A, which means A can accept more different values.
> 
> In that mindset, void seems like the logical top type, because it
> describes no information at all about any value it could hold.

I believe this view of things results directly from the fact that there
are different meanings to `void`. In particular, `void*` is a pointer to
_any_ type, so it is the "top type of all pointer types". If you think
of `void` in the same way, then yes, `void` would be the top type.

However this is not the way `void` works. At the moment `void` signals
"no information" which in type theory is the unit type's responsibility.
Because think about it: Which values should a type that cannot convey
any information hold? Exactly one, otherwise you can have at least two
different values which you can tell apart by looking at them (printing
them, or whatever else you want to do with them). It is true that a top
type can hold values of any type, so naively you'd think that you loose
the original type information and thus it is basically the same as "no
information". But this is not true because the actual values can still
be different at runtime. Also usually a major feature of a top type is
that you can check at runtime what the original type of the variable it
holds is. For an example, take a look std.Variant. It has a `type`
property which returns the typeid of the type it currently holds. (Note
that this is not the case for `void*`: Without remembering, you can't
actually know what type of data a variable of type `void*` points to.)

If we were to fix `void`, we would need to let go of one of those views
as they are inherently incompatible.

One option would indeed be to make `void` a top type. But I don't think
that makes much sense because then we would have to change the meaning
of returning `void` (it would then mean to return anything, not no
information). In my opinion, the interpretation of `void` as "no
information" is its _main_ interpretation and thus the correct way would
be to preserve that meaning and get rid of the other incompatible
meanings, which means that `void` would not a top type but a unit type.

We could even go a completely different route and get rid of the symbol
`void` alltogether in order to not give people who are used to C, C++,
Java, D (and 1000s of other languages which have copied C's _bad_ usage
of void) false ideas.

The last idea is the route that Kotlin went: They don't have a `void`
type. Their unit type is called `Unit`, their bottom type is called
`Nothing` and their top type is called `Any`. The type `Any?` (optional
any, a type that can hold a value of any type or `null`) is very similar
to what our `void*` is at the moment. Similarly, `Nothing?` is basically
the same as our `typeof(null)`.

This is actually quite nice, because it does not result in any wrong
expectations–those types simply don't exist in C, C++, Java etc.

However, all of this does not consider at all how to get
C-interoperability to work. Kotlin is able to work with Java, so maybe
there is actually a chance of getting this to work (though they don't
have to deal with `void*` which makes it a lot easier). Additionally it
means massive breaking changes. Even if there is a way to actually make
it work with C, I still fear that there is simply too much code breakage
for all of this to ever become reality.