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

Venge

By the way, you say strong typing, but I think you mean static typing. There is a difference. For example, Python is strongly typed, but dynamically typed. C is weakly typed, but statically typed. – Pinwork

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.

Bonniebonns

I hear what you're saying; I've been putting a lot of thought into this, and while it seems very simply to cover the most basic cases (i.e. catching local x:int = "hello" as an error) things get very difficult when you start worrying about tables or returning typed tuples from functions. But those guys at Adobe figured it out with Javascript! – Venge

Table and the infinite number of ways they are used is definitely the problem. If you're willing to have lots of annotations things probably get simpler. – Bonniebonns

Norman, knowledge should be shared. I for one would be very interested in learning what were the conclusions of your study! – Laskowski

@Armentage: Note that another difficulty is that you would need to expose this type system to things like userdata, allowing the creation of new types that can be checked. Remember: the primary purpose of Lua is embedding, so if you have type safety, it needs to combine well with user extensions of the language. – Camphorate

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!

Darwen

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.

Isochronous

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.

Pinwork

I am not looking for LUA.NET. LUA.NET implies some sort of .NET runtime. The .NET runtime is nothing like the LUA ByteCode VM. What I am looking for would only apply strong-typing at byte-compile time, and then run the resulting code blissfully unaware that anything unusually happened to it at compile time. – Venge

Unfortunately, I am already working with a large (and growing) LUA code base. Due to LUA's nature, changing any existing library code is pretty much impossible. An optional strong-typing front end would solve this problem, without necessarily changing the basic feel of the language. – Venge

@Armentage, Lua is not an acronym, it is a proper noun. It is written "Lua", not "LUA". See lua.org/about.html#name for the official story. – Mcduffie

@Armentage: If you want to pursue this in the fall I might be able to find a student who would be interested. – Bonniebonns

We had an intern at my firm build something like this over the summer. Results were interesting... his mentor actually had him build his type-safe lua pre-processor in Haskell... – Venge

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.

Enosis

The slides for the Dyla14 paper are available: lua.org/wshop14/Murbach.pdf – Impregnate

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)

Bergh

Answer 7

I recommend EmmyLua.

This is an Intellij/VSCode plugin that supports typing documentation. I found the overall documenting approaching method to be very friendly. Also thanks to its IDE support, EmmyLua also support hinting.

Here is a little snippet for EmmyLua doc:

--- @alias recipe_prototype any
--- @alias recipe_name string
--- @alias ingredient_name string

--- @class Coordinate
--- @field x number
--- @field y number

--- @class Entity
--- @field entity_number number unique identifier of entity
--- @field name string entity name
--- @field position Coordinate
--- @field direction any defines.direction.east/south/west/north

--- @class BlueprintSection
--- @field entities Entity[]
--- @field inlets number[] index of inlets in entities list
--- @field outlets number[] index of outlets in entities list

--- @type BlueprintSection
BlueprintSection = {}

--- @return BlueprintSection
function BlueprintSection.new()
    --- ...
end

--- @param other BlueprintSection
--- @param xoff number optional, x-offset of the other section, default to width of self
--- @param yoff number optional, y-offset of the other section, default to 0
--- @return BlueprintSection new self
function BlueprintSection:concat(other, xoff, yoff)
   -- ...
end

For more doc reference, check https://emmylua.github.io

Linn