Re: TypedLua

[Fabien <fleutot+lua@...>]

On Sun, Mar 2, 2014 at 7:57 PM, Kevin Clancy <kclanc@gmail.com> wrote:

My idea, which wouldn't involve altering the type system, works as
follows. When checking an table argument's type, I imagine that you
would be using bidirectional type-checking in check mode. When checking
a table constructor _expression_, you know that any unmentioned entries
are definitely absent. If the expected table type contains keys which
are not mentioned in the constructor being checked, you would include
those keys in the computed type, giving them type Nil.

It's important to have both "nil" and "I don't know" as typed for the unset keys: without the former you lose table extensibility; without the latter you lose subtyping among tables. The details are exposed at length in Abadi & Cardelli's book on sigma calculus, although I prefer the presentation made by Dider Remy in his record calculi, which ended up inspiring parts of OCaml's object orientation.

I've tried to give an overwiew of those issues in my Lua workshop '13 talk [slides] [notes] [video]

PS: I'd never heard of Lua Air before, I'll check it out with great interest.