Hacker News Reader

Typescript has something that can be used as dependent types, but it wasn't intended as a language feature, so the Syntax is not as ergonomic as Agda: https://www.hacklewayne.com/dependent-types-in-typescript-se...

That whole blog is one big and fascinating rabbit hole into type theory! Thanks for the link!

Idris is slightly more mainstream I would say, but not wildy so. If you like the Haskell interop then I'd recommend staying with Agda.

Scala 3 is much more mainstream and has path dependent types. I've only used Scala 2, and there the boilerplate for dependent types was frustrating imo, but I've heard its better in 3.

Ah yes Idris rings a bell. I’ll try that one again.

Scala 3 indeed is more mainstream but it seems also on the way out. At least here in corporate world it is replaced by Kotlin and Java 21+ for a large part.

You can have range-constrained numeric types and collections in Haskell via Liquid Haskell, which has almost seamless integration with the compiler starting from GHC-9.12+

lean 4