10 ms·

Rust's type system is Turing-complete (2017)

114 points by lukastyrychtr 6y ago

dang 6y ago
Discussed at the time: Rust's Type System Is Turing-Complete: Type-Level Programming in Rust - https://news.ycombinator.com/item?id=13843288 https://news.ycombinator.com/item?id=13843288 - March 2017 (117 comments)
weberc2 6y ago
Relatedly, I found this out the hard way yesterday evening: https://stackoverflow.com/questions/66631251/overflow-evaluating-the-requirement-for-simple-trait-implementation https://stackoverflow.com/questions/66631251/overflow-evalua...
bodhiandphysics 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!).
- 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.
lmm 6y ago
To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, make sure that you're getting a return on that complexity by ensuring that your type system has the features that you need to do useful things.
- slavapestov 6y ago
  I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here. Higher-kinded types, dependent types and kind polymorphism don't actually mean your type system becomes undecidable. They do vastly complicate the implementation in other ways, though.
  - TheCoelacanth 6y ago
    It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
    - continuational 6y ago
      That makes it nearly impossible for the programmer to predict what will type check and what will not.
      - viuphiet 6y ago
        This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.
        mannerheim 6y ago
de6u99er 6y ago
This is impressive and hilarious at the same time. Thanks for sharing!
cphoover 6y ago
One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type system) only furthers my belief that the complexity of some type systems is not worth it. I feel I'm in a minority here... but I like the nimbleness of dynamic languages, or languages where the type system has a minimal presence.
- okareaman 6y ago
  You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.
  - konjin 6y ago
    Yes and? I have the full power of the language to force type correctness instead of some janky meta language.
    - whatshisface 6y ago
      Most dependently typed languages allow you to use the full power of the language to specify types.
    - creata 6y ago
      You also don't have the power to force anything, just the power to check if it's correct in a few of the infinitely many cases. And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.
    - feoren 6y ago
      And if you're really good, you'll use that full power to develop a toolset of useful ways to verify that certain properties about your code hold! You'll see common errors and write infrastructure to help your unit tests ensure those errors aren't happening. You might even add annotations into your code as you write it to automatically write those unit tests for you. And you will have invented ... the Inner Type System!
jhanschoo 6y ago
> Most if not all Turing-complete systems are also known to be Turing-equivalent. (I regret not being able to find a better citation for this.) It links to Wikipedia (WP), which defines "system" by: > a computational system (such as an abstract machine or programming language) there is no better citation[0], because it's not true under some definitions of "computational system", per WP's definition of "computational system" [3]. For example, under the WP definition of "abstract machine", a non-computable function satisfies the definition. Or we can define it as follows: input: strings in an alphabet A, output: {true, false}, operations allowed: check for membership in a language L in alphabet A. So we see that theoretical formal languages are a subset of computational systems. But there are uncountably many formal languages and only countably many TM. Crucially, we can easily turn each language into one that acts as a universal turing machine while still being distinct. Hence there are uncountably many Turing-complete languages for a given alphabet A[2] [0]: incidentally, the linked WP page claims slightly differently (unimportantly) that "All known Turing-complete systems are Turing-equivalent, which adds support to the Church–Turing thesis." [1]: "A typical abstract machine consists of a definition in terms of input, output, and the set of allowable operations used to turn the former into the latter." Absent a more precise definition, I assume the set may include arbitrary mathematical operations (and it is useful to define non-computable abstract machines, and in general usage in the field abstract machines may refer to languages more powerful than Turing machines). [2]: Sketch: Let U' be a Universal TM in alphabet A (hence U is Turing-complete), let M' denote the language it accepts, and let 0 be a symbol of A. Define M such that if i' in M', then i in M, where i is i' with every symbol duplicated and 0 prefixed (hence if i'="123", i="0112233") Define N such that if i' in complement(M'), then i in N, where i is i' with every symbol duplicated and 0 prefixed. Observe that every language disjoint from N that contains M is Turing-complete (wrt a slightly modified description for TMs and the simulated input than the one for U'). Now, let L be an arbitrary language in A. Define f(L) = { j | j' in L, j is j' with every symbol duplicated }. Then we see that f(L), M, N are all disjoint. And if T, U are distinct languages, so (f(T) union M) and (f(U) union M) are distinct languages that simulate Turing machines (i.e. they are Turing-complete). Hence there are uncountably many Turing-complete languages. There are only countably many Turing machines, hence only countably many Turing-equivalent languages, so in fact most Turing-complete languages are not Turing-equivalent languages. [3]: of course,
c3534l 6y ago
The article is fascinating and I love fun stuff like this, but the discussion is a bit off the rails. There are a lot of things that are accidentally Turing complete. Turing complete is not synonymous with complicated and unwieldy to use. I mean, okay, maybe if you are doing the stuff that the author is doing it is complicated and unwieldy - in fact to the point that you would never do it in the first place. But Turing completeness is really not a high bar to reach.
- Kranar 6y ago
  You are correct, furthermore having a Turing complete system does not forbid one from choosing an expressive subset of the system that isn't Turing complete.
  - ObscureScience 6y ago
    That's true, but I you really don't need the computational power, you might want to have that well defined limited semantic to either not accidentally shoot you in foot (the least important), or being able to statically verify it's properties in finite time.
