This is a great question! I've written up an internal blog post at Stripe about this, and now that the beans are spilled I might port it over to my personal blog or the Sorbet blog. The tl;dr:
- The Sorbet types are hints for optimizations in the Compiler. The compiler doesn't blindly trust them, but rather it checks whether they're correct and if so does something faster.
- The Sorbet compiler can frequently check types much faster than the interpreter could because it can look directly at the object representation, rather than having to fall back to calling a full-blown method like .is_a? or .nil?. Many common type checks are a single assembly instruction, so type checks are actually fast most of the time.
- Sorbet is and has always been designed to have runtime type checks.[1] These have been a part of Sorbet since even before we open sourced the typechecker. Every method already does runtime signature checking, when interpreted, and this is no different when compiled.
- The power of LLVM means that a lot of these type tests end up coalescing. For example, if a signature says "this method accepts ints" and then the compiler sees "if this is an int, I can do something faster," that's frequently only one type test, because the power of LLVM magically coalesces the checks.
This is really interesting, thanks. As an academic working on gradual typing and dynamic checks, the sorbet experience is extremely valuable. (I've cited the threshold someone on your team mentioned for when the cost of checks gets too high.) So I'd love to see the blog post.
It sounds like you're taking an approach fairly similar to what Facebook is doing with Hack these days: Dynamic checks implied by types help catch bugs and can be often optimized away, and static types are hints but not trusted, but the type checker means that using the hint is almost always a good idea. Is that accurate?
Yep, that's accurate. If anything, there aren't enough hints in Stripe's codebase, so much so that I'd love people to add more!
When I'm looking at a production performance profile result, trying to figure out why the compiler didn't speed something up, the first thing I do is add or improve types. It has never slowed down the resulting compiled code, and usually speeds it up substantially.
- The Sorbet types are hints for optimizations in the Compiler. The compiler doesn't blindly trust them, but rather it checks whether they're correct and if so does something faster.
- The Sorbet compiler can frequently check types much faster than the interpreter could because it can look directly at the object representation, rather than having to fall back to calling a full-blown method like .is_a? or .nil?. Many common type checks are a single assembly instruction, so type checks are actually fast most of the time.
- Sorbet is and has always been designed to have runtime type checks.[1] These have been a part of Sorbet since even before we open sourced the typechecker. Every method already does runtime signature checking, when interpreted, and this is no different when compiled.
- The power of LLVM means that a lot of these type tests end up coalescing. For example, if a signature says "this method accepts ints" and then the compiler sees "if this is an int, I can do something faster," that's frequently only one type test, because the power of LLVM magically coalesces the checks.
[1] https://sorbet.org/docs/runtime