🌴 Kailua
Kailua is an experimental type checker and integrated development environment (IDE) for the Lua programming language (currently only Lua 5.1 is supported).
THIS IS VERY EXPERIMENTAL PROJECT AND NO WARRANTY OR SUPPORT IS PROVIDED!
Installation and Usage
Kailua can be used as a standalone checker or an IDE plugin.
Standalone Checker
To install a standalone checker, install Rust first (1.15 or later required), then type the following:
cargo install -f kailua
(-f
will cause the existing installation to be upgraded.)
You can run kailua check <path to the entry point>
now.
You can also run kailua check <path to the directory>
, if you have kailua.json
or .vscode/kailua.json
in that directory. The configuration format is described in the later section.
Visual Studio Code
Kailua can be used as an IDE support for Visual Studio Code. Install Kailua by typing ext install kailua
from the Quick Launch (Ctrl-P
). If you are not on Windows, you should also install the standalone checker as above.
You will see a warning that the configuration file is missing when you open a folder containing Lua codes. You need it for real-time checking.
You can either create .vscode/kailua.json
by hand, or search "Kailua" from the Command Palette (Ctrl-Shift-P
) to edit one.
The following content is required for .vscode/kailua.json
, in case you are editing it by hand:
{
"start_path": "<path to the entry point>",
"preload": {
// This indicates that we are using Lua 5.1 and all built-in libraries of it.
"open": ["lua51"],
},
}
You need to reload the current window (Ctrl-R
or Cmd-R
) to apply the configuration.
Your First Kailua Code
Once you've set the entry point, you can write your first Kailua code:
--# open lua51
print('Hello, world!')
If you are using the configuration file, the first code can be made much simpler:
print('Hello, world!')
Play a bit with this code to see which errors Kailua can detect.
Supported IDE Functions
-
Real-time syntax checking (for all files).
-
Real-time type checking, starting from given start path.
-
Auto-completions for names and fields.
-
Help for function signatures.
-
Help for types of most subexpressions on hover.
-
Go to definition for local and global names.
-
Mass renaming of local and global names.
Kailua the Language
Special Comments
Kailua is a subset of valid Lua code---you don't need any transpilation or compilation. The additional annotations are described in special comments:
-
--: <type>
describes the type(s) of preceding item(s).It is valid anywhere a new name can be possibly defined:
local
(either individual names or statement),function
(arguments),for
(individual names) and assignment (either individual names or statement).When used right after the name, for the ease of typing, you can put a comma or closing parenthesis before the type like this:
function f(x, --: integer y, --: integer z) --: integer -- ... end
For the common case of defining multiple names you can put types after the statement. In this case types are delimited by commas.
-
--> <type>
describes the type(s) of function returns.It is valid only after the closing parenthesis of function arguments. It is valid to put
--:
(for the last argument) and-->
in the same line. -
--v function(<name>: <type> ...) [--> <type>]
describes a function type.It is valid before the
function
keyword (yes, also for anonymous functions). This is equivalent to--:
and-->
, but much more readable. All names should be identical to the corresponding declarations. Variadic arguments can be written as...: <type>
at the end of arguments. Multiple returns need parentheses.The general rule of the thumb is that all functions have to be typed with either
--v
or--:/-->
unless it is obvious from the preceding context. This allows you to write a code likef(function(a, b) ... end)
, but only whenf
is known to accept such a function. -
--v method(<name>: <type> ...) [--> <type>]
describes a method type.It is same to
function
, but for declarations likefunction A:b(...)
. Kailua tries to infer the type ofself
, and if it's not possible you should usefunction A.b(self, ...)
and--v function(...)
instead for the clarity. -
--# ...
is a special directive for the type checker.--# open <built-in library name>
loads the corresponding built-in names and also implicitly specifies what language variant is currently in use. The only supported name so far islua51
, for the vanilla Lua 5.1. This is whatpreload.open
configuration options actually do, and you should probably put it to the first non-comment line in the entry point if you don't have those options.--# type [local | global] <name> = <type>
can be used to declare a type alias. There are three flavors of typa alises:local
is locally scoped (much likelocal
statements),global
is globally scoped (much likeA = ...
), and no modifier indicates that the type is exported from the current file and they should be locally visible afterrequire
. Only local types can be in the inner scopes. Unlike variable names, inner type names should not overwrite outer names.--# assume [global] <name>: <type>
overrides the type for given name. Theglobal
keyword forces the global assignment, otherwise a new scope is created likelocal
statements. It is useful for sidestepping the checker issue, but it is also highly unsafe. Use at your own risk.More directives are likely to come.
The equal kind of special comments can span multiple lines.
--# type Date = {
--# hour: integer;
--# min: integer;
--# sec: integer;
--# }
Types
The following basic types are recognized:
-
nil
,boolean
(orbool
),number
,string
,function
,userdata
,thread
,table
for primitive Lua types. -
integer
(orint
) for a check-time integral subset ofnumber
. (In the future, in the Lua 5.3 mode or later, it will be also recognized as primitive.) -
true
orfalse
, integer and string literals are valid subtypes ofboolean
,integer
andstring
, respectively. -
The table type is divided into four useful cases.
Importantly, first two cases are not automatically inferred from the use and should be explicitly annotated like
local tab = {} --: vector<integer>
.-
vector<T>
for a table with consecutive integer keys. -
map<Key, Value>
for a homogeneous associative table. -
{ key1: T1, key2: T2 }
for records, whose keys are strings and fixed at the check time. You can use semicolons in place of commas.Explicitly declared records are "inextensible" by default, meaning that the list of fields is complete and cannot be altered. You can make it extensible by putting
...
at the end of fields; this allows a lazy initialization of records liketable.field = 'string'
. On the other hands, a normal Lua table is implicitly typed as extensible records, only made inextensible when required. -
{ T1, T2, T3 }
for tuples, whose keys are consecutive integers. Otherwise they are similar to records.
-
-
function(Arg, ...)
orfunction(Arg, ...) --> Ret
for functions.Ret
can be multiple types, in which case you need parentheses (function(vector<T>, integer) --> (integer, string)
). Arguments can be named likefunction(a: string, b: number)
. -
T | T | ...
for union types. They are mostly useful for literal types (e.g."read" | "write" | "execute"
). Kailua has very limited support for checking other kinds of union types. -
any
has no type information.--# assume
is the only way to make it useful. -
WHATEVER
(note the case) is a hole that the type checker always accepts.map<integer, WHATEVER>
andmap<WHATEVER, string>
are compatible;map<integer, WHATEVER>
andmap<string, string>
are not. As this thwarts the basic of type checking, use at your own risk.
The Kailua types are by default not checked for nil
. That is, you can assign nil
to integer
but you can also add two integer
s; the valid Kailua code can still result in a runtime error therefore. This restriction was required for making a practical type checker without changing the source programming language.
You can opt in two other nil
-handling modes if you need to make it explicit. As they are (transitively) freely assignable, consider them more a machine-readable documentation.
-
T?
also acceptsnil
but it is aware that it can containnil
. Twointeger?
s cannot be added. It also allows for missing fields and missing arguments (they are not allowed otherwise): the type{a: integer?, b: integer}
can contain either{a = 42, b = 54}
or{b = 54}
, but not{a = 42}
. -
T!
guarantees that it cannot containnil
.
Also, the table values are always T
or T?
(for the obvious reason).
Finally, types for the names and table values can optionally have a const
prefix. You cannot modify the innard of const
types: map<integer, const vector<string>>
. You can still assign to them (otherwise this type won't be useful at all).
Avoiding the type checker
As annotating everything is not practical, Kailua supports two ways to avoid the type checking with more localized guarantees:
-
--v [NO_CHECK] function(...)
disables the type checking for the following function.Kailua essentially believes the specified function type, which can be no longer omitted.
-
You can override what file to check by having
.kailua
files.When
require()
was used with a check-time string Kailua makes use ofpackage.path
andpackage.cpath
set. Forpackage.path
, it will tryF.kailua
first before reading a fileF
. Forpackage.cpath
, it will alwaysF.kailua
asF
would be probably binary. (Note that this will normally result in two extensions.lua.kailua
unless you have a sole?
in the search paths.).kailua
files would frequently use--# assume
as you should assume that the original code has given types.
Configuration Format
You can configure the exact behavior of Kailua with kailua.json
. It is a JSON with comments (//
) and stray comma allowed for convenience:
{
// This indicates where to start. This is the only mandatory field in the file.
//
// This can be a single string or an array of strings, and in the latter case
// multiple paths are separately (but possibly parallelly) checked against.
// Checking sessions do not affect others, but reports are merged.
"start_path": ["entrypoint.lua", "lib/my_awesome_lib.lua"],
// These are values for `package.path` and `package.cpath` variables, respectively.
// They are always relative to the base directory
// (a directory containing `.vscode` or `kailua.json` whichever being used).
// Refer to the Lua manual for the exact format.
//
// In the configuration one can use a special `{start_dir}` sequence
// which gets replaced by the directory containing the *current* start path.
// so if there are two start paths `foo/a.lua` and `bar/b.lua`,
// the path of `{start_dir}/?.lua` will expand to `foo/?.lua` or `bar/?.lua`
// for each start path. This is useful when you are working with multiple projects
// with individual directories, only sharing a portion of common codes.
//
// If they are not explicitly set, they are inferred from any assignments to
// `package.path` and `package.cpath` variables. This can be handy for scripts,
// but will be cumbersome for most other cases.
//
// It should be also noted that any path in `package_cpath` won't be directly
// read by Kailua; only `.kailua` files associated to them will be read.
"package_path": "?.lua;contrib/?.lua",
"package_cpath": "native/?",
// The preloading options to populate the environment before checking.
// They are executed in the following order, and in each array, in given order.
"preload": {
// A list of `--# open` arguments.
"open": ["lua51"],
// A list of `require()` arguments. Affected by `package_*` options.
"require": ["depA", "depB.core"],
},
}
Class System
Lua normally does not natively support classes and any other object-oriented features. Instead, it defers the difficult job of designing a class system to the users (or library authors). Consequently there are multiple class systems used in the wild, and whatever Kailua supports has to cover all of them.
This is close to impossible, so Kailua offers a customizable class system support. Currently the feature is in the early stage of development and not all possible features are implemented, mainly due to the authors' inability to analyze all of them. Analyses and suggestions for other class systems will be appreciated.
Declaring the class system
The class systems available in the current session are identified with unique global names, and have to be explicitly declared.
--# class system gideros
Currently the name of each class system is fixed and should be chosen from the following list:
Name | Description | Inheritance | [make_class] |
---|---|---|---|
gideros | Gideros class system | Single | Supported |
Declaring a class
The class can be declared in two ways.
--# assume class
directive can declare and assume the existing class.- If the class system has a support, a function with a
[make_class(<class system>)]
attribute will generate a new class whenever called.
--# assume class
directive
The --# assume class
directive can declare a class without class system. This is useful for defining a simple class with no inheritance and special semantics.
-- defines a global name `Hello` to be a class prototype for
-- the newly defined global class `Hello`.
--# assume global class Hello
Since this is an ordinary directive (that is going to be ignored by Lua), a local class (without global
) requires the name to be already a local name.
local Hello = {}
--# assume class Hello
The class system, if any, should be enclosed with parentheses. If the class system supports inhertiance the parent class can be also specified.
--# assume global class(gideros) Object
--# assume global class(gideros) Sprite: Object
In general different class systems (including those with no class system) do not mix.
[make_class]
attribute
A function with the [make_class]
attribute is much closer to how ordinary Lua code defines a new class. This attribute is exclusive to class systems, and such a function can be --# assume
d like this:
--# assume global `class`: [make_class(gideros)] function() --> table
Or can be explicitly declared with a function specification:
--v [NO_CHECK] -- because the gory detail of classes is hard to check
--v [make_class(gideros)]
--v function() --> table
function make_class()
-- ...
end
In many cases calling without any arguments will define a new class without explicit parents, and calling with an argument of the parent class prototype will do the inheritance. The exact interpretation of those arguments is however up to the class system.
A new class prototype returned by the [make_class]
function should be assigned to the variable as soon as possible. This is when the class receives its name:
local Hello = class() -- will also define a local type `Hello`
Sprite = class() -- will also define a global type `Sprite`
It is possible but not recommended to use a class without name (there are some backdoors). Such classes will be uniquely identified in the messages.
Defining fields and methods
Once the class is declared, fields and methods can be freely added to them as long as it does not break the class system's own limitations:
--# assume global class Person
--v function(name: string) --> Person
function Person.new(name)
local person = {}
set_metaclass_for_person(person) -- up to your imagination
--# assume person: Person
person.name = name -- will define a new field
return person
end
-- declares a new class field
Person.HELLO = 'Hello'
-- declares a new method (which is just a class field with a function receiving `self`)
--v method()
function Person:greet()
print(self.HELLO .. ', ' .. self.name)
end
local person = Person.new('J. Random Hacker')
person:greet()
As one can observe:
-
Without a class system,
--# assume
is essential to produce a new instance type. On the other hands, class systems will typically have their own ways to automatically derive anew
method or similar from a constructor. -
The instance field can be created via assignments. Reading a missing field still errors, so if we have transmuted the
person
variable after setting aname
field the checker will miss its existence. -
The method can be defined with the same syntax as functions, but it uses the
method
keyword and theself
argument is omitted (and inferred).
--# assume
also works for classes. The code above will look like the following if we can assume they already exist and we only want to add types:
--# assume global class Person
--# assume static Person.new: function(name: string) --> Person
--# assume static Person.HELLO: string
--# assume Person.greet: method()
local person = Person.new('J. Random Hacker')
person:greet()
This is same to ordinary --# assume
, but please note several differences:
-
Conceptually
Person.greet
should be astatic
function with the first argument typed asPerson
. Themethod
keyword was used here for the convenience (it is not a true type). -
Fields of globally defined class can be only
--# assume
d in the topmost scope. This is because--# assume
generally creates a copy of given name in the current local scope, but creating a new field will globally affect that class. -
Some fields can simply not be defined depending on the class system.
Gideros Support
The gideros
class system mimics the behavior of Gideros classes. This class system was chosen because, besides from the existing requirements, it represents a typical instance of naively defined class system that can be problematic for the type checker.
A typical declaration for the gideros
class system is as follows:
--# class system gideros
--# assume global class(gideros) Object
--# assume global Core: {}
--# assume Core.class: [make_class(gideros)] function(parent: table?) --> table
This defines the Object
class and a Core.class
class-generating function.
Constructor
The new
method is automatically created when the init
method is created.
--# assume global class(gideros) Foo: Object
--v method(text: string)
function Foo:init(text)
self.text = text
end
local x = Foo.new('string')
Note that the actual creation currently occurs at the first invocation of new
, so the error may be delayed to the usage site.
Inheritance
The Gideros class system supports the single inheritance and shares the general syntax and behavior described in the earlier section.
Fields in child classes simply shadows a previously defined field in a parent, which would break the subtyping (using a child class to the place expecting a parent class) if not restricted. Therefore in Kailua fields cannot be normally overriden. The exception is made for constructors (init
), which cannot be explicitly called through instances anyway.
In Gideros every class is assumed to be a descendant of the Object
class. Kailua recognizes the first (and only) class defined without a parent as such a class and disallows multiple such classes. The Core.class
function will use Object
as a parent if no other parent is specified. Since this implicit behavior is confusing otherwise, though, --# assume class
should always specify the parent class even when it would be Object
.
The Internals of Kailua
Kailua is a Rust application. For now, use the generated documentations hosted by docs.rs:
kailua_env
kailua_diag
kailua_test
kailua_syntax
kailua_types
kailua_check
kailua_workspace
kailua_langsvr
kailua_langsvr_protocol
kailua
License
Copyright © 2015–2017 Nexon Corporation. All rights reserved.
Kailua is dual-licensed under the MIT license and Apache license 2.0 at your option. By contributing to Kailua you agree that your contributions will be licensed under these two licenses.
Kang Seonghoon at devCAT Studio is the original developer of Kailua and remains as a primary project maintainer.