5 ms·

I had not thought of pattern-exhaustiveness checking like that. Isn't compiling several languages, including Rust, actually undecidable though? Seems like if y

I had not thought of pattern-exhaustiveness checking like that. Isn't compiling several languages, including Rust, actually undecidable though? Seems like if your type system or metaprogramming systems are Turing complete, this has to be the case. So that's ~worse than NP-hard already (though calling it NP-hard is still technically correct).

Zababa 5y ago
Rust's type system is undecidable. You can see a few languages listed here: https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html
- silon42 5y ago
  I believe there are limits to recursion (as mentioned in link above), so not strictly true. Perhaps they are too big?
  - kibwen 5y ago
    Rust's recursion limit is fairly low, I believe it's 128. However, you can override this if you find it too restrictive.
  - randomswede 5y ago
    So (tongue firmly in cheek), no Rust compiler actually fully implements Rust?
simiones 5y ago
This ends up in some discussion about what "compiling" actually means. Is macroexpanding a part of "compiling"? Most languages with complex type systems avoid Turing completeness by having an explicit limit for all type level expansions - at least, that is how Java and C# do it.
- kadoban 5y ago
  I think metaprogram expansion has to be considered part of compiling. You have sourcecode, you need machinecode. If the lang says that the process of getting there requires running some metaprogram, so be it. For Rust I think the type system itself is probably enough though even without that. If neither type checking or metaprogramming are part of compiling, I think your (for hypothetical you) definition of compiling is a bit too restrictive.
  - aj3 5y ago
    Even makefiles are Turing complete.
BBC-vs-neolibs 5y ago
Thanks, I couldn't quite put it in words, but that is exactly my reaction.
jacoblambda 5y ago
Compiling a complete language and verifying correctness is undecidable but that's not necessarily what Rust does. The complier can still fail to compile/verify otherwise correct parts of a program. Because it's only operating on a subset of the entire possible language and it's not verifying all properties of the language, it's not quite undecidable but it is still very much NP-hard. Languages like C, C++, or Ada on the other hand take the other approach. They compile all parts of the language but make little to no attempt to enforce correctness on all those parts. You see verifying compilers for those languages only allowing a subset that they can actually verify which is the same as Rust. At the moment Rust the language is what the main Rust compiler says it is but once there are meaningfully different compilers you'll start to notice the issue a bit more and there will likely be parts of the language that one compiler can verify but the other can't (and therefore fail to compile).
- kibwen 5y ago
  Any hypothetical standards-conformant Rust implementation would have to be as or more restrictive than rustc, not less. Something like mrustc, which performs no borrow checking, would not be allowed to call itself a conformant Rust implementation. (I say hypothetical because until there's a spec, it's simply not feasible to build a conformant alternative implementation, as you'd need to be bug-for-bug compatible with rustc.)
  - ncmncm 5y ago
    This is also not correct. As in, completely wrong. Presuming a formal spec that rustc happens to enforce, another compiler could simply try longer to resolve types before giving up, admitting some set of programs that rustc gives up on.
    - tialaramex 5y ago
      The spec. could specify exactly the rules rustc actually has including iteration limits, this would freeze rustc (and so it would be undesirable) but it is an option. The thing we're talking about here has changed after Rust 1.0, Rust 1.0 shipped with a rule that said if you match integers you have to provide a default. In lots of code that feels natural. But not everywhere. If you match all possible integers (e.g. for a i8 that's from -128 to 127), the compiler would say "Not good enough" until you write the default match it will never actually need. That was fixed with feature(exhaustive_integer_patterns) in 2018 or so AIUI. But you could imagine Rust being standardised with the old behaviour and, even though it's clearly possible to write a compiler which implements feature(exhaustive_integer_patterns) that would then be non-standard because Rust programs lacking the default match for integers are forbidden in the standard.
