-
Notifications
You must be signed in to change notification settings - Fork 12.6k
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). |
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. |
Two years ago I wrote a toy language interpreter using typescript's type system in order to learn typescript's type gymnastics. |
I've been curious about writing types to parse GraphQL queries at type time, and, together with generated types from the schema, determine the query data and variables types. I've been using codegen for this for a long time but it gets kind of annoying. I found a medium article where one dev tried this and ran into a lot of recursion depth limits. This is one example of a case where it would be better if we could just use loops, stacks, and other procedural constructs at type time, rather than trying to use declarative constructs to accomplish the same thing. Some people might say running procedural code at type time is a scary pandora's box kind of situation. But pandora's box is already open! The reality of complicated types slowing down the language server or hitting the recursion depth limit is a lot more of a nightmare than the idea of running efficient procedural code, if you think about it. |
We're really of the opinion that code to generate types from a source artifact should run once (when the source artifact changes), not once per keystroke (what happens if you do it in the type system via whatever means). |
@jedwards1211 I actually agree both with you in that there's room for better abstractions here and @RyanCavanaugh that they shouldn't be a part of the language itself. I mentioned ArkType earlier in the thread if you're interested in a highly-optimized type-level string parsing strategy. Currently, the runtime and type-level implementation parsers are implemented in parallel by hand: We've tossed around the idea a bit of creating a package that would provide an API for defining a parser that could generate optimized types and a runtime implementation from a single definition. Probably not our top-priority, but if you're interested in contributing, I'd love to help facilitate making those strategies more reusable! Feel free to reach out on our community Discord. |
I don't understand, doesn't the language server already re-evaluate as you type? |
@ssalbdivad even though ArkType is highly optimized, the size of strings it can parse must be limited by TS recursion depth, right? Since ArkType lets you mix object literals and type strings, a lot of the example strings it parses are short. GraphQL queries tend to be much larger. |
@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. |
@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. |
@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. |
@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. |
@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. |
@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 For example:
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. |
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 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, Even if we moved 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 |
What @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: 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. |
@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! |
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 |
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: