YOyogthos·Jul 1, 2019
HM style type inference is nice, but the root problem is that the static type system restricts you to a set of statements that it is able to verify at compile time. This necessarily leads to code that prioritizes the needs of the compiler over those of the human reader. The more things you try to encode using the type system, the more complex your code becomes because proving something correct for all cases is typically significantly more difficult than just stating it and testing for the set of cases you care about. Furthermore, there is no way to verify that your type definitions themselves are correct. When you start moving program logic into types, the compiler cannot help you ensure that it's correct.
Here's a fully typed insertion sort [1] written in Idris. It's over 260 lines long, and it takes non trivial amount of effort to under
Read the rest
stand it fully, and know that what it specifies is indeed what was intended. Meanwhile, I can trivially read and understand a 10 line Python version in its entirety.
Of course, you could argue that it's an extreme case, and that in practice you probably wouldn't have such an exhaustive type specification. At that point you'd be agreeing that relaxing type constraints does provide a benefit, and we'd just be arguing about our respective levels of comfort.
[1] https://github.com/davidfstr/idris-insertion-sort/blob/maste...