Stamping Out Overflow Checks in Ruby
chrisseaton.com
chrisseaton.com
Another detail I think is important is that injecting the stamp is not the same as writing a proof and informing the compiler that some property is true. You're doing what other languages would call an unsafe operation and asserting that something is true. Providing a proof would be interesting and some languages do have the ability to express such proofs (a static type system is one way, among others).
That said, it's still interesting to see details about how to get a dynamic language like Ruby to extract some static properties from the source code. I did some work on this at Microsoft when they were working on IronPython, it's definitely challenging stuff. At the time the consensus was that the pay-off wasn't worth it, it ends up being a lot of work to extract very small guarantees and that one is almost certainly better off off-loading performance related code to C# (or C in the case of CPython). But that was 15 years ago, it's nice to see progress being made.
> Didn’t we say that jo didn’t add much of an impact? Well that’s what I was always taught - maybe I should reconsider that and measure it a bit more.
I was also expecting to be writing about how removing overflow checks enables multiple arithmetic operations to be selected into single LEA instructions using addressing modes, as that’s the other common wisdom, but I couldn’t get the instruction selector to do that. Don’t know why yet either.
And the injection isn’t the proof - the mask was the proof. The injection is to see if we can do it without the actual mask instruction if we cared about that. You’re right it’s unsafe - I have an example of the failure mode of abusing it in the article. Turns out we didn’t need it in this case anyway as it’s the same performance.
It states that as the conventional wisdom, very explicitely, and before going any further already states that it will hinder further optimisations (because the arithmetics operations can’t be merged / fused).
Paired with my current reading of Crafting Interpreters, these posts make me really excited for all the cool things you can do when implementing a language.
...so, they're just types - they define sets of values. Not quite sure why one would have to call it "a kind of micro-types". Especially when it's not even clear what a "micro-type" should be.
And while you're correct that the stamps appear to be an alternative type system, for most people these types will be "unlike types you’ve usually worked with", because most people aren't heavily into Haskell or ML or other languages where it's natural to construct complex type systems like this.
That ultimately causes more confusion though. These really are nothing more or less than types and you can do this kind of thing in a plain old type system and it's actually a lot easier and more effective. Maybe if enough people hear about types we can eventually drag programming culture kicking and screaming into the 1980s.
It would be really cool to work with a language that allows the user such fine-grained types, which is one reason I keep eyeing Idris.
Yeah, that's a normal type. For example in Common Lisp, it's the type defined by the type specifier (INTEGER 0 255).
For example a type could be `0 | 1 | 2 | 3 | 4 | 5`, though there's no way right now to specify that as `0..5`
(I’m not a type theorist though.)
By this argument I might as well call everything a 'thing' since everything is still just a thing.
Different names for subclasses of things that already have names is useful.
I get this discussion with people who don't like the word 'transpiler' because they reason it's just another compiler. Yeah nobody's denying that - it's a subclass of compiler with a specific name.
Great article though, really interesting look into how the sausage gets made that most of us don't get to see very often