As I get more experience with powerful type systems like that of Idris and Mercury, I’m noticing a strange phenomenon. These type checkers deal with powerful logics, but the checkers themselves are not very smart; they can only verify a property if it’s syntactically obvious. And if you don’t have much experience with such a type checker, and haven’t learned the quirks of exactly what “syntactically obvious” means, programming in that language can be a chore. It’s been a while since I felt lost in Idris, but since lately I’ve been learning Mercury, I’m getting reacquainted with the despair of “Why won’t you accept this obviously-correct code, compiler?”
But as you get more familiar with what exactly the compiler checks, your relationship with it starts to change. The question changes from “Why can’t the stupid compiler see this?” to “Well, how do I know my code is correct?” And something that very often happens is, once I’ve thought for a few moments about how I know what’s going on, it’s immediately clear how to rewrite the code so that the compiler knows what’s going on.
But more importantly: sometimes, when I’ve taken a moment to think rigorously, I realize that my code isn’t correct. Maybe the Mercury predicate that is supposed to be deterministic actually has multiple solutions — not just the way I wrote it but the way I meant it, and I have to come up with a different plan for writing the predicate because my old one is flawed. And I would never have noticed it before because as far as I can tell, the code is obviously correct.
I admit that stupid typecheckers verifying complicated properties is a bit of a usability problem for people inexperienced with the typechecker. I have felt that pain and frustration, and I know it isn’t pleasant.
But I think it might be worth it. Once the pain goes away, you’re left with an obligation to strengthen your understanding of your code — to go from “This obviously does what I want it to do” to “Here, Stupid Compiler, you can’t understand my higher level thought processes, so let me walk you through it.”