Hacker News new | ask | show | jobs
by debugnik 401 days ago
> 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).
2 comments
ufo 401 days ago
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.

link
lolinder 401 days ago
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.

link
debugnik 401 days ago
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.

link