36 ms·

Compiling Rust is NP-hard

417 points by lovasoa 5y ago

FartyMcFarter 5y ago
> What's the most efficient algorithm you can write to do this? As it turns out, you can't do well in the worst case — and we'll prove this by a reduction from SAT. Correction: you can't do well in the worst case, assuming P ≠ NP (where "well" means "in polynomial runtime").
- gizmo 5y ago
  Pedantic and wrong. Considering there is no known algorithm that can sat solve in P, nobody in the world can do well in the worst case. And if nobody can do it, then you can't do it either, for any you. QED.
  - FartyMcFarter 5y ago
    I'm not a native English speaker, but I thought "you can't do well" is equivalent to "it's impossible to do well", which is how I read the original sentence. As an aside, I find it a bit ironic that you're complaining about pedantry while interpreting the "you" word literally.
    - gizmo 5y ago
      It’s not ironic that my response was pedantic, it was the entire point. When you engage in pedantic nerd sniping you just open yourself up for even more pedantic nerd sniping. “Can’t” can mean impossible, or it can mean nobody can do it. Compare “you can’t go back in time” with “you can’t lift a horse”.
  - gugagore 5y ago
    It's awkward to abbreviate "in polynomial time" as "in P". P is a set of (decision) problems. We don't know that 3-SAT is in P. We don't know that it's not. To say that a solver is not in P is a type error.
  - OgAstorga 5y ago
    Your “proof” it’s more like. No one has ever stepped on Mars. Therefore no one will. Yet another pedantic fallacy.
    - __s 5y ago
      Not that no one will, just that no one can I give you until the end of today to show me someone (anyone!) step on Mars It was just someone being cheeky about someone being cheeky. Now I'm being cheeky about you being cheeky over someone being cheeky about someone being cheeky
sischoel 5y ago
While this is an interesting result, isn't basically every compiler NP-hard, because of register allocation?
- srl 5y ago
  Compilers don't guarantee (or try to find) the absolute optimal allocation, right?
  - WJW 5y ago
    This depends on the compiler of course. Most will not because it is not worth it, but I expect that there is at least one compiler out there with the option to exhaustively search the allocation space for that very last nanosecond of runtime optimization. Probably inside an HFT firm somewhere.
    - astrange 5y ago
      There's some material on this under "superoptimizers", but I think if you want this then you should get an FPGA.
- chrisseaton 5y ago
  No - you can express register allocation as an NP-hard problem if you want to, but you don’t have to and not all compilers do it like that. You don’t need an optimal register allocation - you get into diminishing returns very quickly.
  - sischoel 5y ago
    Yes, I hadn't thought about that before, but of course the difference here is that the Rust compiler cannot just produce a "good enough" result for pattern matching.
    - kadoban 5y ago
      Well, it probably _could_ do "good enough". If a set of matches gets too large/hairy it could just output a "here be dragons" warning and go ahead with compiling it, no? That may not count as a correct Rust compiler though, I'm not 100% sure how that's defined, or if it is.
srl 5y ago
TFA notes that rustc is not a particular _efficient_ SAT solver, taking something like 10^4 times as long as a commonly used algorithm [1] would on a small example. So, I'm curious: what's the _strongest_ case one could make for including a more robust SAT solver as part of the exhaustiveness checking? Is there any reasonable place where this could matter? (Extremely autogenerated code?) [1] https://en.wikipedia.org/wiki/DPLL_algorithm https://en.wikipedia.org/wiki/DPLL_algorithm
- ygra 5y ago
  I was under the impression that cases where it would matter are typically code that wouldn't usually be written. E.g. C# and Java also can solve SAT as part of overload resolution with generic types and it's an interesting peculiarity, but not a pattern that is interesting enough to optimize. Perhaps that's the case here as well. I could also imagine the compiler code being easy to read, understand and modify are often more valuable traits than compilation speed of highly atypical patterns in a language. But that may well depend on how atypical those are.
- trissylegs 5y ago
  Rust's proc-macro system makes it pretty easy to create some hard to compile code. but there's many ways to generate very slow compiling code with proc macros.
