TypeScripts Type System Is Turing Complete
github.com
github.com
However, even being myself a CS student close to finishing my BA degree and stronlgy interested in CS theory, I didn't know that result and I couldn't imagine how powerful TS's typesystem is. So, there actually are a lot of people who underestimate the power of typescripts typesystem completely and who could write even safer code if they knew about it.
I don't know exactly anymore how I "rediscovered" this turing-completeness-property, but at that time I was developing a "fully" typed SQL builder as an alternative to knex (https://github.com/hediet/ts-typed-sql) and did some research on how to make certain SQL constructs typesafe in TypeScript. For example, one thing I needed, was a type RecordTypeToJson<T> which could recursively transform a sql record type T to a proper json type: https://github.com/hediet/ts-typed-sql/blob/master/src/AST/T...
Without the devices discovered in the TC-proof I wouldn't have been able to implement that particular type. And once I recognized the power of TS, I found some other useful devices, e.g. how to use overloading to report custom error messages for invalid types (https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Q...) or how to track whether more than one column is selected (https://github.com/hediet/ts-typed-sql/blob/master/src/AST/Q...).
I hope that these ideas inspire other libraries as well!
And that can also mean that it is error prone.
But with every power comes a weakness. Compile times can no longer just seem endless. They can actually be endless, and there is no way to prove otherwise.
What I find unconvincing about many Turing complete type systems is that pragmatically speaking they are really shitty general purpose programming languages.
If we create Turing complete type systems and suffer the consequences, why not go all the way and make it actually practical to write proper meta programs the way Lisp has done?
And along with Turing machines you've got problems, like undecidability and the halting problem.
Closer and closer to reality. ;)
I tried porting it to Rust a bit back but got stymied by, uh, the typesystem trying to resolve equality in the wrong direction (by adding type constructors instead of removing them) or something. I guess that's UndecidableInstances maybe?
That said, there's some contention in that thread over whether or not Turing completeness has been demonstrated.
In general, having a turing complete type system isn't a major issue, many languages have that property.
When speaking of a general-purpose language you usually want it to be Turing complete. However, you may not want a single subsystem of that language to be Turing complete on its own. That's a lot of complexity for one thing.
Another reason you might not want a Turing-complete language inside your language is it'd be possible to write type declarations that do things semantically separate from the rest of the code. If you're looking at a program you typically think the only logic embedded in the types is constraining the way data is used in the program. All the code to actually do things with the data is elsewhere. If you have a type system that is by itself Turing complete, it could do any calculation someone wanted to encode into it without assistance from the rest of the source code. That's potentially a security nightmare to audit.
Adding time limits radically changes things.
Arbitrary code execution is the holy grail of exploits. If the type system is Turing complete or even nearly so you can encode arbitrary behavior into the types without using any of the language's mainstream operative syntax. One could put an entire subsystem of the running program into what looks like descriptive, conscriptive statements about the data the operative syntax is to use. This is ripe for hiding a source-level trojan in a part of the code that needs little to no support from the rest of the program. When you're first looking at code from others, is your first instinct before compiling it to check deeply in the types defined to make sure there's nothing untoward going on semantically?
Looping forever is a very simple DoS or a very complex mistake. It would also be very simple to end the compilation run and investigate. Intentionally obfuscated malicious code would likely be able to pass unnoticed much longer and do much more damage. The halting problem, realistically, is a problem but is the least of your problems here. It's already quite easy to write a non-halting piece of code on purpose and it's possible accidentally.
The big problem is the unexpected computational power of this sort of thing being abused, not that it's accidentally going to take forever to compile. Nobody's going to die of old age watching an uninterrupted compilation.
This whole argument is nothing more than equivocation: the phrase "arbitrary code execution" means one thing in the security sense but it means something completely different when you are talking about theory of computation.
A Turing machine can execute "arbitrary code" in the sense that it can evaluate any computation. That does not mean that it can effect arbitrary changes to a host computer emulating a Turing machine. That's why sandboxing works. Try writing an HTTP server with a Turing machine: you can't, because Turing machines have no facility for networking. Similarly, just because a type system lets you execute arbitrary code doesn't mean that you can write an exploit in that code, you would need some exploitable endpoint accessible from the type system.
Or in short, just because you can simulate a Turing machine on someone else's computer doesn't mean you can take over their computer.
And yes, nobody's going to die waiting for compilation, but if you can DoS somebody's CI server by making a change to an upstream module which makes compilation take forever, maybe your victim will be pretty unhappy about that.
What I said was that if you are able to hide arbitrary computation of an obfuscated form into what looks like a bunch of innocuous type definitions then run a program that takes over from that point, you can potentially hide malicious code in the type declarations before the program proper even begins to run.
A Turing complete type system can theoretically change the initial state the rest of the compiled code starts under.
Picture this: you clone a repo. There's a file that contains operative code in some paradigm (non-OO imperative, OO imperative, non-OO functional, OO functional, logic, whatever). There's another file that's just types used by that first file. How much attention do you honestly pay to the types before looking at the operative code and then compiling and running it? Now, let's assume someone's found a bit of a bug in your compiler that lets this Turing-machine equivalent type system change the memory addresses of some structures or fill certain parts of memory with machine language. After all, you've not written your compiler to check everything a Turing complete language might do. Then the operative code you're counting on, that you've assumed starts with a clean slate other than the types assumed to be straightforwardly declared, copies that memory somewhere, or seeds a state machine or eval with it.
A Turing complete language means you can do anything any other Turing complete language can do. And having a Turing complete type system without making that clear to language users potentially means it can be obfuscated and effectively hidden. In TypeScript we're talking about a Turing complete subsystem (the type system) that feeds into a Turing complete system (the rest of the language) that translates into another Turing complete system (JavaScript), that gets compiled down to another Turing complete system (the JIT code for the VM). In all that complexity there be dragons.
You might not be familiar with the concept of multi-layer attacks or think they're unlikely to work, but that doesn't mean they don't exist or aren't used in the field.
Now, this really shouldn't be an issue unless someone is deliberately abusive. Java's generic types are also Turing complete[0], and it hasn't been problematic. Just because an abusive program exists doesn't mean it will be written.
But who am I kidding... this is the JavaScript community. I'll give it 2 weeks until someone releases a framework allowing you to write functions that don't compile unless their input is a prime number.
Honestly that seems like it could be pretty useful for making sure that "correct" data is passed at compile-time...
runtime vs compile time. For example someone could write some TypeScript that would forever compile, which is intuitively unexpected when compiling.
The halting problem says that you can't write a halting decision procedure that takes an arbitrary program as input and determines whether that program halts, for any program. That doesn't mean that no programs halt. On the contrary, most programs in Turing complete languages obviously do halt and it's often trivial to tell if a particular program halts or not (e.g., `print "hello"` obviously halts). A Turing complete language can compute anything that is computable. So if the type system is Turing complete, you should be able to type a function that only takes primes... in theory.
Sure, typescript program may never finish compiling, although it will still halt: Just `kill -9`. The halting problem solved! ;-)
Seriously though, there are many languages / systems that are 'accidentally Turing complete', including CSS + HTML, and it doesn't really impede them. See http://beza1e1.tuxen.de/articles/accidentally_turing_complet...
The problem is that you can't really tell when a long compile is an infinite or just a really long one. You want non-Turing completeness because your tools need to be reliable.
Seems like a non-opinionated classification of "overrated".
Or we could go even more meta, since no physical system is Turing complete due to the Bekenstein bound, so any expressible system is necessarily at most an FSA.
If the type checker takes too long, sonething isn't right.
At least if your type checker weren't Turing complete, you know it will finish at some point.
In most cases, you know something is wrong once your typescript compilation takes more than a few seconds. At most, it could be an interesting DOS attack, but most continuous integration systems should have a limit on how much seconds they can run the compiler for. So it's really not a problem if you have constraints on resources...
So, if not turing complete, what kind of automata would you use to accept your language, say if you were designing your own language?
AFAIK, CSS + HTML is not Turing complete, but CSS + HTML + "Human pumping tab and space" is, which makes infinite loops less of a problem.
Specifically, for any implementation of a TS compiler, there is some correct TS program that will never finish compiling.
Every program has a TS compiler that will compile it, but no compiler can work on all programs.
This is addressed by (1) not finishing in these cases or (2) imposing practical limits on the compilation and concluding failure if these are surpassed.
How would you correctly compile a program that has an actual infinite loop in the type system. Some equivalent of while (1) {}
For example, you could translate "the Turning program yields 1" as "the types are valid", and anything else (0 or nontermination) as "the types are not valid".
So "while (true) {}" would correspond to invalid types. And a sufficiently smart interpreter/runtime could conclude that "while (true) {}" does not yield 1, just as a sufficiently smart complier could conclude the type constraints are not met.
But no interpreter (and no compiler) would be able to reach a correct conclusion in all cases.
I think the more motivating reason why this might be a bad thing is it implies the type system is pretty complex and that complexity can be a problem. When users are reading and writing programs, they are running the type system in their head to decide what code to write and reason about how it behaves. If you can create types that cause arbitrary computation to be performed, then you're forcing the user to run a pretty complex simulation in their head.
Worse, unlike the dynamic runtime behavior of their program, they need to do that reasoning before they can even begin to run their program. It's not like "well, sure, you can maybe get the program into a weird state". It's "you won't be able to even run the code at all until you understand and fix all the type errors."
Given that, it's important to keep the type system simple where you can. The challenge is balancing that with the need to make the type system sophisticated enough to not prevent users from writing programs that are dynamically correct. All type systems are inherently pessimistic — there are programs you can write that would do the write thing but where the type system can't prove that so it generates a "false positive" error.
A few of those are tolerable. Most users don't seem to mind adding a seemingly pointless cast here and there, or reorganizing some already-correct code to please the checker. But if they have to do that too much, they start to feel like the language is stupid or getting in their way. See, for example, the perennial complaint about the lack of generics in Go.
Lately, I've been evaluating Relay Modern for a new project, and one of its new features is the ability for the Relay Compiler to generate Flow type definitions based on your GraphQL schema, which makes for a very compelling case to choose Flow if I were to go with Relay Modern for the project. Are there similar tools for generating TypeScript or Flow type definitions from GraphQL schemas for use in the Redux + Apollo ecosystem?
Also, do either type system have a story for leveraging type definitions to perform generative testing like you could in Clojure with Spec?
You can indeed generate TypeScript types from a GraphQL schema, using apollo-codegen: https://github.com/apollographql/apollo-codegen
Generative testing from types in TypeScript isn't something I've seen. With a static type system, if the code compiles then you know it's correct with respect to the types - no amount of automated testing would prove otherwise. In a dynamic language like Clojure where there are no types then you need generated values and tests to try and get some (still incomplete) safety. So you want a rich type system which can capture as much information about your data as possible - TypeScript does a nice job of this, on the whole .
Having said that, if you wanted to provide testing data or constraints along side your types, @decorators provide a means of adding custom annotations - so you, or someone could certainly generate test for data beyond the richness of the type system, e.g. a valid email.
Though now I'm curious how the two systems differ, if at all, in their handling of third party libraries that _lack_ type definitions? From slackingoff2017's response below, it sounds like Flow might handle this scenario a bit more gracefully by still providing some level of static checks, whereas TypeScript would give up on checking any usages of the library altogether, correct?
> Generative testing from types in TypeScript isn't something I've seen. With a static type system, if the code compiles then you know it's correct with respect to the types - no amount of automated testing would prove otherwise. In a dynamic language like Clojure where there are no types then you need generated values and tests to try and get some (still incomplete) safety. So you want a rich type system which can capture as much information about your data as possible - TypeScript does a nice job of this, on the whole .
It's certainly true that in a static type system, generative testing can't derive any value from the types alone, and both Flow and TypeScript are static type systems. That was probably the wrong way to frame my question.
I guess what I'm trying to ask is if there's a runtime property specifications system for JavaScript, similar to Clojure Spec, that can specify more than just properties of a system that are statically provable, and can test those specifications using a generative approach.
Typescript is more of a traditional typing system and discourages you from using variable types in the first place.
The important distinction is that if you tell typescript a function can take in any value it makes no attempt to type check. Flow will look at each usage of the function and try to determine if the value being run through is valid.
My personal preference is to typescript so I'm probably biased. Typescript community, tooling, and general ease of use is better. MS has long been known for good dev tools and it shines here.
If you end goal is to statically type your whole application then flow has little or no advantages. In this case it's better to go with Typescript for ease of use, community support, friendlier error warnings, and better tooling. If your goal is to keep using JavaScript and use type checking as a fancy linter then flow is clearly superior.
Something else I noticed that may be very important down the road: typescript is easier to get rid of. The JavaScript it outputs is very readable and mostly looks hand-written. IMO the best tools are the ones easy to get rid of, especially since JS is such a moving target. If Typescript dies one day you can compile down to JS one more time and throw the TS code away and still have a decent codebase. Flow and Babel produce some really crazy stuff, and codegen of clean and readable JavaScript seems like more of an afterthought.
I'm not sure if I'm misinterpreting what you're saying here, but on the face of it, this is not correct. Flow is just annotations over JS, it is not a compile to JS language like TS.
Flow doesn't produce anything. It's absolutely trivial to remove by just stripping the annotations. There is a babel plugin for doing that, but that's all it does. If there's any output after that that doesn't seem to map well to the original JS code, that's all babel on the remaining JS, nothing to do with Flow. It would be the same with or without Flow. Or did you mean something else?
Typescript combines typing and transpilation together, essentially doing what flow+Babel does. Typescript allows you use newer JS features like Babel but produces much cleaner JavaScript.
If the choice is Typescript or flow without Babel Typescript is the winner by a mile. Without Babel hooked up to flow you can't use any new JS features.
A couple of things which mitigate that downside with babel though, at least for my setup & way of working:
(1)
Sourcemaps. For me, the only practical purpose of touching the transpiled code is debugging. For this purpose I find the sourcemaps output by babel gives me 1-1 mapping to my source anyway, pretty flawlessly with chrome dev tools. So, I have no issues with the messiness or non-messiness of the transpiled code.
(2)
With babel, your source is just JS. Eventually, at some glorious point in the future, we will have enough of those great features available natively in enough browsers that it's possible to turn babel transpilation off.
At that point, Flow has a massive ace up its sleeve in terms of being just an additional layer on top of JS - the build step will be incredibly fast and tiny. Typescript on the other hand will never be just JS. There will never be a total 1-1 mapping (TS is, by design philosophy, a superset of JS), and even if it gets really fast there will always be more of a transpilation step, always source mapping, etc. It will never go away.
So, TS feels like a nice packaged solution now, but will it look so attractive in 5 years? Or maybe a touch over engineered for a problem that doesn't really exist any more? In this sense, to me, Flow feels a bit more future-proof.
It's important to keep in mind that the simplicity of TS's ES5 codegen comes with the tradeoff that it isn't spec-compliant.
For example, given a program `for (const el of arr) { }`, TS's codegen is a loop like `for(var i = 0; i < arr.length; i++) { var el = arr[i]; }` whereas Babel's codegen uses `Symbol.iterator`. The former is technically wrong in an environment where `arr` happens to have a custom `[Symbol.iterator]`.
Another example is ES2015 classes, for which Babel's codegen asserts the constructor is being called with `new` whereas TS's doesn't.
> The important distinction is that if you tell typescript a function can take in any value it makes no attempt to type check. Flow will look at each usage of the function and try to determine if the value being run through is valid.
This reads to me to mean that while annotations are optional in both systems, if you don't provide them for a particular subsystem in TypeScript, the static analysis will simply perform no checks for usages of that particular subsystem, while in Flow it will still attempt to validate your subsystem with properties it can infer on a best-effort basis from things like the way its functions are called.
Heck, I've seen people write whole programs just using clojure.spec which is supposed to be only for type annotations.
Dart has a pretty sophisticated type system — generics, generic methods, function types, subtyping, etc. — but isn't Turing-complete as far as I know.
What is a bit unsettling is that somebody noticed that it was in fact TC: this property should be clear from the type system design and not something to be discovered afterwards.
Pretty sure OCaml type checking is decidable, as is C# and F#, at the very least.
There are two undecidable bit in OCaml's typechecker: 1) Checking module types, due to the possibility of naming and manipulating type signatures, in particular in functors. It's extremely hard to hit by accident, since computing in signatures is quite unidiomatic (and unwieldy). 2) Exhaustiveness of pattern matching for GADTs. You can hit that one (although, not "by accident") fairly easily, so the exploration is bounded and always terminate.
As for Haskell, the base system for typeclasses is not turing complete, you need a specific combination of extensions which are known to be dangerous together.
Finally, to answer the first question ... Most dependently typed languages (Coq, Agda) are not turing complete. People who do research in type systems are usually rather careful about the whole thing.