When I discussed my discovery with a friend of mine who is doing his PhD, he was not really excited about it and once I showed him the features of TypeScripts typesystem, he immediately explained me why it has to be turing complete.
So in theory, this result is nothing new and nothing "newsworthy".
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...
A turing complete system doesn't necessarily mean it's powerful, or useful, it just means that it's equivalent with a turing machine and in the case of type systems, that usually happens because general recursivity is allowed.
It doesn't mean useful, but in my opinion it definitely means powerful. Being expressive enough to describe any possible algorithm is a power. No self respecting super hero would deny that, not even TypeScript's worst enemy.
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?
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?
Turing complete systems are highly capable, and thus, are harder to prove anything about. The halting problem notwithstanding, there's first the "there are things that don't halt" problem: that is, you can write a valid TypeScript program that will never finish compiling.
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.
> Sure, typescript program may never finish compiling, although it will still halt: Just `kill -9`. The halting problem solved! ;-)
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.
Turing complete means that it's a simulation of a Turing machine, but not actually one. A TM is something purely abstract that was invented to prove the halting problem, and infinity of the tape is arguably the most crucial concept. Computers do not have infinite memory / power / time so the halting problem doesn't really make sense unless you talk about a pure Turing machine with infinite tape.
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...
Sure, I can see your point. It's a problem for computer scientists, and good to know as an anecdote. I'm talking about it in practice - when using TypeScript the 'halting problem' has never been an issue. I was joking about the 'kill -9' but also meant it in a half-hearted way!
So, if not turing complete, what kind of automata would you use to accept your language, say if you were designing your own language?
How could you possibly quantify "too long" when you can perform arbitrary computation at compile-time? How do you know the library you're using doesn't need you to compute and embed the first N primes in the final output?
At least if your type checker weren't Turing complete, you know it will finish at some point.
What's not an opinion is that most programs we write are more easily and compactly expressed with general recursion, but often don't need general recursion to reproduce the same output.
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.
Aha! I had a look to confirm, and you are right! In essence, html + css is not. However if we have a human hitting tabs and spaces for a long enough time, then for all intents and purposes, perhaps it is? Anyhow, it's still very impressive that we can do a lot of complex computations simply by hitting tabs and spaces!
I'd like to emphasize what you said---that's not an inherently bad thing, but as most powerful features of languages, it can be abused. A lot of languages have Turing-complete type systems, and I have yet to see a serious abuse of this in production code. For example, C++ has some really cool libraries that do a lot of stuff at the type-level, and this has been acknowledged and even made more explicit and usable, with the introduction of constexpr, which basically lets you run plain old imperative code at compile-time.
> you can write a valid TypeScript program that will never finish compiling.
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.
The equivalent of "while (true) {}" depends on how you want to reduce your Turing program to the type system.
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.
A program like that isn't a valid typescript program, so failing to compile it is less of a bug. The point is that there are correctly-typed typescript programs that the compile won't compile.
How can you, specifically you the human, typecheck the program if it has an infinite loop in the types? If you can typecheck it, then I can write a compiler to typecheck it, repeat until my compiler can typecheck every correctly-typed program a human can write, at which point the problem becomes moot.
For every specific typescript compiler, there is a correct typescript program that that complier fails to compile. The ones for particular humans will generally not be the same as the ones for particular compilers.
Not necessarily. You should be able to write a halting computation to determine whether a number is prime in a Turing complete language. It may be stupid hard to encode, or take a really long time to run, however.
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.
I don't understand how this is fundamentally different from just doing it in regular javascript. You could write a javascript function that recurses forever on condition x:
just write a function that calls itself with the same parameters unless condition x is met. How is it fundamentally different if the type system does it?
I think most people knowing C++ know that. But since then we've tried to avoid the same complexity in most newer languages. Thus, the fact that TypeScript, Java, and C# all have Turing-completeness more or less by accident in their type systems may be surprising. (Granted, template metaprogramming was also more an accidental discovery than a design goal of C++, but it's been around for a while longer.)
The typical answer here is "It means the type checker might run forever". That's a sort of scary worst-case scenario, but I don't think it's that relevant in practice.
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.
The halting problem, basically. It's possible for something constructed in the type system (not the program that's being typed, like a type declaration) to recurse infinitely and never stop running until terminated.
That said, there's some contention in that thread over whether or not Turing completeness has been demonstrated.
I don't think Turing completeness is necessarily bad here.
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.
We generally want the compiler to finish within a reasonable amount of time and either give a compiled version of the program or an error message. This is literally impossible if the type system is Turing complete, because the type checker could loop forever and you'd be unable to detect the difference between a program that can't be compiled and one that just takes a long time to compile.
There are problems well beyond infinite compile times and infinite runtimes with a Turing-complete sublanguage hidden in something as innocuous looking as the type system.
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.
> There are problems well beyond infinite compile times and infinite runtimes with a Turing-complete sublanguage hidden in something as innocuous looking as the type system.
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.
You have yourself one heck of a strawman there. Never did I say it enabled execution of arbitrary code injected from outside.
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.
A naive question: Is it only the type inference that will recurse indefinitely? I.e. If you always specify your types and cast them explicitly, is the Turing completeness still an issue?
The properties that enable TS' type system to be turing complete are recursive types and indexer types.
Indexer types allow you to write `{ foo: string }["foo"]` which results in the type `string`.
The language still is, just not the environment in which it runs. Much like a language can be Turing-complete without having infinite tape/memory to run on.
When people say "Turing-complete" it's usually assumed that we are talking about computational models which could emulate Turing machines given infinite memory. But we don't have infinite memory.
It doesn't have to loop forever, it could just take a few minutes to calculate. There are plenty of useful, real-world projects that take hours to compile (see: any large project in C++). To reject these programs due to an arbitrary timeout is a non-starter.
Because it was probably accidental. As opposed to using something like Lisp macros, where meta programming doesn't require using the type system language and shoving it into the shape you need, and is basically normal programming. Now that it's been discovered people are going to rely on the quirks that enabled it, and it's now an accidently designed meta programming language inside your type system. See C++ for why that is bad.
Opinions of this differ, see C++ templates etc: Simplistically, this now makes it easier for code to get very complex (a la C++ templates). The question is, should this be in the hands of the language designers or the users of said language?
Not entirely on topic, but I'm curious if anyone could comment on the similarities and differences between TypeScript and Flow in their more recent iterations. I've been doing a bit of research and it seems like they've grown to become fairly similar in terms of syntax and overall capability, but I'd love to hear if anyone has compelling reasons as to why you'd choose one over the other.
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?
My personal take on this is that TypeScript has surpassed Flow in its feature set and the availability of typings for existing libraries. The features which previously made Flow unique have been incorporated into TypeScript, two particular favourites of mine being string literal types and tagged unions.
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.
Thanks for the response. TypeScript definitely seems to be the community favorite, and availability of third-party type definitions is definitely an important concern. Will definitely take a look at apollo-codegen.
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.
The two are converging in a lot of ways. Flow maintains it's impressive ability to determine types based on individual usages of functions. Basically checking type safety based on what you passed in rather than what the function says it's supposed to take.
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.
> If Typescript dies one day you can compile down to JS... flow and babel produce some really crazy stuff
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?
Typically you use flow with Babel so you can use newer JavaScript features. Babel creates messy JavaScript in the process of transpilation.
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.
>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.
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.
Thanks for the response. I have no interest in statically typing my entire application, so being able to preserve JavaScript's dynamic nature to maximize iterate speed while still deriving some value from static type analysis (and having the option to specify manual types to improve the analysis) is an extremely attractive prospect for me. I was under the impression that both TypeScript and Flow would support this, but your account definitely pushes me a bit further in favor of Flow.
"If you end goal is to statically type your whole application then flow has little or no advantages" does not somehow translate to: If your end goal is to /not/ statically type your whole application then typescript has a disadvantage. Both TypeScript and Flow are gradually typed and annotations are completely optional at every step of the way. Neither TypeScript nor Flow differ whatsoever in this regard.
Hmm... did I somehow misinterpret this statement from the GP?
> 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.
Typescript also tries to infer types, and falls back to an implicit "any" type when it can't. Flow was better at type inference, but I don't know if it still is.
Okay, but you know what else is Turing complete? BASIC. Bash script. Assembly. In 2017 I'm not sure that something being Turing complete should be considered a shocker, or even that meaningful.
Heck, I've seen people write whole programs just using clojure.spec which is supposed to be only for type annotations.
Why is this considered newsworthy? How many practical type systems do you know that are not Turing-complete, yet powerful enough as development aids? (Hindley-Milner doesn't count. HM might have decidable type checking, but actual programming languages don't just use HM. In particular, OCaml and GHC Haskell do not have decidable type checking.) Heck, maybe computer scientists ought to do more research into non-Turing-complete development tools.
OCaml's _type_ system is not turing complete (unless you have a new striking example to provide, but this would be considered a critical soundness bug).
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.
To me, the issue is not the type system being TC, which may or may not be desirable depending on applications.
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.
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!