Proposal: type-level addition (+) #15794

Solves #12290, #12512.

TypeScript Version: current (2.3.1-insiders.20170416)

Currently TypeScript recognizes type-level values, e.g. String Literal Types (as well as true, 123), but there is no way to operate on these at the type level. This proposal is about support for one specific part of that: addition (+).
Specifically, there are two sides to this:

Current behavior:

let one: 1;
let two = one + one; // type: number :(
type Two = 1 + 1; // syntax error, no type-level +

That is:

• Even if number values are statically known, the type-level number literals are not actually added, but degenerate to number.
• The addition operator (+) is not currently exposed as an operator on the type level. That makes sense, as this only becomes useful if the above point is resolved. Fortunately, from there the type-level logic used by the expression-level + operator could be reused by such a type-level operator.

Desired behavior:

let one: 1;
let two = one + one; // type: 2
type Two = 1 + 1; // 2

Relevance:

I'll concede: let two = one + one; yielding type 2 does not seem particularly important -- it's the type level operator I care about though, and presuming a shared implementation, I suppose enabling better handling for the expression-level operator would just be a side effect.

So why care about type Two = 1 + 1; // 2?
It's the missing link to enabling type-level array iteration (that is for e.g. type [1, 2, 3], not number[]). We can make conditionally recursive types (examples demonstrated at #14833, e.g. his type Add<T1 extends AnyNumber, T2> = { "true": T2, "false": Next<Add<Prev<T1>, T2>> }[IsZero<T1>];), and we can check if a type-level array containers a certain index (type HasKey<Arr extends any[], I extends number> = ({[K in keyof Arr]: 1 } & Array<0>)[I];). Given those, the only thing stopping us from iterating over an array now is, well, the ability to increment a type-level numerical counter serving as the index.

So why array iteration?
For one, this would immediately enable properly typing more complex functions such as Ramda's path function (see #12290), as well as other functions using reduce-like logic (a few dozen examples at #12512). Add function application to that (needs #6606), and we could properly type reduce itself. I imagine impact would go further, but these are what came to mind first.

Which parts are affected, and how?

• syntax: + operator exposed on type level
• type system: 1 + 1 evaluating to type 2 -- indeterminate cases e.g. 1 + number could be handled as they are now, yielding number
• JavaScript emitter: unaffected

Are other language features impacted?
AFAICT, no.

How does the feature interact with generics?
As other operators, evaluate when generic values are resolved.

How does the feature impact subtype, supertype, identity, and assignability relationships?
I'll go for "doesn't".

Can the feature be implemented without negatively affecting compiler performance?
Presumably yes.