- Quekid5 5y ago
  One perhaps-interesting use case might be to use the fastest possible solver in the case of compiling generated/foreign code, so basically code that's expected to always compile (but which still needs to be checked for safety). One could even imagine using it as a first-pass for code and to just fall back to a slower-but-with-better-error-messages type checker if errors are found. (Of course you'd end up with two orthogonal implementations of the type checker, but that might not even be a bad thing since you'd be easily able to check for inconsistencies between them, aka. type checker bugs.)
- gpm 5y ago
  If you were using rustc as some sort of JIT compiler compile times could become extremely important, and error messages less important, at which point things like this might be worth it. If you wanted the SAT solver for some other reason (optimization? proving code correct?) it might make sense to use it for this too.
EdSchouten 5y ago
It's only NP-hard if you want the compiler to give you proper warnings/errors, right? As far as I know, the first matching arm is used. This means that if a compiler doesn't do any analysis on it, but naively generates machine code to compare the value, then there is no complexity at all. (Not saying that that's acceptable...)
- tialaramex 5y ago
  Here's what Rust's compiler actually does today: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/pattern/check_match/index.html https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_bu... Rust lets you say either "There are four specific possible Clowns, and I want everybody to explicitly deal with that" or you can write #[non_exhaustive] to say "There are several Clowns, right now I defined four of them, but maybe I'll add more some day" in which case you are allowed to only write code for those four Clowns, but everybody else is obliged by the compiler to handle the case with more Clowns than that since they can't depend on there only being four, and they have no idea how to name the additional ones that don't yet exist. So, a compiler that just punts is not a correct Rust compiler. It needs to do this analysis or it's compiling a different less useful language. In the real world the (default) exhaustive case is great for types that reflect some truth about the world being modelled, where you really do mean that all the code relying on this enumerated type should refuse to compile and needs re-engineering if your list is subsequently discovered not to really be exhaustive. Teapot not withstanding, there are definitely only five PlatonicSolids, such as Tetrahedron and Cube. The non-exhaustive case is great for types that reflect a truth you know or strongly suspect will change and everybody using your system needs to be prepared for that up front. In 2016 the enumerated list of US FederalHolidays didn't need Juneteenth, but in 2021 it does, we don't want random code to blow up because it had never imagined Congress would make new ones.
  - EdSchouten 5y ago
    Sure. But a naive compiler whose only purpose is to stomp out a poorly optimized executable can safely ignore that annotation, right?
kadoban 5y ago
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.
w-m 5y ago
Presumably there’s another SAT solver in the realm of the Rust tool chain: cargo surely has one for dependency resolution. This is a big time sink in other package managers (looking at you, Anaconda). Does someone have an insight how solving is implemented in Cargo?
- littlestymaar 5y ago
  There is one[1] but Rust allows different major versions of the same package to exist in parallel, so dependency resolution is usually trivial unless someone in the dependency tree explicitly adds an upper limit of the acceptable version [2], which is pretty uncommon (I don't think I've ever met one in practice). [1]: https://github.com/rust-lang/cargo/blob/master/src/cargo/core/resolver/mod.rs https://github.com/rust-lang/cargo/blob/master/src/cargo/cor... [2]: https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#comparison-requirements https://doc.rust-lang.org/cargo/reference/specifying-depende...
rocqua 5y ago
> he standard representation of such a formula is the conjunctive normal form, or simply: AND-of-ORs. Our previous example would look like this when transformed: A and B and (A or B) and (!A or !B) There is another normal form, the disjunctive normal form. This is in the form of An OR of ANDs. Interestingly, every formula can be represented in this form. And SAT is rather easy to determine for this form. The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process.
- maweki 5y ago
  > And SAT is rather easy to determine for this form. Gave me a chuckle, as that's quite an understatement, as the decision procedure is only: is there a single clause and is it just "False"? > The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process. Basically writing out all assignments that make the formula true. Potentially exponentially many, as there are 2^n possible assignments of n variables. So this transformation is basically just solving and writing down all models.
  - mmarx 5y ago
    The conjunctive normal form can be exponentially large in the worst case as well, though, see the footnote in the article. In practice that is not a problem, since it suffices to find a formula in CNF that is satisfiable precisely when the original formula is satisfiable, even though it might not be equivalent.
donatj 5y ago
I had rare occasion to compile a Rust application recently because a prebuilt binary didn’t exist for my platform. It took just over two hours! Coming from primarily Go development recently, I was astonished. How do you get anything done when the cost of testing an idea is several hours?! I’d feel like the sunk cost fallacy would kick in for even the most lackluster of changes just because you took the time to try it.
- swiftcoder 5y ago
  What on earth did you compile? I can't recall ever having compiled a rust project that took more than 10 minutes from scratch. I do have memories of the days when compiling Chromium or AOSP was a 4 hour battle, though :)
  - deleted 5y ago
    [deleted]
  - jynelson 5y ago
    The rust compiler itself can take as long as 2 hours on a modern laptop if you do a full stage 2 build. I don't think that's what the top poster was talking about though, it sounded like they had a rust toolchain already.
    - steveklabnik 5y ago
      (You know this, but for anyone else reading, don't forget that that doing this compiles LLVM, which is in of itself a massive C++ project, as well as compiling the compiler itself multiple times. That's part of why it would be such an outlier.)
      - swiftcoder 5y ago
        Right. Nested C/C++ dependencies are the only case I can think of where drastically-long compile times are common.
lower 5y ago
For languages with Hindley-Milner typing, like SML and OCaml, it has long been known that type-checking is even worse in the worst case (DEXPTIME hard) [1]. But the programs where this matters aren't what one would write by hand, typically. [1] https://dl.acm.org/doi/10.1145/96709.96748 https://dl.acm.org/doi/10.1145/96709.96748
- contravariant 5y ago
  To some extent it wouldn't even be surprising for a sufficiently powerful language to be EXPSPACE. Pretty much anything with sufficiently powerful macros would be EXPSPACE, or worse.
- Ericson2314 5y ago
  Note that is is polynomial with respect to the size of the output. That is to say, pathological expressions don't stay small but induce horrendous searching, but rather merely get a log bigger (and that can cause more trouble for the rest of the program). That means a heuristic to bail out when something grows a lot probably not violate the users intent and get it back into polynomial time.
  - chalst 5y ago
    No, this is the time complexity of type checking before any computation on the terms is performed.
    - Ericson2314 5y ago
      Yes I am saying that while it is exponential with respect to the input, and it is polynomial with respect to the output.
- lower 5y ago
  Maybe it's a good idea to add a concrete example (can't edit the reply anymore): OCaml: let x1 = fun y -> (y, y) in let x2 = fun y -> x1 (x1 y) in let x3 = fun y -> x2 (x2 y) in let x4 = fun y -> x3 (x3 y) in let x5 = fun y -> x4 (x4 y) in let x6 = fun y -> x5 (x5 y) in x6 (fun z -> z) Haskell: test = let x1 = \y -> (y, y) x2 = \y -> x1 (x1 y) x3 = \y -> x2 (x2 y) x4 = \y -> x3 (x3 y) x5 = \y -> x4 (x4 y) x6 = \y -> x5 (x5 y) in x6 (\z -> z) If you can compile these, add x7. The effort increases exponentially as one adds x7, x8 and so on.