trissylegs 5y ago
I think in Haskell you need to add: {-# LANGUAGE UndecidableInstances #-} to get an Undecidable type system.
- arianvanp 5y ago
  There are other language extensions to make the haskell type system undecidable. The classic example is `RankNTypes` E.g. you can proof that type systems of rank n >= 3 are undecidable. [0] I think that's why haskell has both Rank2Types and RankNTypes as a language extension. So you can still use higher rank types without running into decidability problems up to rank 2. [0] https://dl.acm.org/doi/10.1145/182409.182456 https://dl.acm.org/doi/10.1145/182409.182456
arianvanp 5y ago
Type checking /compiling often is conservative for this purpose. It's sound (Rejects all incorrect programs), decideable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). There are exceptions of course (C++ templating is turing complete; so type-checking is undecidable) but often you want your compiler to be sound and decidable Also see https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html (edit: Apparently , as the link I posted shows, rust is indeed undecidable in certain edge cases. However you can usually reason about a subset of the language (Restrict using certain features) that is still decidable. I have the feeling Rust might have such a subset but it's just a fuzzy feeling)
- thaumasiotes 5y ago
  > It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that. If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.
  - cedilla 5y ago
    Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually. In my opinion, OP is incorrect and those systems are sound but indecidable.
    - thaumasiotes 5y ago
      > Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.
volta83 5y ago
> Isn't compiling several languages, including Rust, actually undecidable though? While Rust is Turing complete, the compiler has a recursion limit, and if you take that into account, then compiling Rust is decidable (you only need to evaluate compilation up to the recursion limit).
- ghosty141 5y ago
  Rusts type system is turing complete if I recall correctly. Obviously, in practice everything is in a way decidable because we have limitations everywhere.
  - lovasoa 5y ago
    There is a low hardcoded limit to how deep you can nest types. But I don't think there is a hardcoded limitation to how large match patterns can be. That's the difference.
    - smitop 5y ago
      It's possible to change that hardcoded limit. By default it is 256, but you can bring it all the way up to 2^64 with #![recursion_limit = "18446744073709551615"].
  - derefr 5y ago
    In other words, the abstract machine specification you’re programming your compile-time logic against in Rust, has Turing-complete semantics; but its extant implementations — any Rust compiler people would care to use — intentionally does not implement compile-time Turing-completeness. But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete; and that compile-time runtime would be conformant to the Rust language spec. (Just, nobody would want to use it, because “unbounded runtime” isn’t a property people tend to want from their compilers.)
    - dllthomas 5y ago
      > But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete Only if your theory allows for infinite storage...

Zababa 5y ago

Rust's type system is undecidable. You can see a few languages listed here: https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html

silon42 5y ago
I believe there are limits to recursion (as mentioned in link above), so not strictly true. Perhaps they are too big?
- kibwen 5y ago
  Rust's recursion limit is fairly low, I believe it's 128. However, you can override this if you find it too restrictive.
- randomswede 5y ago
  So (tongue firmly in cheek), no Rust compiler actually fully implements Rust?

simiones 5y ago

This ends up in some discussion about what "compiling" actually means. Is macroexpanding a part of "compiling"? Most languages with complex type systems avoid Turing completeness by having an explicit limit for all type level expansions - at least, that is how Java and C# do it.

kadoban 5y ago
I think metaprogram expansion has to be considered part of compiling. You have sourcecode, you need machinecode. If the lang says that the process of getting there requires running some metaprogram, so be it. For Rust I think the type system itself is probably enough though even without that. If neither type checking or metaprogramming are part of compiling, I think your (for hypothetical you) definition of compiling is a bit too restrictive.
- aj3 5y ago
  Even makefiles are Turing complete.

BBC-vs-neolibs 5y ago

Thanks, I couldn't quite put it in words, but that is exactly my reaction.

jacoblambda 5y ago

Compiling a complete language and verifying correctness is undecidable but that's not necessarily what Rust does. The complier can still fail to compile/verify otherwise correct parts of a program. Because it's only operating on a subset of the entire possible language and it's not verifying all properties of the language, it's not quite undecidable but it is still very much NP-hard. Languages like C, C++, or Ada on the other hand take the other approach. They compile all parts of the language but make little to no attempt to enforce correctness on all those parts. You see verifying compilers for those languages only allowing a subset that they can actually verify which is the same as Rust. At the moment Rust the language is what the main Rust compiler says it is but once there are meaningfully different compilers you'll start to notice the issue a bit more and there will likely be parts of the language that one compiler can verify but the other can't (and therefore fail to compile).

