6 ms·

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other wo

It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!).

golergka 6y ago
Out of curiosity — has there ever been a type system that was discovered to be Turing-complete and then actually have caused a bug for a real application that was caused by the fact that it allowed an invalid program through? I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.
- frivoal 6y ago
  I suspect the opposite situation is what you run into: it is possible to write programs that are valid and out to be accepted by the type system, but get rejected because you blew the stack of the type checker. Had the type checker been allocated more memory / time, it could have accepted the program, but it crashed before that. This reminds me of that: http://litherum.blogspot.com/2019/03/addition-font.html http://litherum.blogspot.com/2019/03/addition-font.html You can craft font files that perform arbitrary calculations… if you give the font shaping engine a (practically) unlimited stack, where it usually limits recursion to 6 levels. If you do so, you can make a font that does math (or whatever you want) as part of computing ligatures. But in practice, you hardly ever hit those kinds of limits unless you're trying to do something silly on purpose. Sure you cannot port Doom to font substitution lookup tables, despite them being Turing complete. But that doesn't make your font shaping engine useless, or even broken.
- deleted 6y ago
  [deleted]
drdeca 6y ago
Can you elaborate on this? I'm not sure what you mean by valid and invalid programs. By "valid", do you mean ones which are well typed under the type system? But then, what does it mean for it to be well typed under the type system, other than that the type system, err, allows it? edit: by which I mean, the theoretically defined type system, not the actual program implementing it.
amelius 6y ago
You mean in case the type-inference doesn't halt? Aren't such programs not very interesting by definition? And why would you call them "valid" programs?
ben-schaaf 6y ago
> In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!). I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.
- TheCoelacanth 6y ago
  Which doesn't matter that much because there is a fairly small limit on how deep recursion can go which you can easily exceed without Turing-completeness, and the distinction between a program that will halt eventually but not within the limit you give it and one that will never halt doesn't matter for practical purposes.
- bodhiandphysics 6y ago
  It’s a consequence of Goedels incompleteness theorem. You cannot create a type system that stops if the program is type valid, and does not stop (or stops indicating invalid) if the program is type invalid. The practical consequences of this are (probably) minimal.
  - bodhiandphysics 6y ago
    The proof is trivial. The valid proofs in Zfc are ennumerable. Let f be a proposition in zfc that is undecidable in zfc. Write a computer program c that checks for a proposition p whether proof number n is a proof of p for all n. Apply that computer program to p. A rust program that is valid iff c(p) either doesn’t stop type checking or is invalid.
    - Kranar 6y ago
      Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article. But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.
DaiPlusPlus 6y ago
> If a type system is Turing complete, than it either has to be inconsistent or incomplete. How is Turing-completeness related to soundness? I am behind on CS theory, but what little I know about category-theory tells me this isn’t the case.
yoneda 6y ago
> It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!). No, you're mixing up concepts (consistency vs. soundness). If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem. A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.
volta83 6y ago
Lol no. The only thing this means is that type checking a Rust program might never terminate. Nothing more, nothing less. It might take 10 seconds, it might take 10 days, it might take till the universe freezes. In practice, the compiler - like pretty much every single compiler with a Turing complete type system - has a recursion limit, that rejects programs that accidentally take too long to type check, but users can increase this limit by adding a source annotation (that's suggested by the compiler). This is completely orthogonal to whether the programs are valid or not. If your program is invalid, the compiler will never accept it, no matter how much compute time you throw at it. Type checking always terminates for valid Rust programs (by definition), so if you throw enough compute at any valid Rust program, the compiler will eventually accept it.

golergka 6y ago

Out of curiosity — has there ever been a type system that was discovered to be Turing-complete and then actually have caused a bug for a real application that was caused by the fact that it allowed an invalid program through? I'm specifically not talking about something like Typescript which is widely known to be unsound, but a type system that was believed to be "safe" before someone figured it is Turing complete.

frivoal 6y ago
I suspect the opposite situation is what you run into: it is possible to write programs that are valid and out to be accepted by the type system, but get rejected because you blew the stack of the type checker. Had the type checker been allocated more memory / time, it could have accepted the program, but it crashed before that. This reminds me of that: http://litherum.blogspot.com/2019/03/addition-font.html http://litherum.blogspot.com/2019/03/addition-font.html You can craft font files that perform arbitrary calculations… if you give the font shaping engine a (practically) unlimited stack, where it usually limits recursion to 6 levels. If you do so, you can make a font that does math (or whatever you want) as part of computing ligatures. But in practice, you hardly ever hit those kinds of limits unless you're trying to do something silly on purpose. Sure you cannot port Doom to font substitution lookup tables, despite them being Turing complete. But that doesn't make your font shaping engine useless, or even broken.
deleted 6y ago
[deleted]

drdeca 6y ago

Can you elaborate on this? I'm not sure what you mean by valid and invalid programs. By "valid", do you mean ones which are well typed under the type system? But then, what does it mean for it to be well typed under the type system, other than that the type system, err, allows it? edit: by which I mean, the theoretically defined type system, not the actual program implementing it.

amelius 6y ago

You mean in case the type-inference doesn't halt? Aren't such programs not very interesting by definition? And why would you call them "valid" programs?

ben-schaaf 6y ago

> In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!). I don't see how this is the case. The type system being Turing complete just makes it undecidable, ie. it's not guaranteed to finish type checking. In a way you could call that "preventing some type valid program", though I wouldn't consider an infinite loop of types valid.