cletus 5y ago
Compiling really is the Achilles heel of Rust I feel. This article really talks about the worst case. As others have noted, Haskell and other languages have this property too. Here’s another perspective on practical issues [1] that’s worth reading. Basically, Rust made some understandable but unfortunate design decisions that are hard to walk back or change now. [1]: https://pingcap.com/blog/rust-compilation-model-calamity https://pingcap.com/blog/rust-compilation-model-calamity
shadowgovt 5y ago
The points made by the Endsay here are key, and actually a good example of trade-offs in software engineering. It is definitely okay to incorporate an algorithm that is NP-hard into the core of a performant system as long as you can have some expectation that the input size on the NP-hard part will be small. Sometimes, it even allows you to simplify another piece of the problem via pre-computation that allows you to avoid making the piece of the system that accepts large inputs require a costly solution algorithm.
comonoid 5y ago
"I'm not just hard, I'm NP-hard, baby".
- speed_spread 5y ago
  Wanna solve my constraints?
- dang 5y ago
  Could you please stop posting unsubstantive comments here? https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html
Ericson2314 5y ago
> Does this mean that rustc should integrate an industrial-strength SAT solver? Well, this is actually what https://github.com/rust-lang/rfcs/blob/master/text/1868-portability-lint.md https://github.com/rust-lang/rfcs/blob/master/text/1868-port... would require. There is already chalk, a logic programming language for traits too. I don't balk at these things. A good logical / relational toolbox is very useful for a lot of tasks.
not2b 5y ago
So just use a SAT solver to check for checking whether pattern matching is exhaustive. Any decent one will have much better performance than the current approach in the Rust compiler for complex cases. The interesting thing about SAT is that although the worst case is exponential (as far as we know until someone proves P = NP), even huge real-life problems (from circuits, program analysis etc) tend to have structure that makes them quickly solvable with a SAT solver. And if not, have a time budget and report "too complex to solve" if exceeded.
- thaunatos 5y ago
  It's worth noting that the author of the arcicle doesn't think it's worth integrating a SAT solver: > Does this mean that rustc should integrate an industrial-strength SAT solver? As hilarious as that would be, I'm advocating no such thing. This will only be a performance issue on pathological examples crafted by bored nerds, and I don't think precious engineering time should be spent on that. Besides, generalizing a SAT algorithm to handle the full expressive power of Rust's patterns might be, to borrow some language from mathematicians, non-trivial.
