Re: TypedLua

[Kevin Clancy <kclanc@...>]

Cool stuff. Right now, I'm assuming that the paper is the most
up-to-date resource in Typed Lua's github repo, and that the document
describing typing rules is being revised (so that, for example, the or
operator acts as a destructor rather than a constructor for union types).

The paper states that typed lua is a strict superset of lua. But I'm
wondering what exactly this means. Does it mean that any program which
compiles under the standard lua compiler also compiles under the typed
lua compiler? If so, I don't understand how you can get away with using
local type inference. To maintain compatibilty with lua, it seems that
you would need to give any unannotated, locally-bound variable the Any
type. As I understand it, a core aspect of local type inference is that
unannotated variables are given a type which is more specific than Any.

It's really fascinating how the syntax and subtyping rules for table
types have been defined. If I understand correctly, instead of using
identifiers as keys, types are used. And because typed lua includes
types which correspond to literal strings, typed lua's table types
subsume the common notion of record types, which use only literal
strings as keys. But these table types are far more expressive than
record types. Really cool. I like it.

Is Typed Lua going to include type system features which allow a
configuration style lua programs, i.e. giving functions a single table
parameter, and passing in the actual parameters as entries in the table,
allowing for named arguments which can be selectively omitted if they
define default values? If so, have you looked at Shriram Krishnamurthi's
paper about typing objects with first-class member names? There's some
interesting stuff in there about how to define a structural subtyping
relation which enables this style of programming, specifically his
discussion of presence annotations (section 4.3). It seems like it is
probably compatible with the table types you have, but I have not
thought about how it would interact with table types which have
non-literal types as keys.

Have you considered providing any typing features which are targeted at
coroutine usage? In my lua type checker, I have two families of function
types: latent and non-latent. Latent functions may call both latent and
non-latent functions, whereas non-latent functions can only call other
non-latent functions. The goal of this is to distinguish between
functions which may yield and functions which will not yield, so
naturally coroutine.yield is typed as a latent function. The two
families of function types are not related via subtyping. It's not a
particularly tricky or interesting feature to add, but it's something
that I saw the need for when working with Lua in the game industry.

Kevin