Runtime error-on-nil for tables

[Veltas]

From Typed Lua: An Optional Type System for Lua, pp4-5:

local t: { string: number } = { foo = 1 }
local x: number = t.foo    -- x gets 1
local y: number = t["bar"] -- runtime error

When accessing a map, there is always the possibility that the key is not there. In Lua, accessing a non-existing key returns nil. Typed Lua is stricter, and raises a runtime error in this case. To get a map with the behavior of standard Lua tables, the programmer can use an union:

local t: { string: number? } = { foo = 1 }
local x: number = t.foo      -- compile error
local y: number = t.bar or 0 -- y gets 0
local z: number? = t["bar"]  -- z gets nil

Now the Typed Lua compiler will complain about the assignment on line two.

In current Typed Lua, all such tables now default to the optional form, e.g. {string: number} becomes {string: number?}.

So I want to know:

• Is it possible to get the runtime checked types in current Typed Lua?
• And, what was the reasoning for changing the rules for tables so much after the paper?

I would personally find the language runtime-checked table types very useful, and even the paper agrees with me that having to type-safe discard nil for all table accesses: "[makes] using the elements more inconvenient".

[mascarenhas]

We decided to not change the semantics of existing Lua operations, to avoid creating confusion. Something like this is should come back in the form of new syntax for asserting that a value is not nil.

[Veltas]

I completely agree. On second thoughts I realise it's better not to change the way the language runs, since programmers will not expect this from a stronger-typing pre-compiler.

For the time being I have been using a function not_nil to 'cast' away the nil possibility (or throw an error).

I'm no language designer, but just "throwing it out there", I'd be interested in a not nil syntax at the very least for tables, something like {string: number!} or {string: number not nil}, to show that I do want runtime checks for this table, and it should not instead give me a {string: number?} automatically. This change is more like syntactic sugar for tables, rather than changing the language's type model (which I think would be required if we had a general second-class type syntax).

EDIT: i.e. {string: number not nil} becomes {string : number}, and {string: number} becomes {string : number U nil}.

[Veltas]

At the moment this would probably be the most helpful addition to the language for me

[mascarenhas]

I want to wait until the changes in the code generator being done in the GSoC branch are merged back in master, as this requires not only changes to the typechecker, but a little bit of runtime library also (wrapping the expression in a call to assert does not work the type of the field can be false, so we need a notnil function similar to assert but that only throws on nil).

Sorry for the inconvenience. With the latest commit you can alias assert to something shorter and at least solve most of the cases with some amount of visual pollution:

local a = assert
local t: { number } = something_that_returns_array()    
local x = x + a(t[3])

[Veltas]

Don't worry, I'm not using typedlua for anything important at the moment, I'm just giving feedback for the sake of the project.

Yeah the alias of assert is a good idea for now, thanks.