multifasciatus 5y ago
> Obviously, every formula can be transformed into this form, by applying the rules of Boolean algebra. Is it so obvious? Why do so many engineers write with these sort of modifiers (obviously, just, of course, etc.)? Edit: I am assuming no ill intent from the author. I also use these sorts of modifiers without thinking about them much when writing. I am just curious as to why we as engineers call deeply technical things obvious when they are not.
- bombela 5y ago
  I don't think it's any malice. Just a way to bring up the idea of a sudden realization. Obviously, I could be wrong.
- NieDzejkob 5y ago
  That sounds like something that could be solved with a linter for prose. Though, I can't think of the search terms that would let me find such a solution, if it exists.
- guga42k 5y ago
  Usually this is a polite way to say that proof/derivation is too long to fit on this page, please look somewhere else if you are interested. Notable example would be Lev Landau's Theoretical Physics. If you see "obviously" there it is probably not obvious at all and can take good few hours to derive the formula.
- joshribakoff 5y ago
  The good faith interpretation is that the author means in the sense of “it follows then that” as opposed to “if you didn’t realize this upon reading the previous section then something is wrong”
- rgoulter 5y ago
  I liked the model in blogpost: https://status451.com/2016/01/06/splain-it-to-me/ https://status451.com/2016/01/06/splain-it-to-me/ It discusses that there can be different ways sharing information comes across. For some people, sharing information demonstration that you're smart enough to know the thing. For others, sharing information is for others' benefit. I wouldn't prefer to interpret "obviously" as "you're not as smart/cool as me if you don't know this", but I can see why there are examples that could come across like that. (I'd sooner interpret it as "I'm not claiming to be smart by saying this").
estebank 5y ago
The actual code that handles exhaustiveness checks has extensive explanations on how it works and what it was inspired by. https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs https://github.com/rust-lang/rust/blob/master/compiler/rustc...
axilmar 5y ago
Regarding Rust's compilation slowness, wouldn't a Rust interpreter be a good solution for developing code? A Rust interpreter would drastically cut down slow compilation times, and then when the final product is needed, the Rust compiler would kick in.
- steveklabnik 5y ago
  It's not clear that it would, or that the execution time of said interpreter would be fast enough to make it work. Miri interprets Rust code and it is, from what I hear, orders of magnitude slower. And for some applications, even debug builds of Rust are too slow. So it really just depends. (It is also going to be slower than an interpreter focused on runtime speed would be, the point is more that interpreters aren't magic.)

417 points by lovasoa 5y ago

> What's the most efficient algorithm you can write to do this? As it turns out, you can't do well in the worst case — and we'll prove this by a reduction from SAT. Correction: you can't do well in the worst case, assuming P ≠ NP (where "well" means "in polynomial runtime").

gizmo 5y ago
Pedantic and wrong. Considering there is no known algorithm that can sat solve in P, nobody in the world can do well in the worst case. And if nobody can do it, then you can't do it either, for any you. QED.
- FartyMcFarter 5y ago
  I'm not a native English speaker, but I thought "you can't do well" is equivalent to "it's impossible to do well", which is how I read the original sentence. As an aside, I find it a bit ironic that you're complaining about pedantry while interpreting the "you" word literally.
  - gizmo 5y ago
    It’s not ironic that my response was pedantic, it was the entire point. When you engage in pedantic nerd sniping you just open yourself up for even more pedantic nerd sniping. “Can’t” can mean impossible, or it can mean nobody can do it. Compare “you can’t go back in time” with “you can’t lift a horse”.
- gugagore 5y ago
  It's awkward to abbreviate "in polynomial time" as "in P". P is a set of (decision) problems. We don't know that 3-SAT is in P. We don't know that it's not. To say that a solver is not in P is a type error.
- OgAstorga 5y ago
  Your “proof” it’s more like. No one has ever stepped on Mars. Therefore no one will. Yet another pedantic fallacy.
  - __s 5y ago
    Not that no one will, just that no one can I give you until the end of today to show me someone (anyone!) step on Mars It was just someone being cheeky about someone being cheeky. Now I'm being cheeky about you being cheeky over someone being cheeky about someone being cheeky

sischoel 5y ago

While this is an interesting result, isn't basically every compiler NP-hard, because of register allocation?

srl 5y ago
Compilers don't guarantee (or try to find) the absolute optimal allocation, right?
- WJW 5y ago
  This depends on the compiler of course. Most will not because it is not worth it, but I expect that there is at least one compiler out there with the option to exhaustively search the allocation space for that very last nanosecond of runtime optimization. Probably inside an HFT firm somewhere.
  - astrange 5y ago
    There's some material on this under "superoptimizers", but I think if you want this then you should get an FPGA.
chrisseaton 5y ago
No - you can express register allocation as an NP-hard problem if you want to, but you don’t have to and not all compilers do it like that. You don’t need an optimal register allocation - you get into diminishing returns very quickly.
- sischoel 5y ago
  Yes, I hadn't thought about that before, but of course the difference here is that the Rust compiler cannot just produce a "good enough" result for pattern matching.
  - kadoban 5y ago
    Well, it probably _could_ do "good enough". If a set of matches gets too large/hairy it could just output a "here be dragons" warning and go ahead with compiling it, no? That may not count as a correct Rust compiler though, I'm not 100% sure how that's defined, or if it is.

srl 5y ago

TFA notes that rustc is not a particular _efficient_ SAT solver, taking something like 10^4 times as long as a commonly used algorithm [1] would on a small example. So, I'm curious: what's the _strongest_ case one could make for including a more robust SAT solver as part of the exhaustiveness checking? Is there any reasonable place where this could matter? (Extremely autogenerated code?) [1] https://en.wikipedia.org/wiki/DPLL_algorithm https://en.wikipedia.org/wiki/DPLL_algorithm

ygra 5y ago
I was under the impression that cases where it would matter are typically code that wouldn't usually be written. E.g. C# and Java also can solve SAT as part of overload resolution with generic types and it's an interesting peculiarity, but not a pattern that is interesting enough to optimize. Perhaps that's the case here as well. I could also imagine the compiler code being easy to read, understand and modify are often more valuable traits than compilation speed of highly atypical patterns in a language. But that may well depend on how atypical those are.
trissylegs 5y ago
Rust's proc-macro system makes it pretty easy to create some hard to compile code. but there's many ways to generate very slow compiling code with proc macros.
Quekid5 5y ago
One perhaps-interesting use case might be to use the fastest possible solver in the case of compiling generated/foreign code, so basically code that's expected to always compile (but which still needs to be checked for safety). One could even imagine using it as a first-pass for code and to just fall back to a slower-but-with-better-error-messages type checker if errors are found. (Of course you'd end up with two orthogonal implementations of the type checker, but that might not even be a bad thing since you'd be easily able to check for inconsistencies between them, aka. type checker bugs.)
gpm 5y ago
If you were using rustc as some sort of JIT compiler compile times could become extremely important, and error messages less important, at which point things like this might be worth it. If you wanted the SAT solver for some other reason (optimization? proving code correct?) it might make sense to use it for this too.

