[REVIEW] Typed Lua (Was: Any plans regarding static typing in core Lua?

[Dirk Laurie <dirk.laurie@...>]

2016-03-05 21:25 GMT+02:00 Dirk Laurie <dirk.laurie@gmail.com>:
> I got the impression that Typed Lua is a project on its own, rather
> than a future direction for Lua. It has a rockspec but has not been
> uploaded to a LuaRocks repository. Its main documentation is
> André Murbach Maidl's PhD thesis.
>
> There is also Ravi, which is currently being developed, with regular
> progress reports in this list.
>
> 2016-03-05 19:32 GMT+02:00 Wojciech Miłkowski <wmilkowski@interia.pl>:
>> Considering this paper:
>> http://www.lifl.fr/dyla14/papers/dyla14-4-typed-lua-an-optional-type-system.pdf
>> and this presentation from Lua Workshop two years ago:
>> http://www.lua.org/wshop14/Murbach.pdf Typed Lua is long term goal, but I'm
>> not aware about any progress in this area.
>>
>> Regards,
>> W.

Typed Lua is an extension of Lua. That is to say, any Lua program
is a valid Typed Lua program, but not vice versa.

I've read some of the thesis and downloaded and run the software.
Bottom line: You can write your program in Typed Lua, check its
adherence to typing rules with 'tlc', and run it in standard Lua.

The program 'tlc' is supplied together with all documentation including
the source code of the thesis and talk slides. I retrieved the rockspec

file://github.com/andremm/typedlua/blob/master/typedlua-scm-1.rockspec

and did "luarocks install typedlua-scm-1.rockspec". It needs 'lpeg'
to be installed first.

The thesis is, as  can be expected, aimed at academic readers.
Sample: "The rule S-FUN defines the subtyping relation for function
types, which are contravariant on the argument type and covariant
on the return type." There is no manual for Typed Lua. One can
cut-and-paste examples from the TeX source of the conference
talks.

Typing is achieved by extending Lua to accept optional annotations,
e.g. "local function succ (n:integer)" declares an argument type but
leaves the return type open.

The compiler 'tlc' does a static analysis of the code and strips off the
annotations, producing as output a standard Lua program. Violations
of type annotations are shown in a familiar form, e.g.

$ tlc ex1.lua
ex1.lua:2:1: type error, attempt to assign '(number, nil*)' to
'(integer, value*)'

There is no indication in the thesis of any work on an interpreter that
would do run-time type checking but it is obviously kept open as
a possibility. The most recent change to the repository, excluding
thesis and talks, is "a year ago".