TypeScripts Type System is Turing Complete

[hediet]

This is not really a bug report and I certainly don't want TypeScripts type system being restricted due to this issue. However, I noticed that the type system in its current form (version 2.2) is turing complete.

Turing completeness is being achieved by combining mapped types, recursive type definitions, accessing member types through index types and the fact that one can create types of arbitrary size.
In particular, the following device enables turing completeness:

type MyFunc<TArg> = {
 "true": TrueExpr<MyFunction, TArg>,
 "false": FalseExpr<MyFunc, TArg>
}[Test<MyFunc, TArg>];

with TrueExpr, FalseExpr and Test being suitable types.

Even though I didn't formally prove (edit: in the meantime, I did - see below) that the mentioned device makes TypeScript turing complete, it should be obvious by looking at the following code example that tests whether a given type represents a prime number:

type StringBool = "true"|"false";

interface AnyNumber { prev?: any, isZero: StringBool };
interface PositiveNumber { prev: any, isZero: "false" };

type IsZero<TNumber extends AnyNumber> = TNumber["isZero"];
type Next<TNumber extends AnyNumber> = { prev: TNumber, isZero: "false" };
type Prev<TNumber extends PositiveNumber> = TNumber["prev"];


type Add<T1 extends AnyNumber, T2> = { "true": T2, "false": Next<Add<Prev<T1>, T2>> }[IsZero<T1>];

// Computes T1 * T2
type Mult<T1 extends AnyNumber, T2 extends AnyNumber> = MultAcc<T1, T2, _0>;
type MultAcc<T1 extends AnyNumber, T2, TAcc extends AnyNumber> = 
		{ "true": TAcc, "false": MultAcc<Prev<T1>, T2, Add<TAcc, T2>> }[IsZero<T1>];

// Computes max(T1 - T2, 0).
type Subt<T1 extends AnyNumber, T2 extends AnyNumber> = 
		{ "true": T1, "false": Subt<Prev<T1>, Prev<T2>> }[IsZero<T2>];

interface SubtResult<TIsOverflow extends StringBool, TResult extends AnyNumber> { 
	isOverflowing: TIsOverflow;
	result: TResult;
}

// Returns a SubtResult that has the result of max(T1 - T2, 0) and indicates whether there was an overflow (T2 > T1).
type SafeSubt<T1 extends AnyNumber, T2 extends AnyNumber> = 
		{
			"true": SubtResult<"false", T1>, 
 "false": {
 "true": SubtResult<"true", T1>,
 "false": SafeSubt<Prev<T1>, Prev<T2>>
 }[IsZero<T1>] 
		}[IsZero<T2>];

type _0 = { isZero: "true" };
type _1 = Next<_0>;
type _2 = Next<_1>;
type _3 = Next<_2>;
type _4 = Next<_3>;
type _5 = Next<_4>;
type _6 = Next<_5>;
type _7 = Next<_6>;
type _8 = Next<_7>;
type _9 = Next<_8>;

type Digits = { 0: _0, 1: _1, 2: _2, 3: _3, 4: _4, 5: _5, 6: _6, 7: _7, 8: _8, 9: _9 };
type Digit = 0 | 1 | 2 | 3 | 4 | 5 | 6 | 7 | 8 | 9;
type NumberToType<TNumber extends Digit> = Digits[TNumber]; // I don't know why typescript complains here.

type _10 = Next<_9>;
type _100 = Mult<_10, _10>;

type Dec2<T2 extends Digit, T1 extends Digit>
	= Add<Mult<_10, NumberToType<T2>>, NumberToType<T1>>;

function forceEquality<T1, T2 extends T1>() {}
function forceTrue<T extends "true">() { }

//forceTrue<Equals< Dec2<0,3>, Subt<Mult<Dec2<2,0>, _3>, Dec2<5,7>> >>();
//forceTrue<Equals< Dec2<0,2>, Subt<Mult<Dec2<2,0>, _3>, Dec2<5,7>> >>();

type Mod<TNumber extends AnyNumber, TModNumber extends AnyNumber> =
 {
 "true": _0,
 "false": Mod2<TNumber, TModNumber, SafeSubt<TNumber, TModNumber>>
 }[IsZero<TNumber>];
type Mod2<TNumber extends AnyNumber, TModNumber extends AnyNumber, TSubtResult extends SubtResult<any, any>> =
 {
 "true": TNumber,
 "false": Mod<TSubtResult["result"], TModNumber>
 }[TSubtResult["isOverflowing"]];
 
type Equals<TNumber1 extends AnyNumber, TNumber2 extends AnyNumber>
 = Equals2<TNumber1, TNumber2, SafeSubt<TNumber1, TNumber2>>;
type Equals2<TNumber1 extends AnyNumber, TNumber2 extends AnyNumber, TSubtResult extends SubtResult<any, any>> =
 {
 "true": "false",
 "false": IsZero<TSubtResult["result"]>
 }[TSubtResult["isOverflowing"]];

type IsPrime<TNumber extends PositiveNumber> = IsPrimeAcc<TNumber, _2, Prev<Prev<TNumber>>>;
 
type IsPrimeAcc<TNumber, TCurrentDivisor, TCounter extends AnyNumber> = 
 {
 "false": {
 "true": "false",
 "false": IsPrimeAcc<TNumber, Next<TCurrentDivisor>, Prev<TCounter>>
 }[IsZero<Mod<TNumber, TCurrentDivisor>>],
 "true": "true"
 }[IsZero<TCounter>];

