I've spent some time investigating sound type-checking for Lua. The
main result will be a paper proposing a formal type system;
there's also an early prototype type-checker, with partial type
inference and gradual typing, to experiment with those proposals.
A detailed description of the type-checker is on Github's readme:
Full developments are accessible in the paper's draft:
Here are some of the key characteristics of Tidal Lock:
* a sound type system, with structural subtyping, and support for Lua's
most idiomatic peculiarities;
* gradual typing, an approach which allows to seamlessly mix typed
program fragments with untyped ones, down to within a single
_expression_; details can be found on the inventor's page:
* partial type inference: by default, when facing an non-annotated
_expression_, the system tries to guess its static type rather than
considering it as dynamic;
* detection of "null^Wnil pointer exceptions".
The paper is still under development; among others, I'm considering
switching to a small-step semantics, to allow a Felleisen-style
soundness theorem demonstration.
In the process of writing the compiler, I've simplified and cleaned up
Metalua, so that it can now run without being installed. Metalua not
being ported to Lua 5.2 yet, this remains a Lua 5.1 program.
To try the type-checker on test terms, clone the repository's 'tilo'
branch, put 'src/' in your lua path, and run tilo as a lib after having
loaded metalua:
$ cd metalua/src
$ lua51 -l metalua -l tilo -e 'tilo[[return function(p) local n=p.x+1; p.y=p.x; return p end]]'
[...lots of logs...]
Result: return (["x"=const number, "y"=var number])->(["x"=const number, "y"=var number])
In its current state, this work's interest is primarily theoretical, and for now
I'm primarily interested by theoretical feedbacks and/or collaboration; but I have
great hopes to turn it into a practical tool!