kibwen 5y ago
Any hypothetical standards-conformant Rust implementation would have to be as or more restrictive than rustc, not less. Something like mrustc, which performs no borrow checking, would not be allowed to call itself a conformant Rust implementation. (I say hypothetical because until there's a spec, it's simply not feasible to build a conformant alternative implementation, as you'd need to be bug-for-bug compatible with rustc.)
- ncmncm 5y ago
  This is also not correct. As in, completely wrong. Presuming a formal spec that rustc happens to enforce, another compiler could simply try longer to resolve types before giving up, admitting some set of programs that rustc gives up on.
  - tialaramex 5y ago
    The spec. could specify exactly the rules rustc actually has including iteration limits, this would freeze rustc (and so it would be undesirable) but it is an option. The thing we're talking about here has changed after Rust 1.0, Rust 1.0 shipped with a rule that said if you match integers you have to provide a default. In lots of code that feels natural. But not everywhere. If you match all possible integers (e.g. for a i8 that's from -128 to 127), the compiler would say "Not good enough" until you write the default match it will never actually need. That was fixed with feature(exhaustive_integer_patterns) in 2018 or so AIUI. But you could imagine Rust being standardised with the old behaviour and, even though it's clearly possible to write a compiler which implements feature(exhaustive_integer_patterns) that would then be non-standard because Rust programs lacking the default match for integers are forbidden in the standard.

trissylegs 5y ago

I think in Haskell you need to add: {-# LANGUAGE UndecidableInstances #-} to get an Undecidable type system.

arianvanp 5y ago
There are other language extensions to make the haskell type system undecidable. The classic example is `RankNTypes` E.g. you can proof that type systems of rank n >= 3 are undecidable. [0] I think that's why haskell has both Rank2Types and RankNTypes as a language extension. So you can still use higher rank types without running into decidability problems up to rank 2. [0] https://dl.acm.org/doi/10.1145/182409.182456 https://dl.acm.org/doi/10.1145/182409.182456

arianvanp 5y ago

Type checking /compiling often is conservative for this purpose. It's sound (Rejects all incorrect programs), decideable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). There are exceptions of course (C++ templating is turing complete; so type-checking is undecidable) but often you want your compiler to be sound and decidable Also see https://3fx.ch/typing-is-hard.html https://3fx.ch/typing-is-hard.html (edit: Apparently , as the link I posted shows, rust is indeed undecidable in certain edge cases. However you can usually reason about a subset of the language (Restrict using certain features) that is still decidable. I have the feeling Rust might have such a subset but it's just a fuzzy feeling)

thaumasiotes 5y ago
> It's sound (Rejects all incorrect programs), decidable (There is an algorithm to reject all incorrect programs) but due to Godel's decidability problem they're incomplete (There are always correct programs which the type checker rejects as incorrect). Isn't that the definition of "semidecidable" as distinct from "decidable"? A decidable question is one where you can determine the answer, whatever that answer may be. A semidecidable question is one where, if the answer is yes, you can determine that, and if the answer is no, you may not be able to determine that. If you can always show that a program is incorrect, but you can't necessarily show that a program is correct, then the correctness of a program isn't decidable.
- cedilla 5y ago
  Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. It's the same as having a generator that generates every correct formula eventually. In my opinion, OP is incorrect and those systems are sound but indecidable.
  - thaumasiotes 5y ago
    > Semi-decidable means that will accept all correct formulas, and either rejects incorrect formulas or gives no answer. By this definition, program incorrectness isn't semidecidable either - the compiler will accept all correct [incorrect] formulas, and will either reject or accept incorrect [correct] formulas.

volta83 5y ago

> Isn't compiling several languages, including Rust, actually undecidable though? While Rust is Turing complete, the compiler has a recursion limit, and if you take that into account, then compiling Rust is decidable (you only need to evaluate compilation up to the recursion limit).

ghosty141 5y ago
Rusts type system is turing complete if I recall correctly. Obviously, in practice everything is in a way decidable because we have limitations everywhere.
- lovasoa 5y ago
  There is a low hardcoded limit to how deep you can nest types. But I don't think there is a hardcoded limitation to how large match patterns can be. That's the difference.
  - smitop 5y ago
    It's possible to change that hardcoded limit. By default it is 256, but you can bring it all the way up to 2^64 with #![recursion_limit = "18446744073709551615"].
- derefr 5y ago
  In other words, the abstract machine specification you’re programming your compile-time logic against in Rust, has Turing-complete semantics; but its extant implementations — any Rust compiler people would care to use — intentionally does not implement compile-time Turing-completeness. But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete; and that compile-time runtime would be conformant to the Rust language spec. (Just, nobody would want to use it, because “unbounded runtime” isn’t a property people tend to want from their compilers.)
  - dllthomas 5y ago
    > But you could in theory write a Rust compiler whose compile-time runtime is fully Turing-complete Only if your theory allows for infinite storage...