forceTrue< IsPrime<Dec2<1,0>> >();
forceTrue< IsPrime<Dec2<1,1>> >();
forceTrue< IsPrime<Dec2<1,2>> >();
forceTrue< IsPrime<Dec2<1,3>> >();
forceTrue< IsPrime<Dec2<1,4>>>();
forceTrue< IsPrime<Dec2<1,5>> >();
forceTrue< IsPrime<Dec2<1,6>> >();
forceTrue< IsPrime<Dec2<1,7>> >();

Besides (and a necessary consequence of being turing complete), it is possible to create an endless recursion:

type Foo<T extends "true", B> ={"true": Foo<T, Foo<T, B>>}[T];
let f: Foo<"true",{}> = null!;

Turing completeness could be disabled, if it is checked that a type cannot use itself in its definition (or in a definition of an referenced type) in any way, not just directly as it is tested currently. This would make recursion impossible.

//edit:
A proof of its turing completeness can be found here

[HerringtonDarkholme]

Just a pedantic tip, we might need to implement a minimal language to prove TypeScript is turing complete.

http://stackoverflow.com/questions/449014/what-are-practical-guidelines-for-evaluating-a-languages-turing-completeness
https://sdleffler.github.io/RustTypeSystemTuringComplete/

hmmm, it seems this cannot prove turing completeness.
Nat in this example will always terminate. Because we cannot generate arbitrary natural number. If we do encode some integers, isPrime will always terminate. But Turing machine can loop forever.

[KiaraGrouwstra]

That's pretty interesting.

Have you looked into using this recursion so as to say iterate over an array for the purpose of e.g. doing a type-level reduce operation? I'd wanted to look into that before to type a bunch more operations that so far did not seem doable, and your idea here already seems half-way there.

The idea of doing array iteration using type-level recursion is raising a few questions which I'm not sure how to handle at the type level yet, e.g.:

• arr.length: obtaining type-level array length to judge when iteration might have finished handling the entire array.
• destructuring: how to destructure arrays at the type level so as to separate their first type from the rest. getting the first one is easy ([0]), destructuring such as to get the rest into a new array, not so sure...

[be5invis]

So, TS can prove False? (as in Curry-Howard)

[hediet]

I think stacks a typed length and with each item having an individual type should be possible by adding an additional type parameter and field to the numbers from my example above and storing the item in the number. Two stacks are half the way to proving formal turing completeness, the missing half is to implement a finite automata on top of that.
However, this is a complex and time consuming task and the typical reason why people want to disprove turing completeness in typesystems is that they don't want the compiler to solve the halting problem since that could take forever. This would make life much harder for tooling as you can see in cpp. As I already demonstrated, endless recursions are already possible, so proving actual turing completeness is not that important anymore.

[hediet]

@be5invis What do you mean with that?
@HerringtonDarkholme
I've implemented a turing machine interpreter: https://gist.github.com/hediet/63f4844acf5ac330804801084f87a6d4

[KiaraGrouwstra]

@hediet: Yeah, good point that in the absence of a way to infer type-level tuple length, we might get around that by manually supplying it. I suppose that'd also answer the destructuring question, as essentially you'd just keep picking out arr[i] at each iteration, using it to calculate an update reduce() accumulator. It'd no longer be very composable if the length could not be read on the fly, but it's still something -- and perhaps this would be relatively trivial to improve on for TS, anyway.

I suppose that still leaves another question to actually pull off the array iteration though. It's coming down to the traditional for (var i = 0; i < arr.length; i++){} logic, and we've already side-stepped the .length bit, while the assignment is trivial, and you've demonstrated a way to pull off addition on the type level as well, though not nearly as trivial.

The remaining question for me would be how to deal with the iteration check, whether as i < arr.length or, if reversed, i == 0. It'd be nice if one could just use member access to distinguish the cases, e.g. {0: ZeroCase, [rest: number]: ElseCase }[i], but this fails as it requires ZeroCase to sub-type ElseCase.

It feels like you've covered exactly these kind of binary checks in your Test<MyFunc, TArg> case. but it seems to imply a type-level function (MyFunc) that could do the checks (returning true / false or your string equivalents). I'm not sure if we have a type-level == (or <) though, do we?

Disclaimer: my understanding of the general mechanisms here may not be as far yet.

[KiaraGrouwstra]

So I think where this would get more interesting is if we could do operations on regular type-level values (e.g. type-level 1 + 1, 3 > 0, or true && false). Inspired by @hediet's accomplishment, I tried exploring this a bit more here.

Results:

• Spoiler: I haven't pulled off array iteration.
• I think I've figured out boolean operations (be it using 0/1, like string here) except Eq.
• I think type checks (type-level InstanceOf, Matches, TypesEq) could be done if Proposal: Get the type of any expression with typeof #6606 lands (alternatives?).
• I'm not sure how to go about number/array operators without more to go by. Array (= vector/tuple) iteration seems doable given a way to increment numbers -- or a structure like @hediet used, if it could be construed from the array. Conversely, number operations could maybe be construed given operations on bit vectors and a way to convert those back and forth... tl;dr kinda stumped.

These puzzles probably won't find solutions anytime soon, but if anything, this does seem like one thread where others might have better insights...

[KiaraGrouwstra]

I made some progress, having tried to adapt the arithmetic operators laid out in the OP so as to work with number literals instead of special types. Skipped prime number stuff, but did add those operators like > etc.
The downside is I'm storing a hard-coded list of +1 increments, making it scale less well to higher numbers. Or negatives. Or fractions.

I mainly wanted to use them for that array iteration/manipulation though. Iteration works, and array manipulation, well, we can 'concatenate' tuple types by constructing a numeric object representing the result (with length to satisfy the ArrayLike interface if desired).

I'm honestly amazed we got this far with so few operators. I dunno much about Turing completeness, but I guess functions seem like the next frontier now.