Re: TypedLua

[Andre Murbach Maidl <andremm@...>]

> 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).

That's right. The paper is the most updated resource.
I'm still porting my old code to use and extend Metalua's  AST,
and that is the reason why the examples from the paper are not
running right now.
I will put more examples when I finish this porting and release version 0.1.

> 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.

You are right.
Typed Lua is not exactly a strict superset of Lua.
For instance, the code [[ local a = 5 ; a = "foo" ]] gives a type error on
the second assignment,
However, the compiler still generates code in spite of the type checking
found type errors.
I was thinking to follow Gilad Bracha's ideas on this and leave inference
as an optional feature that you can turn on and off.
However, right now I'm not sure if I really want to do that and I will
probably stay with local type inference, because I believe that it helps
to indicate the programmer's intention on most of the cases.
Under theses circumstances, perhaps I should not say that Typed Lua
is a strict superset of Lua.

> 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.

Thanks for the positive feedback. I'm really glad for that. :)

> 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?

Maybe. But I haven't gone that far on the design yet.

> 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.

Are you talking about the paper "TeJaS: Retrofitting Type Systems for
JavaScript"?

> 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.

To be honest, I haven't thought about coroutines yet.
Anyway, it is very helpful to hear the experience of someone that
already wrote a type checker for Lua.

André