[Ciantic]

Typed Lua is something I've always wanted, but writing a very comprehensive type-checker and LSP for another dynamic language is pretty difficult. All dynamic languages have similar problems to those TypeScript encountered, as most dynamic languages have a sort of structural typing in the form of dictionaries or objects.

I do wonder if we could reuse TypeScript in other dynamic languages.

Transform Luau to a subset of TypeScript, check with tsc, transform errors and results back to Luau. In the same way, one could reuse a TypeScript language server. This way of utilising TypeScript's engine could jump-start many other type checkers for other dynamic languages.

[cjbgkagh]

Like a LLVM but for type systems instead of compilation / interpreters / JIT. I don’t see why that couldn’t work.

My thinking in this space has always started from a type inferred MetaLanguage but starting from a dynamic language does enable some interesting options. I tend not to touch dynamic languages, even going so far as to use transpilers, but I definitely would be more open to the idea of working with them if they had TypeScript level of gradual type checking and tool support. As you mention such a bidirectional transpiler would work I guess for things that don’t translate it could just give up and that’ll be part of the gradual typing aspect.

I would love to have TypeScripts type system on a Lua runtime, so I’ve been keeping an eye on Luau.

[parenwielder]

> Like a LLVM but for type systems instead of compilation / interpreters / JIT.

This would be a very cool project, but depending on what you actually want out of it is basically open research in programming languages. Racket #langs and their general approach to type-checking are one sort of answer to this: it's basically a "language-building lab" with an underlying philosophy that we should all be approaching programming in a language-oriented way, that is, by building domain-specific languages that raise the level of abstraction for what you're talking about. That's probably the most developed approach to this sort of thing, but it's still very much something that the Racket folks continue to iterate on and design further.

If you want more conventional _static_ type systems with a much harder delineation between "compile-time" and "runtime" than exists in Racket, you start getting into a sort of compiler-generator-framework territory with the type system, and you'd probably want a language for metatheory to program the type system in, and that starts to look like compiler-generator frameworks embedded into proof assistants like Agda or Rocq. There's some research in that space as well, but certainly nothing that has anything near universal agreement that it works well.

Right now, the state-of-the-art for designing type systems for any language is essentially "employ a bunch of people with very, very deep specialization in this subject matter to painstakingly design and implement the type system with careful consideration of the runtime semantics of the language it's being built for." It's not easy, and it's not cheap, which is why the successful instantiations of this kind of thing are all massive corporate-backed projects. As someone who is really a type system designer first and a corporate-tech-worker a very distant second, I'd love to be able to democratize building type systems more (or to see that be democratized), but it feels very, very far away from being solved.

[deviaze]

Luau already has Luau Language Server which works extremely well for vscode w/ nvim & zed support as well. It surfaces Luau's own diagnostics w/ autocomplete, strict type checking, etc., leading to a better DX (for me) than using Ruby or Python. I primarily use Luau as a shell scripting & general purpose programming language w/ my own runtime (ala node is to js) called seal. Many Roblox devs use a different (much more popular) runtime called Lune for Roblox CI/CD, unit & integration testing, etc.

[giraffe_lady]

For all its success typescript demonstrates the downside of this approach. Like you said it's just difficult, and the end result of having every corner of the dynamic language expressible in the type system forces you into the most complex & novel type systems.

IMO a better approach is the one used by rescript and gleam. With a few careful restrictions of the target language you can fit it into a hindley-milner type system. These are extremely well understood, robust & usable, and give you a much smaller interface than the expansive turing complete one of TS.

I'm kind of surprised there's not an active project for a small ML language outputting lua code. I really wish gleam could pick it up as a third backend, it would be an amazing fit.

[dicytea]

It already exists actually: https://github.com/TypeScriptToLua/TypeScriptToLua.

I had a pretty good experience with it while trying out Love2D.

[Ciantic]

That is one way.

What I meant was transpiling Luau (in memory or cached to disk) -> TypeScript -> typecheck with tsc -> take error outputs and line numbers -> transform back to Luau code via sourcemaps etc. This is potentially way easier than making your own checker for another structurally typed language.

User only sees Luau script in their editor, but it gets checked by TSC in the background.

Roblox might is such a big maker that they can re-invent the whole structural typing themselves, so they don't need to do that.