- nestorD 6y ago
  To further push the point that many things are Turing complete and that it should not be seen as synonymous with complex, Gwern has a nice list of Surprisingly Turing complete things [0] that includes Peano Arithmetic, Pokemon Yellow and Magic the Gathering. I personally find lists of programming language that made the conscious decision to not be Turing complete (such as Coq the theorem prover) more intriguing. [0]: https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete
  - dragontamer 6y ago
    > To further push the point that many things are Turing complete and that it should not be seen as synonymous with complex, Gwern has a nice list of Surprisingly Turing complete things [0] that includes Peano Arithmetic, Pokemon Yellow and Magic the Gathering. If you know how to reach Turing completeness in those systems, you wouldn't call any of those "simple". MtG for instance is considered one of the more complicated card games. Pokemon Yellow's turing completeness proof involved arbitrary code execution by swapping memory locations around. Peano axioms / Arithmetic underlies an entire theory of abstract mathematics. --------------- EDIT: I think decidable is an important attribute of systems that are weaker than Turing Complete. There are still very powerful decidable equations (ex: 3SAT, most famously), which has an answer (either satisfiable, or unsatisfiable), but may need O(2^n) time (or longer) to calculate the result. Turing Complete is only semi-decidable: if something halts it will halt in finite time. If something won't halt, you'll never know.

114 points by lukastyrychtr 6y ago

dang 6y ago

Discussed at the time: Rust's Type System Is Turing-Complete: Type-Level Programming in Rust - https://news.ycombinator.com/item?id=13843288 https://news.ycombinator.com/item?id=13843288 - March 2017 (117 comments)

weberc2 6y ago

Relatedly, I found this out the hard way yesterday evening: https://stackoverflow.com/questions/66631251/overflow-evaluating-the-requirement-for-simple-trait-implementation https://stackoverflow.com/questions/66631251/overflow-evalua...

bodhiandphysics 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!).

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.

lmm 6y ago

To me the main takeaway of results like this is: you're already paying the full price of using whatever complicated type system feature you care to name. So I have limited sympathy for people who are scared of the complexity of, say, higher-kinded types, or dependent types, or kind polymorphism. Your type system is already as complicated as possible, adding more features won't make it more Turing-complete - rather, make sure that you're getting a return on that complexity by ensuring that your type system has the features that you need to do useful things.

slavapestov 6y ago
I disagree. A terminating type checker is much more valuable than a possibly non-terminating one. Also I think you're possibly conflating multiple issues here. Higher-kinded types, dependent types and kind polymorphism don't actually mean your type system becomes undecidable. They do vastly complicate the implementation in other ways, though.
- TheCoelacanth 6y ago
  It's easy enough to turn a non-terminating type checker into a terminating one, just add a recursion limit.
  - continuational 6y ago
    That makes it nearly impossible for the programmer to predict what will type check and what will not.
    - viuphiet 6y ago
      This isn't a problem at all for modern type systems. OCaml, Haskell, and even C++ have Turing complete type systems and this is one of the last concerns for developers.
      - mannerheim 6y ago

de6u99er 6y ago

This is impressive and hilarious at the same time. Thanks for sharing!

cphoover 6y ago

One of the reasons I like weak type systems or duck typing as is with vanilla JS is because I don't have cognitive overload... I don't have to think about abstractions as types I only need to think how to solve the problem in front of me. My unit tests can check for correctness after I've solved the problem. The fact that you can have Turing completeness in a type-system (not the language itself but within it's type system) only furthers my belief that the complexity of some type systems is not worth it. I feel I'm in a minority here... but I like the nimbleness of dynamic languages, or languages where the type system has a minimal presence.

okareaman 6y ago
You do realize that you're moving part of the cognitive load until later and increasing it when you have to implement a type checker in unit tests for every program you write.
- konjin 6y ago
  Yes and? I have the full power of the language to force type correctness instead of some janky meta language.
  - whatshisface 6y ago
    Most dependently typed languages allow you to use the full power of the language to specify types.
  - creata 6y ago
    You also don't have the power to force anything, just the power to check if it's correct in a few of the infinitely many cases. And yes, as a sibling comment said, dependently typed languages let you use the entire language to specify types.
  - feoren 6y ago
    And if you're really good, you'll use that full power to develop a toolset of useful ways to verify that certain properties about your code hold! You'll see common errors and write infrastructure to help your unit tests ensure those errors aren't happening. You might even add annotations into your code as you write it to automatically write those unit tests for you. And you will have invented ... the Inner Type System!

