Special bottom type

[Artazor]

I think that it should be special bottom type with the following properties:

• ( T | bottom ) = ( bottom | T ) = T — bottom is unit for type unions;
• expression of type bottom is assignable to any other type;
• bottom type could be used only as return type of the function (out-only);
• if function has return type bottom then all branches of the control flow either throw exceptions or return expression of type bottom;
• if all branches of the control flow either throw exceptions or return expression of type bottom and function has no explicit return type then bottom type inferred as the result type;
• two functional types are not assignable to each other if exactly one of them has return type bottom (?);
• bottom type can't be used as the actual type parameter for the generic type.

rationale

Let's consider the function that always throws:

function alwaysThrows() {
    throw new Error("!");
}

and other function that uses it

function test(a: boolean) {
    return a ? 123 : alwaysThrow();
}

We expect that test should have type number instead of ( number | void )

In more sophisticated example that involves Promise type declarations:

declare class Promise<T> {
    catch<U>(
        handler: (reason: any) => U | Promise<U>
    ): Promise<T | U>;  // Note the union here (!)
    then<U>(
        fulfilled?: (result: T) => U | Promise<U>,
        rejected?: (reason: any) => U | Promise<U>
    ): Promise<U>
}

We expect that

promiseOfString.catch(function(e) {
   throw new BusinessError(e);
});

should have the type of Promise<string> instead of Promise<string | void>.

See petkaantonov/bluebird#589 (comment)

Possible explicit annotation that function always throws is using undefined as the type

function alwaysThrows(): undefined {
    throw new Error("!");
}

[Artazor]

It's obviously related to the #1613

[jbondc]

Also related to removing 'void' from a union type and allowing its use as a type guard #1806

Still find it odd that number|void doesn't collapse to -> number.

[Artazor]

I think that bottom !== void and we can not collapse number|void to number because it represents the state where value is either number or undefined, meanwhile the number means a guaranted number.

Um?

[jbondc]

What do you mean? A number type can have values 'null' or 'undefined', a void type can have values 'null' or 'undefined'. A void type is clearly a subset of the number type, it's redundant in a union.

[Artazor]

I think that you are wrong, but the explanation is tricky. This is the consequence of the "carefully corrupted" type system by @ahejlsberg.

null and undefined values are assignable to the number not because of they are part of the numbers domain. They are assignable because of an explicit ad-hoc rule (their type is any). The type system of the TypeScript purposely allows such assignments, and it is valid to expect that

function(a: number) {
    return a.toExponential();
}

will fail when it is called with null or undefined.

type number is not a strict guarantee that the value is a number, it is a hint that in normal circumstances it should be a number. If you purposely pass the null value to it, then you probably know what you do. In opposite (number|void) says that it is normal to expect an "undefined" value.

@ahejlsberg, am I right?

[Artazor]

I think that it implicitly correlates with the typeof null drama of the ES6.

I'd say that

• null is a special marker for missing value
• undefined is the result of querying of things that never was assigned intentionally
• bottom - is the total absence of the result (exception thrown)

where "throw" statement is actually an expression of type bottom

[spion]

Since TS has no model for exceptions in the type system, I think this workaround would be nice.

Other than the unions rule, I'm assuming it would behave the same as void? i.e. if you get a value of type bottom (outside of a union), you cannot call any methods on it...

I don't like void being used for this, as I'd prefer if void got its 1.4 meaning again (void | T = void)

[jbondc]

@Artazor Not sure if there's a right or wrong about 'void' at the moment, it's just ambiguous:

var v1 = function() {} // infers void

var v1Assign = v1();
v1Assign = null; // not really a bottom type
v1Assign = undefined;

var v2 = function () {
    return null; // infers any
}

var v3 = function () {
    return undefined; // infers any
}

var v4 = function () {
    return void 0; // infers any, a bit odd looking
}
var v4Assign = v4();
v4Assign = null;
v4Assign = undefined;

var v5 = function () {
    throw new Error('?') // infers void
}

var v5 = function () {
    if (0) {
        return ""; // infers 'string'
    }
    if (0) {
        return null;
    }
    if (0) {
        return undefined;
    }
    throw 0; 
}

We do agree there should be a bottom type, in my world I call it void!null!undefined.
type Bottom = void!null!undefined;

[Artazor]

@jbondc your type exclusion syntax is very relevant (have you proposed the syntax itself anywehere?)

I'd say that

type Bottom = number!number // or any other type

Nevertheles, both null and undefined has type any. This is why they are assignable to any type.
So they are not in the domain of the corresponding types. For them type checking is simply off.

var x:string = null  // ok
var y:string = (() => null)() // ok (any is propogated outside)
var z:string = (():void => null)() // error: can't assign void to string

