New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
TypeScripts Type System is Turing Complete #14833
Comments
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 hmmm, it seems this cannot prove turing completeness. |
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 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.:
|
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. |
@be5invis What do you mean with that? |
@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 I suppose that still leaves another question to actually pull off the array iteration though. It's coming down to the traditional The remaining question for me would be how to deal with the iteration check, whether as It feels like you've covered exactly these kind of binary checks in your Disclaimer: my understanding of the general mechanisms here may not be as far yet. |
So I think where this would get more interesting is if we could do operations on regular type-level values (e.g. type-level Results:
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 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 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. |
@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. |
This is like c++ template metaprogramming ? |
@iamandrewluca From what I understand -- yes. |
Possible relevant tickets: I'm just wondering if this would affect how recursive type definitions are currently handled by TypeScript. |
so we can we write an undecidable type in ts, cant we? |
Assuming TypeScript type system is indeed Turning complete, yes. For any TS compiler, there would be a program that the compiler could not correctly type check. Whether this matters practically is an entirely different story. There are already programs you could not compile, due to limited stack space, memory, etc. on your computer. |
If you try to take idiomatic functional programming concepts from JS to TS (generics, currying, composition, point-free function application), type inference breaks down pretty much immediately. The run-time JS though runs fine. Hardware isn't the bottleneck there. |
This is true regardless of whether the type system itself is Turing-complete. function dec(n: number): boolean {
return n === 0 ? true : dec(n - 1);
}
let x: boolean = dec(10) ? true : 42; TypeScript can't typecheck this program, even though it doesn't evaluate to an error. Turing Completeness in the type-system just means type-checking now returns yes/no/loop, but this can be dealt with by bounding the type-checker (which I think already happens). @tycho01 checking !== inferring (Though I agree with your point). |
What do you mean? The TS compiler checks that program just fine and properly finds the type-error? |
@paldepind The point is that the else clause of the ternary is unreachable so the program should in fact pass the type checker (but it does not); i.e., dec(10) returns true (and 10 is a compile time constant/literal). |
|
How 'bout Brainf*ck https://github.com/sno2/bf (I made it)
The Brainf*ck interpreter can also have an infinite loop by the following program so it seems that your final note is over now: // Type instantiation is excessively deep and possibly infinite.
type Output = BF<{
program: "+[]";
outputType: "ascii";
}>; |
@sno2 that is an absolute delight, thank you |
Turing completeness meaning all can describe computable problems can be solved. |
Since 4.8 you can now make complex calculus : |
@ecyrbe what does the |
It's the JavaScript Bigint notation for numbers that are too Big to be represented by a number: |
A little over a year ago, I decided I liked TypeScript. In fact, I decided liked it so much, I didn't just want it to be stuck in my editor— I wanted to use the same syntax to validate my data at runtime! And what better way to achieve that than to use TypeScript's own type system to parse its own syntax. Much to my surprise, what I ended up with was not a toy, but a remarkably performant static parser that allows definitions built from arbitrarily parenthesized and nested TS operators like At this point, it can handle hundreds of cyclic types seamlessly and import between scopes. As far as I'm aware, ArkType is the most advanced application of TypeScript's type system to date: arktype.mp4This is what it looks like to interact with a scope of 100 cyclic types: typePerf.mp4Props to the TypeScript team- it's genuinely incredible that TS is so well-built that it can literally parse itself in real-time without being remotely optimized for it. |
Considering this I think TS might as well implement a way for users to run arbitrary procedural code to destruct and construct types at compile time. There are numerous situations where you end up writing some type mapping magic that's doing O(n^2) or worse computation because you have to do something in a roundabout way when straightforward procedural code could do it in O(n). |
okay this thread is crazy. |
not to mention the fact that only Functional Programming Galaxy Brains™️ can figure out how to do much more with the type system than generics and maybe mapped types. the type system is effectively a functional programming language, weaved into a multi-paradigm language, with a completely different syntax - it resembles C# on the surface, and it obviously resembles JS below the surface, but it's extremely foreign (even hostile at times) to people coming from either of those languages. I love TS despite this glaring design problem, and front-end development at any real scale would be unbearable without it - but unless at some point there's a reckoning, I'm starting to think tides will eventually turn and TS won't last. 😥 I wish they would discuss possible avenues such as #41577 to break free of this. |
Deepkit Runtime Types is far more advanced and you only have to use TypeScript types. Deepkit Runtime Types support complex types such as the following: |
@marcus-sa Deepkit is a very cool project, but it is not built within TypeScript's type system. Rather it parses native TS types externally and adds runtime metadata, so it's orthogonal to this thread. |
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:
with
TrueExpr
,FalseExpr
andTest
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:
Besides (and a necessary consequence of being turing complete), it is possible to create an endless recursion:
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
The text was updated successfully, but these errors were encountered: