Teal – A statically-typed dialect of Lua

People get this way about TypeScript too, and it always perplexes me. These projects are about adding types to untyped languages, and that comes with a few givens:

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

> Your type system cannot be sound. It's going to have escape hatches and exceptions because that's how dynamic languages roll.

I think you could prove that you can't construct a sound & complete type system for Lua. But just saying "Your type system cannot be sound" by itself is definitely wrong. I don't understand why people are throwing out both soundness & completeness, instead of at least retaining one (and I think the choice here is pretty obvious, a sound but incomplete type system is much more useful than an unsound one).

From Flow's website[1] (a type checker for JavaScript):

> Flow tries to be as sound and complete as possible. But because JavaScript was not designed around a type system, Flow sometimes has to make a tradeoff. When this happens Flow tends to favor soundness over completeness, ensuring that code doesn't have any bugs.

I don't understand why other type systems for dynamically typed languages cannot strive for that, and in particular I am pretty salty at TypeScript for explicitly not caring about soundness.

[1]: https://flow.org/en/docs/lang/types-and-expressions/#toc-sou...

> Your type system cannot be sound.

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

TypeScript supports runtime type assertions, but it doesn't mandate them or write them for you.

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.

Why, though? Completeness matters more than soundness in practice for this kind of language, which is a large part of what gave TypeScript its edge. The only people who complain about soundness seem to be those whose approach to TypeScript is one of theoretical interests rather than practical application.

A tricky tradeoff is that, because Teal compiles to Lua source, adding those run-time type checks would incur some considerable overhead. I've seen other languages in this space easily run 2 or 3 times slower when run-time checks are turned on. It's an open research problem.

You might be interested in checking out Pallene. Like Teal it's also Lua with types but it does check types at run-time, in an efficient way. However, Pallene's type system is currently not as featureful and production ready as Teal.

The problem is not that it doesn't write them for you, but that `as MyType` is way too ergonomic of a syntax for unchecked assertions, whereas checked assertions require effectively parsing the structure manually with typeof checks.

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.