Typed lua binds the type self the closed table type

run-time performance [AFT13]. We believe that a careful evaluation of run-time checks should be done before inserting them in the type system. However, this evaluation is out of scope of this work.

Lua values can have one of eight tags: nil, boolean, number, string, function, table, userdata, and thread. Typed Lua includes types for the first six. Typed Lua also includes a syntactical extension that programmers can use to define the types of userdata. We use this syntactical extension to define the type thread. In this section we present the Typed Lua types that may appear on annotations. We explain all Typed Lua types and syntactical extensions in this chapter.

Types

Typed Lua uses consistent-subtyping to check the interaction among the dynamic type any and other types. The dynamic type any is a subtype of value, but it is neither a supertype nor a subtype of any other type. Our consistent-subtyping relationship follows the standards defined by the gradual typing of objects [ST07, SVB13]. In practice, we can pass a value of the dynamic type anytime we want a value of some other type, and we can pass any value where a value of the dynamic type is expected, but the compiler tracks these operations, and the programmer can choose to be warned about

local function succ (n:integer):integer
return n + 1
end
local x:integer = 7
x = succ(x)
print(x) --> 8

Chapter 3. Typed Lua 32

This example compiles without any warnings because we annotated the return type of factorial. Local type inference cannot use the type of the returned expression when it includes a function call to the function that is being type checked, as its return type is still unknown to the type checker. For this reason, we need to annotate the return type of recursive local functions to inform the type checker what type it should use while type checking their body.

We use the following example to illustrate the omission of type annota-

The function distance receives two parameters of type any and returns a value of type integer. The compiler assigns the dynamic type any to the input parameters of distance because they do not have type annotations and the compiler does not use global type inference, as we mentioned previously. Even though we did not annotate the return type of distance, the compiler is able to infer its return type because it is local and not recursive.

In this example, Typed Lua cannot guarantee that distance is never going to call absolute with a parameter that is not an integer, because in the semantics of Lua the minus operator can result in a value that is not an integer

function even (n:integer):boolean

One way to overcome these warnings is to predeclare these functions with an empty body before the actual declaration. Even though this is a

Chapter 3. Typed Lua 35

Function types

functiontype ::= tupletype ‘->’ rettype
tupletype ::= ‘(’ [typelist] ‘)’
typelist ::= type {‘,’ type} [‘*’]
rettype ::= type | uniontuple [‘?’]
uniontuple ::= tupletype | uniontuple ‘|’ uniontuple

to both parts of the function type. Even though it still uses nil* to replace missing values, it also uses nil* instead of value* to catch arity mismatch.

In the strict mode, sum has type (integer, integer, nil*) -> (integer, nil*). The compiler adds nil* to the type of the parameter list to catch arity mismatch. For instance, the call sum(1, 2, 3) compiles with a warning because we are passing an extra argument 3 to sum.

Even though these modes of operation affect function calls, they do not affect other multiple assignments. This means that both modes discard extra arguments in multiple assignments and they also use nil to replace missing arguments in multiple assignments. We made this design decision to avoid being too restrictive, that is, we did not want to give unnecessary warnings to programmers, as discarded values do not have any implications during run-time.

local function m ():(integer, string)
return 2, "foo"
end

As an example,

We can also type variadic functions. For instance,

local function v (...:string):(string*)
return ...

use of optional values, the overloading based on the tags of input parameters, and the overloading on the return type of functions.

In fact, we do not need to declare a new variable greeting that shadows the optional parameter:

local function message (name:string, greeting:string?) greeting = greeting or "Hello "
return greeting .. name
end

different actions depending on what those tags are. The simplest case overloads on just a single parameter:

local function overload (s1:string, s2:string|integer) if type(s2) == "string" then
return s1 .. s2
else
-- string.rep : (string, integer, string?) -> (string) return string.rep(s1, s2)
end
end

something failed during its execution. Next, we show an example:

local q, r = idiv(a, b)
if q then
print(a == b * q + r)
else
print("ERROR: " .. r)
end

When Typed Lua finds a union of tuples in the right-hand side of a de-claration, it assigns projection types to the variables that appear unannotated in the left-hand side of the declaration. Projection types do not appear in type annotations, but Typed Lua uses them to project unions of tuple types into

of the if statement, but (integer, integer, nil*) inside the then block, and (nil, string, nil*) inside the else block. Thus, variable q has type integer|nil and variable r has type integer|string outside of the if statement; but variable q has type integer and variable r also has type integer inside the then block; and variable q has type nil while variable r has type string inside the else block.

We could have used math.type(q) == "integer" or even math.type(r) == "integer" as the predicate of our example, as both predicates would produce the same result. However, the form that appears in our example is much more succinct and idiomatic. Note that the type integer is restricted to Lua 5.3, as we use the function math.type to decide whether a number is integer.

This example means that we cannot write a function that is guaranteed to return a number when we pass a number and guaranteed to return a string

Chapter 3. Typed Lua 43

Table types

type nil, because Lua returns nil when we use a non-existing key to index

a table. The types of the keys are restricted to either base types or the type

--> y gets nil
--> z gets 0

The second line of this example raises a warning, because we are attempt-ing to assign a value of type integer|nil to a variable that accepts only values of type integer. Although the field bar does not exist in t, the third line of this example does not raise a warning, because the annotated type matches the type of the values that can be stored in t. The last line shows that the or idiom is also useful to give a default value to a missing table field.

