Statically typed Lua

Question

I am looking for a Lua front-end compiler that is type-checked at compile time, but outputs standard Lua 5.1 byte-code (that has only run-time types). What I want is a decent amount of static, compile-time syntactic analysis and optional typing, to detect trivial errors sooner than run-time. The resulting byte-code would have to play nicely with existing Lua byte-code that was compiled with the standard LoadString().

To be clear -- any difference would only occur at byte-compilation time. At runtime, the byte code would have no idea that anything different/unusual happened to it during the compile phase.

What I have in mind sounds a lot like ActionScript; I wouldn't even mind an ActionScript compiler that outputs Lua byte code!

Has anyone heard of such an effort? I've seen some references to using MetaLua to do this, but honestly I am not bright enough to make heads of tails of their documentation

Answer 1

In the summer of 2005 or thereabouts, I worked with an incredibly smart undergraduate student on the problem of doing some compile-time type inference for Lua, possibly assisted by annotations. This problem turns out to be incredibly hard! (My student wrote a short technical note, but it's not really intended for general circulation.)

If I wanted to solve the problem you have posed, with the twin constraints that it allow significant static type checking and that it interoperate with standard bytecode-compiled Lua code, I would design a new language from scratch to satisfy these two constraints. It would be a substantial amount of work but significantly easier than trying to retrofit a type system to Lua.

Answer 2

Please see this Metalua blog post.

-{ extension "types" }

function sum (x :: list(number)) :: number
  local acc :: number = 0
  for i=1, #x do acc=acc+x[i] end
  return acc
end

This is looks like a run-time solution though.

Anyway, feel free to ask your question in Metalua mailing list. If you want to extend Lua syntax, Metalua is the first tool to look at.

P.S. Please never write Lua as all-caps!

Answer 3

This question is six years old... but here's a new answer: http://terralang.org/

Like C, Terra is a simple, statically-typed, compiled language with manual memory management. But unlike C, it is designed from the beginning to interoperate with Lua. Terra functions are first-class Lua values created using the terra keyword. When needed they are JIT-compiled to machine code.

Answer 4

There is no such thing. It may be possible to extend MetaLua to do this but nobody has done it, and AFAIK, there are no plans to do so. Lua is meant to be a dynamic language, if you want a statically typed language, use one.

What you are essentially looking for is something like Java or C#. In that case, you could use a project like Lua.NET to integrate existing Lua code with C#. There is also Kahlua for Java.

Answer 5

There is a new paper "Typed Lua: An Optional Type System for Lua" from PUC-Rio just published in Dyla'14. http://dl.acm.org/citation.cfm?id=2617553

It is about "initial design of Typed Lua, an optionally-typed extension of the Lua scripting language". It's still in progress, and the type system is still relatively simple. No type inference/type checking tool provided.

Regarding the metalua based typing system, Tidal Lock: optional static type checking and inference for Lua from Fabien. http://lua-users.org/lists/lua-l/2013-02/msg00403.html.

Answer 6

There is also Ravi https://github.com/dibyendumajumdar/ravi

Ravi Programming Language is a derivative of Lua 5.3 with limited optional static typing and LLVM and libgccjit based JIT compilers

I really enjoy programing in Terra (see above)