2 ms·

You know I have some Ruby code that could use your skills. I really do wish my Ruby would run as fast as my C and you seem to know the magic to making that happ

You know I have some Ruby code that could use your skills. I really do wish my Ruby would run as fast as my C and you seem to know the magic to making that happen. Can I see some of that code and those papers? I really do want the dynamism of Ruby but combined with the runtime static goodness of C with none of the runtime checking I currently have to deal with. Your confident tone has convinced me those type system folks are a bunch of quacks. The compiler really doesn't need all that information to optimize anything. Seems like all I need to do is bone up on alias analysis, JITing, and inlining and I'm good to go.

DannyBee 10y ago
Okay, i give up. you don't want to actually have a conversation here. In the meantime, i'll just point out, you can have the nicest type system in the world. It still has to translate into concrete aliasing info about pointers that is usable by both high and lower levels, and is queryable in O(1) time, without taking up a ton of space. Otherwise, it's just sitting there making guarantees no one can use. "Seems like all I need to do is bone up on alias analysis, JITing, and inlining and I'm good to go." For most code, yes, actually, that's probably just about right.
- dkarapetyan 10y ago
  We indeed could have had a conversation but you opened right out of the gate with "This is trivially wrong". Instead of assuming good faith and seeing the example for what it was, a stand-in for sufficiently complicated code with sufficiently complicated code paths that a compiler would be unable to sufficiently analyze and be sufficiently clever with unless the programmer gave the compiler more information. Instead you made a bunch of disparaging remarks, trivialized large swaths of CS theory, and failed to see the actual point of my comment in connecting type annotations as mechanically verifiable invariants/assumptions that can be used in optimization pipelines.
  - DannyBee 10y ago
    Throughout this entire thread, your responses to roughly everyone amount to saying that everyone but you is both 1. wrong 2. just not understanding you. When pressed, you change your arguments and become super-snarky. I would re-evaluate the way you are communicating here. IMHO, it is not effective at communicating whatever interesting and useful insights you may have here.
    - dkarapetyan 10y ago
      I didn't have insights. Everything I said is pretty standard fare in optimizing compiler design. You can't turn the optimizer crank without assumptions that the type system lets the programmer express and that the compiler can mechanically verify. Information for optimization passes doesn't come for free and as terminating programs compilers can only fill-in so many holes before the programmer must fill-in the rest or barring that pay a performance penalty which is what happens in dynamic languages even with a JIT.
      - DannyBee 10y ago
        "and as terminating programs compilers" You keep using this phrase, as if the halting problem has any real bearing on what compilers do. Certainly you realize it's solvable for machines with finite bounded memory (IE all real machines. Especially since, for example each intel chipset/processor has finite bounded memory they can even be hooked up to) The problem there is it takes too long. Not that it's impossible.
        dkarapetyan 10y ago
        Let me know when you manage to optimize "if (collatz(n) == 1) { ... }" to just "{ ... }" since you seem to think issues of logic like independence and termination and how all of that is tied into the type system have no bearing on optimization. The fact that you don't know if "collatz(n)" is always 1 or not means you are limited by the compiler's termination limit for inling and simplifying certain expressions. So the fact that the compiler terminates indeed has a lot of bearing on what kinds of optimizations are allowed and derivable in the absence of an expressive enough type system. Some people might object to that example but the fact remains that logic and type systems are intimately tied to program analysis and optimization. In the domain of pointer alias analysis there is something known as separation logic which allows for statically analyzing aliasing relations. Now if this information is encoded as part of the type system then certain mechanical derivations about aliasing become much simpler which leads to more optimization opportunities. Rust's type system I believe is more related to affine logic but similar arguments still apply. You can not express the invariants that can be expressed with Rust's type system in C++. Actually I take that back. You could in theory encode affine or separation logic with the template system and then encode your program using those templates but that's basically the same work as re-implementing Rust in C++. This means Rust's type system allows for program optimizations that would not be possible otherwise. Similar to how knowing "collatz(n)" always being 1 allows you to elide that condition entirely. No amount of inlining and simplifying will allow you to perform that same optimization.

DannyBee 10y ago

Okay, i give up. you don't want to actually have a conversation here. In the meantime, i'll just point out, you can have the nicest type system in the world. It still has to translate into concrete aliasing info about pointers that is usable by both high and lower levels, and is queryable in O(1) time, without taking up a ton of space. Otherwise, it's just sitting there making guarantees no one can use. "Seems like all I need to do is bone up on alias analysis, JITing, and inlining and I'm good to go." For most code, yes, actually, that's probably just about right.

dkarapetyan 10y ago
We indeed could have had a conversation but you opened right out of the gate with "This is trivially wrong". Instead of assuming good faith and seeing the example for what it was, a stand-in for sufficiently complicated code with sufficiently complicated code paths that a compiler would be unable to sufficiently analyze and be sufficiently clever with unless the programmer gave the compiler more information. Instead you made a bunch of disparaging remarks, trivialized large swaths of CS theory, and failed to see the actual point of my comment in connecting type annotations as mechanically verifiable invariants/assumptions that can be used in optimization pipelines.
- DannyBee 10y ago
  Throughout this entire thread, your responses to roughly everyone amount to saying that everyone but you is both 1. wrong 2. just not understanding you. When pressed, you change your arguments and become super-snarky. I would re-evaluate the way you are communicating here. IMHO, it is not effective at communicating whatever interesting and useful insights you may have here.
  - dkarapetyan 10y ago
    I didn't have insights. Everything I said is pretty standard fare in optimizing compiler design. You can't turn the optimizer crank without assumptions that the type system lets the programmer express and that the compiler can mechanically verify. Information for optimization passes doesn't come for free and as terminating programs compilers can only fill-in so many holes before the programmer must fill-in the rest or barring that pay a performance penalty which is what happens in dynamic languages even with a JIT.
    - DannyBee 10y ago
      "and as terminating programs compilers" You keep using this phrase, as if the halting problem has any real bearing on what compilers do. Certainly you realize it's solvable for machines with finite bounded memory (IE all real machines. Especially since, for example each intel chipset/processor has finite bounded memory they can even be hooked up to) The problem there is it takes too long. Not that it's impossible.
      - dkarapetyan 10y ago
        Let me know when you manage to optimize "if (collatz(n) == 1) { ... }" to just "{ ... }" since you seem to think issues of logic like independence and termination and how all of that is tied into the type system have no bearing on optimization. The fact that you don't know if "collatz(n)" is always 1 or not means you are limited by the compiler's termination limit for inling and simplifying certain expressions. So the fact that the compiler terminates indeed has a lot of bearing on what kinds of optimizations are allowed and derivable in the absence of an expressive enough type system. Some people might object to that example but the fact remains that logic and type systems are intimately tied to program analysis and optimization. In the domain of pointer alias analysis there is something known as separation logic which allows for statically analyzing aliasing relations. Now if this information is encoded as part of the type system then certain mechanical derivations about aliasing become much simpler which leads to more optimization opportunities. Rust's type system I believe is more related to affine logic but similar arguments still apply. You can not express the invariants that can be expressed with Rust's type system in C++. Actually I take that back. You could in theory encode affine or separation logic with the template system and then encode your program using those templates but that's basically the same work as re-implementing Rust in C++. This means Rust's type system allows for program optimizations that would not be possible otherwise. Similar to how knowing "collatz(n)" always being 1 allows you to elide that condition entirely. No amount of inlining and simplifying will allow you to perform that same optimization.