Hard decision to type the void <expression> as any (instead of void) was made only for accommodating for common void 0 usage instead of undefined for the purpose of initial value. (facepalm)

UPD
unfortunately, it effectively kills the type checking in the following (otherwise idiomatic) simple lambda expression

x => void f()

for example

promiseOfString.then(x => void f(x))

Has type Promise<any> instead of Promise<void>

[zpdDG4gta8XKpMCd]

what is wrong with defining alwaysThrow as follows:

function alwaysThrow<a>() : a { throw new Error(''); }

it works immediately without requiring the presence of the bottom type which, unfortunately, needs runtime support from javascript to be what it is

[Artazor]

@Aleksey-Bykov hm?

I'm talking about purely static type inference.The primary goal for the bottom type is preventing pollution of union types when inferred implicitly.

If I understood your suggestion correctly you are talking about writing

function test(a: boolean) {
   return a ? 123 : alwaysThrows<number>();
}

This, unfortunately, kills the idea of type inference (or at least seriously affects its reputation).

[Artazor]

@spion

Other than the unions rule, I'm assuming it would behave the same as void? i.e. if you get a value of type bottom (outside of a union), you cannot call any methods on it...

Exactly. But you can pass this type to anywhere, because of in real life this passing will never happen because of the exception already thrown.

as I'd prefer if void got its 1.4 meaning again (void | T = void)

Here I don't understand. I think the rule of (void | T = void) is very dangerous and irrelevant. Can you elaborate why you ever thought that it would be useful?

I think that this discussion lacks people from the actual TS team, @mhegazy?

[Artazor]

Anyway, now I start to think that bottom type should have no name at all. It should be inferred statically.
And if you want to to constrain your function explicitly that it should throw in every branch of the control flow you should write something like

function parseAndThrow(errorInfo: IErrorInfo) throw {
     ...
}

This is a limited and the strongest form of the checked exceptions which states that the function always throws. And it can be implemented without checked exceptions machinery at all - it simply needs the bottom type internally.

[Artazor]

@jbondc excluding would be nice, also I would highly anticipate the intersection type, for the immediate intersection of interfaces:

var x: IMyInterface & IRunnable

In fact, I would be happy if TypeScript would have the following type structure:

(I've mentioned this already in petkaantonov/bluebird#589)

The Type System

of my dream for TypeScript

τ ::= tcon | α | (τ τ) | (Λα.τ) | (τ → τ) | (τ × τ) | ⊤ | ⊥ | (τ ⋂ τ) | (τ ⋃ τ) | (!τ) | (τ ^ τ)

where

• tcon — type constructor like Either, Maybe, Promise, Int etc.;
• α — formal type;
• (τ τ) — type application e.g. Maybe Int;
• (Λα.τ) — type abstraction (generic type) (suggested Type aliases requiring type parameters #1616);
• (τ → τ) — function type;
• (τ × τ) — tuple type, associative;
• ⊤ — top type (equivalent to any);
• ⊥ — bottom type (suggested here);
• (τ ⋂ τ) — type intersection, associative, commutative;
• (τ ⋃ τ) — type union, associative, commutative;
• (!τ) — type negation (type complement to ⊤);
• (τ ^ τ) — checked exceptions, associative.

This system has usual parentheses elimination conventions and two aliases:

• τ₁ + τ₂ = τ₁ ⋃ τ₂
• τ₁ - τ₂ = τ₁ ⋂ !τ₂

Checked exceptions (τ_result ^ τ_error) have two simple properties:

• (τ₁ ^ τ₂) ^ τ₃ = τ₁ ^ (τ₂ ⋃ τ₃) — exception propagation from inner computations;
• τ₁ ^ (τ₂ ^ τ₃) = τ₁ ^ (τ₂ ⋃ τ₃) — exception union.

that makes (τ ^ τ) associative. (there are more rules, of course)
In fact if there will be interest I can write down all the sematic rules with typing context in strict algebraical format (using ASF+SDF or Rascal)

[jbondc]

@Artazor Do you have examples of use cases for type negation? Never seen that before, which programming language?

[jbondc]

I guess:

type a = string;
type b = number;
type c = boolean;
type d = a | b | c;
type lotsOfThings = d!a; // b | c ?

It doesn't seem too difficult to implement, you just pluck it out of your set of union types.

[spion]

@Artazor I meant void | T = void in terms of supported methods / operations. With a type guard val != null

[weswigham]

The bottom type described in this thread is very close to describing the correct behavior of the nothing type which is now surfaced as a result of control flow analysis, IMO.

[Artazor]

@weswigham exactly! The bottom type was proposed to reflect the result of the control flow analysis, and surely could not be implemented without proper CFA, which now is available. Isn't it?