Re: TypedLua

[Kevin Clancy <kclanc@...>]

I think I understand what you are saying, but I'm not sure. What chapter
of Abadi and Cardelli talks about this?

All I was trying to say is that giving the type { L1 : T1, ..., Ln : Tn
} to the table constructor { L1 = t1, ..., LN = tn }, where T1 ... TN
are the types of the terms t1 ... tn, is somewhat naive. That type does
not convey that we know all other labels will yield nil when selected.
>From reading the Typed Lua paper, I suspect that you might be able to
convey this with the type { L1 : T1, ..., Ln : Tn, Any : Nil }. If I
remember correctly, Tidal Lock has something similar as well. [L1 : T1,
... Ln : Tn | const nil]?

Another interesting thing about passing table constructors directly into
functions is that it should be sound to perform depth subtyping on all
fields, even fields which are non-const in the expected table type.

I noticed that the Typed Lua paper doesn't mention depth subtyping in
its examples. Are there plans to add this?

On 3/3/2014 8:08 AM, Fabien wrote:
> 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] <https://www.dropbox.com/s/8mfvnzagx2gixdb/luawshop13-fleutot.pptx>
> [notes] <https://github.com/fab13n/metalua/blob/tilo/src/tilo/readme.md>
> [video]<http://2013.capitoledulibre.org/conferences/lua-workshop/towards-practical-type-checking-for-lua.html>
> 
> PS: I'd never heard of Lua Air before, I'll check it out with great
> interest.
>