4 ms·

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?

• doctor_phil 8mo ago
  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.
  • spockz 8mo ago
    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.
• throw_await 8mo ago
  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-seriously https://www.hacklewayne.com/dependent-types-in-typescript-se...
  • codethief 8mo ago
    That whole blog is one big and fascinating rabbit hole into type theory! Thanks for the link!
• instig007 8mo ago
  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+
• yuppiemephisto 8mo ago
  lean 4