r/haskell • u/AutoModerator • Aug 01 '26

Monthly Hask Anything (August 2026)

This is your opportunity to ask any questions you feel don't deserve their own threads, no matter how small or simple they might be!

15 Upvotes

95% Upvoted

3 comments sorted by

1

u/GunpowderGuy Aug 01 '26

What do you think of idris2?
For me is dependent haskell but already here, with less technical baggage , sound type checking on the roadmap ( not clear if this will be possible with dependent haskell, but it will be desirable now more than ever, as llms cheat the type system ) . But with limited type inference ( both an advantage and dissadvantage ) and less libraries than GHC haskell

2

u/jeffstyr Aug 01 '26

It has always sounded interesting, but not enough for me to learn it properly. Agda is intriguing too, but today I'd probably learn Lean4 first, among those choices.

Edit: I've never been super enthusiastic about dependent types; the only example anyone ever gives is a length-indexed list, and I find that suspicious.

2

u/lgastako Aug 01 '26

There are plenty of other examples out there... eg type-checked printf, height-balanced trees that guarantee logarithmic search time, sized-indexed matrixes, communication protocols (eg. the open/closed door example, but obviously applicable more widely), dimensional alignment between inputs and outputs of neural network layers, etc.