Reputation: 9521
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?
Upvotes: 1
Views: 111
Reputation: 2653
"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.
Upvotes: 2