EdSchouten 5y ago

It's only NP-hard if you want the compiler to give you proper warnings/errors, right? As far as I know, the first matching arm is used. This means that if a compiler doesn't do any analysis on it, but naively generates machine code to compare the value, then there is no complexity at all. (Not saying that that's acceptable...)

tialaramex 5y ago
Here's what Rust's compiler actually does today: https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_build/thir/pattern/check_match/index.html https://doc.rust-lang.org/nightly/nightly-rustc/rustc_mir_bu... Rust lets you say either "There are four specific possible Clowns, and I want everybody to explicitly deal with that" or you can write #[non_exhaustive] to say "There are several Clowns, right now I defined four of them, but maybe I'll add more some day" in which case you are allowed to only write code for those four Clowns, but everybody else is obliged by the compiler to handle the case with more Clowns than that since they can't depend on there only being four, and they have no idea how to name the additional ones that don't yet exist. So, a compiler that just punts is not a correct Rust compiler. It needs to do this analysis or it's compiling a different less useful language. In the real world the (default) exhaustive case is great for types that reflect some truth about the world being modelled, where you really do mean that all the code relying on this enumerated type should refuse to compile and needs re-engineering if your list is subsequently discovered not to really be exhaustive. Teapot not withstanding, there are definitely only five PlatonicSolids, such as Tetrahedron and Cube. The non-exhaustive case is great for types that reflect a truth you know or strongly suspect will change and everybody using your system needs to be prepared for that up front. In 2016 the enumerated list of US FederalHolidays didn't need Juneteenth, but in 2021 it does, we don't want random code to blow up because it had never imagined Congress would make new ones.
- EdSchouten 5y ago
  Sure. But a naive compiler whose only purpose is to stomp out a poorly optimized executable can safely ignore that annotation, right?

kadoban 5y ago

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.

w-m 5y ago

Presumably there’s another SAT solver in the realm of the Rust tool chain: cargo surely has one for dependency resolution. This is a big time sink in other package managers (looking at you, Anaconda). Does someone have an insight how solving is implemented in Cargo?

littlestymaar 5y ago
There is one[1] but Rust allows different major versions of the same package to exist in parallel, so dependency resolution is usually trivial unless someone in the dependency tree explicitly adds an upper limit of the acceptable version [2], which is pretty uncommon (I don't think I've ever met one in practice). [1]: https://github.com/rust-lang/cargo/blob/master/src/cargo/core/resolver/mod.rs https://github.com/rust-lang/cargo/blob/master/src/cargo/cor... [2]: https://doc.rust-lang.org/cargo/reference/specifying-dependencies.html#comparison-requirements https://doc.rust-lang.org/cargo/reference/specifying-depende...

rocqua 5y ago

> he standard representation of such a formula is the conjunctive normal form, or simply: AND-of-ORs. Our previous example would look like this when transformed: A and B and (A or B) and (!A or !B) There is another normal form, the disjunctive normal form. This is in the form of An OR of ANDs. Interestingly, every formula can be represented in this form. And SAT is rather easy to determine for this form. The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process.

maweki 5y ago
> And SAT is rather easy to determine for this form. Gave me a chuckle, as that's quite an understatement, as the decision procedure is only: is there a single clause and is it just "False"? > The catch is that taking a logical formula, and placing it in Disjunctive normal form is actually a rather arduous, non polynomial process. Basically writing out all assignments that make the formula true. Potentially exponentially many, as there are 2^n possible assignments of n variables. So this transformation is basically just solving and writing down all models.
- mmarx 5y ago
  The conjunctive normal form can be exponentially large in the worst case as well, though, see the footnote in the article. In practice that is not a problem, since it suffices to find a formula in CNF that is satisfiable precisely when the original formula is satisfiable, even though it might not be equivalent.

donatj 5y ago

I had rare occasion to compile a Rust application recently because a prebuilt binary didn’t exist for my platform. It took just over two hours! Coming from primarily Go development recently, I was astonished. How do you get anything done when the cost of testing an idea is several hours?! I’d feel like the sunk cost fallacy would kick in for even the most lackluster of changes just because you took the time to try it.

swiftcoder 5y ago
What on earth did you compile? I can't recall ever having compiled a rust project that took more than 10 minutes from scratch. I do have memories of the days when compiling Chromium or AOSP was a 4 hour battle, though :)
- deleted 5y ago
  [deleted]
- jynelson 5y ago
  The rust compiler itself can take as long as 2 hours on a modern laptop if you do a full stage 2 build. I don't think that's what the top poster was talking about though, it sounded like they had a rust toolchain already.
  - steveklabnik 5y ago
    (You know this, but for anyone else reading, don't forget that that doing this compiles LLVM, which is in of itself a massive C++ project, as well as compiling the compiler itself multiple times. That's part of why it would be such an outlier.)
    - swiftcoder 5y ago
      Right. Nested C/C++ dependencies are the only case I can think of where drastically-long compile times are common.

lower 5y ago

For languages with Hindley-Milner typing, like SML and OCaml, it has long been known that type-checking is even worse in the worst case (DEXPTIME hard) [1]. But the programs where this matters aren't what one would write by hand, typically. [1] https://dl.acm.org/doi/10.1145/96709.96748 https://dl.acm.org/doi/10.1145/96709.96748

contravariant 5y ago
To some extent it wouldn't even be surprising for a sufficiently powerful language to be EXPSPACE. Pretty much anything with sufficiently powerful macros would be EXPSPACE, or worse.
Ericson2314 5y ago
Note that is is polynomial with respect to the size of the output. That is to say, pathological expressions don't stay small but induce horrendous searching, but rather merely get a log bigger (and that can cause more trouble for the rest of the program). That means a heuristic to bail out when something grows a lot probably not violate the users intent and get it back into polynomial time.
- chalst 5y ago
  No, this is the time complexity of type checking before any computation on the terms is performed.
  - Ericson2314 5y ago
    Yes I am saying that while it is exponential with respect to the input, and it is polynomial with respect to the output.
lower 5y ago
Maybe it's a good idea to add a concrete example (can't edit the reply anymore): OCaml: let x1 = fun y -> (y, y) in let x2 = fun y -> x1 (x1 y) in let x3 = fun y -> x2 (x2 y) in let x4 = fun y -> x3 (x3 y) in let x5 = fun y -> x4 (x4 y) in let x6 = fun y -> x5 (x5 y) in x6 (fun z -> z) Haskell: test = let x1 = \y -> (y, y) x2 = \y -> x1 (x1 y) x3 = \y -> x2 (x2 y) x4 = \y -> x3 (x3 y) x5 = \y -> x4 (x4 y) x6 = \y -> x5 (x5 y) in x6 (\z -> z) If you can compile these, add x7. The effort increases exponentially as one adds x7, x8 and so on.

