Re: TypedLua

[Kevin Clancy <kclanc@...>]

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

Agreed on both counts. If you give programmers the option of omitting
type annotations from variable declarations, they will do it. And
without local type inference, the type checker isn't going to be able to
find any errors involving those variables. Having a fruitful type
checker is far more important than maintaining backward compatibility, IMHO.

I'm not sure I agree with Bracha's "errors as warnings" policy either.
In my experience, the vast majority of type errors correspond to
legitimate problems. Even in cases where they don't correspond to
runtime errors, they often do correspond to bad design. Allowing
programmers to ignore errors may give them some extra flexibility in a
few corner cases, but far more often it will allow them to ignore errors
which genuinely need to be fixed.

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

I was actually talking about "Semantics and Types for Objects with
First-Class Member Names". The subtyping parable in section 4.3.1
presents an issue that you would probably have to deal with to enable
typed, configuration style code. I was thinking about this yesterday,
and I realized that presence annotations would probably be overkill for
typed lua, especially considering how elegant its table types are
shaping up to be.

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.