jhanschoo 6y ago

> Most if not all Turing-complete systems are also known to be Turing-equivalent. (I regret not being able to find a better citation for this.) It links to Wikipedia (WP), which defines "system" by: > a computational system (such as an abstract machine or programming language) there is no better citation[0], because it's not true under some definitions of "computational system", per WP's definition of "computational system" [3]. For example, under the WP definition of "abstract machine", a non-computable function satisfies the definition. Or we can define it as follows: input: strings in an alphabet A, output: {true, false}, operations allowed: check for membership in a language L in alphabet A. So we see that theoretical formal languages are a subset of computational systems. But there are uncountably many formal languages and only countably many TM. Crucially, we can easily turn each language into one that acts as a universal turing machine while still being distinct. Hence there are uncountably many Turing-complete languages for a given alphabet A[2] [0]: incidentally, the linked WP page claims slightly differently (unimportantly) that "All known Turing-complete systems are Turing-equivalent, which adds support to the Church–Turing thesis." [1]: "A typical abstract machine consists of a definition in terms of input, output, and the set of allowable operations used to turn the former into the latter." Absent a more precise definition, I assume the set may include arbitrary mathematical operations (and it is useful to define non-computable abstract machines, and in general usage in the field abstract machines may refer to languages more powerful than Turing machines). [2]: Sketch: Let U' be a Universal TM in alphabet A (hence U is Turing-complete), let M' denote the language it accepts, and let 0 be a symbol of A. Define M such that if i' in M', then i in M, where i is i' with every symbol duplicated and 0 prefixed (hence if i'="123", i="0112233") Define N such that if i' in complement(M'), then i in N, where i is i' with every symbol duplicated and 0 prefixed. Observe that every language disjoint from N that contains M is Turing-complete (wrt a slightly modified description for TMs and the simulated input than the one for U'). Now, let L be an arbitrary language in A. Define f(L) = { j | j' in L, j is j' with every symbol duplicated }. Then we see that f(L), M, N are all disjoint. And if T, U are distinct languages, so (f(T) union M) and (f(U) union M) are distinct languages that simulate Turing machines (i.e. they are Turing-complete). Hence there are uncountably many Turing-complete languages. There are only countably many Turing machines, hence only countably many Turing-equivalent languages, so in fact most Turing-complete languages are not Turing-equivalent languages. [3]: of course,

c3534l 6y ago

The article is fascinating and I love fun stuff like this, but the discussion is a bit off the rails. There are a lot of things that are accidentally Turing complete. Turing complete is not synonymous with complicated and unwieldy to use. I mean, okay, maybe if you are doing the stuff that the author is doing it is complicated and unwieldy - in fact to the point that you would never do it in the first place. But Turing completeness is really not a high bar to reach.

Kranar 6y ago
You are correct, furthermore having a Turing complete system does not forbid one from choosing an expressive subset of the system that isn't Turing complete.
- ObscureScience 6y ago
  That's true, but I you really don't need the computational power, you might want to have that well defined limited semantic to either not accidentally shoot you in foot (the least important), or being able to statically verify it's properties in finite time.
nestorD 6y ago
To further push the point that many things are Turing complete and that it should not be seen as synonymous with complex, Gwern has a nice list of Surprisingly Turing complete things [0] that includes Peano Arithmetic, Pokemon Yellow and Magic the Gathering. I personally find lists of programming language that made the conscious decision to not be Turing complete (such as Coq the theorem prover) more intriguing. [0]: https://www.gwern.net/Turing-complete https://www.gwern.net/Turing-complete
- dragontamer 6y ago
  > To further push the point that many things are Turing complete and that it should not be seen as synonymous with complex, Gwern has a nice list of Surprisingly Turing complete things [0] that includes Peano Arithmetic, Pokemon Yellow and Magic the Gathering. If you know how to reach Turing completeness in those systems, you wouldn't call any of those "simple". MtG for instance is considered one of the more complicated card games. Pokemon Yellow's turing completeness proof involved arbitrary code execution by swapping memory locations around. Peano axioms / Arithmetic underlies an entire theory of abstract mathematics. --------------- EDIT: I think decidable is an important attribute of systems that are weaker than Turing Complete. There are still very powerful decidable equations (ex: 3SAT, most famously), which has an answer (either satisfiable, or unsatisfiable), but may need O(2^n) time (or longer) to calculate the result. Turing Complete is only semi-decidable: if something halts it will halt in finite time. If something won't halt, you'll never know.