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.

[0] https://arxiv.org/pdf/1605.05274.pdf

> you can write a valid TypeScript program that will never finish compiling

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

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

Except you know no such thing, that's the point. That could very well be the intended and correct behaviour of the compiler for that input.

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?

Isn't that irrelevant in that case?

If the type checker takes too long, sonething isn't right.

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.

But if you got a deadline, everything over it is bad.

Sure, but "not fast enough for me because X" and simply "wrong/incorrect" are completely different claims.

Yes, but you want your tools to be powerful at the same time.

There's plenty of power below Turing completeness. Turing completeness is overrated.

That's an opinion, of course.

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.

>CSS + HTML

AFAIK, CSS + HTML is not Turing complete, but CSS + HTML + "Human pumping tab and space" is, which makes infinite loops less of a problem.

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.

Yea, turns out programmers are pretty good at writing code that halts in Turing complete languages.

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

> Every program has a TS compiler that will compile it, but no compiler can work on all programs.

How would you correctly compile a program that has an actual infinite loop in the type system. Some equivalent of while (1) {}

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.

I see. I got confused by the fact that for me a program that never ends is still valid, but I understand how this makes no sense for a type system.

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.

In my mentioned bug report I even showed an implementation of a type "IsPrime<T>" which can only be instantiated if T represents a prime number :D

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

I believe "don't compile," in this context, is short for "their compilation doesn't halt." That seems like a bad thing to me. ;)

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?

> How is it fundamentally different if the type system does it?

runtime vs compile time. For example someone could write some TypeScript that would forever compile, which is intuitively unexpected when compiling.

C++ templates are also Turing complete.

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.

That can be solved by setting a reasonable upper bound on how many types can be nested.

In general, having a turing complete type system isn't a major issue, many languages have that property.

This is how the TypeScript team fixed this issue: https://github.com/Microsoft/TypeScript/pull/15011

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?

Type inference is not necessary in general nor does it look like the TypeScript example here uses type inference in any significant way.

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

It's not impossible, the error message will just be "timeout".

That's redefining the problem—if you add a timeout, you are explicitly making the language not Turing complete any more.

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.

Adding time limits radically changes things.

Then you get valid programs timing out when they would have compiled otherwise.

Even if it's technically valid it's not likely to be a useful program if it has an unhalting loop in its data type declarations and enforcement.

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?