How confident are you in the soundness of the type system?
Also, are there any Lua constructs that are difficult/impossible to type?
Is type checking decidable? (Is the type system Turing complete?)
replies(3):
Also, are there any Lua constructs that are difficult/impossible to type?
Is type checking decidable? (Is the type system Turing complete?)
* Your type system cannot be sound. It's going to have escape hatches and exceptions because that's how dynamic languages roll.
* There will always be constructs that you can't type. See above.
* If your type system is going to usefully type enough of the ecosystem, it will be Turing complete.
All of these things are the trade-offs you make when you set out to layer types on a dynamic language, and they're well worth it to get 99% of the way to type safety in a language that otherwise couldn't scale. Theoretical purity is meaningless if the language isn't useful.
This one I disagree with. Type assertions with runtime checks could keep the typed fragments sound, unlike TypeScript and Python. Also see Elixir's strong arrow proposal for how to encode which assertions can be elided on function calls (because the function will assert them already).
I should have said your type system cannot be sound without runtime overhead. And I don't believe that choosing automatic runtime overhead is the right move.
TypeScript desperately needs a way to derive type-guarding functions from types (and so does every gradually-typed language). There're libraries for this but you need to define the types themselves through combinators.