Software engineering benefits of type systems used in functional languages

1
votes

In high level statically typed functional languages like Haskell or OCaml, the type system is used canonically to enforce constraints on the types of entities being modelled in some problem domain.

From a software engineering point of view, are there any practical benefits to such type systems beyond simply enforcing constraints? For example can they make reasoning about the problem domain easier? Can they make design abstractions more flexible/robust in the face of changing requirements? Can they help manage the complexity in large systems? etc...

And if such benefits do exist, can we somehow try to replicate them in dynamic languages such as Ruby, Python or Clojure?

1
typesfunctional-programmingdynamic-languages
The compiler can check and optimize the code if the type of variables are known at compile time - less runtime errors, better perfomance – Binkan Salaryman
Please don't vote on closing this question, it's not broad as it may seem on first sight. The reader may think of any single benefit (no matter how small) and cast his answer accordingly. – Rabih Kodeih
I believe most of your examples fall under the "simply enforcing constraints" category - with a powerful type system you can (comfortably) express a much wider range of constraints than in lesser systems. – molbdnilo

1 Answers

2
votes

"simply enforcing the constraint" - well that's exactly the point. You want to express the specification of the program (and each subprogram) by its type. Then type-checking is actually "enforcing correctness" (and it's not simple). Haskell is not the end of this, there are languages with more expressive type systems (Agda, Idris) where you can actually achieve the goal of expressing the specification completely.

Replication in other languages - see, e.g., Hack and TypeScript.

Note: before Haskell experts jump at me about "more expressive": there are several (compiler specific) extensions of the Haskell type system (towards dependent types) that make it much more expressive as well. - "Complete" means "as expressive as mathematical logic", which is the universal specification language. I'll leave it at that, if you want more, you'll find it in papers and books on theory and principles of programming languages.