7 ms·

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

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.

klodolph 9y ago
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.
- krastanov 9y ago
  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?
  - klodolph 9y ago
    Type inference is not necessary in general nor does it look like the TypeScript example here uses type inference in any significant way.
    - Gehinnn 9y ago
      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`.
  - deleted 9y ago
    [deleted]
- icebraining 9y ago
  It's not impossible, the error message will just be "timeout".
  - chongli 9y ago
    Then you get valid programs timing out when they would have compiled otherwise.
    - cestith 9y ago
      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.
      - chongli 9y ago
        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.
  - klodolph 9y ago
    That's redefining the problem—if you add a timeout, you are explicitly making the language not Turing complete any more.
    - icebraining 9y ago
      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.
      - klodolph 9y ago
        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.
- cestith 9y ago
  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.
  - deleted 9y ago
    [deleted]
  - deleted 9y ago
    [deleted]
  - klodolph 9y ago
    > 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.

klodolph 9y ago

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.

krastanov 9y ago
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?
- klodolph 9y ago
  Type inference is not necessary in general nor does it look like the TypeScript example here uses type inference in any significant way.
  - Gehinnn 9y ago
    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`.
- deleted 9y ago
  [deleted]
icebraining 9y ago
It's not impossible, the error message will just be "timeout".
- chongli 9y ago
  Then you get valid programs timing out when they would have compiled otherwise.
  - cestith 9y ago
    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.
    - chongli 9y ago
      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.
- klodolph 9y ago
  That's redefining the problem—if you add a timeout, you are explicitly making the language not Turing complete any more.
  - icebraining 9y ago
    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.
    - klodolph 9y ago
      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.
cestith 9y ago
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.
- deleted 9y ago
  [deleted]
- deleted 9y ago
  [deleted]
- klodolph 9y ago
  > 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.