18 ms·

CS student here, why is Turing completeness a bad thing in this case?

cwyers 9y ago
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.
- amenghra 9y ago
  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.
  - Gehinnn 9y ago
    This is how the TypeScript team fixed this issue: https://github.com/Microsoft/TypeScript/pull/15011 https://github.com/Microsoft/TypeScript/pull/15011
cestith 9y ago
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.
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 ago
    I 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 ago
      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?
      - 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.
mhh__ 9y ago
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?
munificent 9y ago
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.
SolarNet 9y ago
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.

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.

amenghra 9y ago
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.
- Gehinnn 9y ago
  This is how the TypeScript team fixed this issue: https://github.com/Microsoft/TypeScript/pull/15011 https://github.com/Microsoft/TypeScript/pull/15011

cestith 9y ago

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.

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 ago
  I 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 ago
    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?
    - 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.

mhh__ 9y ago

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?

munificent 9y ago

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.

SolarNet 9y ago

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.