Proposal: Expose `Undefined` type as an occupied bottom type

[Eyas]

Proposal

The TypeScript spec says that Undefined is the subtype of all types (see 3.2.6).

The keyword Undefined or Nothing should be added to the language to refer to the type of undefined.

typeof(undefined) currently yields any. This should be corrected to return the undefined type.

Detail

See http://en.wikipedia.org/wiki/Bottom_type & http://james-iry.blogspot.com/2009/08/getting-to-bottom-of-nothing-at-all.html

The neat thing about structural typing TypeScript is that you don't need to explicitly think about generic type variance. Instead, when you use two generic implementations of non-identical types, then TypeScript uses the input and return types of the different methods and properties to figure out if these two generic types are subtypes or not.

One missing feature, however, seems to be a bottom Nothing/None/Nil type that is a subtype of all types. This then allows us to create neat "empty" types in generic.

[Igorbek]

void is bottom type.

[basarat]

As Igorbek said, this is allowed in TypeScript var foo:void. And Nil would be undefined.

PS: An option type would be different and would require runtime support.

[metaweta]

Types in TypeScript are all occupied types, akin to nonempty sets. The smallest nonempty set is the set with one element, which is both initial and terminal in the category of TypeScript types and functions between them. There are two named types that the spec claims have one element, "Undefined" and "Null"; for some reason, both are unmentionable. 3.2.5 says "Null" is not a subtype of "Undefined". Since, according to 3.2.6,

The "Undefined" type is a subtype of all types.

"Undefined" has the only claim in the spec to being the bottom type, though this conflicts with 3.2.5's assertion that there is only one value of type "Null", namely null; if the statement above from 3.2.6 is true, "Null" has two values, undefined and null. If instead each type has only one element, then there is no unique bottom type---but the universal property of the initial object only holds up to isomorphism, so both the "Undefined" type and the "Null" type could be called bottom.

The "Void" type, strangely, has two elements, the value undefined and the value null, and is a supertype of "Null" and "Undefined", so "Void" can't be the bottom type. Despite being a subtype of all mentionable types, the "Void" type is treated as though it weren't a subtype of anything except "Any" to to avoid mistakes where the programmer forgets to return a value.

It would be convenient to have the bottom type be mentionable for use in generics. The fact that undefined is a valid value for all types makes the sets not only nonempty, but pointed. It would be nice, from a type theory perspective, to have language support for pointed functions, but exceptions are more practical.

If there were an unoccupied type (say, empty), any function of type empty would have to fail to return at all: the only function into the empty set is the identity function on the empty set. For the compiler to typecheck that a function's return value was of type empty, the compiler would need to prove that the function either goes into an infinite loop or throws an exception. The wikipedia article describes this notion of bottom type, which does not apply to TypeScript.

I propose that 3.2.6 be altered so that the "Undefined" type can be mentioned in generics to allow e.g. functions that explicitly return undefined. I also propose that the "Null" type be removed, since it's either redundant with "Undefined" or with "Void".

[Eyas]

@basarat: I'm mainly referring to a user-defned Option generic type. The parameter there doesn't seem to work. It potentially fails because typescript doesn't accept void function arguments, perhaps?

I'm glad void is indeed seen as the bottom type, but the use case I provide doesn't seem to work with void, at least the 1.1 compiler complained about putting void there.

[metaweta]

There doesn't seem to be any mentionable type one can give to baz below that will pass the type checker.

function baz() { return undefined; }
var s:string = baz();
var t:number = baz();

By explicitly returning undefined, baz has the "Undefined" type; if the return statement is elided, it will be typed as "Void", which causes the type checker to complain.

[Eyas]

It also should be clearly noted that void already doesn't behave as a bottom type in all contexts.

function vf(): void {}
var sf: ()=>string = vf;

If void is a subtype of string, then structural typing implies that this should compile. However, the compiler indeed gives us a type error here.

As @metaweta said, function uf() /* : no mentionable type available */ { return undefined; } works.

[RyanCavanaugh]

typeof undefined is indeed the bottom type; see 3.10.3 in the spec ("S is a subtype of a type T [...] if [...] S is the Undefined type.").

In 1.4 you'll be able to write type undefined = typeof undefined; to make a user-defined alias for the Undefined type. Can you post a few examples of how you might use this in practice? Without generic specialization or runtime type information, I'm not clear on how this would be useful.

