lua-users home
lua-l archive

[Date Prev][Date Next][Thread Prev][Thread Next] [Date Index] [Thread Index]

Tidal Lock: optional static type checking and inference for Lua

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:

    $ git clone -b tilo git://
    $ 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!