YOyogthos·Jan 13, 2019
Haskell was my first FP language, I used it for about a year, and worked with Scala briefly after. My experience is that you're really trading one set of problems for another in practice. Static typing can guarantee that you avoid a certain class of errors, but it often results in code that's longer and more difficult to understand opening opportunities for different kinds of errors. There is absolutely no empirical evidence to suggest that the trade off is strictly superior in practice.
Static typing can catch inconsistencies at the cost of structuring your code in a way that the type checker can understand. This is often at odds with making it readable for the human. A proof only has value as long as the human reader can understand it. Here's a concrete example of what I'm talking about: https://github.com/davidfstr/idris-insertion-sort
Read the rest
/blob/maste...
An insertion sort written in Idris has over 250 lines of code that you have to understand to know that it's implemented correctly. A python version would have about 10 lines or less. I'd have much easier time guaranteeing that the 10 lines do exactly what was intended than the 250 lines of type specifications. Of course, you could relax the type guarantees in Idris as well, but at that point you accept that working around the static checker has benefit and it's just a matter of degrees of comfort.
In general, the more constraints you specify via types the more of your program logic moves into type specifications. What this really means is that you're writing a metaprogram that emits your logic. However, there's no automated checker for that metaprogram that you wrote using the types. You still have to understand it to be correct in order to know that it's doing what you want it to. At this point you're basically living in a programmer version of the Plato's Cave.
The real question is not whether you can do something using a static type system or not. The discussion has to center around how that compares to alternative approaches such as testing, gradual typing, and runtime contracts.