Why does Sorbet sometimes need type annotations?
… for methods?
Sorbet never attempts to infer types for methods. This is a key part of what allows Sorbet to type check a codebase quickly. It means that the result of doing inference on one method can never affect the result of doing inference on another method, meaning that all methods can be typechecked entirely in parallel.
In # typed: strict
files, Sorbet requires type annotations for
methods, so that programmers have an explicit reminder that Sorbet does not do
method signature type inference.
… for constants?
Similarly, Sorbet only attempts to do type inference for constants when the type of the constant is knowable without needing to do type inference.
This means that simple constants like X = ""
, Y = 1
, or Z = [1, ""]
do not
need type annotations—Sorbet can syntactically see that the type of these
constants are String
, Integer
, and T::Array[T.any(Integer, String)]
respectively.
However, to know the type of constant assignments like A = MyClass.new
or
B = 1 + 1
, Sorbet needs to know the result type of the new
and +
methods,
respectively. To know a method’s result type, Sorbet has to do type inference,
and Sorbet does not do type inference until all constants have been given type
annotations (which would be a cycle). Keep in mind that Sorbet respects
overloaded and redefined methods, so even simple expressions like these do not
always have well-known result types.
Newer versions of Sorbet will attempt to assume that the type of
A = MyClass.new
is in fact MyClass
, and require an explicit annotation
only when that assumption turns out to be incorrect, for example due to an
override.
Also, for frozen array literals assigned to constants, Sorbet assumes a tuple type instead of an array type, because it knows that the array cannot be re-assigned or mutated.
MutableArray = [1, 2]
T.reveal_type(MutableArray) # => `T::Array[Integer]`
FrozenArray = [1, 2].freeze
T.reveal_type(FrozenArray) # => `[Integer, Integer] (2-tuple)`
… for instance variables?
Sorbet always requires type annotations for instance and class variables, with a similar justification as the previous point for constants.
There is one exception, which is when an instance variable is declared in the
body of an initialize
method by being assigned a variable whose type was
mentioned in the signature for initialize
:
class A
sig {params(x: Integer).void}
def initialize(x)
@x = x
end
end
In cases like these, Sorbet infers that the type of @x
should be Integer
,
without needing an explicit annotation. This means that if @x
should be
allowed to store more types than just Integer
(for example, maybe it should
also be allowed to store nil
), an explicit annotation becomes required.
… for local variables?
Sorbet requires type annotations when widening the type of a variable within a loop. This, again, is for performance. Sorbet’s inference algorithm is very simplistic—it examines each expression in a method body at most once. (Other inference algorithms use separate type constraint generation and type constraint solving passes over a method body to infer types, leading to fewer required type annotations but potentially slower performance.)
Because real-world code has branches and loops, and Sorbet must pick a single order to examine each individual expression in, Sorbet sometimes type checks statements before knowing any updates that might happen to that variable. Concretely:
x = 123
2.times do
x + 1
x = nil
end
By the time Sorbet typechecks the x + 1
line, Sorbet thinks that x
has type
Integer
, and says that expression has no error. Then on the next line, the
type of x
is changed to nil
, which would then introduce a runtime exception
when the x + 1
is encountered on the second iteration of the loop. Since
Sorbet decides whether x + 1
typechecks before looking at the x = nil
assignment, it has to report an error on x = nil
.
true
and false
?
Couldn’t Sorbet at least special case Sorbet’s type inference system is smart enough to track things like this:
sig {params(banking_account: String).returns(T::Boolean)}
def is_risky_merchant(banking_account); ...; end
sig {params(banking_account: T.nilable(String)).void}
def example(banking_account)
should_check_balance = false
if banking_account && is_risky_merchant(banking_account)
should_check_balance = true
end
if should_check_balance
T.reveal_type(banking_account) # error: `String`
end
end
→ View full example on sorbet.run
In this example, Sorbet knows that banking_account
on the indicated line
actually has type String
, not type T.nilable(String)
. It knows this despite
the if
guard checking whether the should_check_balance
variable is true
,
not whether the banking_account
is non-nil
. To achieve this, Sorbet
maintains sophisticated sets of implications saying “if we’re in an environment
where a certain variable is truthy, then another variable must have a certain
type.”
If Sorbet blindly assumed that false
and true
literals had type
T::Boolean
, it would forget in which individual branches the variable had type
TrueClass
or FalseClass
, and be unable to maintain these knowledge sets.
Real-world code depends on patterns like this surprisingly frequently.
We have decided that the error message for changing a variable in a loop or
block is very clear, has an autocorrect, and the resulting T.let
'd code is
very obvious. But if we did it the other way, sometimes requiring people to
explicitly annotate T.let(true, TrueClass)
:
- this pattern would look odd (“of course
true
has typeTrueClass
, isn’t this annotation useless?”), and also - we wouldn’t be able to easily build good error messages to suggest people to
do this in the first place. Instead, the error messages would be reported far
downstream from where the error actually happened, and be reported as
something confusing like “this thing might sometimes be
nil
.”
Type annotations and strictness levels
Sorbet allows the programmer to opt-in to greater levels of static type rigor. At lower strictness levels, Sorbet allows definitions to be implicitly untyped and therefor doesn’t require type annotations.
At the # typed: strict
level, Sorbet starts requiring explicit type
annotations on any definitions where it would have otherwise assumed a type of
T.untyped
. (This is similar to TypeScript’s noImplicitAny
flag, for those
familiar with it.)
Specifically, in a # typed: strict
file it’s an error to omit type annotations
for:
- methods
- instance variables
- class variables
- constants
It may seem counterintuitive that Sorbet does not require type annotations in
a file marked # typed: true
, but this is an intentional part of Sorbet’s
implementation of gradual typing. In the # typed: true
strictness level, unannotated methods, instance variables, and constants are
assumed to be T.untyped
. This allows a programmer to write untyped or
partially-typed definitions while still benefiting from type checking when
static type information is present.