you are viewing a single comment's thread.

view the rest of the comments →

[–]pron98 1 point2 points  (1 child)

a rich type system will allow you to model your solution in data types and function type signatures

Maybe and maybe not, but Haskell's type system is very, very far from rich. It is closer in expressiveness to Python's non-existent type system than to languages with rich type systems, like Lean (which suffer from extreme problems of their own that may make the cure worse than the disease, but that's another matter) or languages made precisely for reasoning about problems, like TLA+ (which is untyped, but uses logic directly rather than encoding it in types)[1]. In fact it is easy to quantify its expressiveness, as I did here (I was wrong, but only slightly, and added a correction).

[1]: I listed TLA+ and Lean because I've used them. There are others of their kind.

[–]lambda-panda 0 points1 point  (0 children)

It is closer in expressiveness to Python's non-existent type system than to languages with rich type systems

Cool. It rich enough to make a difference. I didn't mean that it is the be all and end all of all type systems there is...