Comment by spockz
5 days ago
Coming from Haskell, I loved Agda 2 as a dependent type language. Is there any newer or more mainstream language that has added dependent types?
5 days ago
Coming from Haskell, I loved Agda 2 as a dependent type language. Is there any newer or more mainstream language that has added dependent types?
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