cletus 5y ago

Compiling really is the Achilles heel of Rust I feel. This article really talks about the worst case. As others have noted, Haskell and other languages have this property too. Here’s another perspective on practical issues [1] that’s worth reading. Basically, Rust made some understandable but unfortunate design decisions that are hard to walk back or change now. [1]: https://pingcap.com/blog/rust-compilation-model-calamity https://pingcap.com/blog/rust-compilation-model-calamity

shadowgovt 5y ago

The points made by the Endsay here are key, and actually a good example of trade-offs in software engineering. It is definitely okay to incorporate an algorithm that is NP-hard into the core of a performant system as long as you can have some expectation that the input size on the NP-hard part will be small. Sometimes, it even allows you to simplify another piece of the problem via pre-computation that allows you to avoid making the piece of the system that accepts large inputs require a costly solution algorithm.

comonoid 5y ago

"I'm not just hard, I'm NP-hard, baby".

speed_spread 5y ago
Wanna solve my constraints?
dang 5y ago
Could you please stop posting unsubstantive comments here? https://news.ycombinator.com/newsguidelines.html https://news.ycombinator.com/newsguidelines.html

Ericson2314 5y ago

> Does this mean that rustc should integrate an industrial-strength SAT solver? Well, this is actually what https://github.com/rust-lang/rfcs/blob/master/text/1868-portability-lint.md https://github.com/rust-lang/rfcs/blob/master/text/1868-port... would require. There is already chalk, a logic programming language for traits too. I don't balk at these things. A good logical / relational toolbox is very useful for a lot of tasks.

