Skip to content

Latest commit

 

History

History
1103 lines (847 loc) · 31.8 KB

tutorial.md

File metadata and controls

1103 lines (847 loc) · 31.8 KB

Programming With Types in Teal

Welcome to Teal!

In this tutorial, we will go through the basics so you can get up and running type checking your Lua code, through the use of Teal, a typed dialect of Lua.

Why Types

If you're already convinced about the idea of type checking, you may skip this part. :)

The data in your program has types: Lua is a high-level language, so each piece of data stored in the memory of the Lua virtual machine has a type: number, string, function, boolean, userdata, thread, nil or table.

Your program is basically a series of manipulations of data of various types. The program is correct when it does what it is supposed to do, and that will only happen when data is matched with other data of the correct types, like pieces of a puzzle: you can multiply a number by another number, but not by a boolean; you can call a function, but not a string; and so on.

The variables of a Lua program, however, know nothing about types. You can put any value in any variable at any time, and if you make a mistake and match things incorrectly, the program will crash at runtime, or even worse: it will misbehave... silently.

The variables of Teal do know about types: each variable has an assigned type and will hold on to that type forever. This way, there's a whole class of mistakes that the Teal compiler is able to warn you about before the program even runs.

Of course, it cannot catch every possible mistake in a program, but it should help you with things like typos in table fields, missing arguments and so on. It will also make you be more explicit about what kind of data your program is dealing with: whenever that is not obvious enough, the compiler will ask you about it and have you document it via types. It will also constantly check that this "documentation" is not out of date. Coding with types is like pair programming with the machine.

Installing tl

To run tl, the Teal compiler, you need a Lua environment. Install Lua and LuaRocks (methods vary according to your operating system), and then run

luarocks install tl

If your environment is set up correctly, you should have a tl command available now!

Your first Teal program

Let's start with a simple example, which declares a type-safe function. Let's call this example add.tl:

local function add(a: number, b: number): number
   return a + b
end

local s = add(1,2)
print(s)

You can type-check it with

tl check add.tl

You can convert it to Lua with

tl gen add.tl

This will produce add.lua. But you can also run it directly with

tl run add.tl

We can also write modules in Teal which we can load from Lua. Let's create our first module:

local addsub = {}

function addsub.add(a: number, b: number): number
   return a + b
end

function addsub.sub(a: number, b: number): number
   return a - b
end

return addsub

We can generate addsub.lua with

tl gen addsub.tl

and then require the addsub module from Lua normally. Or we can load the Teal package loader, which will allow require to load .tl files directly, without having to run tl gen first:

$ rm addsub.lua
$ lua
> tl = require("tl")
> tl.loader()
> addsub = require("addsub")
> print (addsub.add(10, 20))

When loading and running the Teal module from Lua, there is no type checking! Type checking will only happen when you run tl check or load a program with tl run.

Types in Teal

Teal is a dialect of Lua. This tutorial will assume you already know Lua, so we'll focus on the things that Teal adds to Lua, and those are primarily type declarations.

Types in Teal are more specific than in Lua, because Lua tables are so general. These are the basic types in Teal:

  • any
  • nil
  • boolean
  • integer
  • number
  • string
  • thread (coroutine)

Note: An integer is a sub-type of number; it is of undefined precision, deferring to the Lua VM.

You can also declare more types using type constructors. This is the summary list with a few examples of each; we'll discuss them in more detail below:

  • arrays - {number}, {{number}}
  • tuples - {number, integer, string}
  • maps - {string:boolean}
  • functions - function(number, string): {number}, string

Finally, there are types that must be declared and referred to using names:

  • enum
  • record
    • userdata
    • arrayrecord

Here is an example declaration of each. Again, we'll go into more detail below, but this should give you an overview:

-- an enum: a set of accepted strings
local enum State
   "open"
   "closed"
end

-- a record: a table with a known set of fields
local record Point
   x: number
   y: number
end

-- a userdata record: a record which is implemented as a userdata
local record File
   userdata
   status: function(): State
   close: function(File): boolean, string
end

-- an arrayrecord: a record which doubles as a record and an array
local record TreeNode<T>
   {TreeNode<T>}
   item: T
end

Local variables

Variables in Teal have types. So, when you declare a variable with the local keyword, you need to provide enough information so that the type can be determined. For this reason, it is not valid in Teal to declare a variable with no type at all like this:

local x -- Error! What is this?

There are two ways, however, to give a variable a type:

  • through declaration
  • through initialization

Declaration is done writing a colon and a type. When declaring multiple variables at once, each variable should have its own type:

local s: string
local r, g, b: number, number, number
local ok: boolean

You don't need to write the type if you are initializing the variable on creation:

local s = "hello"
local r, g, b = 0, 128, 128
local ok = true

If you initialize a variable with nil and don't give it any type, this doesn't give any useful information to work with (you don't want your variable to be always nil throughout the lifetime of your program, right?) so you will have to declare the type explicitly:

local n: number = nil

This is the same as omitting the = nil, like in plain Lua, but it gives the information the Teal program needs. Every type in Teal accepts nil as a valid value, even if, like in Lua, attempting to use it with some operations would cause a runtime error, so be aware!

Arrays

The simplest structured type in Teal is the array. An array is a Lua table where all keys are numbers and all values are of the same type. It is in fact a Lua sequence, and as such it has the same semantics as Lua sequences for things like the # operator and the use of the table standard library.

Arrays are described with curly brace notation, and can be denoted via declaration or initialization:

local values: {number}
local names = {"John", "Paul", "George", "Ringo"}

Note that values was initialized to nil. To initialize it with an empty table, you have to do so explicitly:

local prices: {number} = {}

Creating empty tables to fill an array is so common that Teal includes a naive inference logic to support determining the type of empty tables with no declaration. The first array assignment to an empty table, reading the code top-to-bottom, determines its type. So this works:

local lengths = {}
for i, n in ipairs(names) do
   table.insert(lengths, #n) -- this makes the  lengths table a {number}
end

Note that this works even with library calls. If you make assignments of conflicting types, the tl compiler will tell you in its error message from which point in the program it originally got the idea that the empty table was an array of that incompatible type.

Note also that we didn't need to declare the types of i and n in the above example: the for statement can infer those from the return type of the iterator function produced by the ipairs call. Feeding ipairs with a {string} means that the iteration variables of the ipairs loop will be number and string. For an example of a custom user-written iterator, see the Functions section below.

Note that all items of the array are expected to be of the same type. If you need to deal with heterogeneous arrays, you will have to use the cast operator as to force the elements to their desired types. Keep in mind that when you use as, Teal will accept whatever type you use, meaning that it can also hide incorrect usage of data:

local sizes: {number} = {34, 36, 38}
sizes[#sizes + 1] = true as number -- this does not perform a conversion! it will just stop tl from complaining!
local sum = 0
for i = 1, #sizes do
   sum = sum + sizes[i] -- will crash at runtime!
end

Tuples

Another common usage of tables in Lua are tuples: tables containing an ordered set of elements of known types assigned to its integer keys.

-- Tuples of type {string, integer} containing names and ages
local p1 = { "Anna", 15 }
local p2 = { "Bob", 37 }
local p3 = { "Chris", 65 }

When indexing into tuples with number constants, their type is correctly inferred, and trying to go out of range will produce an error.

local age_of_p1: number = p1[2] -- no type errors here
local nonsense = p1[3] -- error! index 3 out of range for tuple {1: string, 2: integer}

When indexing with a number variable, Teal will do its best by making a union of all the types in the tuple (following the restrictions on unions detailed below)

local my_number = math.random(1, 2)
local x = p1[my_number] -- => x is a string | number union
if x is string then
   print("Name is " .. x .. "!")
else
   print("Age is " .. x)
end

Tuples will additionally help you keep track of accidentally adding more elements than they expect (as long as their length is explicitly annotated and not inferred).

local p4: {string, integer} = { "Delilah", 32, false } -- error! expected maximum length of 2, got 3

One thing to keep in mind when using tuples versus arrays is type inference, and when you should or shouldn't need it. A table will be inferred as an array if all of its elements are the same type, and as a tuple if any of its types aren't the same. So if you want an array of a union type instead of a tuple, explicitly annotate it as such:

local array_of_union: {string | number} = {1, 2, "hello", "hi"}

And if you want a tuple where all elements have the same type, annotate that as well:

local tuple_of_nums: {number, number} = {1, 2}

Maps

Another very common type of table is the map: a table where all keys of one given type, and all values are of another given type, which may or may not be the same as that of the keys. Maps are notated with curly brackets and a colon:

local populations: {string:number}
local complicated: {Object:{string:{Point}}} = {}
local modes = { -- this is {boolean:number}
   [false] = 127,
   [true] = 230,
}

In case you're wondering, yes, an array is functionally equivalent to a map with keys of type number.

When creating a map with string keys you may want to declare its type explicitly, so it doesn't get mistaken for a record. Records are freely usable as maps with string keys when all its fields are of the same type, so you wouldn't have to annotate the type to get a correct program, but the annotation will help the compiler produce better error messages if any errors occur involving this variable:

local is_vowel: {string:boolean} = {
   a = true,
   e = true,
   i = true,
   o = true,
   u = true,
}

For now, if you have to deal with heterogeneous maps (that is, Lua tables with a mix of types in their keys or values), you'll have to use casts.

Records

Records are the third major type of table supported in Teal. They represent another super common pattern in Lua code, so much that Lua includes special syntax for it (the dot and colon notations for indexing): tables with a set of string keys known in advance, each of them corresponding to a possibly different value type. Records (named as such in honor of the Algol/Pascal tradition from which Lua gets much of the feel of its syntax) can be used to represent objects, "structs", etc.

To declare a record variable, you need to create a record type first. The type describes the set of valid fields (keys of type string and their values of specific types) this record can take. You can declare types using local type and global types using global type.

local type Point = record
   x: number
   y: number
end

Types are constant: you cannot reassign them, and they must be initialized with a type on declaration.

Just like with functions in Lua, which can be declared either with local f = function() or with local function f(), there is also a shorthand syntax available for the declaration of record types:

local record Point
   x: number
   y: number
end

Tables that match the shape of the record type will be accepted as an initializer of variables declared with the record type:

local p: Point = { x = 100, y = 100 }

This, however, won't work:

local p1 = { x = 100, y = 100 }
local p2: Point = p1 -- Error!

Just because a table has fields with the same names and types, it doesn't mean that it is a Point. A Distance could also be defined as fields x and y, but a distance is not a point.

You can always force a type, though, using the as operator:

local p2 = p1 as Point -- Ok, I'll trust you...

Note we didn't even have to declare the type of p2. The as expression resolves as a Point, so p2 picks up that type.

You can also declare record functions after the record definition using the regular Lua colon or dot syntax, as long as you do it in the same scope block where the record type is defined:

function Point.new(x: number, y: number): Point
   local self: Point = setmetatable({}, { __index = Point })
   self.x = x or 0
   self.y = y or 0
   return self
end

function Point:move(dx: number, dy: number)
   self.x = self.x + dx
   self.y = self.y + dy
end

When using the function, don't worry: if you get the colon or dot mixed up, tl will detect and tell you about it!

If you want to define the function in a later scope (for example, if it is a callback to be defined by users of a module you are creating), you can declare the type of the function field in the record and fill it later from anywhere:

local record Obj
   location: Point
   draw: function(Obj)
end

A record can also have an array part, making it an "arrayrecord". The following is an arrayrecord. You can use it both as a record, accessing its fields by name, and as an array, accessing its entries by number.

local record Node
   {Node}
   weight: number
   name: string
end

Note the recursive definition in the above example: records of type Node can be organized as a tree using its array part.

Finally, records can contain nested record type definitions. This is useful when exporting a module as a record, so that the types created in the module can be used by the client code which requires the module.

local record http

   record Response
      status_code: number
   end

   get: function(string): Response
end

return http

You can then refer to nested types with the normal dot notation, and use it across required modules as well:

local http = require("http")

local x: http.Response = http.get("http://example.com")
print(x.status_code)

Generics

Teal supports a simple form of generics that is useful enough for dealing collections and algorithms that operate over abstract data types.

You can use type variables wherever a type is used, and you can declare them in both functions and records. Here's an example of a generic function:

local function keys<K,V>(xs: {K:V}):{K}
   local ks = {}
   for k, v in pairs(xs) do
      table.insert(ks, k)
   end
   return ks
end

local s = keys({ a = 1, b = 2 }) -- s is {string}

we declare the type variables in angle brackets and use them as types. Generic records are declared and used like this:

local type Tree = record<X>
   {Tree<X>}
   item: X
end

local t: Tree<number> = {
   item = 1,
   { item = 2 },
   { item = 3, { item = 4 } },
}

Metamethods

Lua supports metamethods to provide some advanced features such as operator overloading. Like Lua tables, records support metamethods. To use metamethods in records you need to do two things:

  • declare the metamethods in the record type using the metamethod word to benefit from static type checking;
  • and assign the metatable with setmetatable as you would normally do in Lua to get the dynamic metatable behavior.

Here is a complete example, showing the metamethod declarations in the record block and the setmetatable declarations attaching the metatable.

local type Rec = record
   x: number
   metamethod __call: function(Rec, string, number): string
   metamethod __add: function(Rec, Rec): Rec
end

local rec_mt: metatable<Rec>
rec_mt = {
   __call = function(self: Rec, s: string, n: number): string
      return tostring(self.x * n) .. s
   end,
   __add = function(a: Rec, b: Rec): Rec
      local res: Rec = setmetatable({}, rec_mt)
      res.x = a.x + b.x
      return res
   end,
}

local r: Rec = setmetatable({ x = 10 }, rec_mt)
local s: Rec = setmetatable({ x = 20 }, rec_mt)

r.x = 12
print(r("!!!", 1000)) -- prints 12000!!!
print((r + s).x)      -- prints 32

Note that we explicitly declare variables as Rec when initializing the declaration with setmetatable. The Teal standard library definiton of setmetatable is function<T>(T, metatable<T>): T, so declaring the correct record type in the declaration assigns the record type to the type variable T in the return value of the function call, causing it to propagate to the argument types, matching the correct table and metatable types.

Operator metamethods for integer division // and bitwise operators are supported even when Teal runs on top of Lua versions that do not support them natively, such as Lua 5.1.

Enums

Enums are a restricted type of string value, which represent a common practice in Lua code: using a limited set of string constants to describe an enumeration of possible values.

You describe an enum like this:

local type Direction = enum
   "north"
   "south"
   "east"
   "west"
end

or like this:

local enum Direction
   "north"
   "south"
   "east"
   "west"
end

Variables and arguments of this type will only accept values from the declared list. Enums are freely convertible to strings, but not the other way around. You can of course promote an arbitrary string to an enum with a cast.

Functions

Functions in Teal should work like you expect, and we have already showed various examples.

You can declare nominal function types, like we do for records, to avoid longwinded type declarations, especially when declaring functions that take callbacks. This is done with using function types, and they can be generic as well:

local type Comparator = function<T>(T, T): boolean

local function mysort<A>(arr: {A}, cmp: Comparator<A>)
   -- ...
end

Another thing to know about function declarations is that you can parenthesize the declaration of return types, to avoid ambiguities when using nested declarations and multiple returns:

f: function(function():(number, number), number)

You can declare functions that generate iterators which can be used in for statements: the function needs to produce another function that iterates. This is an example taken the book "Programming in Lua":

local function allwords(): (function(): string)
   local line = io.read()
   local pos = 1
   return function(): string
      while line do
         local s, e = line:find("%w+", pos)
         if s then
            pos = e + 1
            return line:sub(s, e)
         else
            line = io.read()
            pos = 1
         end
      end
      return nil
   end
end

for word in allwords() do
   print(word)
end

The only changes made to the code above were the addition of type signatures in both function declarations.

Variadic functions

Just like in Lua, some functions in Teal may receive a variable amount of arguments. Variadic functions can be declared by specifying ... as the last argument of the function:

local function test(...: number)
   print(...)
end

test(1, 2, 3)

In case your function returns a variable amount of values, you may also declare variadic return types by using the type... syntax:

local function test(...: number): number...
   return ...
end

local a, b, c = test(1, 2, 3)

If your function is very dynamic by nature (for example, you are typing a Lua function that can return anything), a typical return type will be any.... When using these functions, often one knows at the call site what are the types of the expected returns, given the arguments that were passed. To set the types of these dynamic returns, you can use the as operator over multiple values, using a parenthesized list of types:

local s = { 1234, "ola" }
local a, b = table.unpack(s) as (number, string)

print(a + 1)      -- `a` has type number
print(b:upper())  -- `b` has type string

Union types

The language supports a basic form of union types. You can register a type that is a logical "or" of multiple types: it will accept values from multiple types, and you can discriminate them at runtime.

You can declare union types like this:

local a: string | number | MyRecord
local b: {boolean} | MyEnum
local c: number | {string:number}

To use a value of this type, you need to discriminate the variable, using the is operator, which takes a variable of a union type and one of its types:

local a: string | number | MyRecord

if a is string then
   print("Hello, " .. a)
elseif a is number then
   print(a + 10)
else
   print(a.my_record_field)
end

As you can see in the example above, each use of the is operator causes the type of the variable to be properly narrowed to the type tested in its respective block.

The flow analysis of is also takes effect within expressions:

local a: string | number

local x: number = a is number and a + 1 or 0

Current limitations of union types

In the current version, there are two main limitations regarding support for union types in Teal.

The first one is that the is operator always matches a variable, not arbitrary expressions. This limitation is there to avoid aliasing.

Since code generation for the is operator used for discrimination of union types translates into a runtime type() check, we can only discriminate across primitive types and at most one table type.

This means that these unions not accepted:

local invalid1: MyRecord | MyOtherRecord
local invalid2: {string} | {number}
local invalid3: {string} | {string:string}
local invalid4: {string} | MyRecord

Also, since is checks for enums currently also translate into type() checks, this means they are indistinguishable from strings at runtime. So, for now this is also not accepted:

local invalid5: string | MyEnum

This restriction between strings and enums may be removed in the future. The restriction on records may also be lifted in the future.

The type any

The type any, as it name implies, accepts any value, like a dynamically-typed Lua variable. However, since Teal doesn't know anything about this value, there isn't much you can do with it, besides comparing for equality and against nil, and casting it into other values using the as operator.

Some Lua libraries use complex dynamic types that can't be easily represented in Teal. In those cases, using any and making explicit casts is our last resort.

Variable attributes

Teal supports variable annotations, with similar syntax and behavior to those from Lua 5.4. They are:

Const variables

The <const> annotation works in Teal like it does in Lua 5.4 (it works at compile time, even if you're running a different version of Lua). Do note however that this is annotation for variables, and not values: the contents of a value set to a const variable are not constant.

local xs <const> = {1,2,3}
xs[1] = 999 -- ok! the array is not frozen
xs = {} -- Error! can't replace the array in variable xs

To-be-closed variables

The <close> annotation from Lua 5.4 is only supported in Teal if your code generation target is Lua 5.4 (see the compiler options documentation for details on code generation targets). These work just like they do in Lua 5.4.

local contents = {}
for _, name in ipairs(filenames) do
   local f <close> = assert(io.open(name, "r"))
   contents[name] = f:read("*a")
   -- no need to call f:close() because files have a __close metamethod
end

Total variables

The <total> annotation is specific to Teal. It declares a const variable assigned to a table value in which all possible keys need to be explicitly declared.

Of course, not all types allow you to enumerate all possible keys: there is an infinite number (well, not infinite because we're talking about computers, but an impractically large number!) of possible strings and numbers, so maps keyed by these types can't ever be total. Examples of valid key types for a total map are booleans (for which there are only two possible values) and, most usefully, enums.

Enums are the prime case for total variables: it is common to declare a number of cases in an enum and then to have a map of values that handle each of these cases. By declaring that map <total> you can be sure that you won't forget to add handlers for the new cases as you add new entries to the enum.

local degrees <total>: {Direction:number} = {
   ["north"] = 0,
   ["west"] = 90,
   ["south"] = 180,
   ["east"] = 270,
}

-- if you later update the `Direction` enum to add new directions
-- such as "northeast" and "southwest", the above declaration of
-- `degrees` will issue a compile-time error, because the table
-- above is no longer total!

Another example of types that have a finite set of valid keys are records. By marking a record variable as <total>, you make it so it becomes mandatory to declare all its fields in the given initialization table.

local record Color
   red: integer
   green: integer
   blue: integer
end

local teal_color <total>: Color = {
   red = 0,
   green = 128,
   blue = 128,
}

-- if you later update the `Color` record to add a new component
-- such as `alpha`, the above declaration of `teal_color`
-- will issue a compile-time error, because the table above
-- is no longer total!

Note however that the totality check refers only to the presence of explicit declarations: it will still accept an assignment to nil as a valid declaration. The rationale is that an explicit nil entry means that the programmer did consider that case, and chose to keep it empty. Therefore, something like this works:

local vertical_only <total>: {Direction:MotionCallback} = {
   ["north"] = move_up,
   ["west"] = nil,
   ["south"] = move_down,
   ["east"] = nil,
}

-- This declaration is fine: the map is still total, as we are
-- explicitly mentioning which cases are left empty in it.

(Side note: the name "total" comes from the concept of a "total relation" in mathematics, which is a relation where, given a set of "keys" mapping to a set of "values", the keys fully cover the domain of their type).

Global variables

Unlike in Lua, global variables in Teal need to be declared, because the compiler needs to know its type. It also allows the compiler to catch typos in variable names, because an invalid name will not be assumed to be some unknown global that happens to be nil.

You declare global variables in Teal using global, like this, doing declaration and/or assignment:

global n: number

global m: {string:boolean} = {}

global hi = function(): string
   return "hi"
end

global function my_function()
   print("I am a global function")
end

You can also declare global types, which are visible across modules, as long as their definition has been previously required:

-- mymod.tl
local mymod = {}

global type MyPoint = record
   x: number
   y: number
end

return mymod
-- main.tl
local mymod = require("mymod")

local function do_something(p: MyPoint)
   -- ...
end

If you have circular type dependencies that span multiple files, you can forward-declare a global type by specifying its name but not its implementation:

-- person.tl
local person = {}

global type Building

global record Person
   residence: Building
end

return person
-- building.tl
local building = {}

global type Person

global record Building
   owner: Person
end

return building
-- main.tl
local person = require("person")
local building = require("building")

local b: Building = {}
local p: Person = { residence = b }

b.owner = p

The Teal Standard Library and Lua compatibility

tl supports a fair subset of the Lua 5.3 standard library (even in other Lua versions, using compat-5.3), avoiding 5.3-isms that are difficult to reproduce in other Lua implementations.

It declares all entries of the standard library as <const>, and assumes that Lua libraries don't modify it. If your Lua environment modifies the standard library with incompatible behaviors, tl will be oblivious to it and you're on your own.

The Teal compiler also supports Lua-5.3-style bitwise operators (&, |, ~, <<, >>) and the integer division // operator on all supported Lua versions. For Lua versions that do not support it natively, it generates code using the bit32 library, which is also included in compat-5.3 for Lua 5.1.

You can explicitly disable the use of compat-5.3 with the --skip-compat53 flag and equivalent option in tlconfig.lua. However, if you do so, the Lua code generated by your Teal program may not behave consistently across different target Lua versions, and differences in behavior across Lua standard libraries will reflect in Teal. In particular, the operator support described above may not work.

Using tl with Lua

You can use tl to type-check not only Teal programs, but Lua programs too! When type-checking Lua files (with the .lua extension or a Lua #! identifier), the type-checker adds support for an extra type:

  • unknown

which is the type of all non-type-annotated variables. This means that in a Lua file you can declare untyped variables as usual:

local x -- invalid in .tl, valid but unknown in .lua

When processing .lua files, tl will report no errors involving unknown variables. Anything pertaining unknown variables is, well, unknown. Think of .tl files as the safer, "strict mode", and .lua files as the looser "lax mode". However, even a Lua file with no annotations whatsoever will still have a bunch of types: every literal value (numbers, strings, arrays, etc.) has a type. Variables initialized on declaration are also assumed to keep consistent types like in Teal. The types of the Lua standard library are also known to tl: for example, the compiler knows that if you run table.concat on a table, the only valid output is a string.

Plus, requiring type-annotated modules from your untyped Lua program will also help tl catch errors: tl can check the types of calls from Lua to functions declared as Teal modules, and will report errors as long as the input arguments are not of type unknown.

Having unknown variables in a Lua program is not an error, but it may hide errors. Running tl check on a Lua file will report every unknown variable in a separate list from errors. This allows you to see which parts of your program tl is helpless about and help you incrementally add type annotations to your code.

Note that even though adding type annotations to .lua files makes it invalid Lua, you can still do so and load them from the Lua VM once the Teal package loader is installed by calling tl.loader().

Further reading

Type definitions for third party libraries

You can also create declaration files to annotate the types of third-party Lua modules, including C Lua modules. For more information, see the declaration files page.