Deep Dive: Does Luau have Type Checking?

No, I think it is very generous to call the current system type checking. This is not necessarily a bad thing, let me explain. We will be getting MASSIVELY unfocused; this one’s for the people who care about how programming languages work. Its necessary complexity to fully understand the why of it.

In the current climate of computer science education, the presence or absence of types in a language, and what form they take, are something of a controversial issue. Languages such as Lua, Python, and Javascript are often promoted as first languages on the basis that they do not have a type system, framing it as an extra complication. This is kind of a poor framing in my opinion. Programming languages must have types, or they would still just be tools for adding subtracting and multiplying whole numbers. The real difference in languages is in how types are handled and to what degree the programmer interracts with them.

Consider the following Lua

a, b = GetMyValues()
local result = a + b

Can you determine the type of result ? You cannot. You need to know the type of a and b in order to make that determination. If they are both numbers, then result will be a number, if one of them is nil, an error will occur. a or b could also be tables with their __add metamethods overloaded to do anything at all.

Despite this, you do not have to specify what the type a or b will be in Lua. The program figures this out exactly as the operation is performed. This system is known as dynamic typing. For our purposes, dynamic means as the code runs. Lua, Python, and JavaScript are dynamically typed languages. The types are there, they do not need to be known in advance, but if they are wrong they will cause an error while the program is running.

Contrast this with static typing. Under a static typing system, the type of all values must be known before that part of the program starts running. (Even is it’s RIGHT before) If you’ve used C, the very first C code you ever saw will have introduced you to this:

int main(int argc, char ** argv)

In C, the programmer specifies what the type of the arguments to the function main will be, and what the return type will be. This is fundamental to a classical compiled, statically typed language. It has to know this because it needs to make room in memory for these values. This is a very limiting situation! But it was a necessary simplification at the time when --and for the purposes which-- C was created. The advantage is that the types can be checked for correctness before the program even runs, this is known as static type checking.

One of the biggest trends in modern languages has been to simplify the process of running them on a wide variety of systems. The original strategy for this was to create compilers, such as C, which could be configured to produce binary code that ran on a variety of targets. After decades of this however, these programs became so complex that adding a new target became very difficult.

To combat this, a new class of languages emerged which ran on arbitrarily made up targets. These virtual machines could be designed however the language designer liked to support all the features they wanted. The only requirement for running these languages on any physical device is that a suitable virtual machine can be run on it. Lua itself runs a custom 32-bit instruction set on a virtual machine written in C. Java runs on the Java Virtual Machine (JVM), which comes in many forms on all sorts of physical devices. These languages have been called interpreted languages, or scripting languages.

The arbitrary design of the virtual machines means that these languages can have many new features that are good for programmer productivity. Lua itself allows multiple return values of arbitrary type, arguments can also have arbitrary types. Functions can be passed around as variables, even created or assigned, while still having access to these features; and functions can make use of values outside their own scope.

The tradeoff for this flexibility is performance. The dynamic type checking process, and the dynamic way in which values are passed to and from functions, takes extra time to perform. In addition to this, there are subtle ways that running an interpreter or virtual machine bypasses some of the optimizations of the underlying compiled language, and even optimizations on the processor itself.

Because of this tradeoff, and because of the increasing use of interpreted languages like Python in high performance tasks like machine learning, there has been a wild goose chase to create a language which combines the advantages of both compiled and interpreted languages. The creator of Lua, Roberto Ierusalimschy, has done a fair amount of work in this field, both for Lua specifically, and for hypothetical other languages.

Lua has thus had a couple cracks at this problem. In the first linked paper, some clever tricks are used to significantly reduce the overhead required by interpretation, while minimally modifying the Lua internals and features. It also compares against LuaJIT, the nuclear option which uses massive complexity to get very impressive performance boosts, and of course C:

There have also been at least two attempts to add static type checking to Lua. No! Not Luau! The self-explanatory Typed Lua, and Pallene:

The gist of this second paper, about Pallene, is that the presence of static types in a language directly facilitates major performance improvements, albeit at the cost of many of Lua’s beloved features. Where it is possible to ensure a value’s type, dynamic type checks can be eliminated. Additionally, it becomes easier to feed the resulting interpretation directly into a C compiler and receive well optimized code out, similar to what LuaAOT would do in the first paper.

Now here’s the clickbait resolution, Roberto calls the system in Pallene gradually typed. Luau also calls their very similar looking system a gradual type system.

So, does Luau provide the benefits of gradual typing? No, and we don’t need a benchmark to discover this, though I did do one just in case. A perfect example of how this should boost performance, and would in Pallene, would be a loop with a high number of repetitions, where removing the dynamic type check would save lots of time.

However, this would mean that type check has to take place before the loop, otherwise the code would not be safe as it would not be checked at all! We know this isn’t happening though, because mismatching the types in Luau does not create an error at the time of the incorrectly typed assignment. Instead it errors exactly how Lua does normally:

image
image

Because of this, I don’t think it’s completely honest to call this gradual typing. Maybe there is or was a long term plan to implement something comparable to Pallene, to extract the actual performance gains. I personally would not be willing to give up my beloved associative arrays, variadic functions, and dynamically-typed returns to have this, though. I will have to downgrade this feature to being called type annotations.

Luau does have a static type checker though, luau-analyze, which appears to be integrated into the Roblox code editor. I would not say its the greatest, it appears to struggle with understanding control flow:

image

Maybe it only irritates me specifically. According to their own docs, Luau should be able to deduce this type as (Vector3 | string). It’s definitely wrong to think it could be both when only one branch of the if statement can be taken.

I consider this to be sort of half-donkey’d. Opinion warning, but the point of static analysis in general, particularly static type checking, should be to prevent malfunctioning code. It should reveal bugs before they happen. Since this analysis only happens while you’re editing, and does not actually stop your code from running, it doesn’t have the chance to catch many of these issues.

If it doesn’t increase performance and doesn’t reliably catch statically detectable bugs, then what is this type system good for? I would argue that despite these deficiencies, this system is still has a few positives, all revolving around clarity. Luau’s type annotations help the code completion system significantly. I also find myself annotating functions arguments and return types, since these are otherwise the least clear on their own. This is partly because I am used to this information always being in the function signature, like it is in C.

If you are very strict about heeding warnings produced by the editor, and I suspect many new programmers are not, then the static type checking is useful. When considering the value of Luau over base Lua overall, we of course have to consider the enormous task of making changes to the Roblox scripting system without breaking existing games. The more heavy hitting possible modifications, such as Pallene and LuaAOT are made impractical by their requirement to then ship a C compiler with Roblox. In this regard, Luau’s type annotations are the safest bet in. They create a superset of Lua where all existing Lua is still valid code, none of Lua’s good features were lost in the process, and keeping up with new Lua features is still relatively easy as a result.

But most importantly of all, +=

18 Likes

I have not read the post yet, but after learning typescript I have found that yes, the Luau type system is not a type system. It basically does the bare minimum.

2 Likes

Exactly.

I wish we had a proper, compiled language, such as C or Rust, but with Roblox’s current model of just ‘click and quickly play on any platform’, it may not be feasible. :frowning:

2 Likes

Much appreciated! From your concise and coherent article, I’m taking a lot.

Seems like a significant portion of devs who do annotate types are half-type-annotators of sorts. I can relate, as stating types helps with clarity and maintainability of the code, especially modules used by others. But type checking of the whole code structure sounds like an overkill requiring more work for no performance gain. So I normally don’t state types for dependency modules.

I’m interested to see if actual performance changes are going to step in in the future, since Roblox has announced possible reading of types by the compiler in the future.

It all just comes down to semantics. I would say Luau has Analysis-Based Type Checking, as opposed to compiled and static based. It is still gradual in a sense, but it doesn’t enforce the same rules as other languages with that description do.


I used to annotate everything— services, modules, instances. I still annotate returning void for functions, but I don’t think it is necessary in strict anymore.

Now I only type for changing globals, function parameters and anything that requires a ‘special’ type, like unions. As long as analysis can determine the type consistently, I’m happy.

1 Like