not2b 5y ago

So just use a SAT solver to check for checking whether pattern matching is exhaustive. Any decent one will have much better performance than the current approach in the Rust compiler for complex cases. The interesting thing about SAT is that although the worst case is exponential (as far as we know until someone proves P = NP), even huge real-life problems (from circuits, program analysis etc) tend to have structure that makes them quickly solvable with a SAT solver. And if not, have a time budget and report "too complex to solve" if exceeded.

thaunatos 5y ago
It's worth noting that the author of the arcicle doesn't think it's worth integrating a SAT solver: > Does this mean that rustc should integrate an industrial-strength SAT solver? As hilarious as that would be, I'm advocating no such thing. This will only be a performance issue on pathological examples crafted by bored nerds, and I don't think precious engineering time should be spent on that. Besides, generalizing a SAT algorithm to handle the full expressive power of Rust's patterns might be, to borrow some language from mathematicians, non-trivial.

multifasciatus 5y ago

> Obviously, every formula can be transformed into this form, by applying the rules of Boolean algebra. Is it so obvious? Why do so many engineers write with these sort of modifiers (obviously, just, of course, etc.)? Edit: I am assuming no ill intent from the author. I also use these sorts of modifiers without thinking about them much when writing. I am just curious as to why we as engineers call deeply technical things obvious when they are not.

bombela 5y ago
I don't think it's any malice. Just a way to bring up the idea of a sudden realization. Obviously, I could be wrong.
NieDzejkob 5y ago
That sounds like something that could be solved with a linter for prose. Though, I can't think of the search terms that would let me find such a solution, if it exists.
guga42k 5y ago
Usually this is a polite way to say that proof/derivation is too long to fit on this page, please look somewhere else if you are interested. Notable example would be Lev Landau's Theoretical Physics. If you see "obviously" there it is probably not obvious at all and can take good few hours to derive the formula.
joshribakoff 5y ago
The good faith interpretation is that the author means in the sense of “it follows then that” as opposed to “if you didn’t realize this upon reading the previous section then something is wrong”
rgoulter 5y ago
I liked the model in blogpost: https://status451.com/2016/01/06/splain-it-to-me/ https://status451.com/2016/01/06/splain-it-to-me/ It discusses that there can be different ways sharing information comes across. For some people, sharing information demonstration that you're smart enough to know the thing. For others, sharing information is for others' benefit. I wouldn't prefer to interpret "obviously" as "you're not as smart/cool as me if you don't know this", but I can see why there are examples that could come across like that. (I'd sooner interpret it as "I'm not claiming to be smart by saying this").

estebank 5y ago

The actual code that handles exhaustiveness checks has extensive explanations on how it works and what it was inspired by. https://github.com/rust-lang/rust/blob/master/compiler/rustc_mir_build/src/thir/pattern/usefulness.rs https://github.com/rust-lang/rust/blob/master/compiler/rustc...

axilmar 5y ago

Regarding Rust's compilation slowness, wouldn't a Rust interpreter be a good solution for developing code? A Rust interpreter would drastically cut down slow compilation times, and then when the final product is needed, the Rust compiler would kick in.

steveklabnik 5y ago
It's not clear that it would, or that the execution time of said interpreter would be fast enough to make it work. Miri interprets Rust code and it is, from what I hear, orders of magnitude slower. And for some applications, even debug builds of Rust are too slow. So it really just depends. (It is also going to be slower than an interpreter focused on runtime speed would be, the point is more that interpreters aren't magic.)