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).
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
(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)
Generics is not really the right cutting point: parametric polymorphism is perfectly decidable. However, few languages stop at just parametric polymorphism. For instance, the OCaml issue in the linked blog post happens at the module level, which mixes parametric polymorphism and subtyping. And typically, while SML has parametric polymorphism, it lacks the OCaml extension that makes the module type system undecidable.
Haskell's System-F is definitely completely is decidable. You need to opt in to undecidable features like RankNTypes (n>=3) explicitly. (which are GHC; and not Haskell specific).
Even then; Undecidability is a bit spectrumy. e.g. RankNTypes become sort of decideable again in the presence of explicit type annotations
For an example of contrary, one can check Agda. It is not Turing complete, but a useful language (I personally wrote many parsers in it and its Haskell FFI is pretty good so you can essentially write unsafe parts of your programs in Haskell, and safe parts in Agda then prove correctness).
> 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.
Decide-ability here means "Can we come to an answer in a known amount of steps". If you have an algorithm for type checking; then that answer is yes! You're _always_ able to come up with an answer that is yes or no.
For example the following algorithm is for typechecking is decideable:
typechecks :: Program -> Bool
typechecks _ = false
We always come to decision. There is no "semi" here. Just a clear yes/no answer.
The algorithm is even sound. It rejects all incorrect programs.
However it is not complete. It might also reject correct programs (In this case it rejects all correct programs).
Of course you want a as little conservative typechecker without getting into trouble. But it's always conservative to some extent. Preferably you would both be sound _and_ complete. But the problem is that any reasonable logic system can't proof its own consistency.
Hence we can't have both. However we can get "as close as we possibly can".
I believe you're explaining what a computable function is. A decidable set S of a type T is defined to be one for which there is a computable function f : T -> Bool such that the set of values x with f x = true is equal to S. A semidecidable set S of a type T is defined to be one for which there is a partial computable function f : T -> Bool such that whenever x is in S, then f x is computable and equals true.
Given a definition for a well-typed program, you get a set W of Program of the well-typed programs. You can ask whether W is decidable or semidecidable -- i.e., whether there is some (partial) computable function f : Program -> Bool with the above properties.
The example you give is certainly computable, but it has nothing to do with the set W, so it says nothing about (semi)decidability of the typechecking decision problem.
However, it is a valid trying to find the largest subset of W that is (semi)decidable. Or trying to redefine what it means to be well-typed so that it is (semi)decidable!
One interesting case of a programming language without a semidecidable typechecking problem is Lean. The typechecker they've implemented will both reject or time out on valid programs (so the typechecker is at least a computable function in a sense), but in practice these cases don't really occur.
> We always come to decision. There is no "semi" here.
That's not really how I understand the "semi" in the terminology. For a decidable question, you can recognize when the answer is yes, and you can recognize when the answer is no. For a semidecidable question, you can recognize when the answer is yes.
It doesn't take much of a stretch to describe that as cutting your capabilities in "half".
The way I usually think about this is that with full decidability, you can rule something in or out. With semidecidability, you can rule something in, but you can't rule things out.
That framework extends well to the situation described above, where if the compiler chooses to compile a program, then the typing in that program was valid, and if the compiler chooses to complain about the typing, we can't draw any conclusions. It doesn't match your example; you can't rule anything in or out.
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.
> 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.
Not really, because for undecidable problems semidecidability can only hold one-way. If it held in both ways then the language would be decidable.
Take the Halting program for example: For a program p which halts, you can determine whether it will halt in finite time (because by definition it halts). However, there is no semidecidable algorithm for "this program runs infinitely long".
I don't understand what you're trying to say. What are you contradicting with "Not really"? The claim above you is "by this definition, program incorrectness isn't semidecidable either". You're saying that it is?
> 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).
Rusts type system is turing complete if I recall correctly. Obviously, in practice everything is in a way decidable because we have limitations everywhere.
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.)
There is nothing preventing the Rust language definition to add a constraint to type checking saying "recursion depth <= 128" or something like that (e.g. depth <= N where N is an implementation-defined constant).
In fact, since rustc is "the spec" today, that's kind of how it is ""specified"".
Any implementation that does not conform to that would be... non-conforming... or using your own point-of-view, they would be implementing some programming language, but that language wouldn't be "Rust".
Then the question is not if Rust programs type-check in finite time, but rather, whether they type check in <= N steps. And e.g. the current implementation answers that question very quickly by just trying.
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.
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"].
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.
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.
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.
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).
> [Rust is] not quite undecidable but it is still very much NP-hard.
> Languages like C, C++, or Ada ... make little to no attempt to enforce correctness
Both statements are laughably false, but for different reasons.
Both are based on the Doctrine of Rust Exceptionalism, which requires that Rust is not just a variation on a theme, but fundamentally different from other languages. Like most doctrines, this one is indefensible.
Rust compilation, like C++ and Haskell, is undecideable, not just NP-hard. Non-terminating compilation is artificially curtailed, thus failing to produce an open set of what would have been correct programs.
The Rust compiler performs certain correctness checks that other languages do not. It rejects an infinite set of correct programs that its correctness checks cannot resolve. In this as in all other particulars, Rust is very much on the continuum with other languages. All strongly-typed languages perform a huge variety of correctness checks, some built-in, others programmed, with great success, rejecting the large majority of incorrect programs people write. As a consequence, it is very common for Rust, C++, and Haskell programs to run correctly the first time, once the compiler is satisified.
I don't believe in any of that Rust exceptionalism BS. Rust is just a strongly typed language just like Haskell or any other strongly typed languages. This strong typing (particularly through the borrow checker) gives the Rust compiler the ability to verify properties about the code like any other strongly typed language. The mistake that Rust makes is that they attempt to make the verification a language requirement while nearly every other language either makes it optional or keeps the verification in a library or tool external to the standard.
With Rust though a significant part of the value in things like the borrow checker is that it has the assertion that if you break the rules set out by the "standard", the code doesn't compile. Even Haskell doesn't make the mistake of trying to enforce something like that (instead it's libraries that normally add that verification but those aren't part of the standard).
My point is that Rust has language requirements that force the language compilable by the compilers to never be close to or equally covering the entire language defined by the "standard".
There will be normal (and emphasis on normal) programs that will not be compilable in Rust on certain compilers but will work just fine on others due to the search space on the type solver or the borrow checker blowing up. These issues will also likely pop up in between versions of the same compiler when changes to the internal representation cause certain cases to fall outside the search space.
The only thing the Rust devs can actually do to solve this problem is to add arbitrary restrictions to the language spec based on the limitations of existing compilers.
This issue isn't unique to Rust but basically every other major language has gotten around the problem by not making it a problem in the first place.
---
This comes back to the point in my original comment. Rust the language based on the compiler will likely not be consistent within Rust the language based on the "spec" (whatever it ends up being). There will be normal code that fails to compile due to seemingly arbitrary changes triggering combinatorial explosions.
With C, C++, Haskell, etc this issue can pop up but the features that can invoke this problem are far more rare, are more self contained, and are easier to diagnose (i.e. template explosions which are localised vs the borrow checker which can be very much not localised).
The original comment was very much a critique of Rust and by no means some type of Rust exceptionalism.
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.)
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.
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.
The type system is also Turing-complete, therefore non-terminating. It would be arbitrarily hard to write a spec in a non-Turing-complete language such that all implementations would admit the same set of programs, or even (responsive to the original claim) reliably only a smaller set.
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).