luau/rfcs/type-states.md

Type states

Summary

Track the most precise types from the assignments to any lvalues.

Motivation

Today, when we check this trivial program, we report a false positive Value of type '{| x: number |}?' could be nil.

local t: {x: number}? = {x = 5}
print(t.x) -- right here

But the program is clearly well formed. The lvalue t is initialized with a table. Alas, Luau doesn't know this because there's nothing indicating the current state of t. As a result whenever we refer to t in Scope::bindings, we have no choice but to look at the type of t which functionally acts like a subtype constraint.

There are some fallout from not doing this. For example

1. many false positive type errors, negatively impacting the UX and value of each type errors
2. in some no errors are reported when there ought to be one, negatively impacting the value of type errors

The solution is blatant: we need to start tracking the types assigned to each lvalues.

Design

A good chunk of the groundwork is already in place for this, RefinementMap. All we'd need to do is build on top of that existing system. It's going to be renamed into TypeState, and it will instead keep a record of every assignments and refinements, order and method preserving.

That is, local t: {x: number}? = {x = 5} should add the lvalue t with {x: number} as the current state. And that's it, it's enough to know that print(t.x) is well formed because t.x is not going to crash the program. Because t was annotated with {x: number}?, it's ok to write t = nil afterwards, all we'll do is update the record saying t is now nil. So the above program will now type check with no type errors.

Let's start by covering some of the basic cases:

local x: string | number | nil = nil

if math.random() > 0.5 then
    x = "hello"
else
    x = 5
end

local y: string | number = x

Here's another one:

local x: string | number = "hi"

local a: string = x

x = 5

local b: number = x

And another:

local x, y = "hi", 5

x, y = y, x

local a: number, b: string = x, y

Not too interesting. Let's kick things up a notch.

Type states does not care about type errors.

Even if type errors occurs, type states is going to just accept it as factual about the code regardless. This is actually an improvement over also reporting an error on the second line.

local x: number = "hello %s" -- type error, number and string mismatches
local y = x:format("world") -- no type errors, `x` is actually a string!

Local initialization with explicit nil are no longer make-pretend.

local x = nil
local y: string = x -- now a type error!

Similarly, type states can now properly track implicit nil.

local function f() return "hi" end

local x, y = f(), 5
x, y = f() -- type error, f() returns 1 value but we expect 2 values.

local z: string = y -- type error, y is nil

Combination of upper and lower bound inference.

Something that we can do with type states is to also infer singleton types without them getting in the way, even though x was not explicitly ascribed a singleton type.

local x = "hello!"
local y: "hello!" = x -- no type errors!

The reason why this can work is because at the expression "hello!" we know the incoming type does not contain a singleton type, so we return the type string. However, we can also return "hello!" as the lower bound of the expression which is stored as a state.

Locals with explicit type annotations

There's one edge case with all this: what to do about locals with explicit type annotations and no initialization?

local x: string

The harsh fact of it is that x's current state will be nil. Reading x will not directly cause an error.

local y: string? = x -- no error because nil <: string?
local z: string  = x -- type error because nil </: string

How about with some initialization?

local function f() return "hi" end

local x: string, y: number = f()

In this case, we'll keep the behavior the same as today, where we will be as strict as we can be. Since f() returns one single value, we report a type error indicating that the values count mismatches. Only difference is, we now know y's current state is nil.

Drawbacks

Something something it's not a perfect solution, something something alias analysis.

This isn't a be all end all solution. There are cases where we may end up introducing unsoundness. Here's a trivial example:

local t: {x: number | string} = {x = 5}
local u = t

t.x = "hi"

local a: string = t.x
local b: string = u.x

And the reason for that is because we only track the state by the syntactic structure of the lvalues themselves. This is a drawback that existed anyway with refinements, so no difference other than increasing the surface area of this particular limitation.

Also, because we are not implementing control flow analysis yet, there will be a subset of type errors which are false positives. Generally as a direct result of loopy constructs or some change in control flow that we aren't tracking.

For example, in the body after the if, we have no choice but to deduce the type number | string because we do not know that the block of the assignment x = "hi" just terminates the function, rendering the assignment useless and irrelevant.

local function f(x: number | string)
    if type(x) == "string" then
        x = "hi"
        return
    else
        x = 5
    end

    -- `x` should be of type `number`, but without control flow analysis, it will be of type `number | string`
end

Alternatives

Do nothing and accept the false positives. This is obviously a non-starter.