6 ms·
Turing complete systems are highly capable, and thus, are harder to prove anything about. The halting problem notwithstanding, there's first the "there are thin
by unholiness 9y ago
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 https://arxiv.org/pdf/1605.05274.pdf
- notamy 9y ago> 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...
- pmiller2 9y agoI believe "don't compile," in this context, is short for "their compilation doesn't halt." That seems like a bad thing to me. ;)
- myusernameisok 9y agoI 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?
- shusson 9y ago> 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.
- deleted 9y ago[deleted]
- mmalone 9y agoNot 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.
- computerex 9y agoC++ templates are also Turing complete.
- ygra 9y agoI 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.)
- thegeomaster 9y agoI'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.
- mmalone 9y agoYea, turns out programmers are pretty good at writing code that halts in Turing complete languages.
- flashmob 9y ago> 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_complete.html http://beza1e1.tuxen.de/articles/accidentally_turing_complet...
- naasking 9y ago> 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.
- amelius 9y agoYes, but you want your tools to be powerful at the same time.
- naasking 9y agoThere's plenty of power below Turing completeness. Turing completeness is overrated.
- amelius 9y agoThat's an opinion, of course.
- naasking 9y agoWhat'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.
- paulddraper 9y ago> 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.
- yoz-y 9y ago> 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) {}
- lmm 9y agoA 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.
- Asooka 9y agoHow 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.
- lmm 9y agoFor 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.
- paulddraper 9y agoThe 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.
- Gehinnn 9y agoIn 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