--> x gets "Sunday"--> y gets nil
--> z gets "Thursday"

In this example, the type of i is integer, while the type of x, y, and z is string|nil. An inconvenient aspect of making the types of maps and arrays always include the type nil is to overload the programmers, as they need to use the logical or operator or the if statement to narrow the type of the elements they are accessing.

When we use the syntax of records to type an array, the compiler raises a warning when we try to access an index that is out of bounds. In the previous example, the expressions days[8] and days[i] would raise warnings if we had used the records syntax, as both the literal type 8 and the base type integer would not map to any value.

We can also use the syntax of records to type heterogeneous tuples:

In these two previous examples, local type inference would infer the very same table types that we used to annotate the variables album and person.

Lua programmers often build records incrementally, that is, they usually declare a local variable with an empty table, and then use assignment to add fields to this table:

particular, this is the case of table constructors, so they always have unique table types. In the previous example, person has an unique type because it has no alias. Any alias to unique tables makes them open, as we use this tag to keep track of unique aliasing. This means that open table types can only have closed aliases, and it is guaranteed that only one reference remains open. Finally, fixed table types can have any number of closed and fixed aliases, so its type cannot change. In Section 3.7 we will show that we use fixed table types to describe the type of classes. Typed Lua also has different subtyping rules that handle these different tags, which we explain in Section 4.2.

Typed Lua type checks this example because the table constructor has an unique table type {"x":1, "y":2} that is consistent with the type in the annotation. However, if the table constructor had an open table type, it would not type check because it does not allow us to convert a table field from integer to integer?. We need this kind of behavior to avoid unsafe constructions while aliasing unique table types, like in the following example:

local t1 = { x = 1 }
local t2:{"x":integer} = t1

types, the following example shows that it is forbidden to change the type of existing fields:

In this example, both third and fourth lines are not valid because they are trying to change the type of fields that already exist. Even though it would be sound to allow changing the type of fields in unique table types because they cannot have any alias, this could still lead to a weak static type checking

Chapter 3. Typed Lua 47

person.firstname = nil end
person.firstname = "Lou" spoil()

--> compile-time warning

3.5 Type aliases and interfaces

Typed Lua includes type aliases for allowing programmers to define their own data types. Figure 3.4 shows the concrete syntax of the typealias construct.

After we define the type Person, we can use it in type annotations:

Chapter 3. Typed Lua 49

" " .. person.lastname
end

--> Goodbye Lou Reed
--> compile-time warning

This example shows that our optional type system is structural rather than nominal, that is, it checks the structure of types instead of their names, and it uses subtyping and consistent-subtyping for checking types.

end

Now we can use Element to annotate a function that inserts an element at the beginning of a list:

Chapter 3. Typed Lua 51

The type Exp is a recursive type that resembles the algebraic data types from functional programming. The small set of type predicates that we mentioned in Section 3.3 also includes a specific rule that is not based on tags. This specific rule lets programmers discriminate unions of table types and resembles the pattern matching from functional programming. We can use this feature to write an evaluation function for our simple language:

An idiomatic way for defining modules in Lua is to declare only locals and return a table constructor at the end of the source file. The returned con-structor includes the members that the module should export. The following example illustrates this case in Typed Lua:

local RADIANS_PER_DEGREE = 3.14159 / 180.0

local mymath = {}
local RADIANS_PER_DEGREE = 3.14159 / 180.0 mymath.deg = function (x:number):number return x / RADIANS_PER_DEGREE
end

Chapter 3. Typed Lua 53

module is not yet statically type checked, Typed Lua statically type checks its source file, and the type returned is the type of the module. Typed Lua raises a compile-time warning when it cannot find the source file of a given module.

After we use require to statically type check a module, Typed Lua can statically type check the usage of this module. In our previous example, the call to require assigns the type of the module mymath to the local mymath, so Typed Lua can catch misuses of the module.

Typed Lua uses closed table types along with the type self to represent objects. We use the following example to discuss this feature:

local Shape = { x = 0.0, y = 0.0 }

"move":(self, number, number) -> () }

While : is syntactic sugar in Lua, Typed Lua uses it to check method calls, binding any occurrence of the type self in the type of the method to the receiver. Indexing a method and not immediately calling it with the correct receiver is a compile-time warning:

Chapter 3. Typed Lua 55

2.5, Lua programmers often use this mechanism to simulate classes. We will use the following example to discuss this feature:

A return statement that appears in the top-level also exports an interface which we can use in type annotations. For instance, our previous example exports the following interface:

interface Shape
x, y:number
const new:(number, number) => (self)
const move:(number, number) => ()
end

Chapter 3. Typed Lua 57

const function Circle:area ():number
return math.pi * self.radius * self.radius end

local Circle = require "circle"
local circle1 = Circle:new(0, 5, 10)
local circle2:Circle = Circle:new(10, 10, 10) local circle3:Shape = circle1
local circle4:Shape = circle2

print(circle2:area()) print(circle3:area())

Chapter 3. Typed Lua 59

The complete syntax of description files

userdata md5_context
__tostring : (self) -> (string)
clone : (self) -> (self)
digest : (self, value) -> (string)
new : (self) -> (self)
reset : (self) -> (self)
update : (self, string*) -> (self)
version : string
end

local m = require "md5"
local x = m.new()
local y = x:clone()