Proposal: type-level addition (+)

[KiaraGrouwstra]

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.

[mhegazy]

Duplicate of #15645.

As noted in #8112, we choose to not do any type arithmetic. the scenarios here seem rather limited to add this whole layer of complexity insider the compiler.

it is also worth noting that an earlier implementation proposal of literal types had literal type asthmatics in, and we chose to disallow it.

[KiaraGrouwstra]

Edit: partial.lenses is another library where this is relevant; afaict, not one of its functions can be usefully typed without this.

the scenarios here seem rather limited

To comment on this, I think that with the right primitives (those basic operators, the iteration it'd enable, and that function application), the type language would start to get on par with the expression language, allowing to infer the exact return values of, hopefully most functions out there, starting with lib.d.ts, and by virtue of that, anything built from those blocks.

In my limited understanding, this would also enable doing things like dependent types, currently taken as a reason that the type system of Idris would be more powerful than that of Haskell.
I'll concede such precise inference becomes more relevant as complexity grows, particularly relevant in FP. And I realize that, though FP has been growing here, particularly with Angular's blessing of RxJS, there is still more code out there that may not directly benefit.
That said, I see it sort of as a cycle though -- I believe proper inference would make FP incredibly attractive in TS, and in return, would have more FP users turn to TS.

[KiaraGrouwstra]

I figured that storing just +1 increments for lookup makes for a fair workaround for the time being, see e.g. here. So support for type-level arithmetic here is no longer that urgent anymore for the purpose of type-level iteration.