TypeScripts Type System is Turing Complete

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

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.

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...

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

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.

Belleve (@be5invis)

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

Henning Dieterichs (@hediet)

Henning Dieterichs (@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.

Henning Dieterichs (@hediet)

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 Henning Dieterichs (@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 Henning Dieterichs (@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...

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.

Belleve (@be5invis)

Belleve (@be5invis) You're thinking of an unsound type system. Turing completeness merely makes type checking undecidable. So, you can't prove false, but you can write something that is impossible to prove or disprove.

Ivan Jager (@aij)

Ivan Jager (@aij) TypeScript has its fair share of unsoundness too: #8459

This is like c++ template metaprogramming ?

@iamandrewluca From what I understand -- yes.

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.

Possible relevant tickets:

I'm just wondering if this would affect how recursive type definitions are currently handled by TypeScript.
If TypeScript uses eager type checking for direct type usages but not interface type usages, then would this restriction still preserve the interface trick for recursive type definitions?

so we can we write an undecidable type in ts, cant we?

Andy Edwards (@jedwards1211)

Andy Edwards (@jedwards1211) Yes, but you could make a very practical gql parser within those limitations.

Character limit is 1001:

Expressions can have up to 46 operands:

And that is with arbitrary grouping, syntactic semantic validation (type-level error messages) etc.:

If it's possible to represent a definition while leveraging JS's built-in structures (object and tuple literals), yes there is a performance advantage to doing so, in addition to other benefits like better highlighting and formatting.

That said, with the right approach the type system will take you quite far, even with pure strings.

David Blass (@ssalbdivad)

David Blass (@ssalbdivad) IMO a 1001 character limit isn't acceptable for this GraphQL use case in a production project, in general no one would want a compiler to have such a severe limit. I will just continue to wish that more were possible.

Andy Edwards (@jedwards1211)

Andy Edwards (@jedwards1211) What you have to consider is the boundary between a "type" (ideally something that can be compared to other types and tested for assignability) and arbitrary linting/static analysis.

What you're describing sounds much more like the second category, so maybe an extension to facilitate the DX you want would be ideal. I do understand the appeal of being able to ship something like that through native TS but it's pretty firmly outside the realm of "types" at that point.

David Blass (@ssalbdivad)

David Blass (@ssalbdivad) I'm not sure what kind of linting you think I mean, I really am just talking about computing the input and output TS types for a GraphQL query. And a type is a type, whether it's created by codegen-ing TS or by using TS type magic. If TS type magic is able to do it for short strings, it feels unfortunate if the length limit is some arbitrary, low number.

Andy Edwards (@jedwards1211)

Andy Edwards (@jedwards1211) What I mean is that the arguments you pass to a generic type are themselves types. They might happen to mirror a literal value, but that will not always be the case.

When you talk about "loops, stacks, and other procedural constructs at type time", I assume you mean writing something like arbitrary imperative logic, which operates on values or terms, not types.

If you want them to be limited to a similar set of operations as can be expressed today via conditionals and mapped types, then sure, loops might be a mild syntactic convenience, but what you really want is perf optimizations and an increased recursion depth limit.

TS is already extremely performant in terms of how it handles this kind of parsing, so the increased limit is probably the more reasonable request of the two.

That said, I'd be surprised if there's not a way to split up a well-structured query such that it could fit within those limits. Maybe I'm misunderstanding and I'm definitely rusty when it comes to GraphQL, but to me, 1000 characters for a single query sounds like a nightmare.

David Blass (@ssalbdivad)

David Blass (@ssalbdivad) no I'm talking about a bold idea (probably too bold, but I always want more powerful capabilities) for a syntax/API for declaring functions that are called with/return API representations of TS types, kind of like the API for inspecting types from the compiler that you can access in ts-morph.

For example:

// new syntax, like a type alias but the code inside runs at type time
type function GreaterThan(A extends number, B extends number) {
  const aValue = A instanceof TS.NumberLiteral
    ? A.value
    : A instanceof TS.Union && A.options.every(opt => opt instanceof TS.NumberLiteral)
    ? Math.min(...A.options.map(opt => opt.value)
    : undefined
  const bValue = ... // likewise, but get max value of union
   
  return aValue == null || bValue == null ? TS.factory.never() : aValue > bValue ? TS.factory.true() : TS.factory.false()
}

// and voila, now it works for number literals of any magnitude:
type Test = GreaterThan<72374812, 8600200> // true

And then for something like parsing ArkType, if the function received a string literal type, it would parse it into an AST using procedural code that isn't limited by the size of the stack, and convert the AST into these TS type representations.

One thing about this TS maintainers would probably not like is, it would be hard to guarantee these type functions are pure and deterministic. With great power comes great responsibility I guess... In any case it would probably be unworkable for reasons like, how do you compute variance?

But I hope to at least make the case that having a Turing-complete system limited to mere thousands of items is really annoying. It's like Genie said in Aladdin..."phenomenal cosmic powers...itty bitty living space."

I wish TS were at least capable of instantiating tail-recursive types without nested invocations, so that we'd no longer be bound by these limits, and type decls would work more like actual functional programming languages.

And no, 1000 characters in a single GraphQL query isn't uncommon or a nightmare by any means. There are three such queries in the production app I'm working on; here is one example.

Maybe this belongs in #41577 instead? (and #39385 is relevant)

not once per keystroke
I don't understand, doesn't the language server already re-evaluate as you type?

If you have something like

// In file stuff.ts
interface Stuff {
  foo: string;
  bar: string;
}

// In the edited file
const p: Stuff = { foo: "hello", <- user is in the process of typing this

At each keystroke, the type of Stuff is getting recomputed, but this work is extremely minimal since it's all statically defined. The AST isn't changing, the symbol maps aren't changing, it's very very cheap.

If instead you had

// In file stuff.ts
type Stuff = ParseMyCoolDSL<"[[foo], string], [[bar], string]]">

// In the edited file
const p: Stuff = { foo: "hello", <- user is in the process of typing this

Similarly here, ParseMyCoolDSL is being re-evaluated every time, but this is a lot more work, and it's work (we as humans who know what the dependency tree is) that always results in the exact same shape. All the work of breaking apart the string, creating the temporary types, etc, creates work for the GC, and is just more work.

Even if we moved ParseMyCoolDSL into some "Just write code to make types" (JWCTMT) system then we have basically the same problem; the same work is being redone over and over and over again to produce the exact same result.

If we ever come up with a way to re-use type computations between program versions (still a great goal and still very much plausible IMO), then the non-code-based version of ParseMyCoolDSL is maybe something that could be identified to be "pure" (e.g. not dependent on inputs present in the file being edited), but the JWCTMT system is not going to work for that because we wouldn't be able to plausibly identify what inputs arbitrary code is depending on. JWCTMT sacrifices all possible future gain for some convenience today and I think it's the wrong thing to be asking for.

Ryan Cavanaugh (@RyanCavanaugh)

What Ryan Cavanaugh (@RyanCavanaugh) describes is also a huge part of the reason that reusing native structures when representing shapes makes a lot of sense- incremental results, syntax highlighting, formatting.

Personally, I'd much rather read a giant gql query like the one you linked with each layer of the query defined individually rather than having everything in-lined. It's more reusable, and allows you to name various key sets based on how they're designed to be used which makes the intent of queries like that clearer compared to a single root name.

Again, definite caveat that I have little familiarity with "best practices" for these scenarios in GraphQL, but those concepts in engineering seem to be pretty universal.

If any change has the potential to create a great API for something like this, IMO it would be this one:

#49552

Being able to compose your queries together naturally like that could offer an amazing DX while allowing you to break up your definitions into clear, composable units.

David Blass (@ssalbdivad)

David Blass (@ssalbdivad) happy to take this discussion elsewhere if you have an idea where, but even if I broke the query text up into interpolated variables (definitely a good suggestion), magic TS types would still have to parse just as many characters, right?

Edit: I guess you're saying one type could parse a chunk that gets interpolated, and another type could parse the surrounding text. It would probably be too verbose for me to completely love it, but it would definitely help us push past the current limits!

David Blass (@ssalbdivad)

David Blass (@ssalbdivad) IMO a 1001 character limit isn't acceptable for this GraphQL use case in a production project, in general no one would want a compiler to have such a severe limit. I will just continue to wish that more were possible.

There are posibilities, I had done some...things long time ago, but I abandoned it shamefully...That's why I never shared it here because of this embrassing fact. Here's the magic.

Take a try at parsing some long javascript-like code with it, it should be compiled into a weired opcode (I did intend to write a vm for that...). Basically it takes advantage of LR parsing, and use some tricks to break through the limits.

Luckily, a friend had translated my thoughts into English, hope it can be helpful. BTW, I'm not looking for a job anymore, I found a nice one :p

A dude just wrote a WebAssemly runtime using the type system and made it run doom

A dude just wrote a WebAssemly runtime using the type system and made it run doom

Video : https://www.youtube.com/watch?v=0mCsluv5FXA

WebAssemly runtime

Initially, my reaction was like "how did they not hit a recursion error?!?!", then I remembered that the definition of a Turing Machine doesn't include the "ability to loop on its own". That's why sed and PowerPoint are Universal Turing Machines, even though they need an "external force" to repeatedly apply the transition function.

This is why I propose the term "Turing Completeness" be split:

Self-"propelling" / independent
Weak / dependent

Note

I'm still looking for better terms 😅

As shown before, TS and its type-system are "self-propelling" TMs, but a subset of it can be "weakly" TC, which is how the "low enough" stack-usage can be achieved.

Important

I haven't watched the video (yet), so please don't assume I'm talking about the DOOM implementation

Edit after watching: So he applied a lot of optimizations and removed artificial limits, but he also did run tsc for each game-tick... wow!

Source

"TypeScripts Type System is Turing Complete" is at best a fun fact. The same can be said for a hammer, or a screw driver - because one day someone may be able to build a computer with it.

Navigation Menu

Repository navigation

TypeScripts Type System is Turing Complete #14833

62 remaining items

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

TypeScripts Type System is Turing Complete #14833

Description

Activity

HerringtonDarkholme commented on Mar 24, 2017

KiaraGrouwstra commented on Mar 24, 2017

be5invis commented on Mar 24, 2017

hediet commented on Mar 24, 2017

hediet commented on Mar 25, 2017

KiaraGrouwstra commented on Mar 25, 2017

KiaraGrouwstra commented on May 11, 2017

KiaraGrouwstra commented on Jul 1, 2017

aij commented on Aug 2, 2017

johanatan commented on Aug 5, 2017

unrevised6419 commented on Aug 10, 2017

CinchBlue commented on Aug 28, 2017

CinchBlue commented on Aug 28, 2017

zpdDG4gta8XKpMCd commented on Dec 8, 2017

62 remaining items

ssalbdivad commented on May 2, 2024

jedwards1211 commented on May 2, 2024

ssalbdivad commented on May 2, 2024

jedwards1211 commented on May 2, 2024

ssalbdivad commented on May 2, 2024

jedwards1211 commented on May 3, 2024

jcalz commented on May 3, 2024

RyanCavanaugh commented on May 3, 2024

ssalbdivad commented on May 3, 2024

jedwards1211 commented on May 6, 2024

YowaiCoder commented on May 30, 2024

RodrigoEliasP commented on Feb 27, 2025

rept0id commented on Feb 27, 2025

Rudxain commented on Feb 28, 2025

KooiInc commented on Mar 2, 2025

Metadata

Metadata

Assignees

Labels

Type

Projects

Milestone

Relationships

Development

Issue actions