[Igorbek]

typeof undefined is inferred as any at the moment:

var x: typeof undefined; // x is any
var y = undefined; // y is any

[Eyas]

An example with generics:

interface Maybe<T> {
    hasValue: boolean;
    value(): T;
}

class Some<T> implements Maybe<T> {
    constructor(value: T) { this._value = value; }
    private _value: T;
    hasValue = true;
    value() { return this._value; }
}

class Nothing<T> implements Maybe<T> {
    hasValue = false;
    value(): T { throw new Error("Attempting to dereference Nothing."); }
}

var None: Nothing<Undefined> = new Nothing<Undefined>();

var x: Maybe<string> = None; // compiles

Same with immutable lists:

interface List<T> {
    x(): T;
    xs(): List<T>;
    map<U>(fn: (t: T) => U): List<U>;
    filter(fn: (t: T)=> boolean): List<T>;
    // etc.
}

class Cons<T> implements List<T> {
    constructor(x: T, xs: List<T>) { this._x = x; this._xs = xs; }
    x(): T { return this._x; }
    xs(): List<T> {return this._xs; }
    private _x: T;
    private _xs: List<T>;
    map<U>(fn: (t: T) => U): List<U> { return new Cons(fn(this._x), this._xs.map(fn)); }
    filter(fn: (t: T)=> boolean): List<T> {
        if (fn(this._x))
            return new Cons(this._x, this._xs.filter(fn));
        else
            return this._xs.filter(fn);
    }
    // etc.
}

class Empty<T> implements List<T> {
    x(): T { throw new Error("Attempting to dereference Empty list."); }
    xs(): List<T> {throw new Error("Attempting to dereference Empty list."); }
    map<U>(fn: (t: T) => U): List<U> {
        return Nil; // compiles
        }
    filter(fn: (t: T)=> boolean): List<T> {
        return Nil; // compiles
    }
}

var Nil: Empty<Undefined> = new Nothing<Undefined>();

var l: List<string> = Nil; // compiles

[Eyas]

@Igorbek indeed it is. any is very curious indeed. The spec says it is the supertype of all types, yet in some contexts it really behaves like a bottom type.

Example:

// both these statements in succession are legal
var any_string: any = "string"; // acts like a supertype for all types
var num: number = any_string; // acts like a bottom type

I'm guessing this is mainly here for some pragmatic JavaScript compatibility purpose. Even if any continues to act this way, typeof undefined should not be inferred as any:

// assuming ts.14
type Undefined = typeof undefined;
var undef_string: Undefined = "string"; // MUST NOT COMPILE; a bottom type has only one legal value: undefined
var num: number = undef_string; // acts like a bottom type, compiles normally

Current behavior is same us the first block.

[Igorbek]

Looks like void is actual type of undefined. Indeed:

function f<T>(g: ()=>T): T { return g(); } // function for extract return type
function g() {} // simple void function, inferred as `() => void`

var x = f(g);   // `x` is inferred as `void`
console.log(x === undefined);   // "true", so `x` is undefined actually

but

function h() { return undefined; }  // it's the same as `g`, but inferred as `() => any`

var y = f(h);   // `y` is `any`
console.log(x === undefined);   // "true", so `y` is undefined as well as `x`

[Igorbek]

Maybe {} is better candidate to be called bottom type.

[Eyas]

It seems, though that undefined is more "empty" than { }. { } ultimately still has valueOf, toString, toLocaleString as members. Its an object with no properties, and in that sense an empty object, true, but undefined is actually empty.

I think the existing behavior of interpreting {} as Object is correct. Imagine:

var unit = {};
var num: number = unit; // currently doesn't compile since we are assigning Object to number
// if it succeeds, then now:
num.toString() === "[Object object]";

The argument is summarized as: Object is definitely not the bottom type, {} is correctly inferred as Object ==> {} can't be the bottom type.

[RyanCavanaugh]

Note that { } has no members, but its apparent type (3.10.1) does. The Undefined type doesn't have toString/etc because it's not an Object type, and therefore does not acquire the members of the top-level Object interface when going through the apparent type process.

[Eyas]

A more obvious argument for {} not being a bottom type is that, per 3.8.6, it would not be a subtype for "type types".