Bottom Type--Type Theory

[Paul Backus]

On Thursday, 17 January 2019 at 13:20:20 UTC, Olivier FAURE wrote:
> On Thursday, 17 January 2019 at 12:40:18 UTC, H. S. Teoh wrote:
>> No! A unit type is one inhabited by a single value. A top type 
>> is a type that can represent *every* value.  Very crudely 
>> speaking, if types were numbers, then a unit type is 1, a 
>> bottom type is 0, and a top type is infinity. Or, to use a set 
>> analogy, a unit type corresponds with a singleton set, a 
>> bottom type to the empty set (the subtype of every type), and 
>> the top type to the universal set (the supertype of every 
>> type).
>
> 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)

It's the other way around--there are things you can do in `foo` 
that you can't do in `bar`.

For example, you can compare two instances of Unit using `==` 
(and in fact such a comparison will always evaluate to true, 
since all instances of Unit have, by definition, the same value). 
However, you cannot compare two instances of Top using `==`, 
because there are types in D that have `@disable opEquals`, and 
Top is a supertype of those types.