TheCoelacanth 6y ago
Which doesn't matter that much because there is a fairly small limit on how deep recursion can go which you can easily exceed without Turing-completeness, and the distinction between a program that will halt eventually but not within the limit you give it and one that will never halt doesn't matter for practical purposes.
bodhiandphysics 6y ago
It’s a consequence of Goedels incompleteness theorem. You cannot create a type system that stops if the program is type valid, and does not stop (or stops indicating invalid) if the program is type invalid. The practical consequences of this are (probably) minimal.
- bodhiandphysics 6y ago
  The proof is trivial. The valid proofs in Zfc are ennumerable. Let f be a proposition in zfc that is undecidable in zfc. Write a computer program c that checks for a proposition p whether proof number n is a proof of p for all n. Apply that computer program to p. A rust program that is valid iff c(p) either doesn’t stop type checking or is invalid.
  - Kranar 6y ago
    Do you mean apply program c to proposition f? That is compute c(f)? Of course no one disputes that if one encoded this in Rust's type system, Rust will enter an infinite loop. That's the point of this article. But none of this has to do with whether Rust's type system is sound or complete as a type system, only that as a logic it is undecidable.

DaiPlusPlus 6y ago

> If a type system is Turing complete, than it either has to be inconsistent or incomplete. How is Turing-completeness related to soundness? I am behind on CS theory, but what little I know about category-theory tells me this isn’t the case.

yoneda 6y ago

> It’s important to understand that this is a big problem. If a type system is Turing complete, than it either has to be inconsistent or incomplete. In other words it either must allow type invalid programs through, or it must prevent some type valid programs (or both!). No, you're mixing up concepts (consistency vs. soundness). If a type system has non-normalizing types (or non-normalizing terms which appear in types), then it is inconsistent as a logic, which means that via Curry-Howard you can prove anything (ex falso quodlibet). Regarding incompleteness, any sufficiently expressive logic is incomplete per Gödel's first incompleteness theorem. A type system which is inconsistent as a logic can still be sound as a type system. Soundness is the property that you described in your second paragraph (not letting "invalid" programs through). A simple example is System U. It's sound as a type system, but inconsistent as a logic. That means it works for programming, but not for proving.

volta83 6y ago

Lol no. The only thing this means is that type checking a Rust program might never terminate. Nothing more, nothing less. It might take 10 seconds, it might take 10 days, it might take till the universe freezes. In practice, the compiler - like pretty much every single compiler with a Turing complete type system - has a recursion limit, that rejects programs that accidentally take too long to type check, but users can increase this limit by adding a source annotation (that's suggested by the compiler). This is completely orthogonal to whether the programs are valid or not. If your program is invalid, the compiler will never accept it, no matter how much compute time you throw at it. Type checking always terminates for valid Rust programs (by definition), so if you throw enough compute at any valid Rust program, the compiler will eventually accept it.